-
InfluxDB
Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
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) ?