Add v10 benchmark results (single-shot, 20 problems)

eval/benchmark_results_v10.csv

@@ -0,0 +1,1072 @@
+model,benchmark_id,name,domain,difficulty,sany_pass,tlc_pass,structural_score,tlc_tier,runtime_s,generated_spec
+chattla:20b,BM001,Mutual Exclusion,scheduling,2,0,0,1.0,bronze,3.7,"---- MODULE MutualExclusion ----
+EXTENDS Integers, Sequences, FiniteSets
+CONSTANTS N
+
+VARIABLES state, turn
+
+
+
+
+    od;
+*)
+
+Init == 
+    /\ state = [i \in 1..N |-> ""idle""]
+    /\ turn \in 1..N
+
+Next == 
+    \E i \in 1..N :
+        /\ state[i] = ""idle""
+        /\ state[i] := ""trying""
+        /\ state[i] = ""trying""
+        /\ state[i] := ""critical""
+        /\ state[i] := ""idle""
+        /\ turn := (turn % N) + 1
+
+Spec == Init /\ [][Next]_<<state, turn>>
+
+TypeOK == 
+    /\ state \in [1..N -> {""idle"", ""trying"", ""critical""}]
+    /\ turn \in 1..N
+
+===="
+chattla:20b,BM002,Two-Phase Commit,transaction,3,0,0,1.0,bronze,10.77,"---- MODULE TwoPhaseCommit ----
+EXTENDS Integers, Sequences, FiniteSets
+
+CONSTANT N
+
+VARIABLES participants, coordinator, messages
+
+(* Participants are numbered 1..N *)
+Participants == 1..N
+
+(* Messages are tuples: [sender \in Participants, receiver \in Participants, type \in {""Prepare"", ""VoteYes"", ""VoteNo"", ""Commit"", ""Abort""}, content \in {"""", ""VoteYes"", ""VoteNo""}] *)
+Message == [sender \in Participants, receiver \in Participants, type \in {""Prepare"", ""VoteYes"", ""VoteNo"", ""Commit"", ""Abort""}, content \in {"""", ""VoteYes"", ""VoteNo""}]
+
+(* Initial state: all participants are in the ""Init"" state, coordinator is in ""Start"" state, no messages *)
+Init == /\ participants = [i \in Participants |-> ""Init""]
+        /\ coordinator = ""Start""
+        /\ messages = {}
+
+(* Coordinator sends Prepare to all participants *)
+SendPrepare == /\ coordinator = ""Start""
+               /\ messages' = messages \cup { [sender |-> coordinator, receiver |-> i, type |-> ""Prepare"", content |-> """"] : i \in Participants }
+               /\ coordinator' = ""WaitingForVotes""
+               /\ participants' = participants
+
+(* Participants receive Prepare and vote Yes *)
+ReceivePrepareAndVoteYes == /\ coordinator = ""WaitingForVotes""
+                           /\ \E msg \in messages : msg.type = ""Prepare"" /\ msg.receiver \in Participants /\ participants[msg.receiver] = ""Init""
+                           /\ messages' = messages \ { msg }
+                           /\ participants' = [participants EXCEPT ![msg.receiver] = ""VotedYes""]
+                           /\ messages' = messages' \cup { [sender |-> msg.receiver, receiver |-> coordinator, type |-> ""VoteYes"", content |-> ""VoteYes""] }
+
+(* Participants receive Prepare and vote No *)
+ReceivePrepareAndVoteNo == /\ coordinator = ""WaitingForVotes""
+                          /\ \E msg \in messages : msg.type = ""Prepare"" /\ msg.receiver \in Participants /\ participants[msg.receiver] = ""Init""
+                          /\ messages' = messages \ { msg }
+                          /\ participants' = [participants EXCEPT ![msg.receiver] = ""VotedNo""]
+                          /\ messages' = messages' \cup { [sender |-> msg.receiver, receiver |-> coordinator, type |-> ""VoteNo"", content |-> ""VoteNo""] }
+
+(* Coordinator receives all Yes votes and sends Commit *)
+SendCommit == /\ coordinator = ""WaitingForVotes""
+              /\ \A i \in Participants : participants[i] = ""VotedYes""
+              /\ messages' = messages \cup { [sender |-> coordinator, receiver |-> i, type |-> ""Commit"", content |-> """"] : i \in Participants }
+              /\ coordinator' = ""Committed""
+              /\ participants' = participants
+
+(* Coordinator receives any No vote and sends Abort *)
+SendAbort == /\ coordinator = ""WaitingForVotes""
+             /\ \E i \in Participants : participants[i] = ""VotedNo""
+             /\ messages' = messages \cup { [sender |-> coordinator, receiver |-> i, type |-> ""Abort"", content |-> """"] : i \in Participants }
+             /\ coordinator' = ""Aborted""
+             /\ participants' = participants
+
+(* Participants receive Commit and transition to Committed *)
+ReceiveCommit == /\ coordinator \in {""Committed"", ""Aborted""}
+                /\ \E msg \in messages : msg.type = ""Commit"" /\ msg.receiver \in Participants /\ participants[msg.receiver] = ""VotedYes""
+                /\ messages' = messages \ { msg }
+                /\ participants' = [participants EXCEPT ![msg.receiver] = ""Committed""]
+                /\ coordinator' = coordinator
+
+(* Participants receive Abort and transition to Aborted *)
+ReceiveAbort == /\ coordinator \in {""Committed"", ""Aborted""}
+               /\ \E msg \in messages : msg.type = ""Abort"" /\ msg.receiver \in Participants /\ participants[msg.receiver] = ""VotedYes""
+               /\ messages' = messages \ { msg }
+               /\ participants' = [participants EXCEPT ![msg.receiver] = ""Aborted""]
+               /\ coordinator' = coordinator
+
+(* Next-state relation *)
+Next == SendPrepare \/ ReceivePrepareAndVoteYes \/ ReceivePrepareAndVoteNo \/ SendCommit \/ SendAbort \/ ReceiveCommit \/ ReceiveAbort
+
+(* Type invariant *)
+TypeOK == /\ participants \in [Participants -> {""Init"", ""VotedYes"", ""VotedNo"", ""Committed"", ""Aborted""}]
+          /\ coordinator \in {""Start"", ""WaitingForVotes"", ""Committed"", ""Aborted""}
+          /\ messages \subseteq Message
+
+Spec == Init /\ [][Next]_<<participants, coordinator, messages>>
+
+===="
+chattla:20b,BM003,Dining Philosophers,scheduling,2,0,0,1.0,bronze,6.17,"---- MODULE DiningPhilosophers ----
+EXTENDS Integers, Sequences, FiniteSets
+
+CONSTANT N
+
+VARIABLES forks, states
+
+(* Forks: a set of fork indices {1, 2, ..., N} *)
+Forks == {1, 2, ..., N}
+
+(* States: a function from philosopher indices to {""thinking"", ""hungry"", ""eating""} *)
+States == [i \in Forks |-> {""thinking"", ""hungry"", ""eating""}]
+
+(* Initial state: all forks are free, all philosophers are thinking *)
+Init == forks = Forks /\ states = [i \in Forks |-> ""thinking""]
+
+(* Helper: determine the left and right fork indices for philosopher i *)
+LeftFork(i) == IF i = 1 THEN N ELSE i - 1
+RightFork(i) == IF i = N THEN 1 ELSE i + 1
+
+(* Helper: check if philosopher i can eat (both adjacent forks are free) *)
+CanEat(i) == LeftFork(i) \in forks /\ RightFork(i) \in forks
+
+(* Action: philosopher i picks up forks and starts eating *)
+TakeForks(i) == 
+    /\ states[i] = ""hungry""
+    /\ CanEat(i)
+    /\ forks' = forks \ {LeftFork(i), RightFork(i)}
+    /\ states' = [states EXCEPT ![i] = ""eating""]
+
+(* Action: philosopher i puts down forks after eating *)
+PutForks(i) == 
+    /\ states[i] = ""eating""
+    /\ forks' = forks \cup {LeftFork(i), RightFork(i)}
+    /\ states' = [states EXCEPT ![i] = ""thinking""]
+
+(* Action: philosopher i becomes hungry *)
+Hungry(i) == 
+    /\ states[i] = ""thinking""
+    /\ states' = [states EXCEPT ![i] = ""hungry""]
+    /\ forks' = forks
+
+(* Next action: any philosopher can become hungry, or any philosopher who can eat can start eating, or any philosopher who is eating can put down forks *)
+Next == \E i \in Forks : 
+    (Hungry(i) \/ TakeForks(i) \/ PutForks(i))
+
+(* Type invariant: forks is a subset of Forks, states is a function from Forks to {""thinking"", ""hungry"", ""eating""} *)
+TypeOK == 
+    /\ forks \subseteq Forks
+    /\ states \in [Forks -> {""thinking"", ""hungry"", ""eating""}]
+
+Spec == Init /\ [][Next]_<<forks, states>>
+
+===="
+chattla:20b,BM004,Lamport's Bakery Algorithm,consensus,3,1,0,1.0,silver,4.48,"---- MODULE Bakery ----
+EXTENDS Integers, Sequences, FiniteSets
+Max(S) == CHOOSE x \in S : \A y \in S : x >= y
+
+
+CONSTANT N
+
+VARIABLES num, flag
+
+(* TypeOK ensures num is a sequence of N integers, flag is a sequence of N booleans *)
+TypeOK == /\ num \in Seq(N)
+          /\ flag \in Seq(N)
+
+(* Helper functions *)
+Less(i, j) == /\ flag[i] /\ flag[j]
+              /\ (num[i] < num[j] \/ (num[i] = num[j] /\ i < j))
+
+MaxNum == IF N = 0 THEN 0 ELSE Max(num)
+
+(* Initialization: all flag false, all num 0 *)
+Init == /\ flag = [i \in 1..N |-> FALSE]
+        /\ num = [i \in 1..N |-> 0]
+
+(* Next action: process i can be in choosing or critical section *)
+Next == \E i \in 1..N :
+        /\ flag' = [flag EXCEPT ![i] = TRUE]
+        /\ num' = [num EXCEPT ![i] = MaxNum + 1]
+        /\ flag' = [flag EXCEPT ![i] = FALSE]
+        /\ UNCHANGED <<num, flag>>
+
+Spec == Init /\ [][Next]_<<num, flag>>
+
+(* Mutual exclusion invariant: no two processes in critical section simultaneously *)
+MutualExclusion == \A i, j \in 1..N : i /= j => ~ (flag[i] /\ flag[j] /\ Less(i, j))
+
+===="
+chattla:20b,BM005,Producer-Consumer Queue,storage,2,0,0,0.778,bronze,3.24,"---- MODULE BoundedFIFO ----
+EXTENDS Integers, Sequences, FiniteSets
+
+CONSTANT K
+
+VARIABLES q, head, tail, size
+
+vars == <<q, head, tail, size>>
+
+Init == /\ q = [i \in 1..K |-> -> 0]
+        /\ head = 1
+        /\ tail = 1
+        /\ size = 0
+
+Producer(x) == /\ size < K
+              /\ q[tail] = 0
+              /\ q' = [q EXCEPT ![tail] = x]
+              /\ tail' = IF tail = K THEN 1 ELSE tail + 1
+              /\ size' = size + 1
+              /\ UNCHANGED <<head, q>>
+
+Consumer(y) == /\ size > 0
+              /\ y = q[head]
+              /\ q' = [q EXCEPT ![head] = 0]
+              /\ head' = IF head = K THEN 1 ELSE head + 1
+              /\ size' = size - 1
+              /\ UNCHANGED <<tail, q>>
+
+Next == \E x \in Nat : Producer(x)
+      \/ \E y \in Nat : Consumer(y)
+
+Spec == Init /\ [][Next]_vars
+
+===="
+chattla:20b,BM006,Raft Leader Election,consensus,4,0,0,1.0,bronze,4.07,"---- MODULE RaftLeaderElection ----
+EXTENDS Integers, Sequences, FiniteSets
+CONSTANTS Servers
+
+VARIABLES currentTerm, votedFor, state
+
+
+
+TypeOK == /\ currentTerm \in Nat
+          /\ votedFor \in {None} \cup Servers
+          /\ state \in {Follower, Candidate, Leader}
+
+Init == /\ currentTerm = 0
+        /\ votedFor = None
+        /\ state = Follower
+
+(* Candidate wins if it gets a majority of votes *)
+MajorityWins == \E votes \in SUBSET Servers :
+  /\ Cardinality(votes) > Cardinality(Servers) \div 2
+  /\ \A s \in votes : s = Candidate
+
+Next == 
+  (* Follower to Candidate transition *)
+  \/ /\ state = Follower
+     /\ currentTerm' = currentTerm + 1
+     /\ votedFor' = Candidate
+     /\ state' = Candidate
+  (* Candidate to Leader transition *)
+  \/ /\ state = Candidate
+     /\ MajorityWins
+     /\ state' = Leader
+  (* No state change *)
+  \/ /\ state' = state
+     /\ currentTerm' = currentTerm
+     /\ votedFor' = votedFor
+
+Spec == Init /\ [][Next]_<<currentTerm, votedFor, state>>
+
+===="
+chattla:20b,BM007,Read-Write Lock,storage,2,1,0,1.0,silver,3.83,"---- MODULE ReadWriteLock ----
+EXTENDS Integers, Sequences, FiniteSets
+
+VARIABLES readers, writer_active
+
+(* --algorithm ReadWriteLock
+end ReadWriteLock *)
+
+TypeOK == 
+  /\ readers \in Seq(Int)
+  /\ writer_active \in BOOLEAN
+
+Init == 
+  /\ readers = <<>>
+  /\ writer_active = FALSE
+
+Next == 
+  \/ /\ writer_active = FALSE
+     /\ writer_active' = TRUE
+     /\ readers' = readers
+  \/ /\ writer_active = FALSE
+     /\ Len(readers) > 0
+     /\ writer_active' = writer_active
+     /\ readers' = Tail(readers)
+
+Spec == Init /\ [][Next]_<<readers, writer_active>>
+
+===="
+chattla:20b,BM008,Distributed Snapshot (Chandy-Lamport),networking,5,0,0,1.0,bronze,7.45,"---- MODULE DistributedSnapshot ----
+EXTENDS Integers, Sequences, FiniteSets
+
+CONSTANT N, Channels
+
+VARIABLES state, channel, markerSent, markerReceived
+
+(* State of each process: 0 = not recorded, 1 = recorded *)
+State == [p \in 1..N |-> 0 |-> 1]
+
+(* Channel state: sequence of messages *)
+ChannelState == [c \in Channels |-> Seq]
+
+(* MarkerSent: set of channels along which marker has been sent *)
+MarkerSent == [c \in Channels |-> BOOLEAN]
+
+(* MarkerReceived: set of channels along which marker has been received *)
+MarkerReceived == [c \in Channels |-> BOOLEAN]
+
+(* Initial state: no process has recorded state, channels empty, no markers sent/received *)
+Init == /\ state = [p \in 1..N |-> 0]
+        /\ channel = [c \in Channels |-> <<>>]
+        /\ markerSent = [c \in Channels |-> FALSE]
+        /\ markerReceived = [c \in Channels |-> FALSE]
+
+(* Next action: either send a regular message or send a marker *)
+Next == 
+  \E p \in 1..N : \E q \in 1..N : \E c \in Channels :
+    /\ c = <<p, q>>
+    /\ \E msg \in 1..N :
+        /\ state[p] = 0
+        /\ channel' = [channel EXCEPT ![c] = Append(channel[c], msg)]
+        /\ UNCHANGED <<state, markerSent, markerReceived>>
+    \/ \E msg \in 1..N :
+        /\ state[p] = 1
+        /\ channel' = [channel EXCEPT ![c] = Append(channel[c], msg)]
+        /\ UNCHANGED <<state, markerSent, markerReceived>>
+    \/ /\ state[p] = 0
+       /\ channel' = channel
+       /\ markerSent' = [markerSent EXCEPT ![c] = TRUE]
+       /\ UNCHANGED <<state, markerReceived>>
+
+(* Receive action: process a message from a channel *)
+Receive == 
+  \E c \in Channels : \E p \in 1..N : \E q \in 1..N :
+    /\ c = <<p, q>>
+    /\ channel[c] /= <<>>
+    /\ msg = Head(channel[c])
+    /\ channel' = [channel EXCEPT ![c] = Tail(channel[c])]
+    /\ IF msg = 0 THEN
+         /\ state' = [state EXCEPT ![p] = 1]
+         /\ markerReceived' = [markerReceived EXCEPT ![c] = TRUE]
+         /\ UNCHANGED <<markerSent>>
+
+         /\ UNCHANGED <<state, markerSent, markerReceived>>
+
+(* Next action: either send or receive *)
+Next == Send \/ Receive
+
+(* Specification *)
+Spec == Init /\ [][Next]_<<state, channel, markerSent, markerReceived>>
+
+(* Type invariant *)
+TypeOK == /\ state \in State
+          /\ channel \in ChannelState
+          /\ markerSent \in [Channels |-> BOOLEAN]
+          /\ markerReceived \in [Channels |-> BOOLEAN]
+
+===="
+chattla:20b,BM009,Token Ring,networking,2,1,1,0.889,gold,1.95,"---- MODULE TokenRing ----
+EXTENDS Integers, Sequences, FiniteSets
+
+CONSTANT N
+
+VARIABLE token
+
+Init == token \in 1..N
+
+Next == token' = IF token = N THEN 1 ELSE token + 1
+
+Spec == Init /\ [][Next]_<<token>>
+
+TypeOK == token \in 1..N
+
+===="
+chattla:20b,BM010,Simple Key-Value Store,storage,3,0,0,1.0,bronze,1.74,"---- MODULE KeyValueStore ----
+EXTENDS Integers, Sequences, FiniteSets
+
+CONSTANTS Keys, Values, NULL
+
+VARIABLES store
+
+Init == store = [k \in Keys |-> NULL]
+
+Next == \E k \in Keys : \E v \in Values :
+          store' = [store EXCEPT ![k] = v]
+
+Spec == Init /\ [][Next]_<<store>>
+
+TypeOK == /\ store \in [Keys -> Values]
+          /\ Keys \in FiniteSets
+          /\ Values \in FiniteSets
+
+===="
+chattla:20b,BM011,Paxos Single-Decree,consensus,4,1,0,0.444,silver,44.62,"---- MODULE Paxos ----
+EXTENDS Integers, Sequences, FiniteSets
+
+CONSTANT N, M
+
+VARIABLES ballot, promised, accepted, chosen
+===="
+chattla:20b,BM012,Bounded Retransmission Protocol,networking,3,0,0,0.778,bronze,8.06,"---- MODULE FileTransfer ----
+EXTENDS Integers, Sequences, FiniteSets
+
+CONSTANTS File, MAX_RETRIES
+VARIABLES ackedChunks, lostChunks, retransCount, sentChunks, seqNum, state
+
+    /\ state \in {""idle"", ""sending"", ""waiting"", ""done"", ""failed""}
+    /\ seqNum \in 0..Len(File)
+    /\ retransCount \in 0..MAX_RETRIES
+    /\ sentChunks \in SUBSET 0..Len(File)
+    /\ ackedChunks \in SUBSET 0..Len(File)
+    /\ lostChunks \in SUBSET 0..Len(File)
+
+Init ==
+    /\ state = ""idle""
+    /\ seqNum = 0
+    /\ retransCount = 0
+    /\ sentChunks = {}
+    /\ ackedChunks = {}
+    /\ lostChunks = {}
+
+SendChunk ==
+    /\ state = ""idle""
+    /\ seqNum < Len(File)
+    /\ state' = ""sending""
+    /\ seqNum' = seqNum + 1
+    /\ retransCount' = 0
+    /\ sentChunks' = sentChunks \cup {seqNum}
+    /\ ackedChunks' = ackedChunks
+    /\ lostChunks' = lostChunks
+
+ReceiveAck ==
+    /\ state = ""waiting""
+    /\ seqNum \in ackedChunks
+    /\ state' = ""idle""
+    /\ seqNum' = seqNum
+    /\ retransCount' = 0
+    /\ sentChunks' = sentChunks
+    /\ ackedChunks' = ackedChunks
+    /\ lostChunks' = lostChunks
+
+Timeout ==
+    /\ state = ""waiting""
+    /\ retransCount < MAX_RETRIES
+    /\ state' = ""sending""
+    /\ retransCount' = retransCount + 1
+    /\ sentChunks' = sentChunks
+    /\ ackedChunks' = ackedChunks
+    /\ lostChunks' = lostChunks
+
+GiveUp ==
+    /\ state = ""waiting""
+    /\ retransCount = MAX_RETRIES
+    /\ state' = ""failed""
+    /\ seqNum' = seqNum
+    /\ retransCount' = retransCount
+    /\ sentChunks' = sentChunks
+    /\ ackedChunks' = ackedChunks
+    /\ lostChunks' = lostChunks
+
+Done ==
+    /\ state = ""idle""
+    /\ seqNum = Len(File)
+    /\ state' = ""done""
+    /\ seqNum' = seqNum
+    /\ retransCount' = retransCount
+    /\ sentChunks' = sentChunks
+    /\ ackedChunks' = ackedChunks
+    /\ lostChunks' = lostChunks
+
+Next ==
+    \/ SendChunk
+    \/ ReceiveAck
+    \/ Timeout
+    \/ GiveUp
+    \/ Done
+
+Spec == Init /\ [][Next]_<<state, seqNum, retransCount, sentChunks, ackedChunks, lostChunks>>
+
+===="
+chattla:20b,BM013,Transaction Isolation (Snapshot Isolation),transaction,4,0,0,1.0,bronze,8.42,"---- MODULE SnapshotIsolationDB ----
+EXTENDS Integers, Sequences, FiniteSets
+
+VARIABLES db, txns, nextTxId, v
+
+
+  txns = <<>>;  (* sequence of transaction records *)
+  nextTxId = 1;  (* next transaction ID *)
+
+actions
+  BeginTx == 
+    /\ txns' = Append(txns, [id |-> nextTxId, status |-> ""active"", snapshot |-> db, writes |-> <<>>])
+    /\ nextTxId' = nextTxId + 1
+    /\ UNCHANGED db
+
+  Read(txId, idx) == 
+    /\ txId \in {t.id : t \in txns}
+    /\ idx \in 1..Len(db)
+    /\ \E t \in txns : t.id = txId /\ t.status = ""active""
+    /\ UNCHANGED db /\ UNCHANGED txns /\ UNCHANGED nextTxId
+
+  Write(txId, val) == 
+    /\ txId \in {t.id : t \in txns}
+    /\ \E t \in txns : t.id = txId /\ t.status = ""active""
+    /\ txns' = [txns EXCEPT ![txId] = [@ EXCEPT !writes = Append(@.writes, val)]]
+    /\ UNCHANGED db /\ UNCHANGED nextTxId
+
+  Commit(txId) == 
+    /\ txId \in {t.id : t \in txns}
+    /\ \E t \in txns : t.id = txId /\ t.status = ""active""
+    /\ \A t \in txns : t.id = txId => 
+        \A v \in t.writes : v \notin {v' : v' \in db}
+    /\ db' = Append(db, t.writes)
+    /\ txns' = [txns EXCEPT ![txId] = [@ EXCEPT !status = ""committed""]]
+    /\ UNCHANGED nextTxId
+
+  Abort(txId) == 
+    /\ txId \in {t.id : t \in txns}
+    /\ \E t \in txns : t.id = txId /\ t.status = ""active""
+    /\ txns' = [txns EXCEPT ![txId] = [@ EXCEPT !status = ""aborted""]]
+    /\ UNCHANGED db /\ UNCHANGED nextTxId
+*)
+
+TypeOK ==
+  /\ db \in Seq(Seq(Int))
+  /\ txns \in Seq([id: Int)), writes: Seq(Seq(Int))])
+  /\ nextTxId \in Nat
+
+Init ==
+  /\ db = <<>>
+  /\ txns = <<>>
+  /\ nextTxId = 1
+
+Next ==
+  BeginTx \/ 
+  \E txId, idx \in 1..Len(txns) : Read(txId, idx) \/ 
+  \E txId, val \in 1..Len(db) : Write(txId, val) \/ 
+  \E txId \in 1..Len(txns) : Commit(txId) \/ 
+  \E txId \in 1..Len(txns) : Abort(txId)
+
+Spec == Init /\ [][Next]_<<db, txns, nextTxId>>
+
+===="
+chattla:20b,BM014,Clock Synchronisation,networking,3,0,0,0.444,bronze,44.69,"---- MODULE ClockSync ----
+EXTENDS Integers, Sequences, FiniteSets
+
+VARIABLES clocks, offsets
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync
+
+(* --algorithm ClockSync *)
+===="
+chattla:20b,BM015,Peterson's Algorithm,scheduling,2,0,0,0.778,bronze,2.95,"---- MODULE Peterson2 ----
+EXTENDS Integers, Sequences, FiniteSets
+
+VARIABLES flag, turn
+
+
+
+TypeOK == /\ flag \in [1..2 -> BOOLEAN]
+          /\ turn \in 1..2
+
+Spec == Init /\ [][Next]_<<flag, turn>>
+
+===="
+chattla:20b,BM016,Gossip Protocol,networking,3,0,0,1.0,bronze,1.69,"---- MODULE Gossip ----
+EXTENDS Integers, Sequences, FiniteSets
+
+VARIABLES known, infected
+
+Init == /\ known = <<>> /\ infected = {}
+
+Next == /\ \E i \in 1..N :
+          /\ known' = Append(known, i)
+          /\ infected' = infected \cup {i}
+
+Spec == Init /\ [][Next]_<<known, infected>>
+
+TypeOK == /\ known \subseteq 1..N
+          /\ infected \subseteq 1..N
+
+===="
+chattla:20b,BM017,Simple Allocator,storage,2,0,0,0.889,bronze,4.03,"---- MODULE MemoryAllocator ----
+EXTENDS Integers, Sequences, FiniteSets
+
+CONSTANTS N, Clients
+
+Pages == 1..N
+
+VARIABLE free, allocated
+
+Init == /\ free = Pages
+       /\ allocated = [c \in Clients |-> {}]
+
+Request(c) == /\ c \in Clients
+              /\ free /= {}
+              /\ c \notin DOMAIN allocated
+                 \/ allocated[c] = {}
+              /\ c \in DOMAIN allocated
+                 /\ allocated[c] = {}
+              /\ c \notin DOMAIN allocated
+                 /\ allocated' = [allocated EXCEPT ![c] = {}]
+                 /\ free' = free \ {CHOOSE p \in free : TRUE}
+              \/ /\ c \in DOMAIN allocated
+                 /\ allocated' = [allocated EXCEPT ![c] = {}]
+                 /\ free' = free \ {CHOOSE p \in free : TRUE}
+              /\ UNCHANGED <<>>  (* placeholder for other variables *)
+
+Release(c) == /\ c \in DOMAIN allocated
+              /\ allocated[c] /= {}
+              /\ allocated' = [allocated EXCEPT ![c] = {}]
+              /\ free' = free \cup allocated[c]
+              /\ UNCHANGED <<>>  (* placeholder for other variables *)
+
+Next == \E c \in Clients : Request(c) \/ Release(c)
+
+Spec == Init /\ [][Next]_<<free, allocated>>
+
+TypeOK == /\ free \subseteq Pages
+          /\ allocated \subseteq [Clients -> SUBSET Pages]
+          /\ \A c \in DOMAIN allocated : allocated[c] \subseteq Pages
+
+===="
+chattla:20b,BM018,Publish-Subscribe Broker,networking,3,0,0,1.0,bronze,3.91,"---- MODULE Broker ----
+EXTENDS Integers, Sequences, FiniteSets
+
+VARIABLES subscribers, messages, inbox
+
+(* Type definitions *)
+Topic == Int
+Message == [topic: Topic, content: Int]
+Subscriber == [id: Int, interests: SUBSET Topic, inbox: Seq Message]
+
+(* State predicates *)
+TypeOK == 
+    /\ subscribers \in SUBSET (SUBSET Topic)
+    /\ messages \in Seq Message
+
+(* Initial state *)
+Init == 
+    /\ subscribers = <<>>
+    /\ messages = <<>>
+
+(* Action: Register a subscriber with interests *)
+Register(sub, interests) == 
+    /\ sub \notin subscribers
+    /\ subscribers' = Append(subscribers, [id |-> sub, interests |-> interests, inbox |-> <<>>])
+    /\ UNCHANGED messages
+
+(* Action: Post a message on a topic *)
+Post(msg) == 
+    /\ msg \in messages
+    /\ messages' = Append(messages, msg)
+    /\ UNCHANGED subscribers
+
+(* Action: Deliver messages to subscribers *)
+Deliver == 
+    /\ \E sub \in subscribers:
+        /\ \E msg \in messages:
+            /\ msg.topic \in sub.interests
+            /\ sub.inbox' = Append(sub.inbox, msg)
+    /\ UNCHANGED messages
+
+(* Next-state relation *)
+Next == 
+    \E sub \in subscribers : \E interests \in SUBSET Topic :
+        Register(sub, interests)
+    \/ \E msg \in messages:
+        Post(msg)
+    \/ Deliver
+
+(* Temporal specification *)
+Spec == Init /\ [][Next]_<<subscribers, messages>>
+
+===="
+chattla:20b,BM019,Dekker's Algorithm,scheduling,3,1,1,1.0,gold,3.89,"---- MODULE Dekker ----
+EXTENDS Integers, Sequences, FiniteSets
+
+VARIABLES turn, wants
+
+Init == /\ turn \in {0,1}
+        /\ wants = [i \in {0,1} |-> FALSE]
+
+Next == 
+  \/ /\ wants[0] = FALSE
+      /\ wants[1] = FALSE
+      /\ turn' = turn
+      /\ wants' = wants
+  \/ /\ wants[0] = FALSE
+      /\ wants[1] = TRUE
+      /\ turn' = 1
+      /\ wants' = [wants EXCEPT ![1] = FALSE]
+  \/ /\ wants[0] = TRUE
+      /\ wants[1] = FALSE
+      /\ turn' = 0
+      /\ wants' = [wants EXCEPT ![0] = FALSE]
+  \/ /\ wants[0] = TRUE
+      /\ wants[1] = TRUE
+      /\ turn' = turn
+      /\ wants' = [wants EXCEPT ![turn] = FALSE]
+
+Spec == Init /\ [][Next]_<<turn, wants>>
+
+TypeOK == /\ turn \in {0,1}
+          /\ wants \in [ {0,1} -> BOOLEAN ]
+
+===="
+chattla:20b,BM020,Eventually Consistent Counter,storage,3,1,0,0.444,silver,44.8,"---- MODULE GCounter ----
+EXTENDS Integers, Sequences, FiniteSets
+
+VARIABLES counts
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm GCounter
+end
+*)
+
+(* --algorithm G *)
+===="