TLA+ Course example not working with latest TLA+ Toolbox

[Sagar Tiwari]

Hi. I'm completely green when it comes to TLA+. I'm going through the course by Leslie Lamport and got stuck at the first TLA+ example. I copy pasted the example provided with the course and the behavior spec doesn't form doesn't look like it does in the course video. You can see the code and the error message in the screenshot. How do I fix this issue?

[Markus Kuppe]

Hi Sagar,

you need to move the module end marker (`=====`) currently on line 4 down to below line 19. As it stands, lines 6 to 19 are not included within the module. After making this adjustment, the Toolbox should allow you to set the behavior specification to the initial predicate Init and the next-state relation Next.

M.

> On Sep 29, 2024, at 2:07 AM, Sagar Tiwari <iaan...@gmail.com> wrote:
>
> Hi. I'm completely green when it comes to TLA+. I'm going through the course by Leslie Lamport and got stuck at the first TLA+ example. I copy pasted the example provided with the course and the behavior spec doesn't form doesn't look like it does in the course video. You can see the code and the error message in the screenshot. How do I fix this issue?<CopyQ.PCHrug.png>

[Sagar Tiwari]

That worked. Thanks!

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/eIZp5nS1WJc/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/018E2EE8-CA89-440D-92CF-D12208B55F6B%40lemmster.de.

--

Best Regards
Sagar Tiwari