search

tlaplus / vscode-tlaplus

TLA+ language support for Visual Studio Code
MIT License
357 stars 33 forks source link

Getting Started page is incorrect #247

Closed rlipscombe closed 2 years ago

rlipscombe commented 2 years ago

If I follow the instructions at https://github.com/tlaplus/vscode-tlaplus/wiki/Getting-Started, it results in the following problems in the translated TLA+:

Couldn't resolve infix operator symbol `..'. [17, 18]
Could not find declaration or definition of symbol '..'. [17, 19]
Couldn't resolve infix operator symbol `<='. [21, 20]
Could not find declaration or definition of symbol '<='. [21, 26]

That's here:

Init == (* Global variables *)
        /\ x \in 1..10             (* here *)
        /\ pc = "Lbl_1"

Lbl_1 == /\ pc = "Lbl_1"
         /\ Assert(x ^ 2 <= 100, "Failure of assertion at line 9, column 5.")       (* here*)
         /\ pc' = "Done"
         /\ x' = x
rlipscombe commented 2 years ago

Changing the EXTENDS TLC line to EXTENDS TLC, Naturals resolves it. If this is the correct fix, the wiki should probably be updated.

lemmy commented 2 years ago

https://github.com/tlaplus/vscode-tlaplus/wiki/Getting-Started/1398a1052f3232761eb0ee19e5e4059fe1c50a9a