Merge pull request #2 from ybbh/main

TLA+ spec

.gitignore

@@ -15,3 +15,7 @@ Cargo.lock
 
 # gcov
 *.profraw
+
+# TLC model checker
+*.toolbox
+

README.md

@@ -1,9 +1,53 @@
 # scupt-raft
 
-Raft consensus algorithm
+TLA+ verified Raft consensus
 
 ![build](https://github.com/scuptio/scupt-raft/actions/workflows/build.yaml/badge.svg)
 
-## Test Coverage
+
+# Specification Development of Raft
+
+## Prerequisite
+
+1. Download and install TLA+ [toolbox](https://github.com/tlaplus/tlaplus/releases)
+
+2. Download and install [sedeve-kit](https://github.com/scuptio/sedeve-kit.git)
+
+   ```
+   git clone https://github.com/scuptio/sedeve-kit.git
+   cd sedeve-kit
+   cargo install -path .
+   ```
+3. [Configure the TLA+ toolbox](https://github.com/scuptio/sedeve-kit/blob/main/doc/configuring_toolbox.md)
+
+## Run model check
+
+   Model setup, filling constant
+
+   Constant example [MC](data/MC_1n.tla)
+
+   After checking finish, output state database.
+
+## Generate trace of the model
+   Use the state database the toolbox output, generate trace file.
+
+   Example,
+   ```
+   cd scupt-raft
+   sedeve_trace_gen  \
+      --state-db-path /tmp/raft_action.db  \
+      --out-trace-db-path /tmp/raft_trace.db \
+      --map-const-path  ./data/raft_map_const.json
+   ```
+
+   After finish executing, the output trace would be store in database file '/tmp/raft_trace.db'
+
+## Validate by running deterministic testing
+
+   Write test code
+
+   Example [test_raft.rs](src/test_raft_1n.rs)
+
+# Test Coverage
 
 [Test Coverage in Docker](doc/coverage.md)

data/raft_map_const.json

@@ -1,9 +1,11 @@
 {
-  "A_n1": 1,
-  "A_n2": 2,
-  "A_n3": 3,
-  "A_v1": 100,
-  "A_v2": 200,
-  "A_v3": 300,
-  "INVALID_NODE_ID": null
+    "A_n1" : 1,
+    "A_n2" : 2,
+    "A_n3" : 3,
+    "A_n4" : 4,
+    "A_n5" : 5,
+    "A_v1" : 100,
+    "A_v2" : 200,
+    "A_v3" : 300,
+    "NULL": null
 }

spec/GenID.tla

@@ -0,0 +1,23 @@
+------------------------------ MODULE GenID ------------------------------
+
+(*Self increasing ID*)
+
+NextID ==
+  (*************************************************************************)
+  (* Generate a self increasing ID                                         *)
+  (*************************************************************************)
+  CHOOSE val : TRUE
+
+GetID ==
+  (*************************************************************************)
+  (* Get current id                                                        *)
+  (*************************************************************************)
+  CHOOSE val : TRUE
+
+SetID(v) ==
+  (*************************************************************************)
+  (* Set current id                                                        *)
+  (*************************************************************************)
+  TRUE
+
+=============================================================================

spec/StateDB.tla

@@ -0,0 +1,27 @@
+------------------------------ MODULE StateDB ------------------------------
+
+LOCAL INSTANCE TLC
+LOCAL INSTANCE Integers
+  (*************************************************************************)
+  (* Imports the definitions from the modules, but doesn't export them.    *)
+  (*************************************************************************)
+
+
+SaveValue(state, path) ==
+  (*************************************************************************)
+  (* NewState would store state to a give database if it not exist         *)
+  (*************************************************************************)
+  TRUE
+
+QueryAllValues(path) ==
+  (*************************************************************************)
+  (* QueryAllStates would load a set of state from the given database.     *)
+  (*************************************************************************)
+  CHOOSE val : TRUE
+
+FlushAll ==
+  TRUE
+
+
+
+============================================================================

spec/action.tla

@@ -0,0 +1,248 @@
+--------------------------------- MODULE action ---------------------------------
+
+EXTENDS message, GenID, StateDB, Sequences, SequencesExt, FiniteSets, Naturals
+
+
+ActionInternal  ==  "T"
+ActionInput     ==  "I"
+ActionOutput    ==  "O"
+ActionSetup     ==  "S"
+ActionCheck     ==  "C"
+
+
+_Action(
+    _action_type, 
+    _payload
+) == 
+    [
+        t |-> _action_type,
+        p |-> _payload
+    ]
+
+
+Action(
+    _action_type, 
+    _payload
+) == 
+    <<
+        _Action(_action_type, _payload)
+    >>
+
+
+Actions(
+    _action_type,
+    _payload_set
+) ==
+    LET _action_set == [
+        t : {_action_type},
+        p : _payload_set
+    ]
+    IN SetToSeq(_action_set)
+
+
+
+CheckAction(_action, _node_id) ==
+    \A i \in DOMAIN _action:
+        /\ _action[i].t \in {ActionInternal, ActionInput, ActionOutput}
+        /\ _action[i].source \in _node_id
+        /\ _action[i].dest \in _node_id
+
+
+AppendActionSeq(_var, _action_seq) ==
+    _var \o _action_seq
+
+
+AppendActionSet(_var, _action_set) ==
+    _var \o SetToSeq(_action_set)
+
+
+_NodeVariable(
+    _var,
+    _id,
+    _node_ids
+) ==
+    [x \in DOMAIN _var |-> _var[x][_id]]  
+
+_NodeChangedVariable(
+    _old_var, 
+    _new_var,
+    _id,
+    _node_ids
+) ==
+    LET changed == {x \in DOMAIN _old_var: _old_var[x][_id] # _new_var[x][_id]}
+    IN  [x \in changed |-> _new_var[x][_id]]
+
+__ActionSeqOfNode(
+    _handle_node_id(_),
+    _node_id,
+    _action_type,
+    _action_name
+) ==
+    LET payload == _handle_node_id(_node_id)
+        msg == Message(_node_id, _node_id, _action_name, payload)
+        action == _Action(_action_type, msg)
+    IN action
+
+__ActionSeqOfEachNodeHandle(
+    _handle_node_id(_),
+    _node_ids,
+    _action_type,
+    _action_name
+) ==
+    LET f == [id \in _node_ids |-> __ActionSeqOfNode(_handle_node_id, id, _action_type, _action_name)]
+        s == {f[id] : id \in DOMAIN f}
+    IN SetToSeq(s)
+
+
+ActionsFromHandle(
+    _handle_node_id(_),
+    _node_ids,
+    _action_type,
+    _action_name
+) ==
+    __ActionSeqOfEachNodeHandle(
+        _handle_node_id,
+        _node_ids,
+        _action_type,
+        _action_name)
+
+
+__ActionSeqOfNodeEx(
+    _handle_node_id(_, _),
+    _node_id,
+    _action_type,
+    _action_name,
+    _context
+) ==
+    LET payload == _handle_node_id(_node_id, _context)
+        msg == Message(_node_id, _node_id, _action_name, payload)
+        action == _Action(_action_type, msg)
+    IN action
+
+
+__ActionSeqOfEachNodeHandleEx(
+    _handle_node_id(_, _),
+    _node_ids,
+    _action_type,
+    _action_name,
+    _context
+) ==
+    LET f == [id \in _node_ids |-> 
+            __ActionSeqOfNodeEx(
+                _handle_node_id,
+                id,
+                _action_type,
+                _action_name,
+                _context
+                )]
+
+        s == {f[id] : id \in DOMAIN f}
+    IN SetToSeq(s)
+
+
+ActionsFromHandleContext(
+    _handle_node_id(_, _),
+    _node_ids,
+    _action_type,
+    _action_name,
+    _context
+) ==
+    __ActionSeqOfEachNodeHandleEx(
+        _handle_node_id,
+        _node_ids,
+        _action_type,
+        _action_name,
+        _context
+      )
+
+PrevIdOfAction(
+    _action
+) ==
+    _action.p
+
+IdOfAction(
+    _action
+) ==
+    _action.i
+
+
+
+ContinuousAction(
+    _action, 
+    _pc) == 
+    /\ "id" \in DOMAIN _pc
+    /\ _pc.id = PrevIdOfAction(_action)
+
+
+InitAction(
+    _action_sequence1,
+    _action_sequence2,
+    _enable
+) ==
+    IF _enable THEN
+        [
+            p |-> GetID,
+            i |-> NextID,
+            s |-> _action_sequence1,
+            a |-> _action_sequence2 
+        ]
+    ELSE
+       [
+            p |-> GetID,
+            i |-> GetID,
+            s |-> <<>>,
+            a |-> <<>> 
+        ]
+
+
+SetAction(
+    _action_variable,
+    _action_sequence1,
+    _action_sequence2,
+    _enable
+) ==
+    IF _enable THEN
+        _action_variable' = [
+            p |-> _action_variable.i,
+            i |-> NextID,
+            s |-> _action_sequence1,
+            a |-> _action_sequence2 
+        ]
+    ELSE
+        _action_variable' = [
+            p |-> GetID,
+            i |-> GetID,
+            s |-> <<>>,
+            a |-> <<>> 
+        ]
+
+
+InitActionT(
+    _action_variable,
+    _action_sequence1,
+    _action_sequence2
+) ==
+    _action_variable = [
+        p |-> NextID,
+        i |-> NextID,
+        s |-> _action_sequence1,
+        a |-> _action_sequence2 
+    ]
+
+SetActionT(
+    _action_variable,
+    _action_sequence1,
+    _action_sequence2
+) ==
+    _action_variable' = [
+        p |-> _action_variable.i,
+        i |-> NextID,
+        s |-> _action_sequence1,
+        a |-> _action_sequence2 
+    ]
+
+
+
+InitActionEmpty == {}
+
+===============================================================================