More clean separation of spec and model checking.

and runner script.

safekeeper/spec/.gitignore

@@ -0,0 +1,3 @@
+*TTrace*
+ProposerAcceptorConsensus.toolbox/
+states/

safekeeper/spec/MCProposerAcceptorStatic.tla

@@ -0,0 +1,19 @@
+---- MODULE MCProposerAcceptorStatic ----
+EXTENDS TLC, ProposerAcceptorStatic
+
+\* Augments the spec with model checking constraints.
+
+\* For model checking.
+CONSTANTS
+  max_entries, \* model constraint: max log entries acceptor/proposer can hold
+  max_term \* model constraint: max allowed term
+
+ASSUME max_entries \in Nat /\ max_term \in Nat
+
+\* Model space constraint.
+StateConstraint == \A p \in proposers:
+                    /\ prop_state[p].term <= max_term
+                    /\ Len(prop_state[p].wal) <= max_entries
+ProposerAcceptorSymmetry == Permutations(proposers) \union Permutations(acceptors)
+
+====

safekeeper/spec/ProposerAcceptorConsensus.cfg

@@ -1,34 +0,0 @@
-\* MV CONSTANT declarations
-CONSTANT NULL = NULL
-CONSTANTS
-p1 = p1
-p2 = p2
-p3 = p3
-a1 = a1
-a2 = a2
-a3 = a3
-\* MV CONSTANT definitions
-CONSTANT
-proposers = {p1, p2}
-acceptors = {a1, a2, a3}
-\* SYMMETRY definition
-SYMMETRY perms
-\* CONSTANT definitions
-CONSTANT
-max_term = 3
-CONSTANT
-max_entries = 3
-\* INIT definition
-INIT
-Init
-\* NEXT definition
-NEXT
-Next
-\* INVARIANT definition
-INVARIANT
-TypeOk
-ElectionSafety
-LogIsMonotonic
-LogSafety
-CommittedNotOverwritten
-CHECK_DEADLOCK FALSE

safekeeper/spec/ProposerAcceptorStatic.tla

@@ -1,4 +1,4 @@
----- MODULE ProposerAcceptorConsensus ----
+---- MODULE ProposerAcceptorStatic ----
 
 \* Differences from current implementation:
 \* - unified not-globally-unique epoch & term (node_id)
@@ -21,12 +21,6 @@ CONSTANT
 
 CONSTANT NULL
 
-ASSUME max_entries \in Nat /\ max_term \in Nat
-
-\* For specifying symmetry set in manual cfg file, see
-\* https://github.com/tlaplus/tlaplus/issues/404
-perms == Permutations(proposers) \union Permutations(acceptors)
-
 \********************************************************************************
 \* Helpers
 \********************************************************************************
@@ -73,6 +67,9 @@ Quorums == {subset \in SUBSET acceptors: Quorum(subset)}
 \* flush_lsn of acceptor a.
 FlushLsn(a) == Len(acc_state[a].wal)
 
+\* Typedefs. Note that TLA+ Nat includes zero.
+Terms == Nat
+Lsns == Nat
 
 \********************************************************************************
 \* Type assertion
@@ -88,14 +85,12 @@ TypeOk ==
       \* in campaign proposer sends RequestVote and waits for acks;
       \* in leader he is elected
       /\ prop_state[p].state \in {"campaign", "leader"}
-      \* 0..max_term should be actually Nat in the unbounded model, but TLC won't
-      \* swallow it
-      /\ prop_state[p].term \in 0..max_term
+      /\ prop_state[p].term \in Terms
       \* votes received
       /\ \A voter \in DOMAIN prop_state[p].votes:
          /\ voter \in acceptors
-         /\ prop_state[p].votes[voter] \in [epoch: 0..max_term, flush_lsn: 0..max_entries]
-      /\ prop_state[p].donor_epoch \in 0..max_term
+         /\ prop_state[p].votes[voter].epoch \in Terms /\ prop_state[p].votes[voter].flush_lsn \in Lsns
+      /\ prop_state[p].donor_epoch \in Terms
       \* wal is sequence of just <lsn, epoch of author> records
       /\ \A i \in DOMAIN prop_state[p].wal:
            prop_state[p].wal[i] \in [lsn: 1..max_entries, epoch: 1..max_term]
@@ -359,5 +354,28 @@ CommittedNotOverwritten ==
          (next_e /= NULL) =>
           ((commit_lsns[a] >= next_e.lsn) => (acc_state[a].wal[next_e.lsn] = next_e))
 
+\********************************************************************************
+\* Invariants which don't need to hold, but useful for playing/debugging.
+\********************************************************************************
+
+\* Limits max commit_lsn. That way we can check that we'are actually committing something.
+MaxCommitLsn == \A a \in acceptors: commit_lsns[a] < 2
+
+
+
+Alias ==
+  [prop_state |-> prop_state,
+   acc_state |-> acc_state,
+   commit_lsns |-> commit_lsns]
+\* Alias == [
+\*     x |-> 2
+\* ]
+    \* [
+    \*     currentTerm |-> currentTerm,
+    \*     state |-> state,
+    \*     log |-> log,
+    \*     config |-> config,
+    \*     committed |-> committed
+    \* ]
 
 ====

safekeeper/spec/modelcheck.sh

@@ -0,0 +1,14 @@
+#!/bin/bash
+
+CFG=models/MCProposerAcceptorStatic_p2_a3_t2_l2.cfg
+SPEC=MCProposerAcceptorStatic.tla
+MEM=7G
+
+# see
+# https://lamport.azurewebsites.net/tla/current-tools.pdf
+# for TLC options.
+# OffHeapDiskFPSet is the optimal fingerprint set implementation
+# https://docs.tlapl.us/codebase:architecture#fingerprint_sets_fpsets
+# add -simulate to run in infinite simulation mode
+java -Xmx$MEM -XX:MaxDirectMemorySize=$MEM -XX:+UseParallelGC -Dtlc2.tool.fp.FPSet.impl=tlc2.tool.fp.OffHeapDiskFPSet \
+  -cp /opt/TLA+Toolbox/tla2tools.jar tlc2.TLC $SPEC -config $CFG -workers 1 -gzip

safekeeper/spec/models/MCProposerAcceptorStatic_p2_a3_t2_l2.cfg

@@ -0,0 +1,18 @@
+\* A very small model just to play.
+CONSTANTS
+NULL = NULL
+proposers = {p1, p2}
+acceptors = {a1, a2, a3}
+max_term = 2
+max_entries = 2
+SPECIFICATION Spec
+CONSTRAINT StateConstraint
+INVARIANT
+TypeOk
+ElectionSafety
+LogIsMonotonic
+LogSafety
+CommittedNotOverwritten
+SYMMETRY ProposerAcceptorSymmetry
+CHECK_DEADLOCK FALSE
+