SPIN TLA+ specification

.vscode/settings.json

@@ -0,0 +1,8 @@
+{
+    "tlaplus.tlc.modelChecker.options": "-dump dot,colorize ${modelName}.dot -deadlock",
+    "[tlaplus]": {
+        "editor.codeActionsOnSave": {
+            "source": "explicit"
+        }
+    }
+}

tla/.gitignore

@@ -0,0 +1,53 @@
+## Ignore all files by default
+*
+
+## Don't ignore TLA+ files
+!*.tla
+
+## Don't ignore TLC model config and results
+!*.cfg
+!*.out  ## Usually .out files are small
+
+## Don't ignore Toolbox model metadata
+!*.launch
+
+## Don't ignore Toolbox spec metadata
+!.project
+!*.prefs
+
+## Don't ignore PDFs
+!*.pdf
+
+## Don't ignore all folders
+!*/
+
+## Ignore TLAPS cache folder
+## See https://github.com/tlaplus/tlapm/issues/16
+__tlacache__
+.tlacache
+
+## Don't ignore CI files
+!.github/**
+
+## Don't ignore READMEs
+!*.md
+
+## Ignore Python artifacts
+__pycache__
+pyvenv.cfg
+
+## Ignore directories used for local CI testing
+deps/
+tree-sitter-tlaplus/
+
+# Ignore TTrace specs
+*_TTrace_*.tla
+
+## Ignore tools/ folder created by .devcontainer.json
+tools/
+
+# Ignore directory created by Apalache
+_apalache-out
+
+## Don't ignore Graphviz files
+!*.dot

tla/spin/leader.cfg

@@ -0,0 +1 @@
+SPECIFICATION Spec

tla/spin/leader.dot

@@ -0,0 +1,77 @@
+strict digraph DiskGraph {
+node [shape=box,style=rounded]
+edge [colorscheme="paired12"]
+nodesep=0.35;
+subgraph cluster_graph {
+color="white";
+-2129222505383092032 [label="alive = {\"v1\", \"v2\", \"v3\", \"v4\", \"v5\"}",style = filled]
+-2129222505383092032 -> -2123624603493679006 [label="",color="2",fontcolor="2"];
+-2123624603493679006 [label="alive = {\"v2\", \"v3\", \"v4\", \"v5\"}",tooltip="alive = {\"v2\", \"v3\", \"v4\", \"v5\"}"];
+-2129222505383092032 -> -7765162563257140054 [label="",color="2",fontcolor="2"];
+-7765162563257140054 [label="alive = {\"v1\", \"v3\", \"v4\", \"v5\"}",tooltip="alive = {\"v1\", \"v3\", \"v4\", \"v5\"}"];
+-2129222505383092032 -> 6588154810387299395 [label="",color="2",fontcolor="2"];
+6588154810387299395 [label="alive = {\"v1\", \"v2\", \"v4\", \"v5\"}",tooltip="alive = {\"v1\", \"v2\", \"v4\", \"v5\"}"];
+-2129222505383092032 -> 2345315966805697744 [label="",color="2",fontcolor="2"];
+2345315966805697744 [label="alive = {\"v1\", \"v2\", \"v3\", \"v5\"}",tooltip="alive = {\"v1\", \"v2\", \"v3\", \"v5\"}"];
+-2129222505383092032 -> -6191826570015327651 [label="",color="2",fontcolor="2"];
+-6191826570015327651 [label="alive = {\"v1\", \"v2\", \"v3\", \"v4\"}",tooltip="alive = {\"v1\", \"v2\", \"v3\", \"v4\"}"];
+-2123624603493679006 -> -2129222505383092032 [label="",color="2",fontcolor="2"];
+-2123624603493679006 -> 1712824352354559804 [label="",color="2",fontcolor="2"];
+1712824352354559804 [label="alive = {\"v3\", \"v4\", \"v5\"}",tooltip="alive = {\"v3\", \"v4\", \"v5\"}"];
+-2123624603493679006 -> -2840532753157167147 [label="",color="2",fontcolor="2"];
+-2840532753157167147 [label="alive = {\"v2\", \"v4\", \"v5\"}",tooltip="alive = {\"v2\", \"v4\", \"v5\"}"];
+-2123624603493679006 -> -6668272953674727610 [label="",color="2",fontcolor="2"];
+-6668272953674727610 [label="alive = {\"v2\", \"v3\", \"v5\"}",tooltip="alive = {\"v2\", \"v3\", \"v5\"}"];
+-2123624603493679006 -> 3020653026633785803 [label="",color="2",fontcolor="2"];
+3020653026633785803 [label="alive = {\"v2\", \"v3\", \"v4\"}",tooltip="alive = {\"v2\", \"v3\", \"v4\"}"];
+-7765162563257140054 -> 1712824352354559804 [label="",color="2",fontcolor="2"];
+-7765162563257140054 -> -2129222505383092032 [label="",color="2",fontcolor="2"];
+-7765162563257140054 -> -3505999373485863089 [label="",color="2",fontcolor="2"];
+-3505999373485863089 [label="alive = {\"v1\", \"v4\", \"v5\"}",tooltip="alive = {\"v1\", \"v4\", \"v5\"}"];
+-7765162563257140054 -> -5424058312653465636 [label="",color="2",fontcolor="2"];
+-5424058312653465636 [label="alive = {\"v1\", \"v3\", \"v5\"}",tooltip="alive = {\"v1\", \"v3\", \"v5\"}"];
+-7765162563257140054 -> 4478782874851559761 [label="",color="2",fontcolor="2"];
+4478782874851559761 [label="alive = {\"v1\", \"v3\", \"v4\"}",tooltip="alive = {\"v1\", \"v3\", \"v4\"}"];
+6588154810387299395 -> -2840532753157167147 [label="",color="2",fontcolor="2"];
+6588154810387299395 -> -3505999373485863089 [label="",color="2",fontcolor="2"];
+6588154810387299395 -> -2129222505383092032 [label="",color="2",fontcolor="2"];
+6588154810387299395 -> 5205351981436691191 [label="",color="2",fontcolor="2"];
+5205351981436691191 [label="alive = {\"v1\", \"v2\", \"v5\"}",tooltip="alive = {\"v1\", \"v2\", \"v5\"}"];
+6588154810387299395 -> -4421643181276218246 [label="",color="2",fontcolor="2"];
+-4421643181276218246 [label="alive = {\"v1\", \"v2\", \"v4\"}",tooltip="alive = {\"v1\", \"v2\", \"v4\"}"];
+2345315966805697744 -> -6668272953674727610 [label="",color="2",fontcolor="2"];
+2345315966805697744 -> -5424058312653465636 [label="",color="2",fontcolor="2"];
+2345315966805697744 -> 5205351981436691191 [label="",color="2",fontcolor="2"];
+2345315966805697744 -> -2129222505383092032 [label="",color="2",fontcolor="2"];
+2345315966805697744 -> -4811665873115766982 [label="",color="2",fontcolor="2"];
+-4811665873115766982 [label="alive = {\"v1\", \"v2\", \"v3\"}",tooltip="alive = {\"v1\", \"v2\", \"v3\"}"];
+-6191826570015327651 -> 3020653026633785803 [label="",color="2",fontcolor="2"];
+-6191826570015327651 -> 4478782874851559761 [label="",color="2",fontcolor="2"];
+-6191826570015327651 -> -4421643181276218246 [label="",color="2",fontcolor="2"];
+-6191826570015327651 -> -4811665873115766982 [label="",color="2",fontcolor="2"];
+-6191826570015327651 -> -2129222505383092032 [label="",color="2",fontcolor="2"];
+1712824352354559804 -> -7765162563257140054 [label="",color="2",fontcolor="2"];
+1712824352354559804 -> -2123624603493679006 [label="",color="2",fontcolor="2"];
+-2840532753157167147 -> 6588154810387299395 [label="",color="2",fontcolor="2"];
+-2840532753157167147 -> -2123624603493679006 [label="",color="2",fontcolor="2"];
+-6668272953674727610 -> 2345315966805697744 [label="",color="2",fontcolor="2"];
+-6668272953674727610 -> -2123624603493679006 [label="",color="2",fontcolor="2"];
+3020653026633785803 -> -6191826570015327651 [label="",color="2",fontcolor="2"];
+3020653026633785803 -> -2123624603493679006 [label="",color="2",fontcolor="2"];
+-3505999373485863089 -> 6588154810387299395 [label="",color="2",fontcolor="2"];
+-3505999373485863089 -> -7765162563257140054 [label="",color="2",fontcolor="2"];
+-5424058312653465636 -> 2345315966805697744 [label="",color="2",fontcolor="2"];
+-5424058312653465636 -> -7765162563257140054 [label="",color="2",fontcolor="2"];
+4478782874851559761 -> -6191826570015327651 [label="",color="2",fontcolor="2"];
+4478782874851559761 -> -7765162563257140054 [label="",color="2",fontcolor="2"];
+5205351981436691191 -> 2345315966805697744 [label="",color="2",fontcolor="2"];
+5205351981436691191 -> 6588154810387299395 [label="",color="2",fontcolor="2"];
+-4421643181276218246 -> -6191826570015327651 [label="",color="2",fontcolor="2"];
+-4421643181276218246 -> 6588154810387299395 [label="",color="2",fontcolor="2"];
+-4811665873115766982 -> -6191826570015327651 [label="",color="2",fontcolor="2"];
+-4811665873115766982 -> 2345315966805697744 [label="",color="2",fontcolor="2"];
+{rank = same; -2129222505383092032;}
+{rank = same; 6588154810387299395;-2123624603493679006;-7765162563257140054;-6191826570015327651;2345315966805697744;}
+{rank = same; -3505999373485863089;-4811665873115766982;-2840532753157167147;-6668272953674727610;3020653026633785803;4478782874851559761;-4421643181276218246;1712824352354559804;5205351981436691191;-5424058312653465636;}
+}
+}

tla/spin/leader.tla

@@ -0,0 +1,52 @@
+---- MODULE leader ----
+EXTENDS Integers, TLC, FiniteSets
+
+Validators == {"v1", "v2", "v3", "v4", "v5"}
+minimumValidatorCount == 3
+
+(*--algorithm leaders
+variables
+    alive = Validators;
+
+process leader = "leader"
+begin
+    Election:
+        while TRUE do
+            with l \in Validators do
+                either
+                    await l \notin alive;
+                    alive := alive \union {l};
+                or
+                    await l \in alive;
+                    await Cardinality(alive) > minimumValidatorCount;
+                    alive := alive \ {l};
+                end either;
+            end with;
+        end while;
+end process;
+
+end algorithm; *)
+\* BEGIN TRANSLATION (chksum(pcal) = "696cd7bf" /\ chksum(tla) = "c5d75fd8")
+VARIABLE alive
+
+vars == << alive >>
+
+ProcSet == {"leader"}
+
+Init == (* Global variables *)
+        /\ alive = Validators
+
+leader == \E l \in Validators:
+            \/ /\ l \notin alive
+               /\ alive' = (alive \union {l})
+            \/ /\ l \in alive
+               /\ Cardinality(alive) > minimumValidatorCount
+               /\ alive' = alive \ {l}
+
+Next == leader
+
+Spec == Init /\ [][Next]_vars
+
+\* END TRANSLATION 
+
+====

tla/spin/spin.cfg

@@ -0,0 +1,3 @@
+PROPERTY AlwaysValidState
+
+SPECIFICATION Spec

tla/spin/spin.dot

@@ -0,0 +1,23 @@
+strict digraph DiskGraph {
+node [shape=box,style=rounded]
+edge [colorscheme="paired12"]
+nodesep=0.35;
+subgraph cluster_graph {
+color="white";
+-8857019723714639812 [label="state = \"operational\"",style = filled]
+-8857019723714639812 -> 4466091959303920822 [label="",color="2",fontcolor="2"];
+4466091959303920822 [label="state = \"fastChainFinalityProved\"",tooltip="state = \"fastChainFinalityProved\""];
+-8857019723714639812 -> 5376352793141087770 [label="",color="2",fontcolor="2"];
+5376352793141087770 [label="state = \"fastChainFinalityNotProved\"",tooltip="state = \"fastChainFinalityNotProved\""];
+4466091959303920822 -> -8857019723714639812 [label="",color="2",fontcolor="2"];
+5376352793141087770 -> -3097599280067440227 [label="",color="2",fontcolor="2"];
+-3097599280067440227 [label="state = \"recovery\"",tooltip="state = \"recovery\""];
+-3097599280067440227 -> -1367225398818136591 [label="",color="2",fontcolor="2"];
+-1367225398818136591 [label="state = \"recoveryEnded\"",tooltip="state = \"recoveryEnded\""];
+-1367225398818136591 -> -8857019723714639812 [label="",color="2",fontcolor="2"];
+{rank = same; -8857019723714639812;}
+{rank = same; 4466091959303920822;5376352793141087770;}
+{rank = same; -3097599280067440227;}
+{rank = same; -1367225398818136591;}
+}
+}

tla/spin/spin.tla

@@ -0,0 +1,23 @@
+---- MODULE spin ----
+VARIABLE state
+
+ValidState == state \in {"operational", "recovery", "fastChainFinalityProved", "fastChainFinalityNotProved", "recoveryEnded"}
+
+AlwaysValidState == [] ValidState
+
+Init == state = "operational"
+
+Trans(a, b) ==
+    /\ state = a
+    /\ state' = b
+
+Next ==
+    \/ Trans("operational", "fastChainFinalityProved")
+    \/ Trans("operational", "fastChainFinalityNotProved")
+    \/ Trans("fastChainFinalityProved", "operational")
+    \/ Trans("fastChainFinalityNotProved", "recovery")
+    \/ Trans("recovery", "recoveryEnded")
+    \/ Trans("recoveryEnded", "operational")
+
+Spec == Init /\ [][Next]_state
+====