tlaplus / examples

A collection of TLA⁺ specifications of varying complexities

TLA⁺ Examples

This is a repository of TLA⁺ specifications and models covering applications in a variety of fields. It serves as:

• a comprehensive example library demonstrating how to specify an algorithm in TLA⁺
• a diverse corpus facilitating development & testing of TLA⁺ language tools
• a collection of case studies in the application of formal specification in TLA⁺

All TLA⁺ specs can be found in the specifications directory. The table below lists all specs and their features, such as whether they are suitable for beginners, come with an additional PlusCal variant (✔), or use PlusCal exclusively. The manifest.json file is the source of truth for this table, and is a detailed human- & machine-readable description of the specs & their models. Its schema is manifest-schema.json. All specs in this repository are subject to CI validation to ensure quality.

Examples Included Here

Here is a list of specs included in this repository, with links to the relevant directory and flags for various features:

Name	Author(s)	Beginner	TLAPS Proof	PlusCal	TLC Model	Apalache
Teaching Concurrency	Leslie Lamport	✔	✔	✔	✔
Loop Invariance	Leslie Lamport	✔	✔	✔	✔
Learn TLA⁺ Proofs	Andrew Helwer	✔	✔	✔	✔
Boyer-Moore Majority Vote	Stephan Merz	✔	✔		✔
Proof x+x is Even	Stephan Merz	✔	✔		✔
The N-Queens Puzzle	Stephan Merz	✔		✔	✔
The Dining Philosophers Problem	Jeff Hemphill	✔		✔	✔
The Car Talk Puzzle	Leslie Lamport	✔			✔
The Die Hard Problem	Leslie Lamport	✔			✔
The Prisoners & Switches Puzzle	Leslie Lamport	✔			✔
Specs from Specifying Systems	Leslie Lamport	✔			✔
The Tower of Hanoi Puzzle	Markus Kuppe, Alexander Niederbühl	✔			✔
Missionaries and Cannibals	Leslie Lamport	✔			✔
Stone Scale Puzzle	Leslie Lamport	✔			✔
The Coffee Can Bean Problem	Andrew Helwer	✔			✔
EWD687a: Detecting Termination in Distributed Computations	Stephan Merz, Leslie Lamport, Markus Kuppe	✔		(✔)	✔
The Boulangerie Algorithm	Leslie Lamport, Stephan Merz		✔	✔	✔
Misra Reachability Algorithm	Leslie Lamport		✔	✔	✔
Byzantizing Paxos by Refinement	Leslie Lamport		✔	✔	✔
EWD840: Termination Detection in a Ring	Stephan Merz		✔		✔
EWD998: Termination Detection in a Ring with Asynchronous Message Delivery	Stephan Merz, Markus Kuppe		✔	(✔)	✔
The Paxos Protocol	Leslie Lamport		✔		✔
Asynchronous Reliable Broadcast	Thanh Hai Tran, Igor Konnov, Josef Widder		✔		✔
Distributed Mutual Exclusion	Stephan Merz		✔		✔
Two-Phase Handshaking	Leslie Lamport, Stephan Merz		✔		✔
Paxos (How to Win a Turing Award)	Leslie Lamport		✔		✔
Dijkstra's Mutual Exclusion Algorithm	Leslie Lamport			✔	✔
The Echo Algorithm	Stephan Merz			✔	✔
The TLC Safety Checking Algorithm	Markus Kuppe			✔	✔
Transaction Commit Models	Leslie Lamport, Jim Gray, Murat Demirbas			✔	✔
The Slush Protocol	Andrew Helwer			✔	✔
Minimal Circular Substring	Andrew Helwer			✔	✔
Snapshot Key-Value Store	Andrew Helwer, Murat Demirbas			✔	✔
Chang-Roberts Algorithm for Leader Election in a Ring	Stephan Merz			✔	✔
MultiPaxos in SMR-Style	Guanzhou Hu			✔	✔
Einstein's Riddle	Isaac DeFrain, Giuliano Losa					✔
Resource Allocator	Stephan Merz				✔
Transitive Closure	Stephan Merz				✔
Atomic Commitment Protocol	Stephan Merz				✔
SWMR Shared Memory Disk Paxos	Leslie Lamport, Giuliano Losa				✔
Span Tree Exercise	Leslie Lamport				✔
The Knuth-Yao Method	Ron Pressler, Markus Kuppe				✔
Huang's Algorithm	Markus Kuppe				✔
EWD 426: Token Stabilization	Murat Demirbas, Markus Kuppe				✔
Sliding Block Puzzle	Mariusz Ryndzionek				✔
Single-Lane Bridge Problem	Younes Akhouayri				✔
Software-Defined Perimeter	Luming Dong, Zhi Niu				✔
Simplified Fast Paxos	Lim Ngian Xin Terry, Gaurav Gandhi				✔
Checkpoint Coordination	Andrew Helwer				✔
Finitizing Monotonic Systems	Andrew Helwer				✔
Multi-Car Elevator System	Andrew Helwer				✔
Nano Blockchain Protocol	Andrew Helwer				✔
The Readers-Writers Problem	Isaac DeFrain				✔
Asynchronous Byzantine Consensus	Thanh Hai Tran, Igor Konnov, Josef Widder				✔
Folklore Reliable Broadcast	Thanh Hai Tran, Igor Konnov, Josef Widder				✔
The Bosco Byzantine Consensus Algorithm	Thanh Hai Tran, Igor Konnov, Josef Widder				✔
Consensus in One Communication Step	Thanh Hai Tran, Igor Konnov, Josef Widder				✔
One-Step Consensus with Zero-Degradation	Thanh Hai Tran, Igor Konnov, Josef Widder				✔
Failure Detector	Thanh Hai Tran, Igor Konnov, Josef Widder				✔
Asynchronous Non-Blocking Atomic Commit	Thanh Hai Tran, Igor Konnov, Josef Widder				✔
Asynchronous Non-Blocking Atomic Commitment with Failure Detectors	Thanh Hai Tran, Igor Konnov, Josef Widder				✔
Spanning Tree Broadcast Algorithm	Thanh Hai Tran, Igor Konnov, Josef Widder				✔
The Cigarette Smokers Problem	Mariusz Ryndzionek				✔
Conway's Game of Life	Mariusz Ryndzionek				✔
Chameneos, a Concurrency Game	Mariusz Ryndzionek				✔
PCR Testing for Snippets of DNA	Martin Harrison				✔
RFC 3506: Voucher Transaction System	Santhosh Raju, Cherry G. Mathew, Fransisca Andriani				✔
Yo-Yo Leader Election	Ludovic Yvoz, Stephan Merz				✔
TCP as defined in RFC 9293	Markus Kuppe				✔
TLA⁺ Level Checking	Leslie Lamport
Condition-Based Consensus	Thanh Hai Tran, Igor Konnov, Josef Widder

Examples Elsewhere

Here is a list of specs stored in locations outside this repository, including submodules. They are not covered by CI testing so it is possible they contain errors, the reported details are incorrect, or they are no longer available. Ideally these will be moved into this repo over time.

Spec	Details	Author(s)	Beginner	TLAPS Proof	TLC Model	PlusCal	Apalache
Blocking Queue	BlockingQueue	Markus Kuppe	✔	✔	✔	(✔)
IEEE 802.16 WiMAX Protocols	2006, paper, specs	Prasad Narayana, Ruiming Chen, Yao Zhao, Yan Chen, Zhi (Judy) Fu, Hai Zhou
On the diversity of asynchronous communication	2016, paper, specs	Florent Chevrou, Aurélie Hurault, Philippe Quéinnec
Caesar	Multi-leader generalized consensus protocol (Arun et al., 2017)	Giuliano Losa			✔	✔
CASPaxos	An extension of the single-decree Paxos algorithm to a compare-and-swap type register (Rystsov)	Tobias Schottdorf			✔
DataPort	Dataport protocal 505.89PT, only PDF files (Biggs & Noriaki, 2016)	Geoffrey Biggs, Noriaki Ando
egalitarian-paxos	Leaderless replication protocol based on Paxos (Moraru et al., 2013)	Iulian Moraru			✔
fastpaxos	An extension of the classic Paxos algorithm, only PDF files (Lamport, 2006)	Leslie Lamport
fpaxos	A variant of Paxos with flexible quorums (Howard et al., 2017)	Heidi Howard			✔
HLC	Hybrid logical clocks and hybrid vector clocks (Demirbas et al., 2014)	Murat Demirbas			✔	✔
L1	Data center network L1 switch protocol, only PDF files (Thacker)	Tom Rodeheffer
leaderless	Leaderless generalized-consensus algorithms (Losa, 2016)	Giuliano Losa			✔	✔
losa_ap	The assignment problem, a variant of the allocation problem (Delporte-Gallet, 2018)	Giuliano Losa			✔	✔
losa_rda	Applying peculative linearizability to fault-tolerant message-passing algorithms and shared-memory consensus, only PDF files (Losa, 2014)	Giuliano Losa
m2paxos	Multi-leader consensus protocols (Peluso et al., 2016)	Giuliano Losa			✔
mongo-repl-tla	A simplified part of Raft in MongoDB (Ongaro, 2014)	Siyuan Zhou			✔
MultiPaxos	The abstract specification of Generalized Paxos (Lamport, 2004)	Giuliano Losa			✔
naiad	Naiad clock protocol, only PDF files (Murray et al., 2013)	Tom Rodeheffer			✔
nfc04	Non-functional properties of component-based software systems (Zschaler, 2010)	Steffen Zschaler			✔
raft	Raft consensus algorithm (Ongaro, 2014)	Diego Ongaro			✔
SnapshotIsolation	Serializable snapshot isolation (Cahill et al., 2010)	Michael J. Cahill, Uwe Röhm, Alan D. Fekete			✔
SyncConsensus	Synchronized round consensus algorithm (Demirbas)	Murat Demirbas			✔	✔
Termination	Channel-counting algorithm (Kumar, 1985)	Giuliano Losa		✔	✔	✔	✔
Tla-tortoise-hare	Robert Floyd's cycle detection algorithm	Lorin Hochstein			✔	✔
VoldemortKV	Voldemort distributed key value store	Murat Demirbas			✔	✔
Tencent-Paxos	PaxosStore: high-availability storage made practical in WeChat. Proceedings of the VLDB Endowment(Zheng et al., 2017)	Xingchen Yi, Hengfeng Wei		✔	✔
Paxos	Paxos				✔
Lock-Free Set	PlusCal spec of a lock-Free set used by TLC	Markus Kuppe			✔	✔
ParallelRaft	A variant of Raft	Xiaosong Gu, Hengfeng Wei, Yu Huang			✔
CRDT-Bug	CRDT algorithm with defect and fixed version	Alexander Niederbühl			✔
asyncio-lock	Bugs from old versions of Python's asyncio lock	Alexander Niederbühl			✔
Raft (with cluster changes)	Raft with cluster changes, and a version with Apalache type annotations but no cluster changes	George Pîrlea, Darius Foom, Brandon Amos, Huanchen Zhang, Daniel Ricketts			✔		✔
MET for CRDT-Redis	Model-check the CRDT designs, then generate test cases to test CRDT implementations	Yuqi Zhang			✔	✔
Parallel increment	Parallel threads incrementing a shared variable. Demonstrates invariants, liveness, fairness and symmetry	Chris Jensen			✔
The Streamlet consensus algorithm	Specification and model-checking of both safety and liveness properties of Streamlet with TLC	Giuliano Losa			✔	✔
Petri Nets	Instantiable Petri Nets with liveness properties	Eugene Huang			✔
CRDT	Specifying and Verifying CRDT Protocols	Ye Ji, Hengfeng Wei			✔
Azure Cosmos DB	Consistency models provided by Azure Cosmos DB	Dharma Shukla, Ailidani Ailijiang, Murat Demirbas, Markus Kuppe			✔	✔

