diff --git a/CHANGES.md b/CHANGES.md index c4b2efee68..93824cd5ca 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -317,7 +317,7 @@ ### Breaking changes - Invalid configuration keys found in configuration sources (e.g., `apalache.cfg` files) will now produce a configuration error on load (see #2125). -- The structure of the apalache.cfg has changed. All configuration keys that were previously supported have been moved under the `common` key. You can update your config files by prefixing each key from the previous versions with `commong.key-name`. For an example config file, see https://apalache.informal.systems/docs/apalache/config.html#file-format-and-supported-parameters. See #2065. +- The structure of the apalache.cfg has changed. All configuration keys that were previously supported have been moved under the `common` key. You can update your config files by prefixing each key from the previous versions with `commong.key-name`. For an example config file, see https://apalache-mc.org/docs/apalache/config.html#file-format-and-supported-parameters. See #2065. - Introduce --features=no-rows for the old record syntax and switch to `--features=rows` by default ### Features @@ -737,7 +737,7 @@ ### Documentation * Restructure and update the Apalache manual: - https://apalache.informal.systems/docs/index.html + https://apalache-mc.org/docs/index.html ## 0.17.5 diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index b5c9408177..82992bbb84 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -149,7 +149,7 @@ contributors and maintainers to make sure: ## Dependencies For setting up the local build, see the [instructions on building from -source](https://apalache.informal.systems/docs/apalache/installation/source.html). +source](https://apalache-mc.org/docs/apalache/installation/source.html). ### Environment diff --git a/docs/README.md b/docs/README.md index 7492cec320..0c69f8728f 100644 --- a/docs/README.md +++ b/docs/README.md @@ -3,7 +3,7 @@ The Apalache documentation is written in markdown files in the [./src](./src) directory and compiled using [mdbook](https://github.com/rust-lang/mdBook). -To view the documentation, visit https://apalache.informal.systems/docs/. +To view the documentation, visit https://apalache-mc.org/docs/. ## Building and previewing the documentation diff --git a/docs/src/adr/002adr-types.md b/docs/src/adr/002adr-types.md index 9f152a7b67..49686524c1 100644 --- a/docs/src/adr/002adr-types.md +++ b/docs/src/adr/002adr-types.md @@ -598,8 +598,8 @@ AtMostOne == ============================================================================= ``` -[Snowcat tutorial]: https://apalache.informal.systems/docs/tutorials/snowcat-tutorial.html -[Snowcat HOWTO]: https://apalache.informal.systems/docs/HOWTOs/howto-write-type-annotations.html +[Snowcat tutorial]: https://apalache-mc.org/docs/tutorials/snowcat-tutorial.html +[Snowcat HOWTO]: https://apalache-mc.org/docs/HOWTOs/howto-write-type-annotations.html [ADR014]: https://github.com/informalsystems/apalache/blob/main/docs/src/adr/014adr-precise-records.md [Issue 401]: https://github.com/informalsystems/apalache/issues/401 [Row polymorphism]: https://en.wikipedia.org/wiki/Row_polymorphism diff --git a/docs/src/adr/003adr-trex.md b/docs/src/adr/003adr-trex.md index 13ff622770..527c72b38e 100644 --- a/docs/src/adr/003adr-trex.md +++ b/docs/src/adr/003adr-trex.md @@ -116,4 +116,4 @@ explain how the parallel checker is working. This is a subject to another ADR. To sum up, this layer is offering you a nice abstraction to write different model checking strategies. -[KerA+]: https://apalache.informal.systems/docs/apalache/kera.html +[KerA+]: https://apalache-mc.org/docs/apalache/kera.html diff --git a/docs/src/adr/004adr-annotations.md b/docs/src/adr/004adr-annotations.md index 0986b8a60c..5dd6af1057 100644 --- a/docs/src/adr/004adr-annotations.md +++ b/docs/src/adr/004adr-annotations.md @@ -158,7 +158,7 @@ This is done because the SANY parser is pruning the linefeed character `\n`, so it would be otherwise impossible to find the end of an annotation. -[ADR-002]: https://apalache.informal.systems/docs/adr/002adr-types.html +[ADR-002]: https://apalache-mc.org/docs/adr/002adr-types.html [JavaTokenParsers]: https://www.scala-lang.org/api/2.12.2/scala-parser-combinators/scala/util/parsing/combinator/JavaTokenParsers.html [Java identifier]: https://docs.oracle.com/javase/specs/jls/se7/html/jls-3.html#jls-3.8 diff --git a/docs/src/adr/005adr-json.md b/docs/src/adr/005adr-json.md index 786dfd3b56..17157286b3 100644 --- a/docs/src/adr/005adr-json.md +++ b/docs/src/adr/005adr-json.md @@ -201,9 +201,9 @@ In general, for any given `oper: TlaOper` of `OperEx`, the value of the `oper` f The implementation of the serialization can be found in the class `at.forsyte.apalache.io.json.TlaToJson` of the module `tla-import`, see [TlaToJson][]. -[ADR-002]: https://apalache.informal.systems/docs/adr/002adr-types.html +[ADR-002]: https://apalache-mc.org/docs/adr/002adr-types.html -[ADR-004]: https://apalache.informal.systems/docs/adr/004adr-annotations.html +[ADR-004]: https://apalache-mc.org/docs/adr/004adr-annotations.html [TlaToJson]: https://github.com/informalsystems/apalache/blob/main/tla-io/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala#L54 [TlaEx]: https://github.com/informalsystems/apalache/blob/main/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaEx.scala#L10 diff --git a/docs/src/adr/011adr-smt-arrays.md b/docs/src/adr/011adr-smt-arrays.md index c5c4106bd6..6e8bd08f20 100644 --- a/docs/src/adr/011adr-smt-arrays.md +++ b/docs/src/adr/011adr-smt-arrays.md @@ -308,7 +308,7 @@ The following changes will be made to implement the new encoding of functions: The use of SMT arrays will be restricted to TLA+ sets and functions for the moment. The encoding of additional features using SMT arrays, or potentially ADTs, will be left for the future. -[KerA+]: https://apalache.informal.systems/docs/apalache/kera.html +[KerA+]: https://apalache-mc.org/docs/apalache/kera.html [core theory]: http://smtlib.cs.uiowa.edu/theories-Core.shtml [arrays with extensionality]: http://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml [Z3]: https://github.com/Z3Prover/z3 @@ -316,6 +316,6 @@ additional features using SMT arrays, or potentially ADTs, will be left for the [Version 2.6]: https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf [TLA+ Model Checking Made Symbolic]: https://dl.acm.org/doi/10.1145/3360549 [Symbolic Model Checking for TLA+ Made Faster]: https://doi.org/10.1007/978-3-031-30823-9_7 -[model checking parameters]: https://apalache.informal.systems/docs/apalache/running.html#model-checker-command-line-parameters +[model checking parameters]: https://apalache-mc.org/docs/apalache/running.html#model-checker-command-line-parameters [represented internally in Z3]: https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-arrays [PR 2027]: https://github.com/informalsystems/apalache/pull/2027 diff --git a/docs/src/adr/014adr-precise-records.md b/docs/src/adr/014adr-precise-records.md index 31e32e9e95..0878fcf9fa 100644 --- a/docs/src/adr/014adr-precise-records.md +++ b/docs/src/adr/014adr-precise-records.md @@ -15,7 +15,7 @@ ## 1. Summary This ADR extends -[ADR-002](https://apalache.informal.systems/docs/adr/002adr-types.html) on +[ADR-002](https://apalache-mc.org/docs/adr/002adr-types.html) on types and type annotations. Virtually every user of Snowcat has faced the issue of record type checking @@ -665,7 +665,7 @@ default untyped implementation for the operators. -[ADR002]: https://apalache.informal.systems/docs/adr/002adr-types.html +[ADR002]: https://apalache-mc.org/docs/adr/002adr-types.html [#401]: https://github.com/informalsystems/apalache/issues/401 [#789]: https://github.com/informalsystems/apalache/discussions/789 [Raft]: https://github.com/ongardie/raft.tla/blob/master/raft.tla diff --git a/docs/src/adr/015adr-trace.md b/docs/src/adr/015adr-trace.md index a8831f65bf..498cc323fb 100644 --- a/docs/src/adr/015adr-trace.md +++ b/docs/src/adr/015adr-trace.md @@ -467,8 +467,8 @@ write a parser of custom ITF traces. Hence, we have decided to keep only the obj as the more general of the two representations. -[ADR005]: https://apalache.informal.systems/docs/adr/005adr-json.html -[ADR002]: https://apalache.informal.systems/docs/adr/002adr-types.html +[ADR005]: https://apalache-mc.org/docs/adr/005adr-json.html +[ADR002]: https://apalache-mc.org/docs/adr/002adr-types.html [MissionariesAndCannibalsTyped]: https://github.com/informalsystems/apalache/blob/main/test/tla/MissionariesAndCannibalsTyped.tla [JSON]: https://en.wikipedia.org/wiki/JSON [RFC7159]: https://datatracker.ietf.org/doc/html/rfc7159.html diff --git a/docs/src/adr/023adr-trace-evaluation.md b/docs/src/adr/023adr-trace-evaluation.md index 3ae4cbecb7..77fe1ce54d 100644 --- a/docs/src/adr/023adr-trace-evaluation.md +++ b/docs/src/adr/023adr-trace-evaluation.md @@ -137,7 +137,7 @@ and trace `testTrace.json` (length 5, `x=1 -> ... -> x=5`). { "name": "ApalacheIR", "version": "1.0", - "description": "https://apalache.informal.systems/docs/adr/005adr-json.html", + "description": "https://apalache-mc.org/docs/adr/005adr-json.html", "modules": [ { "kind": "TlaModule", diff --git a/docs/src/apalache/features.md b/docs/src/apalache/features.md index fc14b1b817..047fde2a0b 100644 --- a/docs/src/apalache/features.md +++ b/docs/src/apalache/features.md @@ -4,7 +4,7 @@ Here is the list of the TLA+ language features that are currently supported by A At the moment, Apalache is able to check state invariants, action invariants, temporal properties, trace invariants, as well as inductive invariants. (See the [page on -invariants](https://apalache.informal.systems/docs/apalache/principles/invariants.html) in +invariants](https://apalache-mc.org/docs/apalache/principles/invariants.html) in the manual.) To check liveness/temporal properties, we employ a [liveness-to-safety][] transformation. ## Language @@ -66,7 +66,7 @@ replaced with a constant. #### Records *Use [type -annotations](https://apalache.informal.systems/docs/tutorials/snowcat-tutorial.html) +annotations](https://apalache-mc.org/docs/tutorials/snowcat-tutorial.html) to help the model checker in finding the right types.* Note that our type system distinguishes records from general functions. @@ -81,14 +81,14 @@ system distinguishes records from general functions. #### Tuples *Use [type -annotations](https://apalache.informal.systems/docs/tutorials/snowcat-tutorial.html) +annotations](https://apalache-mc.org/docs/tutorials/snowcat-tutorial.html) to help the model checker in finding the right types.* Note that our type system distinguishes records from general functions. | Operator | Supported? | Milestone | Comment | |------------------------|:----------:|:---------:|------------------------------------------------------------------------------------------------------------------------------------------------| | `e[i]` | ✔ / ✖ | - | Provided that `i` is a constant expression | -| `<< e1, ..., e_n >>` | ✔ | - | Use a [type annotation](https://apalache.informal.systems/docs/tutorials/snowcat-tutorial.html) to distinguish between a tuple and a sequence. | +| `<< e1, ..., e_n >>` | ✔ | - | Use a [type annotation](https://apalache-mc.org/docs/tutorials/snowcat-tutorial.html) to distinguish between a tuple and a sequence. | | `S1 \X ... \X S_n` | ✔ | - | | | `[ t EXCEPT ![i] = e]` | ✔/✖ | - | Provided that `i` is a constant expression | @@ -158,7 +158,7 @@ For the moment, the model checker does not differentiate between integers and na | Operator | Supported? | Milestone | Comment | |----------------------------------------------------------|:----------:|:---------:|----------------------------------------------------------------------------------------------------------| -| `<<...>>` | ✔ | | Often needs a [type annotation](https://apalache.informal.systems/docs/tutorials/snowcat-tutorial.html). | +| `<<...>>` | ✔ | | Often needs a [type annotation](https://apalache-mc.org/docs/tutorials/snowcat-tutorial.html). | | `Head`, `Tail`, `Len``, `SubSeq`, `Append`, `\o`, `f[e]` | ✔ | - | | | `EXCEPT` | ✔ | | | | `SelectSeq` | ✔ | - | Not as efficient, as it could be, see [#1350](https://github.com/informalsystems/apalache/issues/1350). | diff --git a/docs/src/apalache/principles/apalache-mod.md b/docs/src/apalache/principles/apalache-mod.md index 2d35d6d7d2..4456ff566c 100644 --- a/docs/src/apalache/principles/apalache-mod.md +++ b/docs/src/apalache/principles/apalache-mod.md @@ -9,4 +9,4 @@ See the detailed description of the [Apalache operators][]. [Apalache.tla]: https://github.com/informalsystems/apalache/tree/main/src/tla/Apalache.tla -[Apalache operators]: https://apalache.informal.systems/docs/lang/apalache-operators.html +[Apalache operators]: https://apalache-mc.org/docs/lang/apalache-operators.html diff --git a/docs/src/apalache/principles/assignments.md b/docs/src/apalache/principles/assignments.md index efd5a49f37..7329dda90c 100644 --- a/docs/src/apalache/principles/assignments.md +++ b/docs/src/apalache/principles/assignments.md @@ -71,7 +71,7 @@ Apalache reports an error as follows: ... PASS #9: TransitionFinderPass To understand the error, [check the -manual](https://apalache.informal.systems/docs/apalache/principles/assignments.html): +manual](https://apalache-mc.org/docs/apalache/principles/assignments.html): Assignment error: No assignments found for: a It took me 0 days 0 hours 0 min 1 sec Total time: 1.88 sec diff --git a/docs/src/apalache/running.md b/docs/src/apalache/running.md index 8f9bf86999..9a64a9df66 100644 --- a/docs/src/apalache/running.md +++ b/docs/src/apalache/running.md @@ -22,7 +22,7 @@ The most important commands are as follows: the types of all expressions in the parsed specification. It terminates successfully if there are no type errors. - `simulate` performs all of the operations of `typecheck` and additionally runs the model checker in simulation mode, - which *randomly* picks a sequence of [actions](https://apalache.informal.systems/docs/apalache/assignments-in-depth.html#slices) + which *randomly* picks a sequence of [actions](https://apalache-mc.org/docs/apalache/assignments-in-depth.html#slices) and checks the invariants for the subset of all executions which only admit actions in the selected order. It terminates successfully if there are no invariant violations. This command usually checks randomized symbolic runs much faster than the `check` command. @@ -32,7 +32,7 @@ The most important commands are as follows: the length of which does not exceed the value specified by the `--length` parameter. It terminates successfully if there are no invariant violations. - - `test` performs all of the operations of `check` in a mode that is designed to [test a single action](https://apalache.informal.systems/docs/adr/006rfc-unit-testing.html#32-testing-actions). + - `test` performs all of the operations of `check` in a mode that is designed to [test a single action](https://apalache-mc.org/docs/adr/006rfc-unit-testing.html#32-testing-actions). ## 1. Model checker and simulator command-line parameters diff --git a/docs/src/lang/user/top-level-operators.md b/docs/src/lang/user/top-level-operators.md index c9b8649e65..837623c66e 100644 --- a/docs/src/lang/user/top-level-operators.md +++ b/docs/src/lang/user/top-level-operators.md @@ -225,5 +225,5 @@ expression to SMT. [Call by macro expansion]: https://en.wikipedia.org/wiki/Evaluation_strategy#Call_by_macro_expansion [Alpha conversion]: https://en.wikipedia.org/wiki/Lambda_calculus#%CE%B1-conversion [Beta reduction]: https://en.wikipedia.org/wiki/Lambda_calculus#%CE%B2-reduction -[Apalache]: https://apalache.informal.systems +[Apalache]: https://apalache-mc.org diff --git a/docs/src/tutorials/entry-tutorial.md b/docs/src/tutorials/entry-tutorial.md index b33c9dae59..7e8c1a8560 100644 --- a/docs/src/tutorials/entry-tutorial.md +++ b/docs/src/tutorials/entry-tutorial.md @@ -386,7 +386,7 @@ If it is your first TLA+ specification, you may be surprised by this error: ... PASS #13: BoundedChecker This error may show up when CONSTANTS are not initialized. -Check the manual: https://apalache.informal.systems/docs/apalache/parameters.html +Check the manual: https://apalache-mc.org/docs/apalache/parameters.html Input error (see the manual): SubstRule: Variable INPUT_SEQ is not assigned a value ... ``` diff --git a/docs/src/tutorials/pluscal-tutorial.md b/docs/src/tutorials/pluscal-tutorial.md index 99f9746f37..967724cc3a 100644 --- a/docs/src/tutorials/pluscal-tutorial.md +++ b/docs/src/tutorials/pluscal-tutorial.md @@ -276,7 +276,7 @@ or drop us a message on [Zulip chat]. [Issue 1412]: https://github.com/informalsystems/apalache/issues/1412 [open an issue]: https://github.com/informalsystems/apalache/issues [Tutorial on Snowcat]: ./snowcat-tutorial.md -[Checking inductive invariants]: https://apalache.informal.systems/docs/apalache/running.html#checking-an-inductive-invariant +[Checking inductive invariants]: https://apalache-mc.org/docs/apalache/running.html#checking-an-inductive-invariant [TLA+ Cheatsheet in HTML]: https://mbt.informal.systems/docs/tla_basics_tutorials/tla+cheatsheet.html [Summary of TLA+]: https://lamport.azurewebsites.net/tla/summary-standalone.pdf [TLA+ Video Course]: http://lamport.azurewebsites.net/video/videos.html diff --git a/mod-infra/src/main/scala/at/forsyte/apalache/infra/ExceptionAdapter.scala b/mod-infra/src/main/scala/at/forsyte/apalache/infra/ExceptionAdapter.scala index af1cde0362..649d83b7b2 100644 --- a/mod-infra/src/main/scala/at/forsyte/apalache/infra/ExceptionAdapter.scala +++ b/mod-infra/src/main/scala/at/forsyte/apalache/infra/ExceptionAdapter.scala @@ -36,7 +36,7 @@ trait ExceptionAdapter extends LazyLogging { def toMessage: PartialFunction[Throwable, ErrorMessage] = { case err: OutOfMemoryError => logger.error(s"Ran out of heap memory (max JVM memory: ${Runtime.getRuntime.maxMemory})") logger.error(s"To increase available heap memory, see the manual:") - logger.error(" [https://apalache.informal.systems/docs/apalache/running.html#supplying-jvm-arguments]") + logger.error(" [https://apalache-mc.org/docs/apalache/running.html#supplying-jvm-arguments]") NormalErrorMessage(s"Ran out of heap memory: ${err.getMessage}") } } diff --git a/mod-infra/src/main/scala/at/forsyte/apalache/infra/tlc/TlcConfigParser.scala b/mod-infra/src/main/scala/at/forsyte/apalache/infra/tlc/TlcConfigParser.scala index dc1021df59..3c9d4ebdd2 100644 --- a/mod-infra/src/main/scala/at/forsyte/apalache/infra/tlc/TlcConfigParser.scala +++ b/mod-infra/src/main/scala/at/forsyte/apalache/infra/tlc/TlcConfigParser.scala @@ -9,7 +9,7 @@ import at.forsyte.apalache.infra.tlc.config.TlcConfig * href="http://research.microsoft.com/users/lamport/tla/book.html">Specifying Systems, Ch. 14] by Leslie Lamport. * TLC configuration files have a rich assignment syntax, e.g., one can write a parameter assignment. The syntax * supported by Apalache is described in [tlc-config]. + * href="https://apalache-mc.org/docs/apalache/tlc-config.html">tlc-config]. * * @author * Igor Konnov diff --git a/mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala b/mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala index f3902ddd35..dbe3854f05 100644 --- a/mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala +++ b/mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala @@ -44,7 +44,7 @@ object Tool extends LazyLogging { // If it is caught here, logging has not been set up yet, so print directly to `Console.err`. Console.err.println(s"Error: Ran out of heap memory (max JVM memory: ${Runtime.getRuntime.maxMemory})") Console.err.println(s"To increase available heap memory, see the manual:") - Console.err.println(" [https://apalache.informal.systems/docs/apalache/running.html#supplying-jvm-arguments]") + Console.err.println(" [https://apalache-mc.org/docs/apalache/running.html#supplying-jvm-arguments]") Console.out.println(s"EXITCODE: ERROR (${ExitCodes.ERROR})") System.exit(ExitCodes.ERROR) } diff --git a/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/ConfigCmd.scala b/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/ConfigCmd.scala index 73dedcf455..37126f8158 100644 --- a/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/ConfigCmd.scala +++ b/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/ConfigCmd.scala @@ -19,7 +19,7 @@ class ConfigCmd extends ApalacheCommand(name = "config", description = "Configur var submitStats: Option[Boolean] = opt[Option[Boolean]](name = "enable-stats", description = "Let Apalache submit usage statistics to tlapl.us\n" - + "(shared with TLC and TLA+ Toolbox)\nSee: https://apalache.informal.systems/docs/apalache/statistics.html") + + "(shared with TLC and TLA+ Toolbox)\nSee: https://apalache-mc.org/docs/apalache/statistics.html") def run() = { logger.info("Configuring Apalache") diff --git a/test/tla/Antipatterns.tla b/test/tla/Antipatterns.tla index 0b5c0f99fe..b8928a23f5 100644 --- a/test/tla/Antipatterns.tla +++ b/test/tla/Antipatterns.tla @@ -1,7 +1,7 @@ ---- MODULE Antipatterns ---- (* Contains a collection of known-to-be-inefficient Apalache constructs, a.k.a. "antipatterns". We explain why these constructs are inefficient in -https://apalache.informal.systems/docs/apalache/antipatterns.html +https://apalache-mc.org/docs/apalache/antipatterns.html The purpose of this file is to collect known antipatterns, so we can measure just how much they affect performance, across various versions of Apalache. diff --git a/test/tla/MC_ERC20.tla b/test/tla/MC_ERC20.tla index b1db62fce4..79a30b3b59 100644 --- a/test/tla/MC_ERC20.tla +++ b/test/tla/MC_ERC20.tla @@ -4,7 +4,7 @@ EXTENDS Integers, ERC20_typedefs \* Use the set of three addresses. \* We are using uninterpreted values, similar to TLC's model values. -\* See: https://apalache.informal.systems/docs/HOWTOs/uninterpretedTypes.html +\* See: https://apalache-mc.org/docs/HOWTOs/uninterpretedTypes.html ADDR == { "Alice_OF_ADDR", "Bob_OF_ADDR", "Eve_OF_ADDR" } \* Apalache can draw constants from the set of all integers diff --git a/test/tla/cli-integration-tests.md b/test/tla/cli-integration-tests.md index cfa06d6d28..90fd5c9435 100644 --- a/test/tla/cli-integration-tests.md +++ b/test/tla/cli-integration-tests.md @@ -362,7 +362,7 @@ $ cat output.json | head { "name": "ApalacheIR", "version": "1.0", - "description": "https://apalache.informal.systems/docs/adr/005adr-json.html", + "description": "https://apalache-mc.org/docs/adr/005adr-json.html", "modules": [ { "kind": "TlaModule", @@ -437,7 +437,7 @@ $ cat output.json | head { "name": "ApalacheIR", "version": "1.0", - "description": "https://apalache.informal.systems/docs/adr/005adr-json.html", + "description": "https://apalache-mc.org/docs/adr/005adr-json.html", "modules": [ { "kind": "TlaModule", @@ -1484,7 +1484,7 @@ An occurence of `Seq(S)` should point to an explanation. ```sh $ apalache-mc check Bug1126.tla | sed 's/[IE]@.*//' ... -Bug1126.tla:15:14-15:27: unsupported expression: Seq(_) produces an infinite set of unbounded sequences. See: https://apalache.informal.systems/docs/apalache/known-issues.html#using-seqs +Bug1126.tla:15:14-15:27: unsupported expression: Seq(_) produces an infinite set of unbounded sequences. See: https://apalache-mc.org/docs/apalache/known-issues.html#using-seqs ... EXITCODE: ERROR (75) ``` @@ -2407,7 +2407,7 @@ EXITCODE: OK ### check profiling Check that the profiler output is produced as explained in -[Profiling](https://apalache.informal.systems/docs/apalache/profiling.html). +[Profiling](https://apalache-mc.org/docs/apalache/profiling.html). ```sh $ apalache-mc check --run-dir=./profile-run-dir --smtprof schroedinger_cat.tla | sed 's/[IEW]@.*//' @@ -2508,7 +2508,7 @@ EXITCODE: OK $ apalache-mc check Test669.tla | sed 's/[IEW]@.*//' ... This error may show up when CONSTANTS are not initialized. -Check the manual: https://apalache.informal.systems/docs/apalache/parameters.html +Check the manual: https://apalache-mc.org/docs/apalache/parameters.html Input error (see the manual): SubstRule: Variable N is not assigned a value ... EXITCODE: ERROR (255) diff --git a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/SmtFreeSymbolicTransitionExtractor.scala b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/SmtFreeSymbolicTransitionExtractor.scala index 42acd07bbb..fe61cd1edb 100644 --- a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/SmtFreeSymbolicTransitionExtractor.scala +++ b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/SmtFreeSymbolicTransitionExtractor.scala @@ -195,7 +195,7 @@ class SmtFreeSymbolicTransitionExtractor( } object SmtFreeSymbolicTransitionExtractor { - val MANUAL_LINK = "https://apalache.informal.systems/docs/apalache/principles/assignments.html" + val MANUAL_LINK = "https://apalache-mc.org/docs/apalache/principles/assignments.html" def apply(tracker: TransformationTracker, sourceLoc: SourceLocator): SmtFreeSymbolicTransitionExtractor = { new SmtFreeSymbolicTransitionExtractor(tracker, sourceLoc) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/config/CheckerExceptionAdapter.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/config/CheckerExceptionAdapter.scala index bad9234a93..25bcbce0ce 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/config/CheckerExceptionAdapter.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/config/CheckerExceptionAdapter.scala @@ -42,7 +42,7 @@ class CheckerExceptionAdapter @Inject() (sourceStore: SourceStore, changeListene case err: AssignmentException => logger.info("To understand the error, read the manual:") - logger.info(" [https://apalache.informal.systems/docs/apalache/principles/assignments.html]") + logger.info(" [https://apalache-mc.org/docs/apalache/principles/assignments.html]") NormalErrorMessage("Assignment error: " + err.getMessage) case err: OutdatedAnnotationsError => diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/IntDotDotRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/IntDotDotRule.scala index 98542fe710..5ea921c3c1 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/IntDotDotRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/IntDotDotRule.scala @@ -51,7 +51,7 @@ class IntDotDotRule(@unused rewriter: SymbStateRewriter, intRangeCache: IntRange case _ => throw new NotInKeraError( - "Expected a constant integer range in [ .. ], found %s. This is a known issue: [https://apalache.informal.systems/docs/apalache/known-issues.html]" + "Expected a constant integer range in [ .. ], found %s. This is a known issue: [https://apalache-mc.org/docs/apalache/known-issues.html]" .format(elems.map(UTFPrinter.apply).mkString("..")), ex) } } diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SubstRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SubstRule.scala index dab6a4474d..a56fbc8141 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SubstRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SubstRule.scala @@ -31,7 +31,7 @@ class SubstRule extends RewritingRule with LazyLogging { state.setRex(cell.toBuilder) } else { logger.error("This error may show up when CONSTANTS are not initialized.") - logger.error("Check the manual: https://apalache.informal.systems/docs/apalache/parameters.html") + logger.error("Check the manual: https://apalache-mc.org/docs/apalache/parameters.html") throw new TlaInputError(s"${getClass.getSimpleName}: Variable $x is not assigned a value") } diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/CherryPick.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/CherryPick.scala index 14076b0089..68843e7b59 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/CherryPick.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/CherryPick.scala @@ -283,7 +283,7 @@ class CherryPick(rewriter: SymbStateRewriter) { case _: IndexOutOfBoundsException => // TODO Remove once sound record typing is implemented val url = - "https://apalache.informal.systems/docs/apalache/known-issues.html#updating-records-with-excess-fields" + "https://apalache-mc.org/docs/apalache/known-issues.html#updating-records-with-excess-fields" val msg = s"""|An updated record has more fields than its declared type: |A record with the inferred type `$thisRecT` has been updated with diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/base/SubstStratifiedRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/base/SubstStratifiedRule.scala index c43c229095..5db8f5b4c8 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/base/SubstStratifiedRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/base/SubstStratifiedRule.scala @@ -29,7 +29,7 @@ class SubstStratifiedRule extends StratifiedRuleInterface with LazyLogging { (startingScope, binding(x)) } else { logger.error("This error may show up when CONSTANTS are not initialized.") - logger.error("Check the manual: https://apalache.informal.systems/docs/apalache/parameters.html") + logger.error("Check the manual: https://apalache-mc.org/docs/apalache/parameters.html") throw new TlaInputError(s"${getClass.getSimpleName}: Variable $x is not assigned a value") } diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/annotations/parser/CommentPreprocessor.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/annotations/parser/CommentPreprocessor.scala index 09d5a2e0fb..6bb5543ae7 100644 --- a/tla-io/src/main/scala/at/forsyte/apalache/io/annotations/parser/CommentPreprocessor.scala +++ b/tla-io/src/main/scala/at/forsyte/apalache/io/annotations/parser/CommentPreprocessor.scala @@ -15,7 +15,7 @@ package at.forsyte.apalache.io.annotations.parser * Perhaps, the first step would be to write a precise grammar for this lexer, instead of write the spaghetti of * if-then-else expressions, as we have in this preprocessor.

