Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

TLC model check .cfg file #3

Merged
merged 2 commits into from
Jun 20, 2024
Merged

TLC model check .cfg file #3

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
7b0516d
TLC model checking cfg
ybbh Jun 20, 2024
897c8a9
Merge branch 'scuptio:main' into main
ybbh Jun 20, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
74 changes: 74 additions & 0 deletions spec/model_check/Model_1n/MC.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
91 changes: 91 additions & 0 deletions spec/model_check/Model_1n/MC.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
2 changes: 1 addition & 1 deletion spec/raft.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down