License

The repository is under the MIT license and you are encouraged to publish your spec under a similarly-permissive license. However, your spec can be included in this repo along with your own license if you wish.

Support or Contact

Do you have any questions or comments? Please open an issue or send an email to the TLA+ group.

Contributing

Do you have your own case study or TLA⁺ specification you'd like to share with the community? Follow these instructions:

1. Fork this repository and create a new directory under specifications with the name of your spec
2. Place all TLA⁺ files in the directory, along with their .cfg model files
3. You are encouraged to include at least one model that completes execution in less than 10 seconds, and (if possible) a model that fails in an interesting way - for example illustrating a system design you previously attempted that was found unsound by TLC
4. Ensure name of each .cfg file matches the .tla file it models, or has its name as a prefix; for example SpecName.tla can have the models SpecName.cfg and SpecNameLiveness.cfg, etc.
5. Consider including a README.md in the spec directory explaining the significance of the spec with links to any relevant websites or publications, or integrate this info as comments in the spec itself
6. Add an entry to the table of specs included in this repo, summarizing your spec and its attributes

Adding Spec to Continuous Integration

To combat bitrot, it is important to add your spec and model to the continuous integration system. To do this, you'll have to update the manifest.json file with machine-readable records of your spec files. If this process doesn't work for you, you can alternatively modify the .ciignore file to exclude your spec from validation. Modifying the manifest.json can be done manually or (recommended) following these directions:

1. Ensure you have Python 3.11+ installed
2. It is considered best practice to create & initialize a Python virtual environment to preserve your system package store; run python -m venv . then source ./bin/activate on Linux & macOS or .\Scripts\activate.bat on Windows (run deactivate to exit)
3. Run pip install -r .github/scripts/requirements.txt
4. Run python .github/scripts/generate_manifest.py
5. Locate your spec's entry in the manifest.json file and ensure the following fields are filled out:
   • Spec title: an appropriate title for your specification
   • Spec description: a short description of your specification
   • Spec sources: links relevant to the source of the spec (papers, blog posts, repositories)
   • Spec authors: a list of people who authored the spec
   • Spec tags:
     • "beginner" if your spec is appropriate for TLA⁺ newcomers
   • Model runtime: approximate model runtime on an ordinary workstation, in "HH:MM:SS" format
   • Model size:
     • "small" if the model can be executed in less than 10 seconds
     • "medium" if the model can be executed in less than five minutes
     • "large" if the model takes more than five minutes to execute
   • Model mode:
     • "exhaustive search" by default
     • {"simulate": {"traceCount": N}} for a simulation model
     • "generate" for model trace generation
   • Model result:
     • "success" if the model completes successfully
     • "assumption failure" if the model violates an assumption
     • "safety failure" if the model violates an invariant
     • "liveness failure" if the model fails to satisfy a liveness property
     • "deadlock failure" if the model encounters deadlock
   • (Optional) Model state count info: distinct states, total states, and state depth
     • These are all individually optional and only valid if your model uses exhaustive search and results in success
     • Recording these turns your model into a powerful regression test for TLC
   • Other fields are auto-generated by the script; if you are adding an entry manually, ensure their values are present and correct (see other entries or the manifest-schema.json file)

Before submitted your changes to run in the CI, you can quickly check your manifest.json for errors and also check it against manifest-schema.json at https://www.jsonschemavalidator.net/.

examples's Issues

Basic math exercises

Unfinished, random math exercises collected from Specifying Systems, LearnTLA, and elsewhere.

---- MODULE F ----
EXTENDS Naturals, FiniteSets, Sequences

(* 1. Set of all permutations of {"T","L","A"} including repetitions. *)
PermsWithReps(S) ==
    [ 1..Cardinality(S) -> S ]
    
ASSUME 
    PermsWithReps({"T","L","A"}) =
        {<<"T", "T", "T">>, <<"T", "T", "L">>, <<"T", "T", "A">>, 
            <<"T", "L", "T">>, <<"T", "L", "L">>, <<"T", "L", "A">>, 
            <<"T", "A", "T">>, <<"T", "A", "L">>, <<"T", "A", "A">>, 
            <<"L", "T", "T">>, <<"L", "T", "L">>, <<"L", "T", "A">>, 
            <<"L", "L", "T">>, <<"L", "L", "L">>, <<"L", "L", "A">>, 
            <<"L", "A", "T">>, <<"L", "A", "L">>, <<"L", "A", "A">>, 
            <<"A", "T", "T">>, <<"A", "T", "L">>, <<"A", "T", "A">>, 
            <<"A", "L", "T">>, <<"A", "L", "L">>, <<"A", "L", "A">>, 
            <<"A", "A", "T">>, <<"A", "A", "L">>, <<"A", "A", "A">>}

(* 2. All combinations of a two-digit lock. *)
TwoDigitLock ==
    [1..2 -> 0..9]

ASSUME
    /\ (0..9) \X (0..9) = TwoDigitLock
    /\ {<<n,m>> : n,m \in 10..19} \notin SUBSET TwoDigitLock

(* 3. All combinations of a three-digit lock. *)
ThreeDigitLock ==
    [1..3 -> 0..9]

ASSUME
    /\ (0..9) \X (0..9) \X (0..9) = ThreeDigitLock
    /\ {<<n,m,o>> : n,m,o \in 10..19} \notin SUBSET ThreeDigitLock

(* 4. All pairs (including repetitions) of the natural numbers. *)
PairsOfNaturals ==
    [1..2 -> Nat]

ASSUME
    {<<n,m>> : n,m \in 0..100} \subseteq PairsOfNaturals

(* 5. All triples... *)
TriplesOfNaturals ==
    [1..3 -> Nat]

ASSUME
    {<<n,m,o>> : n,m,o \in 0..25} \subseteq TriplesOfNaturals

(* 6. Set of all pairs and triples... *)
PairsAndTriplesOfNaturals ==
    [1..2 -> Nat] \cup [1..3 -> Nat]

ASSUME
    /\ {<<n,m>> : n,m \in 0..100} \subseteq PairsAndTriplesOfNaturals
    /\ {<<n,m,o>> : n,m,o \in 0..25} \subseteq PairsAndTriplesOfNaturals

(* 7. What is the Cardinality of 3. ? *)
Cardinality3 ==
    Cardinality(ThreeDigitLock)

ASSUME Cardinality3 = 1000

(* 8. What is the Cardinality of 6. (PairsAndTriplesOfNaturals) ? *)

--------------------------------------------------------------

(* 9. The range/image/co-domain of a function. *)
Range(f) == { f[x]: x \in DOMAIN f }

ASSUME Range([a |-> 1, b |-> 2, c |-> 3]) = 1..3

(* 10. The permutations of a set _without_ repetition. *)
Perms(S) ==
    { f \in [S -> S] :
        Range(f) = S }

ASSUME Perms({1,2,3}) =
             {<<1, 2, 3>>, <<1, 3, 2>>,
              <<2, 1, 3>>, <<2, 3, 1>>,
              <<3, 1, 2>>, <<3, 2, 1>>}

Perms2(S) ==
    \* If for all w in S there exists a v in S for which f[v]=w,
    \* there can be no repetitions as a consequence. The predicate
    \* demands for all elements of S to be in the range of f.
    { f \in [S -> S] :
        \A w \in S :
            \E v \in S : f[v]=w }

ASSUME Perms2({1,2,3}) =
             {<<1, 2, 3>>, <<1, 3, 2>>,
              <<2, 1, 3>>, <<2, 3, 1>>,
              <<3, 1, 2>>, <<3, 2, 1>>}

