Markus Alexander Kuppe

[BUG] RewriterException: Expected a constant integer range in .., found 1..N)

9

```tla -------------------------- MODULE AsyncGameOfLife -------------------------- (***********************************************************************) (* Evolution in Asynchronous Cellular Automata *) (* by Chrystopher L. Nehaniv. *) (* https://uhra.herts.ac.uk/bitstream/handle/2299/7041/102007.pdf *) (***********************************************************************) EXTENDS Integers, FiniteSets CONSTANT N ASSUME N...

[BUG] Fairness constraints cause bogus warning about Spec not in canonical form

8

The example below has been fixed. For a follow up, see https://github.com/informalsystems/apalache/issues/468#issuecomment-853259723 ```shell markus@avocado:~/Desktop/ewd998$ apalache check --config=EWD998.cfg EWD998.tla # Tool home: /home/markus/src/TLA/_community/apalache # Package: /home/markus/src/TLA/_community/apalache/mod-distribution/target/apalache-pkg-0.8.2-SNAPSHOT-full.jar # JVM args: -Xmx4096m -DTLA-Library=/home/markus/src/TLA/_community/apalache/src/tla...

[BUG] Bogus "Expected Spec to be in the canonical form Init /\ [][Next]_vars"

2

Reported as not in canonical form: ```tla VARIABLE x Init == x = TRUE Spec == Init /\ [][UNCHANGED x]_x ``` Works fine: ```tla VARIABLE x Init == x =...

[BUG] CHOOSE semantics wrong

12

Specifying Systems page 73 ```tla ---- MODULE C ---- EXTENDS Integers S == {1,2,3} VARIABLE \* @type: Int; x Init == x = CHOOSE n \in S: TRUE Next ==...

[BUG] How to replace z3-turnkey with z3 installed via a package manager?

7

Note that "aarch64" = "arm64". ```shell (Please report an issue at: [https://github.com/informalsystems/apalache/issues],java.lang.UnsatisfiedLinkError: Unsupported CPU architecture: aarch64) Unhandled exception E@18:44:42.428 java.lang.UnsatisfiedLinkError: Unsupported CPU architecture: aarch64 at com.microsoft.z3.Z3Loader$CPUArchitecture.identify(Z3Loader.java:183) at com.microsoft.z3.Z3Loader.loadZ3(Z3Loader.java:57) at com.microsoft.z3.Native.(Native.java:36)...

[BUG] No rewriting rule applies to expression: x ∈ ({t_2$1 ∈ Apalache!Expand(SUBSET {1, 2}): ¬t_2$1 ∈ {{}}})

1

```tla ------- MODULE Foo ------- EXTENDS Integers VARIABLE \* @type: Set(Int); x ConstInit == x \in ((SUBSET {1,2}) \ {{}}) Init == x = {1,2} Next == UNCHANGED x Inv...

[BUG] Bogus violation with ConstInit and SUBSET (A set filter over PowSet[FinSet[Int]] is not implemented)

1

```tla ------- MODULE Foo ------- EXTENDS Integers CONSTANT \* @type: Set(Int); S ConstInit == S \in ( (SUBSET {1,2}) \ {{}} ) VARIABLE \* @type: Set(Int); x Init == x...

[BUG] Unbounded CHOOSE causes bogus warning "WORKAROUND #130: labelling operator Null as recursive, though SANY did not tell us so."

3

```tla ---- MODULE Spec ---- EXTENDS Sequences \* Super lucky that the unbounded CHOOSE picks an element that happens to match Seq(Int) Null == CHOOSE Null : TRUE \* but...

https://code.visualstudio.com/blogs/2021/10/11/webview-ui-toolkit https://github.com/tlaplus/vscode-tlaplus/issues/260 https://github.com/tlaplus/vscode-tlaplus/issues/259 https://github.com/tlaplus/vscode-tlaplus/issues/258 https://github.com/tlaplus/vscode-tlaplus/issues/257 https://github.com/tlaplus/vscode-tlaplus/issues/256 https://github.com/tlaplus/vscode-tlaplus/issues/255 https://github.com/tlaplus/vscode-tlaplus/issues/250 https://github.com/tlaplus/vscode-tlaplus/issues/239 https://github.com/tlaplus/vscode-tlaplus/issues/229 https://github.com/tlaplus/vscode-tlaplus/issues/215 https://github.com/tlaplus/vscode-tlaplus/issues/164

Syntax highlighting broken for single-line LET with multiple definitions

3

```tla LET from == GraphNodePos[u[1]] to == GraphNodePos[u[2]] ... IN ... ``` Note the `to` that is not highlighted.