### Search Repository Specifications by Feature Source: https://context7.com/tlaplus/examples/llms.txt Use grep commands to discover specifications with specific features across manifest.json files. Enables finding PlusCal implementations, proofs, safety violations, symbolic checking compatibility, and beginner-friendly examples. ```bash # Find all PlusCal specifications ls specifications/*/manifest.json | xargs grep -l "pluscal" # Find specifications with proofs ls specifications/*/manifest.json | xargs grep -l "proof" # Find specifications that fail with safety violations ls specifications/*/manifest.json | xargs grep -l "safety failure" # Find specifications checked with Apalache ls specifications/*/manifest.json | xargs grep -l "symbolic" # Find beginner-friendly specifications ls specifications/*/manifest.json | xargs grep -l "beginner" ``` -------------------------------- ### TLA+ Die Hard Problem Specification Source: https://context7.com/tlaplus/examples/llms.txt Demonstrates measuring exactly 4 gallons using a 5-gallon jug and 3-gallon jug. Shows basic TLA+ specification structure including variable declarations, state transitions, invariants, and temporal formulas. This is a beginner-friendly example illustrating state machine modeling in TLA+. ```tla ------------------------------ MODULE DieHard ------------------------------- EXTENDS Naturals VARIABLES big, \* The number of gallons of water in the 5 gallon jug. small \* The number of gallons of water in the 3 gallon jug. TypeOK == /\ small \in 0..3 /\ big \in 0..5 Init == /\ big = 0 /\ small = 0 FillSmallJug == /\ small' = 3 /\ big' = big FillBigJug == /\ big' = 5 /\ small' = small EmptySmallJug == /\ small' = 0 /\ big' = big EmptyBigJug == /\ big' = 0 /\ small' = small Min(m,n) == IF m < n THEN m ELSE n SmallToBig == /\ big' = Min(big + small, 5) /\ small' = small - (big' - big) BigToSmall == /\ small' = Min(big + small, 3) /\ big' = big - (small' - small) Next == \/ FillSmallJug \/ FillBigJug \/ EmptySmallJug \/ EmptyBigJug \/ SmallToBig \/ BigToSmall Spec == Init /\ [][Next]_<> NotSolved == big # 4 ============================================================================= ``` -------------------------------- ### Run TLC Model Checker Commands Source: https://context7.com/tlaplus/examples/llms.txt Execute TLC model checker for exhaustive verification, simulation, and deadlock detection. Includes commands for verifying TLA+ specifications with configuration files and interpreting output traces. Useful for finding invariant violations and counter-examples. ```bash # Exhaustive model checking java -jar tla2tools.jar -workers auto DieHard.tla -config DieHard.cfg # Simulation mode (generate random traces) java -jar tla2tools.jar -simulate num=1000 DieHard.tla -config DieHard.cfg # Generate counter-example trace java -jar tla2tools.jar -deadlock DieHard.tla -config DieHard.cfg # Expected output for Die Hard: # Error: Invariant NotSolved is violated. # The behavior up to this point is: # State 1: big = 0, small = 0 # State 2: big = 5, small = 0 # State 3: big = 2, small = 3 # State 4: big = 2, small = 0 # State 5: big = 0, small = 2 # State 6: big = 5, small = 2 # State 7: big = 4, small = 3 ``` -------------------------------- ### Search TLC Model Configuration Features Source: https://context7.com/tlaplus/examples/llms.txt Discover TLC model configurations using advanced features like symmetry reduction and custom views. Searches across .cfg files to identify models with specific TLC optimization or visualization settings. ```bash # Find models using symmetry reduction ls specifications/*/*.cfg | xargs grep -l "SYMMETRY" # Find models with custom views ls specifications/*/*.cfg | xargs grep -l "VIEW" ``` -------------------------------- ### Update Repository README Table Entry Source: https://context7.com/tlaplus/examples/llms.txt Add new specification entry to the repository README table with proper markdown formatting. Includes links to specification directory, author information, and status indicators for different verification features. ```markdown | [My Algorithm](specifications/MyAlgorithm) | Your Name | ✔ | | | ✔ | | ``` -------------------------------- ### Create TLA+ Specification with Model Files Source: https://context7.com/tlaplus/examples/llms.txt Generate a complete TLA+ specification project including module definition, configuration file, and manifest. Process involves creating directory structure, writing TLA+ code with Init/Next actions, defining invariants, and generating metadata for repository integration. ```bash # 1. Create specification directory mkdir specifications/MyAlgorithm cd specifications/MyAlgorithm # 2. Write TLA+ specification cat > MyAlgorithm.tla << 'EOF' ---- MODULE MyAlgorithm ---- EXTENDS Integers VARIABLE x, y Init == x = 0 /\ y = 0 Next == x' = x + 1 /\ y' = y + 1 Spec == Init /\ [][Next]_<> TypeOK == x \in Nat /\ y \in Nat ==== EOF # 3. Write model configuration cat > MyAlgorithm.cfg << 'EOF' SPECIFICATION Spec INVARIANTS TypeOK EOF # 4. Generate manifest.json python .github/scripts/generate_manifest.py # 5. Edit manifest.json to add metadata: # - sources: papers, blog posts, repositories # - authors: list of spec authors # - tags: ["beginner"] if appropriate # - runtime: actual runtime in "HH:MM:SS" format # - result: "success", "safety failure", "deadlock failure", etc. ``` -------------------------------- ### Check Specifications with Apalache SMT Solver Source: https://context7.com/tlaplus/examples/llms.txt Use Apalache for bounded symbolic model checking with SMT solvers. Requires type annotations in specifications. Configuration through manifest.json enables symbolic checking mode with success or failure results. ```bash # Check with Apalache (requires type annotations) apalache-mc check --length=10 --inv=TypeOK Spec.tla # Configuration in manifest.json: # "mode": "symbolic" # "result": "success" ``` -------------------------------- ### TLA+ Model Configuration File Source: https://context7.com/tlaplus/examples/llms.txt Specifies which TLA+ specification to check and what properties to verify. Model files (.cfg) define invariants, properties, and constant values for model checking. Used by TLC to perform exhaustive state space exploration and verification of safety and liveness properties. ```tla SPECIFICATION Spec INVARIANTS TypeOK SafetyProperty PROPERTIES LivenessProperty CONSTANTS Value = {v1, v2, v3} Acceptor = {a1, a2, a3} Quorum = {{a1,a2}, {a1,a3}, {a2,a3}} ``` -------------------------------- ### TLA+ Ma's Puzzle Specification Source: https://github.com/tlaplus/examples/blob/master/specifications/SlidingPuzzles/README.md Defines the dimensions (W, H) and the initial configuration (Mas) for Ma's Puzzle. It also specifies the goal configuration (MasGoal). ```tla W == 5 H == 5 Mas == {{<<0, 0>>, <<1, 0>>, <<2, 0>>}, {<<3, 0>>, <<4, 0>>,<<4, 1>>}, {<<0, 1>>, <<1, 1>>}, {<<2, 1>>, <<3, 1>>}, {<<0, 2>>, <<0, 3>>, <<1, 3>>}, {<<1, 2>>, <<2, 2>>}, {<<3, 2>>, <<4, 2>>}, {<<2, 3>>, <<3, 3>>, <<4, 3>>}, {<<2, 4>>}} MasGoal == {{<<3, 0>>, <<4, 0>>,<<4, 1>>}, {<<3, 1>>, <<3, 2>>, <<4, 2>>}} \subseteq board ``` -------------------------------- ### TLA+ Pennant Puzzle Specification Source: https://github.com/tlaplus/examples/blob/master/specifications/SlidingPuzzles/README.md Defines the dimensions (W, H) and the initial configuration (Pennant) for the Pennant variation of the sliding block puzzle. It also specifies the goal configuration (PennantGoal). ```tla W == 4 H == 5 Pennant == {{<<0, 0>>, <<0, 1>>, <<1, 0>>, <<1, 1>>}, {<<2, 0>>, <<3, 0>>}, {<<2, 1>>, <<3, 1>>}, {<<0, 2>>}, {<<1, 2>>}, {<<0, 3>>, <<0, 4>>}, {<<1, 3>>, <<1, 4>>}, {<<2, 3>>, <<3, 3>>}, {<<2, 4>>, <<3, 4>>}} PennantGoal == {<<0, 3>>, <<0, 4>>, <<1, 3>>, <<1, 4>>} \in board ``` -------------------------------- ### TLA+ Paxos Specification Source: https://context7.com/tlaplus/examples/llms.txt Defines the Paxos consensus algorithm using TLA+. It includes constants for values, acceptors, and quorums, message types, state variables, type checking, initialization, message sending, and the phases of the Paxos algorithm (Phase 1a, 1b, 2a, 2b). ```tla -------------------------------- MODULE Paxos ------------------------------- EXTENDS Integers CONSTANT Value, Acceptor, Quorum ASSUME QuorumAssumption == \/ \A Q \in Quorum : Q \subseteq Acceptor /\ \A Q1, Q2 \in Quorum : Q1 \cap Q2 # {} Ballot == Nat None == CHOOSE v : v \notin Value Message == [type : {"1a"}, bal : Ballot] \cup [type : {"1b"}, acc : Acceptor, bal : Ballot, mbal : Ballot \cup {-1}, mval : Value \cup {None}] \cup [type : {"2a"}, bal : Ballot, val : Value] \cup [type : {"2b"}, acc : Acceptor, bal : Ballot, val : Value] VARIABLE maxBal, \* Maximum ballot number seen by each acceptor maxVBal, \* Ballot number of the last vote cast maxVal, \* Value of the last vote cast msgs \* Set of all messages sent vars == <> TypeOK == /\ maxBal \in [Acceptor -> Ballot \cup {-1}] /\ maxVBal \in [Acceptor -> Ballot \cup {-1}] /\ maxVal \in [Acceptor -> Value \cup {None}] /\ msgs \subseteq Message Init == /\ maxBal = [a \in Acceptor |-> -1] /\ maxVBal = [a \in Acceptor |-> -1] /\ maxVal = [a \in Acceptor |-> None] /\ msgs = {} Send(m) == msgs' = msgs \cup {m} \* Leader initiates a ballot Phase1a(b) == /\ Send([type |-> "1a", bal |-> b]) /\ UNCHANGED <> \* Acceptor responds to ballot b if b > maxBal[a] Phase1b(a) == /\ \E m \in msgs : /\ m.type = "1a" /\ m.bal > maxBal[a] /\ maxBal' = [maxBal EXCEPT ![a] = m.bal] /\ Send([type |-> "1b", acc |-> a, bal |-> m.bal, mbal |-> maxVBal[a], mval |-> maxVal[a]]) /\ UNCHANGED <> \* Leader proposes value v for ballot b Phase2a(b, v) == /\ ~ \E m \in msgs : m.type = "2a" /\ m.bal = b /\ \E Q \in Quorum : LET Q1b == {m \in msgs : /\ m.type = "1b" /\ m.acc \in Q /\ m.bal = b} Q1bv == {m \in Q1b : m.mbal \geq 0} IN /\ \A a \in Q : \E m \in Q1b : m.acc = a /\ \/ Q1bv = {} \/ \E m \in Q1bv : /\ m.mval = v /\ \A mm \in Q1bv : m.mbal \geq mm.mbal /\ Send([type |-> "2a", bal |-> b, val |-> v]) /\ UNCHANGED <> \* Acceptor votes for value in ballot Phase2b(a) == \E m \in msgs : /\ m.type = "2a" /\ m.bal \geq maxBal[a] /\ maxBal' = [maxBal EXCEPT ![a] = m.bal] /\ maxVBal' = [maxVBal EXCEPT ![a] = m.bal] /\ maxVal' = [maxVal EXCEPT ![a] = m.val] /\ Send([type |-> "2b", acc |-> a, bal |-> m.bal, val |-> m.val]) Next == \/ \E b \in Ballot : \/ Phase1a(b) \/ \E v \in Value : Phase2a(b, v) \/ \E a \in Acceptor : Phase1b(a) \/ Phase2b(a) Spec == Init /\ [][Next]_vars ============================================================================= ``` -------------------------------- ### JSON Manifest Schema Definition Source: https://context7.com/tlaplus/examples/llms.txt Defines the metadata structure for TLA+ specifications including sources, authors, tags, modules, features, proof information, and model configurations. Each specification directory contains a manifest.json file describing its dependencies, runtime characteristics, and verification results. ```json { "sources": ["https://example.com/paper.pdf"], "authors": ["Author Name"], "tags": ["beginner"], "modules": [ { "path": "specifications/Example/Example.tla", "communityDependencies": [], "features": ["pluscal"], "proof": { "runtime": "00:05:30" }, "models": [ { "path": "specifications/Example/Example.cfg", "runtime": "00:00:15", "mode": "exhaustive search", "result": "success", "distinctStates": 1234, "totalStates": 5678, "stateDepth": 42 } ] } ] } ``` -------------------------------- ### Weight Combination Solver in Orc Language Source: https://github.com/tlaplus/examples/blob/master/specifications/CarTalkPuzzle/orc-solution.txt Complete implementation of weight combination solver that enumerates weight tuples and validates if they can produce all values from 1 to n through signed combinations. Uses Orc's parallel processing and signal-based coordination for efficient solution finding. Input: nw (number of weights), n (target sum). Output: First valid weight combination. ```Orc val nw = 5 -- number of weights val n = 40 -- number of values to be measured {- Enumerate all distinct nw-tuples that sum to n. - Each tuple is represented as a list - the list elements are in ascending order from head onward Below, for(i,j) publishes all k, i <= k < j. enum(last, remsum, k) enumerates all lists in ascending order - starting at last - adding up to remsum - having k elements -} def enum(last, remsum, 1) = [remsum] def enum(last, remsum, k) = for(last, remsum/k+1) >x> enum(x,remsum-x,k-1) >xs> (x:xs) {- psum(zs), where zs is a list, publishes all values j where j can be obtained by multiplying each element of zs independently by -1,0 or 1, and adding the result. -} def psum([]) = 0 def psum(x:xs) = psum(xs) >y> (-x+y | y | x+y) {- check(zs) checks if list zs is a solution; it outputs zs if it is and halts silently otherwise. An array b of write-once cells are used. Counter c holds the number of distinct values in b that have been written to; once n different values have been written, it outputs zs. -} def check(zs) = val b = Table(n+1, lambda (_) = Cell()) val c = Counter(n) psum(zs) >j> Ift(j :> 0) >> b(j) := signal >> c.dec() >> stop | c.onZero() >> zs {- Enumerate all tuples and for each check if it is a solution. Stop after finding the first one. -} Let(enum(1,n,nw) >zs> check(zs)) ``` -------------------------------- ### Implement Dining Philosophers with PlusCal in TLA+ Source: https://context7.com/tlaplus/examples/llms.txt Defines the Chandy-Misra solution to the Dining Philosophers problem using PlusCal syntax transpiled to TLA+. Models philosophers as processes competing for forks with cleanliness states to prevent deadlock. Uses TLA+ definitions for fork/philosopher relationships and eating conditions. ```tla ---- MODULE DiningPhilosophers ---- EXTENDS Integers, TLC CONSTANTS NP \* Number of philosophers ASSUME NP \in Nat \ {0} (* --algorithm DiningPhilosophers variables forks = [ fork \in 1..NP |-> [ holder |-> IF fork = 2 THEN 1 ELSE fork, clean |-> FALSE ] ] define LeftFork(p) == p RightFork(p) == IF p = NP THEN 1 ELSE p + 1 LeftPhilosopher(p) == IF p = 1 THEN NP ELSE p - 1 RightPhilosopher(p) == IF p = NP THEN 1 ELSE p + 1 IsHoldingBothForks(p) == forks[LeftFork(p)].holder = p /\ forks[RightFork(p)].holder = p BothForksAreClean(p) == forks[LeftFork(p)].clean /\ forks[RightFork(p)].clean CanEat(p) == IsHoldingBothForks(p) /\ BothForksAreClean(p) end define; fair process Philosopher \in 1..NP variables hungry = TRUE; begin Loop: while TRUE do either \* Request fork from neighbor if needed await ~IsHoldingBothForks(self); \* Request logic here or \* Hand over dirty fork to requesting neighbor await \E fork \in {LeftFork(self), RightFork(self)} : /\ forks[fork].holder = self /\ ~forks[fork].clean; \* Hand over logic here or \* Eat when holding both clean forks await CanEat(self); hungry := FALSE; forks[LeftFork(self)].clean := FALSE; forks[RightFork(self)].clean := FALSE; end either; end while; end process; end algorithm; *) ==== ``` -------------------------------- ### TLA+ Actions for Prisoner Puzzle Source: https://github.com/tlaplus/examples/blob/master/specifications/Prisoners_Single_Switch/README.md These TLA+ actions model the behavior of prisoners interacting with a light switch. 'StandardAction' represents a normal prisoner turning the light on, while 'CounterAction' represents the designated counter turning the light off and incrementing a count. This implementation aims for a close model of individual prisoner decision-making. ```TLA+ StandardAction(p) == /\ p \in NormalPrisoner /\ light = "off" /\ signalled[p] < SignalLimit /\ light' = "on" /\ signalled' = [signalled EXCEPT ![p] = @ + 1] /\ UNCHANGED <> CounterAction(p) == /\ p = Designated_Counter /\ light = "on" /\ light' = "off" /\ count' = count + 1 /\ announced' = (count' >= VictoryThreshold) /\ UNCHANGED <> ``` -------------------------------- ### Regex Pattern for ShiViz JSON Logging Compatibility Source: https://github.com/tlaplus/examples/blob/master/specifications/ewd998/EWD998ChanTrace.md Regular expression pattern used to parse JSON log entries for ShiViz vector clock visualization. The regex captures event types (<, >, d), node identities, packet information including source/destination nodes and message types, and vector clock data for distributed system event ordering analysis. ```regex ^{\"event\":\"(<|>|d)\",\"node\":(?[0-9]?),\"pkt\":{(\"snd\":(?[0-9]?),\"rcv\":(?[0-9]?),\"msg\":(?({\"type\":\"tok\",\"q\":-?[0-9]*,\"color\":\"(white|black)\"}|{\"type\":\"(pl|trm|w|d)\"})),|)\"vc\":(?.*)}} ``` -------------------------------- ### Implement AtTerminationDetected Logging in TLA+ Source: https://github.com/tlaplus/examples/blob/master/specifications/ewd998/README.md Provides the AtTerminationDetected state constraint that writes simulation statistics to a CSV file when termination is detected. It records feature flags, node count, level information, and counts of sub‑actions, then resets the TLC list element. The snippet uses CSVWrite, TLCGet, and TLCSet primitives and accesses environment variable IOEnv.Out. ```tla AtTerminationDetected == EWD998!terminationDetected => /\ LET o TLCGet("stats").behavior.actions IN /\ CSVWrite("%1$s#%2$s#%3$s#%4$s#%5$s#%6$s#%7$s#%8$s#%9$s", << F, N, TLCGet("level"), TLCGet("level") - TLCGet(1), o["InitiateProbe"],o["PassTokenOpts"], \\* Note "Opts" suffix! o["SendMsg"],o["RecvMsg"],o["Deactivate"] >>, IOEnv.Out) /\ TLCSet(1, 0) ``` -------------------------------- ### TLA+ Trace Validation Sub-Action Definition Source: https://github.com/tlaplus/examples/blob/master/specifications/ewd998/EWD998ChanTrace.md TLA+ specification defining a sub-action for trace validation that handles inbox state transitions and message matching. This fragment demonstrates the challenge of validating extremely partial traces where not all variables are logged, requiring infinite set definitions that become impractical for TLC model checking. ```tla SomeSubAction == /\ ... /\ inbox' \in [Node -> Seq(Msg)] /\ \E idx \in DOMAIN inbox[Initiator]': inbox[Initiator][idx]' = Trace[TLCGet("level")].msg /\ ... ```