Perms3(S) ==
    { f \in [S -> S] :
        \A i,j \in DOMAIN f :
            i # j => f[i] # f[j] }

ASSUME Perms3({1,2,3}) =
             {<<1, 2, 3>>, <<1, 3, 2>>,
              <<2, 1, 3>>, <<2, 3, 1>>,
              <<3, 1, 2>>, <<3, 2, 1>>}

(* 11. Reverse a sequence (a function with domain 1..N). *)
Reverse(seq) ==
    [ i \in 1..Len(seq) |-> seq[Len(seq)+1 - i] ]

ASSUME Reverse(<<1, 2, 3>>) = <<3, 2, 1>>
ASSUME Reverse(<<>>) = <<>>

(* 12. An (infix) operator to quickly define a function mapping an x to a y.  *)
x :> y ==
    [ e \in {x} |-> y ]

ASSUME "x" :> 42 = [ x |-> 42 ]

(* 13. Merge two functions f and g *)
f ++ g ==
  [x \in (DOMAIN f) \cup (DOMAIN g) |-> IF x \in DOMAIN f THEN f[x] ELSE g[x]]

ASSUME <<1,2,3>> ++ [i \in 1..6 |-> i] = <<1, 2, 3, 4, 5, 6>>

(* 14. Advanced!!! Inverse of a function f (swap the domain and range). *)
Inverse(f) ==
   CHOOSE g \in [ Range(f) -> DOMAIN f] : \A s \in DOMAIN f: g[f[s]]=s

ASSUME Inverse(("a" :> 0) ++ ("b" :> 1) ++ ("c" :> 2)) =
              ((0 :> "a") ++ (1 :> "b") ++ (2 :> "c"))
====

-------------------------- MODULE SyntaxExcercises --------------------------
(* The idea is that learners get the spec with the operator _definitions_ replaced 
    with TRUE. A learner can then check their definitions with TLC. *)
EXTENDS Integers, Sequences, TLC

(***************************************************************************)
(* The set of the fibonacci numbers: 1,1,2,3,5,8,13,...                    *)
(***************************************************************************)
MyNat == 1..21 \* perhaps, introduce model definitions right away?
fib[n \in MyNat] == IF n <= 2 THEN 1 ELSE fib[n-1] + fib[n-2]

ASSUME fib[12] = 144

RECURSIVE fibRecurse(_)
fibRecurse(n) == IF n <= 2 THEN 1 ELSE fibRecurse(n - 1) + fibRecurse(n - 2)

ASSUME fibRecurse(12) = 144

(***************************************************************************)
(* The set of fibonacci numbers in the range [10,20).                      *)
(***************************************************************************)
FibSet == { fib[n] : n \in 10..19 }

ASSUME FibSet = {55, 89, 144, 233, 377, 610, 987, 1597, 2584, 4181}

FibSetRecurse == { fibRecurse(n) : n \in 10..19 }

ASSUME FibSetRecurse = {55, 89, 144, 233, 377, 610, 987, 1597, 2584, 4181}

(***************************************************************************)
(* The sequence of fibonacci numbers in the range [10,20).                 *)
(***************************************************************************)
FibSeq == [ e \in 1..10 |-> fib[e+9] ]

ASSUME FibSeq = <<55, 89, 144, 233, 377, 610, 987, 1597, 2584, 4181>>

(***************************************************************************)
(* The range of a function func.                                           *)
(***************************************************************************)
Range(func) == { func[e] : e \in DOMAIN func }

(* Change the 5., 10, 15. element of a function f to "abc", "def" and "ghi" *)
(* TCommit video Minute 12:30 *)
Replace(func, pos, value) == [func EXCEPT ![pos] = value ]

ASSUME [ i \in 1..3 |-> i^2 ] = Replace(Replace(Replace([i \in 1..3 |-> 0], 1, 1), 2, 4), 3, 9)

(***************************************************************************)
(* Excercise page 235/70                                                   *)
(* The sequence obtained by removing the i-th element of seq.              *)
(***************************************************************************)
Remove(seq, i) == [ j \in (1..Len(seq) - 1) |-> (IF j < i THEN seq[j] ELSE seq[j+1]) ]

(***************************************************************************)
(* Excercise page 341/91                                                   *)
(* Recursive definition of the Len(seq) _operator_ with Tail.              *)
(***************************************************************************)
RECURSIVE RecLen(_)
RecLen(seq) == IF seq = <<>> THEN 0
               ELSE 1 + RecLen(Tail(seq))

(***************************************************************************)
(* An alternative variant which treats seq as the function it is and       *)
(* returns the maximum of its DOMAIN which corresponds to the number of    *)
(* elements in seq.                                                        *)
(***************************************************************************)
DomLen(seq) == CHOOSE m \in (DOMAIN seq): (DOMAIN seq) = 1..m

(***************************************************************************)
(* Write an operator that returns the cardinality of a given set.          *)
(***************************************************************************)
RECURSIVE Card(_)
Card(S) == IF S = {} THEN 0 ELSE 1 + Card(S \ {CHOOSE e \in S : TRUE})

ASSUME Card({}) = 0 /\ Card({1,1,2,2,3,3}) = 3

(***************************************************************************)
(* Write an operator that takes a tuple/sequence and, if the tuple is      *)
(* length two, returns the reversed tuple, and otherwise raises an error.  *)
(***************************************************************************)
ReverseOfTwo(seq) == IF Len(seq) = 2 THEN <<seq[2], seq[1]>>
                                     ELSE Assert(FALSE, "")

ASSUME <<4,5>> = ReverseOfTwo(<<5,4>>)

(***************************************************************************)
(* Write an operator that takes a sequence seq and, if the sequence is of  *)
(* uneven length, returns the reversed sequence, otherwise return seq.     *)
(***************************************************************************)
Uneven(n) == n % 2 = 1
Reverse(seq) == [ i \in 1..Len(seq) |-> seq[Len(seq) - (i-1)] ]
ReverseUneven(seq) == IF Uneven(Len(seq)) THEN Reverse(seq)
                                     ELSE seq

ASSUME <<1,2,3,4,5>> = ReverseUneven(<<5,4,3,2,1>>)
ASSUME <<1,2,3,4>> = ReverseUneven(<<1,2,3,4>>)

(* Sum of elements in seq *)

(***************************************************************************)
(* Remove those elements from sequence seq for which Filter(_) holds.      *)
(***************************************************************************)
RECURSIVE Subseq(_,_)
Subseq(Filter(_), seq) == IF seq = <<>>
                          THEN <<>>
                          ELSE IF Filter(Head(seq))
                               THEN <<Head(seq)>> \o Subseq(Filter, Tail(seq))
                               ELSE Subseq(Filter, Tail(seq))

Even(n) == ~Uneven(n)

ASSUME Subseq(Even, <<1,2,1,3,3,6,8,8,23,42>>) = <<2,6,8,8,42>>

SelectSeq2(Test(_), s) ==
  LET S[i \in 0..Len(s)] ==
        IF i = 0 THEN << >> \* As a basis set the s[0] = <<>>
                 ELSE IF Test(s[i]) THEN S[i-1] \o <<s[i]>> \* copy previous value and concat with s[i]
                                    ELSE S[i-1] \* just copy the previous value
  IN S[Len(s)] \* The maximum (last function position) contains the collected sequence


ASSUME Subseq(Even, <<1,2,1,3,3,6,8,8,23,42>>) = SelectSeq2(Even, <<1,2,1,3,3,6,8,8,23,42>>)

(***************************************************************************)
(* Given DOMAIN Tuple is the set of numbers Tuple is defined over, write   *)
(* an operator that gives a set of the values of the Tuple, ie the range.  *)
(***************************************************************************)




(***************************************************************************)
(* Write an operator that takes two sets S1 and S2 and determines if the   *)
(* double of every element in S1 is an element of S2.                      *)
(***************************************************************************)




(***************************************************************************)
(* Given a sequence of sets, write an operator that determines if a given  *)
(* element is found in any of the sequence’s sets.                         *)
(* IE Op("a", <<{"b", "c"}, {"a", "c"}>>) = TRUE.                            *)
(***************************************************************************)


(* Given the (built-in) set Nat (Naturals), create a subset of S whose largest element is 42. *)
(* Hint: Override Nat with 1..1000 on the Advanced Options page of the Model editor. By default *)
(* Nat is represented as a UserValue in TLC. A UserValue is _not_ enumerable, whereas a 1..1000 *)
(* is represented as a (finite) IntervalValue which subsequently can be enumerated. *)
Subset42 == { i \in Nat: i < 43 }

\*ASSUME Subset42 = 1..42


(* The inverse of a function *)
Inverse(f) == 
   CHOOSE g \in [ Range(f) -> DOMAIN f] : \A s \in DOMAIN f: g[f[s]]=s

ASSUME Inverse("a" :> 0 @@ "b" :> 1 @@ "c" :> 2) = (0 :> "a" @@ 1 :> "b" @@ 2 :> "c")

(* Merge two functions f and g *)
Merge(f, g) == 
  [x \in (DOMAIN f) \cup (DOMAIN g) |-> IF x \in DOMAIN f THEN f[x] ELSE g[x]]

ASSUME Merge(<<1,2,3>>, [i \in 1..6 |-> i]) = <<1, 2, 3, 4, 5, 6>>

(* The permutations of a set *)
Perms(S) == 
    {f \in [S -> S] : \A w \in S : \E v \in S : f[v]=w}

ASSUME Perms({1,2,3}) = {<<1, 2, 3>>, <<1, 3, 2>>, <<2, 1, 3>>, <<2, 3, 1>>, <<3, 1, 2>>, <<3, 2, 1>>}
=============================================================================

Graphs

1. With the definitions from the Graphs module, under what conditions
   is <<p>> an element of Path(G)?

2. Find the following values, and use TLC to check your answers.
   (See the file PrintValues.tla in the folder AsynchronousMemory.)

   [i \in Nat |-> i^2][42]

   LET f == [i \in Nat |-> i^2] 
   IN  [f EXCEPT ![42] = 24][42]

   LET f == [i \in Nat |-> i^2] 
   IN  [f EXCEPT ![42] = @ - 24, ![24] = 42][42]
   
   LET f[i \in Nat] == IF i = 0 THEN 0 ELSE f[i-1] + i
   IN  f[42]

   [i \in {"a", "bc", "d"} |-> IF i = "a" THEN 17
                                          ELSE 42].a
   
   [i \in {"a", "bc", "d"} |-> IF i = "a" THEN 17
                                          ELSE 42].bc
   
   [a |-> 17, bc |-> 42, d |-> 42]["a"]

   [a |-> 17, bc |-> 42, d |-> 42]["bc"]

   DOMAIN [a |-> 17, bc |-> 42, d |-> 42]

   LET f(a) == [i \in Nat |-> a^i]
       g    == [j \in Nat |-> f(j)]
   IN  g[2][3]

   LET f(a) == [i \in Nat |-> a^i]
       g    == [j \in Nat |-> f(j)]
   IN  g[2][3]

   [i \in Nat, j \in 1..10 |-> i*j][3,4]

2. Define an operator AF such that, if r is a record, then:
   if r has a "count" field, then AF(r) is r with the count
   field incremented by 1, otherwise, AF(r) is obtained from
   r by adding a "count" field with value 0.

3. Define an operator Reverse, so if s is any sequence, then
   Reverse(s) is sequence s in reverse order. (Hint: you
   don't have to use recursion.) Test it with
   TLC. (Don't forget to check that it works on the empty
   sequence, << >> .)

4. Define a function Sum whose domain is Seq(Nat) such
   that Sum(s) is the sum of the elements of s. (Let
   Sum(<< >>) equal 0.)

5. Determine which of the following formulas are tautologies.

   (F => G) /\ (G => F) <=> (F <=> G)
   (~F /\ ~G) <=> (~F) \/ (~G)
   F => (F => G)
   (F => G) <=> (~G => ~F)
   (F => (G => H)) => ((F => G) => H) 
   (F <=> (G <=> H)) => ((F <=> G) <=> H) 
   (\A x : F /\ G) <=> (\A x : F)  /\ (\A x : G) 
   (\E x : F /\ G) <=> (\E x : F)  /\ (\E x : G) 
   (\A x : F \/ G) <=> (\A x : F)  \/ (\A x : G) 
   (\E x : F \/ G) <=> (\E x : F)  \/ (\E x : G) 

2. Which of the following formulas are valid for all sets S, T, and U?

   (S \subseteq T) <=> (S \cup T = T)
   (S \subseteq T) <=> \A x \in S : x \in T
   (S = T) <=> (S \subseteq T) /\ (T \subseteq S)
   (S \subseteq T) <=> (S \ T = {})
   (S \ T) \cup (T \ S) = (S \cup T) \ (S \cap T)
   (S \ (T \cap U)) = (S \ T) \cup (S \ U)

2. Determine which of the following formulas are temporal
   tautologies. For each one that isn't, give a counterexample.

   (a) <>[]<>F <=> []<>F
   (b) []<>[]F <=> []<>F
   (c) ~[](F \/ G) => <>~F /\ <>~G
   (d) []([]F => G) => ([]F => []G)
   (e) [](F => []G) => ([]F => []G)
   (f) [][A /\ B]_v <=> [][A]_v /\ [][B]_v
   (g) []<><<A /\ B>>_v <=> []<><<A>>_v  /\ []<><<B>>_v 
   (h) [][A => B]_v <=> [][<<A>>_v => B]_v 
   (i) WF_v(A) /\ WF_v(B) => WF_v(A \/ B)
   (j) SF_v(A) /\ SF_v(B) => SF_v(A \/ B)
   (k) ENABLED (A /\ B) => (ENABLED A) /\ (ENABLED B)

1. (a) Use TLC to print all Pythagorean triples <<i,j,k>> with
   i^2 + j^2 = k^2 for natural numbers i,j,k \leq N.
   Start with N=20. (Don't be clever and use the formula for
   generating Pythagorean triples; have TLC to it in a straightforward
   fashion.)

   (b) Next, get TLC to print only essentially Pythagorean triples--that
   is, Pythagorean triples <<i, j, k>> such that i \leq j and i,j, and k
   have no common factor. Try it with N = 50, 100, ... . Why does TLC
   take longer to generate each example as N increases?

https://github.com/tlaplus/Examples/blob/master/specifications/SpecifyingSystems/SimpleMath/README
https://github.com/tlaplus/Examples/blob/master/specifications/SpecifyingSystems/AdvancedExamples/README
https://github.com/tlaplus/Examples/blob/master/specifications/SpecifyingSystems/TLC/README
https://github.com/tlaplus/Examples/blob/master/specifications/SpecifyingSystems/HourClock/README
https://github.com/tlaplus/Examples/blob/master/specifications/SpecifyingSystems/Liveness/README
https://github.com/tlaplus/Examples/blob/master/specifications/SpecifyingSystems/FIFO/README
https://github.com/tlaplus/Examples/blob/master/specifications/SpecifyingSystems/CachingMemory/README
https://github.com/tlaplus/Examples/blob/master/specifications/SpecifyingSystems/RealTime/README

Deactivate macOS CI runners?

Currently the macOS CI takes over twice as long to run as the linux and windows CI runs: https://github.com/tlaplus/Examples/actions/runs/7835386801

This got substantially worse after the work to add models to most of the specs, because macOS CI runners see a strange amount of overhead for each model (for example a model taking 1 second to run on the other runners takes 8 seconds to run on the macOS runner). Looking online it seems slow macOS CI runners is a common problem experienced by developers across github.

Ideally the CI would run for ten minutes at most, and I don't think the macOS runner is providing enough value (given the similarity to linux) to justify keeping it around. Perhaps we could add a scheduled CI run to test on macOS once per week.

Question about the specification of reliable broadcast algorithm by Bracha & Toueg (1985)

I'm confused about some of the choices made when the specification for this algorithm was encoded in TLA+. If I'm understanding things correctly, sendEcho() method for example seems to be prioritizing hosts that "start" in the v1 location, as if 1 is always the value proposed by the transmitter. In the original paper, before the algorithm even starts, the transmitter (which is effectively the leader) is supposed to send out initial messages. In your TLA+ spec, these messages don't even exist. Why is this the case, and how do I convince myself that this simplification, or rewrite, is still safe and equivalent to the original algorithm?

My other concern is about the Byzantine processes. My intuition about this bit of your specification is that their behavior is "abstracted away", and that all the progress that the non-faulty hosts in the protocol are making is due to correct messages being sent and received. Although this makes sense to me on a high level, I'm still not seeing why the TLA+ spec is not encoding in some way the ability of faulty processes to send, for example, echo messages with differing values.

Concurrent increments to a shared variable

I've been using the example of concurrently incrementing a shared variable for demonstrating TLA+.

Since this can be split up into t = i, and i = t + 1 actions, it demonstrates many of the interesting facets of TLA+ model checking while being a tiny example:

• Basic TLA+ syntax and TLC usage
• Non-determinism
• Counter-examples
• Liveness and fairness
• State space explosion and symmetry reduction

Classify specifications by TLA+ / PlusCal

As discussed on twitter.

Possible TLC regression on specifications/ewd998/EWD998ChanID.cfg

This is either a regression or actually a bug that was fixed - on nightly, running the specifications/ewd998/EWD998ChanID.cfg model (with -deadlock flag) has TLC return the value success. But on an older version of nightly (downloaded probably a few months ago? I overwrote it sadly, didn't think to set it aside) it returns a liveness failure.

Overhaul Tower of Hanoi specification

• Modeling towers as Naturals in Hanoi.tla is rather low-level/close to an implementation. A high-level spec is likely simpler to grasp if it models towers as sequences...
  • Current Hanoi.tla refinement for high-level spec?!
• Add comments to Bits And operator and explain what it is doing Moved to CommunityModules](https://github.com/tlaplus/CommunityModules/blob/master/modules/Bitwise.tla)
  • Existing comments limited to TLC module overwrite
• State Hanoi problem at the beginning of Hanoi.tla in case the file is passed around without README.md
• TypeOK not a type invariant because it omits that tower is a function
  • Comment states that a tower is a number in 1..2^D, while the formula says it's a number in 0..(2^D-1)

(see personal email "RE: Github examples" dated 07/17/19 from LL)

---

And more explicit variant of how to specify logical and. It is broken when Len(by) # Len(bx)

LOCAL INSTANCE Sequences

LOCAL Max(n, m) == IF n < m THEN m ELSE n

RECURSIVE ToBase2(_, _)
ToBase2(d, b) == IF d > 0 
                     THEN ToBase2(d \div 2, b) \o <<d % 2>>
                     ELSE b

ToBase10(b) == LET d[i \in DOMAIN b] == IF i = 1 
                                          THEN b[Len(b) + 1 - i] * (2^(i-1)) 
                                          ELSE b[Len(b) + 1 - i] * (2^(i-1)) + d[i - 1]
               IN d[Len(b)]
LOCAL And2(x,y) == LET bx == ToBase2(x, <<>>)
                      by == ToBase2(y, <<>>)
                      and == [ i \in DOMAIN bx \cup DOMAIN by |-> 
                                     IF bx[i] = 1 /\ by[i] = 1 THEN 1 ELSE 0 ]
                  IN ToBase10(and)

Specs failing proof validation

I whipped up a quick script then downloaded & ran TLAPS 1.4.5 on macOS against all the modules containing proofs, and the following failed validation (no additional solvers installed, no additional command-line parameters given other than -I for include directory):

specifications/LoopInvariance/BinarySearch.tla
specifications/LoopInvariance/SumSequence.tla
specifications/Paxos/Consensus.tla
specifications/Paxos/Voting.tla
specifications/PaxosHowToWinATuringAward/Consensus.tla
specifications/PaxosHowToWinATuringAward/Voting.tla
specifications/ewd998/AsyncTerminationDetection_proof.tla
specifications/ewd998/EWD998_proof.tla
specifications/lamport_mutex/LamportMutex_proofs.tla

@muenchnerkindl I'd be interested in knowing how many of these are real proof failures and how many are due to wrong options or lack of installed solvers. My script was very simple, it just ran tlapm against each file and printed out the path if it returned a nonzero error code.

ChangRoberts!TypeOK refers to non-existing PlusCal label "n2"

Examples/specifications/chang_roberts/ChangRoberts.tla

Line 119 in 22e6b2d

/\ pc \in [Node -> {"n0", "n1", "n2", "Done"}]

Parameterize version of TLA+ tools used during CI run

@lemmy in an earlier issue you mentioned it would be useful to parameterize the version of the TLA+ tools used during the CI run, so you could for example trigger a build of the tlaplus/tlaplus repo and have the resulting binary be used during a CI run for the tlaplus/examples repo. Are you still interested in this feature? Will look into implementing it if so.

ERROR in specifications/SpecifyingSystems/Composing/CompositeFIFO.tla: In evaluation, the identifier in is either undefined or not an operator.

I tried both toolbox and the VScode TLC and both show the same behavior (shown below). In VScode I'm using the TLC2 Version 2.16 of 31 December 2020 (rev: cdddf55).

 In evaluation, the identifier in is either undefined or not an operator.

line 9, col 16 to line 9, col 17 of module CompositeFIFO

where line 9 is
SenderInit == (in.rdy \in BOOLEAN) /\ (in.val \in Message)

The first few lines of the "Full output" are as follows:

java -cp /home/me/.vscode-server/extensions/alygin.vscode-tlaplus-1.5.4/tools/tla2tools.jar -XX:+UseParallelGC -Dtlc2.TLC.ide=vscode tlc2.TLC CompositeFIFO.tla -tool -modelcheck -coverage 1 -config CompositeFIFO.cfg -dump dot,actionlabels CompositeFIFO.dot

TLC2 Version 2.16 of 31 December 2020 (rev: cdddf55)
Running breadth-first search Model-Checking with fp 122 and seed -6287525116577388646 with 1 worker on 8 cores with 3538MB heap and 64MB offheap memory [pid: 18014] (Linux 5.15.90.1-microsoft-standard-WSL2 amd64, Oracle Corporation 18.0.1.1 x86_64, MSBDiskFPSet, DiskStateQueue).

TLCMC spec

Spec below needs polish to become an example.

------------------------------- MODULE TLCMC -------------------------------
EXTENDS Integers, Sequences, FiniteSets, TLC, TestGraphs

(***************************************************************************)
(* Converts the given Sequence seq into a Set of all the                  *) 
(* Sequence's elements. In other words, the image of the function          *)
(* that seq is.                                                            *)
(***************************************************************************)
SeqToSet(seq) == {seq[i] : i \in 1..Len(seq)} 

(***************************************************************************)
(* Returns a Set of those permutations created out of the elements of Set  *)
(* set which satisfies Filter.                                               *)
(***************************************************************************)
SetToSeqs(set, Filter(_)) == UNION {{perm \in [1..Cardinality(set) -> set]: 
                            \* A filter applied on each permutation
                            \* generated by [S -> T]       
                            Filter(perm)}}

(***************************************************************************)
(* Returns a Set of all possible permutations with distinct elements     *)
(* created out of the elements of Set set. All elements of set occur in    *)
(* in the sequence.                                                        *)
(***************************************************************************)
SetToDistSeqs(set) == SetToSeqs(set, 
                    LAMBDA p: Cardinality(SeqToSet(p)) = Cardinality(set))

(***************************************************************************)
(* A (state) graph G is a directed cyclic graph.                           *)
(*                                                                         *)
(* A graph G is represented by a record with 'states' and 'actions'        *)
(* components, where G.states is the set of states and G.actions[s] is the *)
(* set of transitions of s -- that is, all states t such that there is an  *)
(* action (arc) from s to t.                                               *)
(***************************************************************************)
IsGraph(G) == /\ {"states", "initials", "actions"} = DOMAIN G
              /\ G.actions \in [G.states -> SUBSET G.states]
              /\ G.initials \subseteq G.states

(***************************************************************************)
(* A set of all permutations of the initial states of G.                    *)
(***************************************************************************)
SetOfAllPermutationsOfInitials(G) == SetToDistSeqs(G.initials)

(***************************************************************************)
(* A Set of successor states state.                                        *)
(***************************************************************************)
SuccessorsOf(state, SG) == {successor \in SG.actions[state]:
                            successor \notin {state}}

(***************************************************************************)
(* The predecessor of v in a forest t is the first element of the pair     *)
(* <<predecessor, successor>> nested in a sequence of pairs. In an actual  *)
(* implementation such as TLC, pair[1] is rather an index into t than      *)
(* an id of an actual state.                                               *)
(***************************************************************************)
Predecessor(t, v) == SelectSeq(t, LAMBDA pair: pair[2] = v)[1][1]

CONSTANT StateGraph, ViolationStates, null

ASSUME \* The given StateGraph is actually a graph
       \/ IsGraph(StateGraph)
       \* The violating states are vertices in the state graph.
       \/ ViolationStates \subseteq StateGraph.states

(***************************************************************************
The PlusCal code of the model checker algorithm
--fair algorithm ModelChecker {
	variables
              \* A FIFO containing all unexplored states. A simple
              \* set provides no order, but TLC should explore the
              \* StateGraph in either BFS (or DFS => LIFO).
              \* Note that S is initialized with each
              \* possible permutation of the initial states
              \* here because there is no defined order
              \* of initial states.
              S \in SetOfAllPermutationsOfInitials(StateGraph),
              \* A set of already explored states.      
              C = {},
              \* The state currently being explored in scsr
              state = null,
              \* The set of state's successor states	          
              successors = {},
              \* Counter
              i = 1,
              \* A path from some initial state ending in a
              \* state in violation.
              counterexample = <<>>,
              \* A sequence of pairs such that a pair is a
              \* sequence <<predecessor, successors>>.
              T = <<>>;
	{
       (* Check initial states for violations. We could
          be clever and check the inital states as part
          of the second while loop. However, we then
          either check all states twice or add unchecked
          states to S. *)
       init: while (i \leq Len(S)) {
             \*  Bug in thesis: 
             \*state := Head(S);
             state := S[i]; 
             \* state is now fully explored,
             \* thus exclude it from any
             \* futher exploration if graph
             \* exploration visits it again
             \* due to a cycle. 
             C := C \cup {state};
             i := i + 1;
             if (state \in ViolationStates) {
                     counterexample := <<state>>;
                     \* Terminate model checking
                     goto trc;
             };
       };
       \* Assert that all initial states have been explored.
       initPost: assert C = SeqToSet(S);

       (* Explores all successor states 
          until no new successors are found
          or a violation has been detected. *)
       scsr: while (Len(S) # 0) {
            \* Assign the first element of
            \* S to state. state is
            \* what is currently being checked.
            state := Head(S);
            \* Remove state from S.
            S := Tail(S);
            
            \* For each unexplored successor 'succ' do:
            successors := SuccessorsOf(state, StateGraph) \ C;
            if (SuccessorsOf(state, StateGraph) = {}) {
                \* Iff there exists no successor besides
                \* the self-loop, the system has reached
                \* a deadlock state.
                counterexample := <<state>>;
                goto trc;
            };
            each: while (successors # {}) {
                with (succ \in successors) {
                     \* Exclude succ in this while loop.
                     successors := successors \ {succ};

                     \* Mark successor globally visited.
                     C := C \cup {succ}; S := S \o <<succ>>;
                     
                     \* Append succ to T and add it
                     \* to the list of unexplored states.
                     T  := T \o << <<state,succ>> >>;
                     
                     \* Check state for violation of a
                     \* safety property (simplified 
                     \* to a check of set membership.
                     if (succ \in ViolationStates) {
                       counterexample := <<succ>>;
                       \* Terminate model checking
                       goto trc;
                     };
                };
            };
       };
       (* Model Checking terminated without finding
          a violation. *)
       \* No states left unexplored and no ViolationState given.
       assert S = <<>> /\ ViolationStates = {};
       goto Done;
       
       (* Create a counterexample, that is a path
          from some initial state to a state in
          ViolationStates. In the Java implementation
          of TLC, the path is a path of fingerprints. 
          Thus, a second, guided state exploration
          resolves fingerprints to actual states. *)
       trc : while (TRUE) {
                if (Head(counterexample) \notin StateGraph.initials) {
                   counterexample := <<Predecessor(T, Head(counterexample))>> \o counterexample;
                } else {
                   assert counterexample # <<>>;
                   goto Done;
                };
       };
	}        
}
 ***************************************************************************)
\* BEGIN TRANSLATION
VARIABLES S, C, state, successors, i, counterexample, T, pc

vars == << S, C, state, successors, i, counterexample, T, pc >>

Init == (* Global variables *)
        /\ S \in SetOfAllPermutationsOfInitials(StateGraph)
        /\ C = {}
        /\ state = null
        /\ successors = {}
        /\ i = 1
        /\ counterexample = <<>>
        /\ T = <<>>
        /\ pc = "init"

init == /\ pc = "init"
        /\ IF i \leq Len(S)
              THEN /\ state' = S[i]
                   /\ C' = (C \cup {state'})
                   /\ i' = i + 1
                   /\ IF state' \in ViolationStates
                         THEN /\ counterexample' = <<state'>>
                              /\ pc' = "trc"
                         ELSE /\ pc' = "init"
                              /\ UNCHANGED counterexample
              ELSE /\ pc' = "initPost"
                   /\ UNCHANGED << C, state, i, counterexample >>
        /\ UNCHANGED << S, successors, T >>

initPost == /\ pc = "initPost"
            /\ Assert(C = SeqToSet(S), 
                      "Failure of assertion at line 116, column 18.")
            /\ pc' = "scsr"
            /\ UNCHANGED << S, C, state, successors, i, counterexample, T >>

scsr == /\ pc = "scsr"
        /\ IF Len(S) # 0
              THEN /\ state' = Head(S)
                   /\ S' = Tail(S)
                   /\ successors' = SuccessorsOf(state', StateGraph) \ C
                   /\ IF SuccessorsOf(state', StateGraph) = {}
                         THEN /\ counterexample' = <<state'>>
                              /\ pc' = "trc"
                         ELSE /\ pc' = "each"
                              /\ UNCHANGED counterexample
              ELSE /\ Assert(S = <<>> /\ ViolationStates = {}, 
                             "Failure of assertion at line 164, column 8.")
                   /\ pc' = "Done"
                   /\ UNCHANGED << S, state, successors, counterexample >>
        /\ UNCHANGED << C, i, T >>

each == /\ pc = "each"
        /\ IF successors # {}
              THEN /\ \E succ \in successors:
                        /\ successors' = successors \ {succ}
                        /\ C' = (C \cup {succ})
                        /\ S' = S \o <<succ>>
                        /\ T' = T \o << <<state,succ>> >>
                        /\ IF succ \in ViolationStates
                              THEN /\ counterexample' = <<succ>>
                                   /\ pc' = "trc"
                              ELSE /\ pc' = "each"
                                   /\ UNCHANGED counterexample
              ELSE /\ pc' = "scsr"
                   /\ UNCHANGED << S, C, successors, counterexample, T >>
        /\ UNCHANGED << state, i >>

trc == /\ pc = "trc"
       /\ IF Head(counterexample) \notin StateGraph.initials
             THEN /\ counterexample' = <<Predecessor(T, Head(counterexample))>> \o counterexample
                  /\ pc' = "trc"
             ELSE /\ Assert(counterexample # <<>>, 
                            "Failure of assertion at line 177, column 20.")
                  /\ pc' = "Done"
                  /\ UNCHANGED counterexample
       /\ UNCHANGED << S, C, state, successors, i, T >>

Next == init \/ initPost \/ scsr \/ each \/ trc
           \/ (* Disjunct to prevent deadlock on termination *)
              (pc = "Done" /\ UNCHANGED vars)

Spec == /\ Init /\ [][Next]_vars
        /\ WF_vars(Next)

Termination == <>(pc = "Done")

\* END TRANSLATION

Live == ViolationStates # {} => <>[](/\ Len(counterexample) > 0
                                     /\ counterexample[Len(counterexample)] \in ViolationStates
                                     /\ counterexample[1] \in StateGraph.initials)

=============================================================================

----------------------------- MODULE TestGraphs -----------------------------
EXTENDS Sequences, Integers
(***************************************************************************)
(* The definitions of some graphs, paths, etc.  used for testing the       *)
(* definitions and the algorithm with the TLC model checker.               *)
(***************************************************************************)

\* Graph 1.
G1 == [states |-> 1..4,
       initials |-> {1,2},
       actions  |-> << {1,2}, {1,3}, {4}, {3} >>
       ]
V1 == {4}

\* Graph 1a.
G1a == [states |-> 1..4,
       initials |-> {3},
       actions  |-> << {1, 2}, {1, 3}, {4}, {3} >>]
\* Graph-wise it's impossible to reach state 1 from state 3
V1a == {1}

\* Graph 2. This graph is actually a forest of two graphs
\*    {1,2} /\ {3,4,5}. {1,2} are an SCC.
G2 == [states |-> 1..5,
       initials |-> {1,3},
       actions  |-> << {1, 2}, {1}, {4, 5}, {}, {} >> ]
V2 == {2,5}      

\* Graph 3.       
G3 == [states |-> 1..4,
       initials |-> {2},
       actions  |-> << {1,2}, {2,3}, {3,4}, {1,4} >> ]
V3 == {1}
      
\* Graph 4.
G4 == [states |-> 1..9,
       initials |-> {1,2,3},
       actions  |-> << {3}, {4}, {5}, {6}, {7}, {7}, {8, 9}, {}, {4} >> ]
V4 == {8}
      
\* Graph 5.
G5 == [states |-> 1..9,
       initials |-> {9},
       actions  |-> << {4,2}, {3}, {4}, {5}, {6}, {7}, {8}, {9}, {2} >> ]
V5 == {8}

\* Graph 6.
G6 == [states |-> 1..5,
       initials |-> {5},
       actions  |-> << {2,4,5}, {2}, {1}, {4}, {3} >> ]
V6 == {2}

\* Graph Medium (node 22 is a sink)
G7 == [states |-> 1..50,
       initials |-> {1},
       actions  |-> << {8,35},{15,46,22,23,50},{20,26,34},{5,18,28,37,43},{18,28},{44},{14,29},{42,45},{20,49},{10,12,31,47},
       {1,8,29,30,35,42},{22,31},{10,12,22,27},{23,24,48},{9,22,49},{9,35,50},{10},{21,25,39},{7,29,33,43},{16,41},{},
       {4,36,39,47},{7},{12,22,23},{5,6,39,44},{3,35},{10,13,17},{6,25,33,32,43},{23,30,40,45},{23,50},{24,38},
       {19,33},{6,7,14,38,48},{3,9,20},{3,20,41},{10,38,47},{21,43},{6,10,36,48},{36,38,39},{19,43},{16},
       {29,45},{32},{38,39},{40},{9,15,16,50},{17},{24,31},{13,22,34},{35,23,50} >> ]
V7 == {50}

\* Graph 8.
G8 == [states |-> 1..4,
       initials |-> {1},
       actions |-> <<{1,2},{2,3},{3,4},{4}>>]
V8 == {}

\* Graph 9.
G9 == [states |-> {1},
       initials |-> {1},
       actions |-> <<{1}>>]
V9 == {1}

\* Graph 10.
G10 == [states |-> {},
       initials |-> {},
       actions |-> <<{}>>]
V10 == {}

\* Graph 11.
G11 == [states |-> 1..10,
       initials |-> {},
       actions |-> <<{}>>]
V11 == {}

\* Graph 12.
G12 == [states |-> 1..3,
       initials |-> {1,2,3},
       actions |-> <<{},{},{}>>]
V12 == {1}

\* Graph 13 (simple sequence.
G13 == [states |-> 1..3,
       initials |-> {1},
       actions |-> <<{2},{3},{}>>]
V13 == {}

=============================================================================

Submodules vs. copying specs into the repo

Was briefly discussed earlier in the year but IMO it would be better to just copy the specs into the repo. Reasons:

1. Avoids link rot; on a long enough timescale this is basically guaranteed, especially as awareness grows that centralizing all FOSS development on github is not ideal and people switch to alternative software forge services. Even if we can backup from local copies, why deal with the hassle of having to detect that then rectify it?
2. Specs are small. It is a trivial amount of duplicated data. They are also not often updated after being published, so tracking a remote repo is not likely to bring much benefit.
3. Copying the files into this repo ensures they can be made amenable to validation by the CI workflow.

Thoughts? I will say that adding the specs as submodules is preferable to them only existing as a hyperlink though. One of the submodules added exposed a bug in tree-sitter-tlaplus pluscal parsing!

Install TLA+ unicode converter into gitpod and codespaces

https://github.com/tlaplus-community/tlauc should be installed as part of https://github.com/tlaplus/Examples/blob/master/.devcontainer/install.sh.

/cc @ahelwer

GitPod & Codespaces - make sure bitrot hasn't set in

As possibly encountered in #104, some bitrot could have set in for the gitpod and codespaces. This issue exists as a reminder to check that these still work.

Index examples in manifest.json

Here's an example entry in the manifest.json:

{
  "specifications": [
    {
      "title": "Multi-Car Elevator System",
      "description": "A simple multi-car elevator system servicing a multi-floor building",
      "source": "https://groups.google.com/g/tlaplus/c/5Xd8kv288jE/m/IrliJIatBwAJ",
      "authors": ["Andrew Helwer"],
      "modules": [
        {
          "path": "specifications/MultiCarElevator/Elevator.tla",
          "communityDependencies": [],
          "tlaLanguageVersion": 2,
          "features": [],
          "models": [
            {
              "path": "specifications/MultiCarElevator/ElevatorLivenessSmall.cfg",
              "runtime": "00:00:10",
              "features": ["liveness"],
              "result": "success"
            },

So you have a specification (directory), with one or more modules (.tla files), where each module can have 0 or more models (.cfg files). Similar to the toolbox! I envision a number of interesting pieces of metadata associated with each of these entities that can be searched or filtered by a program consuming this repo:

• Spec title/description/source/authors: pretty self-explanatory
• Module communityDependencies: also self-explanatory
• module features: pluscal/proof/unicode
• model runtime: approximate runtime, we could encourage users to add at least one model that runs for less than ten seconds, for example - consumers of this repo could test-execute every model with a sub-10-second runtime
• model features: liveness/symmetry/state restriction
• result: success/liveness failure/safety failure/deadlock

I will write a CI script that runs to validate the following when a PR is open:

• The manifest.json file conforms to a json schema
• Every path in the manifest.json corresponds to a file in the repo
• Every .tla or .cfg file in the repo corresponds to an entry in the manifest
• Use tree-sitter queries to ensure the pluscal/proof feature tags are correct
• Use file search for .cfgs to ensure model feature tags are correct

I agree it would not be useful to have this information duplicated in a manifest and a README, which could get out of sync. I will look into whether it's possible to pull this info into an HTML file and have it displayed or something of that sort. It does look like this work would resolve that issue you linked.

Originally posted by @ahelwer in #55 (comment)

EWD998 spec fails parsing due to name collision between TLAPS and Community Modules

From here: #61 (comment)

ewd998, which runs into a naming collision between the TLAPS and community modules. Specifically Functions.tla; it tries to use operators in the Community version of Functions.tla, while also importing various modules from the TLAPS standard library (which itself includes a Functions.tla that doesn't have those operators).

I confirm that the name clash between the TLAPS standard theorem library and some of the Community Modules (in particular Functions) is known and should be fixed in the long overdue release of TLAPS.

Enforce correspondence between manifest.json and README.md table in CI

This isn't work I'm planning to do anytime soon but it would be a nice little project if someone else wants to take it on. Markdown is a very difficult language to work with, tooling-wise, but there are nice full-featured parsers like goldmark (used by the Hugo static site generator, for example) which make it tractable. A CI script could parse the README.md file with goldmark, find the table & its entries, and check its correspondence to the manifest.json file. This would include not only the existence of specs in the table but also whether they are properly labeled as including proofs, pluscal, TLC models, and whatever other traits we care to define. This could also implement whatever clustering & categorization is desired in #15. This could all possibly be implemented as a goldmark extension. Alternatively, there are a number of python markdown parsers of varying quality levels that could be used.

Bakery-Boulangerie specs don't satisfy `DeadlockFree` or `StarvationFree` liveness properties

I've been defining models as part of work on #107. Currently these properties fail so these specs can only be subject to safety checking. Some fairness assumptions are required for the properties to be satisfied. @muenchnerkindl any idea what those fairness assumptions would be? The one in Spec is insufficient.

Remove deadlock flag in manifest.json in favor of `CHECK_DEADLOCK` in config file

Recently learned about CHECK_DEADLOCK being an option in model files. Currently whether to check deadlock for each model is defined in the manifest.json, for example:

{
  "path": "specifications/Huang/Huang.cfg",
  "runtime": "00:00:40",
  "size": "medium",
  "mode": "exhaustive search",
  "config": [
    "ignore deadlock"
  ],
  "features": [
    "alias",
    "liveness",
    "state constraint"
  ],
  "result": "success"
}

which the Python script reads then passes on to the TLC command line flags. I think it would be better to remove this config item in favor of CHECK_DEADLOCK in the model file.

Add optional fields to manifest.json recording total and unique states for each model

The check_small_models.py script will then validate that TLC execution produces the expected values. This will significantly improve the value of these models as TLC regression tests, since this number should not ever change unless the spec or model changes.

Do not suppress TLC output

@ahelwer Diagnosing CI failures becomes much easier when you have TLC's output included. I'm wondering, is there a particular reason why TLC's stdout/stderr is currently being suppressed?

https://github.com/tlaplus/Examples/blob/7d129a9c90bf6d4d9c3f7f3fe2db5f30f3bb6913/.github/scripts/tla_utils.py#L102C13-L102C27

More termination detection algorithms

• https://en.wikipedia.org/wiki/Huang's_algorithm (related tlaplus/CommunityModules#4)
• https://dl.acm.org/doi/10.5555/647172.716117

Case study to share: Specifying and Verifying SDP Protocol based Zero Trust Architecture

My case to share is about the TLA+ Spec of Software Defined Perimeter (SDP) architecture and algorithm based on the open source project fwknop.

https://github.com/10227694/SDP_Verification

The subdirectory SDP_Attack_Spec contains the specification based on the following materials:
(* https://cloudsecurityalliance.org/artifacts/software-defined-perimeter-zero-trust-specification-v2/ )
( http://www.cipherdyne.org/fwknop/ *)

The subdirectory SDP_Attack_New_Solution_Spec contains the specification for the improved SDP architecture and algorithm which fixed the discovered vulnerability.

The slide "Specifying and Verifying SDP Protocol Based Zero Trust Architecture Using TLA+.pptx" contains the key description of the reserach work.

For detail descriptions, please refer to:

https://dl.acm.org/doi/10.1145/3558819.3558826

How do I create .cfg files?

I noticed that some examples have .cfg files. Does anyone knows how to create them?
I did find a .cfg file somewhere in the in the Model_* directories but those config files seem to have added numbers to variable names.

Can I generate a clean .cfg file somehow?

Example:
https://github.com/tlaplus/Examples/tree/master/specifications/Prisoners
https://github.com/tlaplus/Examples/blob/master/specifications/Prisoners/Prisoners.cfg

Add TLC models for all specs for which it's viable

The README table validation work reveals that a bit more than half the specs in this repo have a TLC model associated with them. Adding TLC models to the remainder (if viable) would be an easy way to have improved confidence that the specs in this repo are actually correct (in the sense of capable of being validated, not exhibiting simple type errors, etc.) and would expand the functional test suite for the TLA+ tools.

Add Raft spec with Apalache type annotations

@konnov Do you have a variant of raft.tla that has been annotated with types for Apalache?

We did it at least once. There was one issue with Raft, where they used a function as a sequence:

https://github.com/ongardie/raft.tla/blob/974fff7236545912c035ff8041582864449d0ffe/raft.tla#L378-L379

There is a simple fix for that: just use SubSeq instead of this explicit construction. I cannot find an annotated version of raft on my laptop though. We could probably add one in tlaplus-examples.

Originally posted by @konnov in tlaplus/tlaplus#677 (comment)

Add support for Github Codespaces

4686a0b adds rudimentary support for Github Codespaces.

TODOs:

• Include the latest version of TLA+ vscode extension (https://github.com/lemmy/vscode-tlaplus/releases which comes with the debugger?)
• Integrate Apalache (informalsystems/apalache#716)

## Waiting for a stable URL.
apt-get install libz3-java libz3-jni libz3-dev libz3-4
mkdir apalache && cd apalache
wget https://github.com/informalsystems/apalache/releases/latest/download/apalache-v0.15.1.tgz
tar xvfz apalache-v0.15.1.tgz

• Consider including the latest version of CommunityModules (e.g. EWD998 Utils.tla would conflict)

https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar

Liveness and Safety properties fail in SpanTreeRandom.tla

In specifications/SpanningTree/SpanTreeRandom.tla, the model uses RandomElement to generate a list of edges between nodes. This causes the properties Liveness and Safety to occasionally fail. Whether this is because of a flaw in the algorithm or by design is uncertain. Here is a model reproducing the failure:

CONSTANTS
  Nodes = {n1, n2, n3, n4, n5, n6}
  MaxCardinality = 6
  Root = n1
INVARIANT TypeOK
PROPERTIES Liveness Safety
SPECIFICATION Spec
CHECK_DEADLOCK FALSE

Here is a failure trace:

tlc SpanTreeRandom
TLC2 Version 2.18 of Day Month 20?? (rev: a77ff3b)
Running breadth-first search Model-Checking with fp 116 and seed 2350910532224203137 with 8 workers on 8 cores with 3541MB heap and 64MB offheap memory [p
id: 187405] (Linux 6.6.10-arch1-1 amd64, N/A 21 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /home/ahelwer/src/tlaplus/examples/specifications/SpanningTree/SpanTreeRandom.tla
Parsing file /tmp/tlc-9076410093698049487/Integers.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /tmp/tlc-9076410093698049487/FiniteSets.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/tlc-9076410093698049487/TLC.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/tlc-9076410093698049487/Naturals.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-9076410093698049487/Sequences.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module SpanTreeRandom
Starting... (2024-01-26 08:12:58)
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2024-01-26 08:12:58.
Error: Invariant Safety is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ mom = (n1 :> n1 @@ n2 :> n2 @@ n3 :> n3 @@ n4 :> n4 @@ n5 :> n5 @@ n6 :> n6)
/\ dist = (n1 :> 0 @@ n2 :> 6 @@ n3 :> 6 @@ n4 :> 6 @@ n5 :> 6 @@ n6 :> 6)

State 2: <Next line 61, col 14 to line 64, col 53 of module SpanTreeRandom>
/\ mom = (n1 :> n1 @@ n2 :> n1 @@ n3 :> n3 @@ n4 :> n4 @@ n5 :> n5 @@ n6 :> n6)
/\ dist = (n1 :> 0 @@ n2 :> 1 @@ n3 :> 6 @@ n4 :> 6 @@ n5 :> 6 @@ n6 :> 6)

State 3: <Next line 61, col 14 to line 64, col 53 of module SpanTreeRandom>
/\ mom = (n1 :> n1 @@ n2 :> n1 @@ n3 :> n3 @@ n4 :> n2 @@ n5 :> n5 @@ n6 :> n6)
/\ dist = (n1 :> 0 @@ n2 :> 1 @@ n3 :> 6 @@ n4 :> 2 @@ n5 :> 6 @@ n6 :> 6)

State 4: <Next line 61, col 14 to line 64, col 53 of module SpanTreeRandom>
/\ mom = (n1 :> n1 @@ n2 :> n1 @@ n3 :> n3 @@ n4 :> n2 @@ n5 :> n1 @@ n6 :> n6)
/\ dist = (n1 :> 0 @@ n2 :> 1 @@ n3 :> 6 @@ n4 :> 2 @@ n5 :> 1 @@ n6 :> 6)

State 5: <Next line 61, col 14 to line 64, col 53 of module SpanTreeRandom>
/\ mom = (n1 :> n1 @@ n2 :> n1 @@ n3 :> n5 @@ n4 :> n2 @@ n5 :> n1 @@ n6 :> n6)
/\ dist = (n1 :> 0 @@ n2 :> 1 @@ n3 :> 2 @@ n4 :> 2 @@ n5 :> 1 @@ n6 :> 6)

State 6: <Next line 61, col 14 to line 64, col 53 of module SpanTreeRandom>
/\ mom = (n1 :> n1 @@ n2 :> n1 @@ n3 :> n5 @@ n4 :> n2 @@ n5 :> n1 @@ n6 :> n2)
/\ dist = (n1 :> 0 @@ n2 :> 1 @@ n3 :> 2 @@ n4 :> 2 @@ n5 :> 1 @@ n6 :> 2)

21742 states generated, 4063 distinct states found, 2041 states left on queue.
The depth of the complete state graph search is 6.
Finished in 01s at (2024-01-26 08:12:59)

This came out of the work in #110.

CI workflow fails on ubuntu

After merging a bug fix for one of the examples (aba-asyn-byz), the CI run succeeded for Windows and Mac OS but failed for Ubuntu due to an error in generating the Isabelle object logic heap. Why is this happening? Also, the updated example doesn't contain any proofs so the problem is clearly unrelated to the fix.

@ahelwer, could you please have a look?

Running the N-Queens example on Linux fails because filename is Pluscal not PlusCal

I fixed this myself by renaming some files, I don't yet have the woo to make a pull request. I have absolutely no idea what I am doing BTW, I was just trying out an example to test I had installed the TLA Toolbox correctly.

Can't come up with working model for cbc_max or spanning

I'm adding basic TLC models to a bunch of specs for #107 and ran into trouble with this spec, could you help? Tagging authors @konnov @josef-widder @banhday

I'm attempting to use this model:

CONSTANTS
  N = 4
  T = 1
  F = 1
  Values = {1, 2}
  Bottom = 0
INVARIANTS TypeOK Validity Agreement
PROPERTIES Termination RealTermination
SPECIFICATION Spec
CHECK_DEADLOCK FALSE

but I get this runtime error (subtract 2 from line numbers to get the current spec, I added a couple assumptions about the constant values in my branch):

TLC2 Version 2.18 of Day Month 20?? (rev: a77ff3b)
Running breadth-first search Model-Checking with fp 16 and seed -7656258344444481100 with 8 workers on 8 cores with 3541MB heap and 64MB offheap memory [p
id: 136262] (Linux 6.6.10-arch1-1 amd64, N/A 21 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /home/ahelwer/src/tlaplus/examples/specifications/cbc_max/cbc_max.tla
Parsing file /tmp/tlc-11021836222741093434/Integers.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /tmp/tlc-11021836222741093434/FiniteSets.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla
)
Parsing file /tmp/tlc-11021836222741093434/TLC.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/tlc-11021836222741093434/Naturals.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-11021836222741093434/Sequences.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module cbc_max
Starting... (2024-01-23 15:05:58)
Implied-temporal checking--satisfiability problem has 2 branches.
Computing initial states...
Computed 2 initial states...
Computed 4 initial states...
Computed 8 initial states...
Computed 16 initial states...
Computed 32 initial states...
Computed 64 initial states...
Finished computing initial states: 81 distinct states generated at 2024-01-23 15:05:58.
Progress(5) at 2024-01-23 15:06:01: 52,442 states generated (52,442 s/min), 27,509 distinct states found (27,509 ds/min), 21,333 states left on queue.
Progress(7) at 2024-01-23 15:07:01: 2,164,207 states generated (2,111,765 s/min), 807,360 distinct states found (779,851 ds/min), 578,295 states left on q
ueue.
Progress(8) at 2024-01-23 15:08:01: 4,337,333 states generated (2,173,126 s/min), 1,525,842 distinct states found (718,482 ds/min), 1,074,077 states left 
on queue.
Progress(8) at 2024-01-23 15:09:01: 6,493,247 states generated (2,155,914 s/min), 2,219,299 distinct states found (693,457 ds/min), 1,548,647 states left 
on queue.
Progress(8) at 2024-01-23 15:10:01: 8,615,301 states generated (2,122,054 s/min), 2,904,446 distinct states found (685,147 ds/min), 2,017,726 states left 
on queue.
Error: TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.RuntimeException
: Attempted to compute the value of an expression of form
CHOOSE x \in S: P, but no element of S satisfied P.
line 44, col 13 to line 45, col 75 of module cbc_max
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ sntMsgs = {}
/\ dval = <<0, 0, 0, 0>>
/\ V = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ v = <<1, 1, 3, 2>>
/\ w = <<0, 0, 0, 0>>
/\ pc = <<"BCAST1", "BCAST1", "BCAST1", "BCAST1">>
/\ nCrash = 0
/\ rcvdMsgs = <<{}, {}, {}, {}>>

State 2: <BcastPhs1(1) line 84, col 3 to line 87, col 52 of module cbc_max>
/\ sntMsgs = {[type |-> "Phs1", value |-> 1, sndr |-> 1]}
/\ dval = <<0, 0, 0, 0>>
/\ V = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ v = <<1, 1, 3, 2>>
/\ w = <<0, 0, 0, 0>>
/\ pc = <<"PHS1", "BCAST1", "BCAST1", "BCAST1">>
/\ nCrash = 0
/\ rcvdMsgs = <<{}, {}, {}, {}>>

State 3: <Receive(2) line 69, col 5 to line 80, col 54 of module cbc_max>
/\ sntMsgs = {[type |-> "Phs1", value |-> 1, sndr |-> 1]}
/\ dval = <<0, 0, 0, 0>>
/\ V = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ v = <<1, 1, 3, 2>>
/\ w = <<0, 0, 0, 0>>
/\ pc = <<"PHS1", "BCAST1", "BCAST1", "BCAST1">>
/\ nCrash = 0
/\ rcvdMsgs = <<{}, {[type |-> "Phs1", value |-> 1, sndr |-> 1]}, {}, {}>>

State 4: <BcastPhs1(3) line 84, col 3 to line 87, col 52 of module cbc_max>
/\ sntMsgs = { [type |-> "Phs1", value |-> 1, sndr |-> 1],
  [type |-> "Phs1", value |-> 3, sndr |-> 3] }
/\ dval = <<0, 0, 0, 0>>
/\ V = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ v = <<1, 1, 3, 2>>
/\ w = <<0, 0, 0, 0>>
/\ pc = <<"PHS1", "BCAST1", "PHS1", "BCAST1">>
/\ nCrash = 0
/\ rcvdMsgs = <<{}, {[type |-> "Phs1", value |-> 1, sndr |-> 1]}, {}, {}>>

State 5: <Receive(2) line 69, col 5 to line 80, col 54 of module cbc_max>
/\ sntMsgs = { [type |-> "Phs1", value |-> 1, sndr |-> 1],
  [type |-> "Phs1", value |-> 3, sndr |-> 3] }
/\ dval = <<0, 0, 0, 0>>
/\ V = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ v = <<1, 1, 3, 2>>
/\ w = <<0, 0, 0, 0>>
/\ pc = <<"PHS1", "BCAST1", "PHS1", "BCAST1">>
/\ nCrash = 0
/\ rcvdMsgs = << {},
   { [type |-> "Phs1", value |-> 1, sndr |-> 1],
     [type |-> "Phs1", value |-> 3, sndr |-> 3] },
   {},
   {} >>

State 6: <BcastPhs1(4) line 84, col 3 to line 87, col 52 of module cbc_max>
/\ sntMsgs = { [type |-> "Phs1", value |-> 1, sndr |-> 1],
  [type |-> "Phs1", value |-> 2, sndr |-> 4],
  [type |-> "Phs1", value |-> 3, sndr |-> 3] }
/\ dval = <<0, 0, 0, 0>>
/\ V = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ v = <<1, 1, 3, 2>>
/\ w = <<0, 0, 0, 0>>
/\ pc = <<"PHS1", "BCAST1", "PHS1", "PHS1">>
/\ nCrash = 0
/\ rcvdMsgs = << {},
   { [type |-> "Phs1", value |-> 1, sndr |-> 1],
     [type |-> "Phs1", value |-> 3, sndr |-> 3] },
   {},
   {} >>

State 7: <Receive(2) line 69, col 5 to line 80, col 54 of module cbc_max>
/\ sntMsgs = { [type |-> "Phs1", value |-> 1, sndr |-> 1],
  [type |-> "Phs1", value |-> 2, sndr |-> 4],
  [type |-> "Phs1", value |-> 3, sndr |-> 3] }
/\ dval = <<0, 0, 0, 0>>
/\ V = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ v = <<1, 1, 3, 2>>
/\ w = <<0, 0, 0, 0>>
/\ pc = <<"PHS1", "BCAST1", "PHS1", "PHS1">>
/\ nCrash = 0
/\ rcvdMsgs = << {},
   { [type |-> "Phs1", value |-> 1, sndr |-> 1],
     [type |-> "Phs1", value |-> 2, sndr |-> 4],
     [type |-> "Phs1", value |-> 3, sndr |-> 3] },
   {},
   {} >>

State 8: <BcastPhs1(2) line 84, col 3 to line 87, col 52 of module cbc_max>
/\ sntMsgs = { [type |-> "Phs1", value |-> 1, sndr |-> 1],
  [type |-> "Phs1", value |-> 1, sndr |-> 2],
  [type |-> "Phs1", value |-> 2, sndr |-> 4],
  [type |-> "Phs1", value |-> 3, sndr |-> 3] }
/\ dval = <<0, 0, 0, 0>>
/\ V = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ v = <<1, 1, 3, 2>>
/\ w = <<0, 0, 0, 0>>
/\ pc = <<"PHS1", "PHS1", "PHS1", "PHS1">>
/\ nCrash = 0
/\ rcvdMsgs = << {},
   { [type |-> "Phs1", value |-> 1, sndr |-> 1],
     [type |-> "Phs1", value |-> 2, sndr |-> 4],
     [type |-> "Phs1", value |-> 3, sndr |-> 3] },
   {},
   {} >>

Error: The error occurred when TLC was evaluating the nested
expressions at the following positions:
0. Line 93, column 3 to line 97, column 58 in cbc_max
1. Line 93, column 6 to line 93, column 19 in cbc_max
2. Line 94, column 6 to line 94, column 40 in cbc_max
3. Line 95, column 6 to line 95, column 65 in cbc_max
4. Line 96, column 6 to line 96, column 39 in cbc_max
5. Line 96, column 11 to line 96, column 39 in cbc_max
6. Line 96, column 29 to line 96, column 37 in cbc_max
7. Line 44, column 13 to line 45, column 75 in cbc_max


9696693 states generated, 3251762 distinct states found, 2254468 states left on queue.
The depth of the complete state graph search is 9.
Finished in 04min 34s at (2024-01-23 15:10:33)

EWD998 model checking failure when running TLC from outside tlaplus/examples repo

Steps to reproduce:

1. Open shell and navigate to directory above tlaplus/examples repo
2. Run ./examples/.github/scripts/linux-setup.sh examples/.github/scripts examples/deps true to install dependencies on Linux & macOS
3. Run the following command to execute TLC:

java -Dtlc2.TLC.ide=Github -Dutil.ExecutionStatisticsCollector.id=abcdef60f238424fa70d124d0c77ffff -XX:+UseParallelGC -cp examples/deps/tools/tla2tools.jar:examples/deps/community/modules.jar:examples/deps/tlapm/library tlc2.TLC examples/specifications/ewd998/EWD998ChanTrace.tla -config examples/specifications/ewd998/EWD998ChanTrace.cfg -workers auto -lncheck final -cleanup

Observe the following error:

TLC2 Version 2.18 of Day Month 20?? (rev: 23f7650)
Running breadth-first search Model-Checking with fp 125 and seed 7822221676660054780 with 8 workers on 8 cores with 3541MB heap and 64MB offheap memory [pid: 34002] (Linux 6.8.2-arch2-1 amd64, N/A 22 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /home/ahelwer/src/tlaplus/examples/specifications/ewd998/EWD998ChanTrace.tla
Parsing file /home/ahelwer/src/tlaplus/examples/specifications/ewd998/EWD998Chan.tla
Parsing file /tmp/tlc-16960620422673853593/Json.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/Json.tla)
Parsing file /tmp/tlc-16960620422673853593/TLC.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/tlc-16960620422673853593/IOUtils.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/community/modules.jar!/IOUtils.tla)
Parsing file /tmp/tlc-16960620422673853593/VectorClocks.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/community/modules.jar!/VectorClocks.tla)
Parsing file /tmp/tlc-16960620422673853593/_TLCTrace.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/_TLCTrace.tla)
Parsing file /tmp/tlc-16960620422673853593/Integers.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /tmp/tlc-16960620422673853593/Sequences.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-16960620422673853593/FiniteSets.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /home/ahelwer/src/tlaplus/examples/specifications/ewd998/Utils.tla
Parsing file /tmp/tlc-16960620422673853593/Naturals.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-16960620422673853593/Functions.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/community/modules.jar!/Functions.tla)
Parsing file /tmp/tlc-16960620422673853593/SequencesExt.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/community/modules.jar!/SequencesExt.tla)
Parsing file /home/ahelwer/src/tlaplus/examples/specifications/ewd998/EWD998.tla
Parsing file /tmp/tlc-16960620422673853593/Randomization.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/Randomization.tla)
Parsing file /tmp/tlc-16960620422673853593/Folds.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/community/modules.jar!/Folds.tla)
Parsing file /tmp/tlc-16960620422673853593/FiniteSetsExt.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/community/modules.jar!/FiniteSetsExt.tla)
Parsing file /home/ahelwer/src/tlaplus/examples/specifications/ewd998/AsyncTerminationDetection.tla
Parsing file /tmp/tlc-16960620422673853593/TLCExt.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/TLCExt.tla)
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module Folds
Semantic processing of module Functions
Semantic processing of module FiniteSetsExt
Semantic processing of module SequencesExt
Semantic processing of module Utils
Semantic processing of module Randomization
Semantic processing of module AsyncTerminationDetection
Semantic processing of module EWD998
Semantic processing of module EWD998Chan
Semantic processing of module Json
Semantic processing of module IOUtils
Semantic processing of module VectorClocks
Semantic processing of module TLCExt
Semantic processing of module _TLCTrace
Semantic processing of module EWD998ChanTrace
Starting... (2024-04-07 09:56:50)
Error: The configuration file substitutes constant N with non-constant TraceN - specifically: Attempted to apply the operator overridden by the Java method
public static tlc2.value.IValue tlc2.overrides.Json.ndDeserialize(tlc2.value.impl.StringValue) throws java.io.IOException,
but it produced the following error:
specifications/ewd998/EWD998ChanTrace.ndjson (No such file or directory)
Finished in 00s at (2024-04-07 09:56:50)

Found during execution of CI in tlaplus/tlaplus repo. It seems like a path is hardcoded somewhere assuming cwd is repo root.

`ctl[p]` is never equal `"req"` in specifications/SpecifyingSystems/Liveness properties

There are typos in the liveness properties in the folder to the chapter "Liveness" of "Specifying Systems". The ctl[p] function value in the properties should equal "req". However, this is never the case as the function range is only {"rdy", "busy", "done"}.
This occurs at least in the following lines:

Examples/specifications/SpecifyingSystems/Liveness/README

Line 39 in c7e0ca3

\A p \in Proc : (ctl[p] = "rdy") ~> (ctl[p] = "req")

Examples/specifications/SpecifyingSystems/Liveness/LiveInternalMemory.tla

Line 30 in c7e0ca3

(* issued a request, so ctl[p] = "req", then a response eventually occurs, *)

Examples/specifications/SpecifyingSystems/Liveness/LiveInternalMemory.tla

Line 35 in c7e0ca3

\A p \in Proc : (ctl[p] = "req") ~> (ctl[p] = "rdy")

IMHO "req" was meant to be "busy".

Add proof checking time to manifest details

Currently we manually exclude specific modules from proof checking in the CI because they run too long. Given that proof checking time can have as high of variability as model checking, it makes sense to include data about proof check time in the manifest then use that to determine whether to check the proof in the CI. Possibly we could have a CI workflow scheduled to run weekly which checks these long-running proofs along with the macOS workflow.

Failing proofs can continue to be manually excluded because ideally this repo would not have or accept any specs with failing proofs.

Towards beginner friendly examples

The current README does not order examples that make it easy to pick beginner-friendly examples.

TLA+ concepts by which to cluster (tag?) specs:

• Constant-level expressions
  • Set of all functions [ S -> T ]
  • recursive function definitions such as sum of all elements in a range of a function
  • recursive operators
  • Second order
  • Standard modules
• "+" in TLA+
  • sets (filter/mapping), functions, records, sequences, ..., TLC!@@, TLC!:>
• CHOOSE vs. \E (existential quantification)
• non-determinism|concurrency|distributed systems
• Safety|Liveness (Fairness)
• Refinement
• PlusCal
• Auxiliary variables (history|prophecy)
• Composition of specs
• Inductive invariants (TLAPS)

Categories

Math:
https://github.com/tlaplus/Examples/tree/master/specifications/SpecifyingSystems/SimpleMath
https://github.com/tlaplus/Examples/tree/master/specifications/SpecifyingSystems/MoreMath
https://github.com/tlaplus/Examples/tree/master/specifications/TransitiveClosure
https://github.com/tlaplus/CommunityModules/blob/master/modules/Graphs.tla
#23

Logic Puzzles:
https://github.com/tlaplus/Examples/blob/master/specifications/Stones/
https://github.com/tlaplus/Examples/tree/master/specifications/DieHard (there are also PlusCal versions somewhere)
https://github.com/tlaplus/Examples/tree/master/specifications/CarTalkPuzzle
https://github.com/tlaplus/Examples/tree/master/specifications/MissionariesAndCannibals
https://github.com/tlaplus/Examples/tree/master/specifications/N-Queens
https://github.com/tlaplus/Examples/tree/master/specifications/Prisoners

Beginner specs based on popular problems in CS:
https://github.com/tlaplus/Examples/tree/master/specifications/tower_of_hanoi
https://github.com/tlaplus/Examples/tree/master/specifications/GameOfLife
https://github.com/tlaplus/Examples/tree/master/specifications/CigaretteSmokers
https://github.com/tlaplus/Examples/tree/master/specifications/SlidingPuzzles

Non-common concepts in TLA+:
https://github.com/tlaplus/Examples/tree/master/specifications/SpecifyingSystems/Syntax (BNF grammar)

Specs of basic concurrent/distributed systems:
https://github.com/tlaplus/Examples/tree/master/specifications/Chameneos
https://github.com/tlaplus/Examples/tree/master/specifications/echo (PlusCal)
https://github.com/tlaplus/Examples/tree/master/specifications/Tla-tortoise-hare (PlusCal)
https://github.com/lemmy/BlockingQueue/ (tutorial)
https://github.com/tlaplus/Examples/tree/master/specifications/dijkstra-mutex
https://github.com/tlaplus/Examples/tree/master/specifications/ewd840
https://github.com/tlaplus/Examples/tree/master/specifications/ewd998

TLAPS:
https://github.com/tlaplus/Examples/tree/master/specifications/sums_even
https://github.com/tlaplus/Examples/tree/master/specifications/LoopInvariance
https://github.com/tlaplus/Examples/tree/master/specifications/TeachingConcurrency

Technical

• git submodules instead of html links where possible
• Standalone examples that rely e.g. on git commits to structuring their content?
• Zero install/browser-based, i.e. open in gitpod or codespaces (would benefit from submodules)
  • What about submodules that bring their own gitpod/codespace config (e.g. BlockingQueue)?
• #8

Models failing smoke testing

# Attempted to access index 0 of tuple <<>>
'specifications/SpecifyingSystems/AdvancedExamples/MCInnerSerial.cfg',
# Attempted to select nonexistent field "traces" from record
'specifications/ewd426/SimTokenRing.cfg',
# Initial error cannot find TLAPS; if fixed, cannot find property "Stable"
'specifications/ewd998/AsyncTerminationDetection_proof.cfg',
# Property is violated by the initial state
'specifications/ewd998/SmokeEWD998.cfg'

Add some Apalache models

Currently no specs included in the repository have an Apalache model. It would be nice to have some examples of this. The Einstein's Riddle spec would be an ideal first candidate, as TLC has a tough time with it. Apalache could then be added to the CI checks.

Minor correction of a comment

Hi, I believe the comment in the spec Bakery.tla that says "MutualExclusion asserts that two distinct processes are in their critical sections." is problematic, because no two distinct processes are allowed to be in the critical sections at the same time.