diff --git a/spec/model_check/Model_1n/MC.cfg b/spec/model_check/Model_1n/MC.cfg new file mode 100644 index 0000000..edb069d --- /dev/null +++ b/spec/model_check/Model_1n/MC.cfg @@ -0,0 +1,74 @@ +\* MV CONSTANT declarations +CONSTANTS +A_v1 = A_v1 +\* MV CONSTANT declarations +CONSTANTS +A_n1 = A_n1 +\* CONSTANT declarations +CONSTANT NULL = NULL +\* MV CONSTANT definitions + +CONSTANT + VALUE <- const_1718865728589375000 +\* MV CONSTANT definitions + +CONSTANT + NODE_ID <- const_1718865728589376000 +\* CONSTANT definitions + +CONSTANT + RESTART <- const_1718865728589377000 +\* CONSTANT definitions + +CONSTANT + MAX_TERM <- const_1718865728589378000 +\* CONSTANT definitions + +CONSTANT + DB_INIT_STATE_PATH <- const_1718865728589379000 +\* CONSTANT definitions + +CONSTANT + ENABLE_ACTION <- const_1718865728589380000 +\* CONSTANT definitions + +CONSTANT + APPEND_ENTRIES_MAX <- const_1718865728589381000 +\* CONSTANT definitions + +CONSTANT + CHECK_SAFETY <- const_1718865728589382000 +\* CONSTANT definitions + +CONSTANT + DB_SAVE_STATE_PATH <- const_1718865728589383000 +\* CONSTANT definitions + +CONSTANT + RECONFIG <- const_1718865728589384000 +\* CONSTANT definitions + +CONSTANT + REPLICATE <- const_1718865728589385000 +\* CONSTANT definitions + +CONSTANT + DB_ACTION_PATH <- const_1718865728589386000 +\* CONSTANT definitions + +CONSTANT + VOTE <- const_1718865728589387000 +\* CONSTANT definitions + +CONSTANT + CLIENT_REQUEST <- const_1718865728589388000 +\* VIEW definition +VIEW +view_1718865728589389000 +\* SPECIFICATION definition +SPECIFICATION +Spec +\* INVARIANT definition +INVARIANT +SaveActions +\* Generated on Thu Jun 20 14:42:08 CST 2024 \ No newline at end of file diff --git a/spec/model_check/Model_1n/MC.tla b/spec/model_check/Model_1n/MC.tla new file mode 100644 index 0000000..310d4f7 --- /dev/null +++ b/spec/model_check/Model_1n/MC.tla @@ -0,0 +1,91 @@ +---- MODULE MC ---- +EXTENDS raft, TLC + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +A_v1 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +A_n1 +---- + +\* MV CONSTANT definitions VALUE +const_1718865728589375000 == +{A_v1} +---- + +\* MV CONSTANT definitions NODE_ID +const_1718865728589376000 == +{A_n1} +---- + +\* CONSTANT definitions @modelParameterConstants:0RESTART +const_1718865728589377000 == +3 +---- + +\* CONSTANT definitions @modelParameterConstants:1MAX_TERM +const_1718865728589378000 == +3 +---- + +\* CONSTANT definitions @modelParameterConstants:2DB_INIT_STATE_PATH +const_1718865728589379000 == +"" +---- + +\* CONSTANT definitions @modelParameterConstants:4ENABLE_ACTION +const_1718865728589380000 == +TRUE +---- + +\* CONSTANT definitions @modelParameterConstants:5APPEND_ENTRIES_MAX +const_1718865728589381000 == +3 +---- + +\* CONSTANT definitions @modelParameterConstants:6CHECK_SAFETY +const_1718865728589382000 == +FALSE +---- + +\* CONSTANT definitions @modelParameterConstants:8DB_SAVE_STATE_PATH +const_1718865728589383000 == +"" +---- + +\* CONSTANT definitions @modelParameterConstants:9RECONFIG +const_1718865728589384000 == +3 +---- + +\* CONSTANT definitions @modelParameterConstants:11REPLICATE +const_1718865728589385000 == +3 +---- + +\* CONSTANT definitions @modelParameterConstants:12DB_ACTION_PATH +const_1718865728589386000 == +"/root/workspace/scupt-raft/spec/model_check/Model_1n/action.db" +---- + +\* CONSTANT definitions @modelParameterConstants:13VOTE +const_1718865728589387000 == +2 +---- + +\* CONSTANT definitions @modelParameterConstants:14CLIENT_REQUEST +const_1718865728589388000 == +2 +---- + +\* VIEW definition @modelParameterView +view_1718865728589389000 == +vars_view +---- + +============================================================================= +\* Modification History +\* Created Thu Jun 20 14:42:08 CST 2024 by ybbh diff --git a/spec/raft.tla b/spec/raft.tla index 7e460f1..78fc9c7 100644 --- a/spec/raft.tla +++ b/spec/raft.tla @@ -1241,7 +1241,7 @@ ClientRequest(nid, v , _node_id_set, _check_safety, _enable_action) == actions1 == ActionCheckState(nid) actions2 == Action(ActionInput, Message(nid, nid, __ActionClientRequest, v)) IN SetAction(__action__, actions0, actions1 \o actions2, _enable_action) - /\ IF NODE_ID = {nid} THEN + /\ IF v_conf_committed[nid].nid_vote \cup v_conf_new[nid].nid_vote = {nid} THEN _HandleAdvanceCommitIndex(v_follower_match_index, v_log', v_snapshot, v_conf_committed, v_conf_new, nid, _node_id_set, _check_safety)