search

hwayne / learntla-v2

Learn TLA+ for free! No prior experience necessary!
https://www.learntla.com
Other
185 stars 39 forks source link

Core->Setup: No Overdrafts in Invariants results in error #15

Closed Svintooo closed 2 years ago

Svintooo commented 2 years ago

File

docs/core/setup.rst

Problem

Adding "No Overdrafts" as an Invariant results in an error when trying to run the model.

Error

***Parse Error***
Was expecting "=== or more Module body"
Encountered "Overdrafts" in Invariants at line 1 and token "No"

Residual stack trace follows:
Module definition starting at line 1, column 1.

Comments

I am complete beginner. I have never heard of TLA or touched it before. I redid the guide from scratch an extra time just to make sure I didn't do anything wrong. But I got the same error both times.

My Setup

OS: Windows 10 (running in a VM) Cores: 1 RAM: 4G Java: Version 8 Update 333 (build 1.8.0_333-b02) Toolbox: https://github.com/tlaplus/tlaplus/releases/tag/v1.8.0 Exec: Unpacked TLAToolbox-1.8.0-win32.win32.x86_64.zip and ran toolbox.exe

hwayne commented 2 years ago

Does NoOverdrafts work without a space?

On Sat, Jul 2, 2022, 5:00 PM Svintooo @.***> wrote:

File

docs/core/setup.rst Problem

Adding "No Overdrafts" as an Invariant results in an error when trying to run the model. Error

Parse Error Was expecting "=== or more Module body" Encountered "Overdrafts" in Invariants at line 1 and token "No"

Residual stack trace follows: Module definition starting at line 1, column 1.

Comments

I am complete beginner. I have never heard of TLA or touched it before. I redid the guide from scratch an extra time just to make sure I didn't do anything wrong. But I got the same error both times. My Setup

OS: Windows 10 (running in a VM) Cores: 1 RAM: 4G Java: Version 8 Update 333 (build 1.8.0_333-b02) Toolbox: https://github.com/tlaplus/tlaplus/releases/tag/v1.8.0 Exec: Unpacked TLAToolbox-1.8.0-win32.win32.x86_64.zip and ran toolbox.exe

— Reply to this email directly, view it on GitHub https://github.com/hwayne/learntla-v2/issues/15, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAUJO5E3HWZNSKSWKINKVLTVSC3ZRANCNFSM52PVMPKQ . You are receiving this because you are subscribed to this thread.Message ID: @.***>

Svintooo commented 2 years ago

Using NoOverdrafts (without a space) seems to resolve the problem. I am now able to continue. Thank you!

hwayne commented 2 years ago

Sounds like something I need to fix!

npalladium commented 2 years ago

Just came here to file this issue/open a tiny PR to fix the space. :P

hwayne commented 2 years ago

Merg'd!