Our great sponsors
-
-
WorkOS
The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.
I am very new to TLA+ and I am trying to learn it through the book Specifying Systems by Leslie Lamport. I am currently working on the InnerFIFO example from Chapter 4. I attempted to use the TLC model checker on this example. So, I created a new model and specified the following value to the constant Message - {"hello", "world"}. Upon running the model checker I get the following error -
NOTE:
The number of mentions on this list indicates mentions on common posts plus user suggested alternatives.
Hence, a higher number means a more popular project.
Related posts
- Suggestions for model checking?
- Formal definitions of "events" and "messages" in distributed systems?
- Why is the IDE telling me my actions will never be enabled? How should a mutable array of booleans be represented?
- Generate (message) sequence diagrams from TLA+ state traces
- Where do I find examples of informal specs (RFCs) AND their formal versions (in TLA+ ideally) ?