[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] TLA+ Course example not working with latest TLA+ Toolbox

From: Sagar Tiwari <iaansagar@xxxxxxxxx>
Date: Sun, 29 Sep 2024 02:07:21 -0700 (PDT)

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?

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/9d96b06e-0a2b-4525-af73-eb11ea47566bn%40googlegroups.com.

Follow-Ups:
- Re: [tlaplus] TLA+ Course example not working with latest TLA+ Toolbox
  - From: Markus Kuppe

Prev by Date: [tlaplus] New blog post: TLA⁺ is more than a DSL for breadth-first search
Next by Date: Re: [tlaplus] TLA+ Course example not working with latest TLA+ Toolbox
Previous by thread: [tlaplus] New blog post: TLA⁺ is more than a DSL for breadth-first search
Next by thread: Re: [tlaplus] TLA+ Course example not working with latest TLA+ Toolbox
Index(es):
- Date
- Thread