Andrew Helwer

ASSUME statements are not checked in imported modules

4

TLC does not check the ASSUME statement in the System module when model-checking the SystemMC module. ```tla ------------------------------- MODULE System ------------------------------- CONSTANT Input ASSUME Input = 0 ============================================================================= ``` ```tla...

SANY NullPointerException when parsing malformed MODULE header

3

**Version Info** TLC version: 1.7.0 release (and 12/11/2020 nightly) JRE version: AdoptOpenJDK build 15.0.1+9 OS version: Windows 10 **What happened?** I ran SANY on this malformed TLA+ spec, which doesn't...

TLC checks wrong TLA file when TLA file of same name is in current working directory

2

**Version Info** TLC version: 11/24/2020 nightly build (also 1.7.0 release) JRE version: AdoptOpenJDK build 15.0.1+9 OS version: Windows 10 **What happened? What did you expect to happen?** I had the...

Toolbox & SANY could improve parse error message when proof step level exceeds 2^31

1

This is clearly a dubious case to handle but I will document it in the interest of completeness (maybe a good project for a first-time contributor?). The upper limit of...

SANY handles it just fine, but syntax highlighting in the toolbox cannot handle strings with escape quotes, for example: ```tla ---- MODULE MySpec ---- op == "escape \" quote" ====...

SANY does not correctly parse lor/land operators in nonfix form

4

The following specs produce parse errors of `Encountered "," at line X, column Y etc.`: ```tla ---- MODULE MySpec ---- op == \/(TRUE, FALSE) ==== ``` ```tla ---- MODULE MySpec...

SANY differs from TLA+ language spec for parsing number values with decimals

1

According to the formal TLA+ grammar found in Specifying Systems, this statement should be syntactically valid: ```tla x == .3 ``` See [this line](https://github.com/tlaplus/Examples/blob/a9c08fd68e4e646855ca9fb5e49db4804ffc07d4/specifications/SpecifyingSystems/Syntax/TLAPlusGrammar.tla#L32) of the formal grammar; it is...

SANY allows LOCAL token in place it shouldn't, which crashes TLAPS

1

Here are two specs reproducing the issue. The `LocalInDefStep` module crashes TLAPS. The `LocalInLetIn` module doesn't seem to crash TLC. Discussion below: ```tla ---- MODULE LocalInDefStep ---- THEOREM TRUE PROOF...

Interpret expressions of the form CHOOSE x : x \in S

1

Occasionally I'll have to write something like this: ```tla RECURSIVE SetSum(_) SetSum(S) == LET e == CHOOSE s \in S : TRUE IN IF S = {} THEN 0 ELSE...

SANY fails to parse certain higher-order operator arguments

3

Using SANY 1.8.0. One spec reproducing issue: ```tla ---- MODULE MySpec ---- EXTENDS Naturals F(Op(_,_)) == Op(1,2) Foo == F(+) ==== ``` SANY generates the following error: ``` Encountered "===="...