* - *

See the annotations HOWTO: https://apalache.informal.systems/docs/HOWTOs/howto-write-type-annotations.html

+ *

See the annotations HOWTO: https://apalache-mc.org/docs/HOWTOs/howto-write-type-annotations.html

* * @author * Igor Konnov diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala index fd936fcd77..98df35bf3a 100644 --- a/tla-io/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala +++ b/tla-io/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala @@ -216,7 +216,7 @@ class TlaToJson[T <: JsonRepresentation]( factory.mkObj( "name" -> "ApalacheIR", versionFieldName -> JsonVersion.current, - "description" -> "https://apalache.informal.systems/docs/adr/005adr-json.html", + "description" -> "https://apalache-mc.org/docs/adr/005adr-json.html", "modules" -> factory.fromIterable(moduleJsons), ) } diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/lir/ItfCounterexampleWriter.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/lir/ItfCounterexampleWriter.scala index 57b9fbf46c..d1fa21b15f 100644 --- a/tla-io/src/main/scala/at/forsyte/apalache/io/lir/ItfCounterexampleWriter.scala +++ b/tla-io/src/main/scala/at/forsyte/apalache/io/lir/ItfCounterexampleWriter.scala @@ -56,7 +56,7 @@ object ItfCounterexampleWriter { ) ) val descriptions = Map[String, ujson.Value]( - FORMAT_DESCRIPTION_FIELD -> "https://apalache.informal.systems/docs/adr/015adr-trace.html", + FORMAT_DESCRIPTION_FIELD -> "https://apalache-mc.org/docs/adr/015adr-trace.html", DESCRIPTION_FIELD -> "Created by Apalache on %s".format(Calendar.getInstance().getTime), ) diff --git a/tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestCounterexampleWriter.scala b/tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestCounterexampleWriter.scala index 0300e299de..9790527c08 100644 --- a/tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestCounterexampleWriter.scala +++ b/tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestCounterexampleWriter.scala @@ -231,7 +231,7 @@ class TestCounterexampleWriter extends AnyFunSuite with TestCounterexampleWriter """{ | "name": "ApalacheIR", | "version": "1.0", - | "description": "https://apalache.informal.systems/docs/adr/005adr-json.html", + | "description": "https://apalache-mc.org/docs/adr/005adr-json.html", | "modules": [ | { | "kind": "TlaModule", @@ -334,7 +334,7 @@ class TestCounterexampleWriter extends AnyFunSuite with TestCounterexampleWriter """{ | "name": "ApalacheIR", | "version": "1.0", - | "description": "https://apalache.informal.systems/docs/adr/005adr-json.html", + | "description": "https://apalache-mc.org/docs/adr/005adr-json.html", | "modules": [ | { | "kind": "TlaModule", @@ -505,7 +505,7 @@ class TestCounterexampleWriter extends AnyFunSuite with TestCounterexampleWriter """{ | "name": "ApalacheIR", | "version": "1.0", - | "description": "https://apalache.informal.systems/docs/adr/005adr-json.html", + | "description": "https://apalache-mc.org/docs/adr/005adr-json.html", | "modules": [ | { | "kind": "TlaModule", diff --git a/tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestItfCounterexampleWriter.scala b/tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestItfCounterexampleWriter.scala index de50228e00..2fa7537f00 100644 --- a/tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestItfCounterexampleWriter.scala +++ b/tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestItfCounterexampleWriter.scala @@ -84,7 +84,7 @@ class TestItfCounterexampleWriter extends AnyFunSuite { s"""{ | "#meta": { | "format": "ITF", - | "format-description": "https://apalache.informal.systems/docs/adr/015adr-trace.html", + | "format-description": "https://apalache-mc.org/docs/adr/015adr-trace.html", | "description": "Created by Apalache" | }, | "params": [ "N" ], @@ -180,7 +180,7 @@ class TestItfCounterexampleWriter extends AnyFunSuite { """{ | "#meta": { | "format": "ITF", - | "format-description": "https://apalache.informal.systems/docs/adr/015adr-trace.html", + | "format-description": "https://apalache-mc.org/docs/adr/015adr-trace.html", | "description": "Created by Apalache" | }, | "vars": [ "a", "b", "c", "d", "e", "f", "g", "h", "n" ], diff --git a/tla-typechecker/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala b/tla-typechecker/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala index 780320bf44..2cd404bc53 100644 --- a/tla-typechecker/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala +++ b/tla-typechecker/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala @@ -898,7 +898,7 @@ class ToEtcExpr( case OperEx(ApalacheOper.withType, _, annotation) => // Met an old type annotation. Warn the user and ignore the annotation. logger.error("Met an old type annotation: " + annotation) - logger.error("See: https://apalache.informal.systems/docs/apalache/typechecker-snowcat.html") + logger.error("See: https://apalache-mc.org/docs/apalache/typechecker-snowcat.html") val msg = s"Old Apalache type annotations (predating 0.12.0) are no longer supported" throw new OutdatedAnnotationsError(msg, ex) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/Feature.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/Feature.scala index b5a804cd35..867b9b9f77 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/Feature.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/Feature.scala @@ -23,8 +23,8 @@ case class RowsFeature( } /** - * Enable imprecise record types, see the discussion in ADR-002. + * Enable imprecise record types, see the + * discussion in ADR-002. * * [[ImpreciseRecordsFeature]] is mutually exclusive with [[RowsFeature]]. It is present only for backwards * compatibility. diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/KeraLanguagePred.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/KeraLanguagePred.scala index 7ca7451a75..5ce282566a 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/KeraLanguagePred.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/KeraLanguagePred.scala @@ -109,7 +109,7 @@ class KeraLanguagePred extends ContextualLanguagePred { } object KeraLanguagePred { - val MANUAL_LINK_SEQ = "https://apalache.informal.systems/docs/apalache/known-issues.html#using-seqs" + val MANUAL_LINK_SEQ = "https://apalache-mc.org/docs/apalache/known-issues.html#using-seqs" private val singleton = new KeraLanguagePred diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/KeramelizerInputLanguagePred.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/KeramelizerInputLanguagePred.scala index 5e481b5e01..2938f3b561 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/KeramelizerInputLanguagePred.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/KeramelizerInputLanguagePred.scala @@ -80,7 +80,7 @@ class KeramelizerInputLanguagePred extends ContextualLanguagePred { } object KeramelizerInputLanguagePred { - val MANUAL_LINK_SEQ = "https://apalache.informal.systems/docs/apalache/known-issues.html#using-seqs" + val MANUAL_LINK_SEQ = "https://apalache-mc.org/docs/apalache/known-issues.html#using-seqs" private val singleton = new KeramelizerInputLanguagePred