Adjust the probabilities based on empirical data to achieve less unev…

…en coverage of the action space during simulation (#6562) Signed-off-by: Markus Alexander Kuppe <[email protected]> Co-authored-by: Amaury Chamayou <[email protected]>
microsoft · Oct 15, 2024 · 999ce8f · 999ce8f
1 parent dae8c25
commit 999ce8f
Show file tree

Hide file tree

Showing 5 changed files with 69 additions and 131 deletions.
diff --git a/tla/consensus/SIMCoverageccfraft.R b/tla/consensus/SIMCoverageccfraft.R
diff --git a/tla/consensus/SIMCoverageccfraft.cfg b/tla/consensus/SIMCoverageccfraft.cfg
diff --git a/tla/consensus/SIMCoverageccfraft.tla b/tla/consensus/SIMCoverageccfraft.tla
@@ -1,65 +1,40 @@
----------- MODULE SIMCoverageccfraft ----------
-EXTENDS ccfraft, TLC, Integers, CSV, TLCExt
 
-CONSTANTS
-    NodeOne, NodeTwo, NodeThree, NodeFour, NodeFive
+  $ wget https://nightly.tlapl.us/dist/tla2tools.jar
+  $ wget https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar
+  ## Run with as many workers as you like to parallelize the nested simulation runs (auto uses all your cores).
+  $ java -jar tla2tools.jar -config SIMCoverageccfraft.tla SIMCoverageccfraft.tla -workers auto
 
-Servers_mc == {NodeOne, NodeTwo, NodeThree, NodeFour, NodeFive}
+----------------------------- MODULE SIMCoverageccfraft -----------------------------
+EXTENDS TLC, Naturals, Sequences, IOUtils
 
-Baseline ==
-    {<<"Next", 0..0, 0..0, 0..0>>}
+CmdLine ==
+    <<"sh", "-c",
+    "java " \o
+    "-XX:+UseParallelGC " \o
+    "-Dtlc2.tool.impl.Tool.cdot=true " \o
+    "-Dtlc2.tool.Simulator.extendedStatistics=true " \o
+    "-jar tla2tools.jar " \o
+    "-depth 1000 " \o
+    "-simulate SIMccfraft.tla >> SIMCoverageccfraft.txt 2>&1">>
 
-Confs == 
-    Baseline \cup
-        ({"SIMNext"} \X {1..1, 1..10, 1..100} \X {201..201, 201..210, 201..300} \X {401..401, 401..410, 401..500})
+-----------------------------------------------------------------------------
 
-VARIABLE conf
+VARIABLE c, d
 
-CCF == INSTANCE ccfraft
+Init ==
+    /\ c \in [ R: {10, 1000}, C: {10, 1000}, Q: {10, 1000}, T: {10, 1000} ]
+    /\ d = FALSE
 
-SIMInitReconfigurationVars == 
-    \/ CCF!InitLogConfigServerVars(Servers, JoinedLog)
-    \/ CCF!InitReconfigurationVars
+Next ==
+    /\ ~d
+    /\ d' = TRUE
+    /\ PrintT(<<"conf", c>>)
+    /\ IOEnvExec(c, CmdLine).exitValue = 0
+    /\ UNCHANGED c
 
-SIMCheckQuorum(i) ==
-    /\ conf[1] # "Next" => RandomElement(1..1000) \in conf[3]
-    /\ CCF!CheckQuorum(i)
-
-SIMChangeConfigurationInt(i, newConfiguration) ==
-    /\ conf[1] # "Next" => RandomElement(1..1000) \in conf[4]
-    /\ CCF!ChangeConfigurationInt(i, newConfiguration)
-
-SIMTimeout(i) ==
-    /\ \/ RandomElement(1..1000) \in conf[2]
-       \/ conf[1] # "Next"
-       \* Always allow Timeout if no messages are in the network
-       \* and no node is a candidate or leader.  Otherwise, the system
-       \* will deadlock if 1 # RandomElement(...).
-       \/ /\ \A s \in Servers: leadershipState[s] \notin {Leader, Candidate}
-          /\ Network!Messages = {}
-    /\ CCF!Timeout(i)
-
-SIMCoverageSpec ==
-    /\ Init
-    /\ conf \in Confs
-    /\ [][UNCHANGED conf /\ Next]_<<vars, conf>>
-
-------------------------------------------------------------------------------
-
-CSVFile == "SIMCoverageccfraft_S" \o ToString(Cardinality(Servers)) \o ".csv"
-
-CSVColumnHeaders ==
-    "Spec#P#Q#R#currentTerm#state#commitIndex#log#node"
-
-ASSUME
-    CSVRecords(CSVFile) = 0 => 
-        CSVWrite(CSVColumnHeaders, <<>>, CSVFile)
-
-StatisticsStateConstraint ==
-    (TLCGet("level") > TLCGet("config").depth) =>
-        TLCDefer(\A s \in Servers : CSVWrite("%1$s#%2$s#%3$s#%4$s#%5$s#%6$s#%7$s#%8$s#%9$s",
-                << conf[1], Cardinality(conf[2]), Cardinality(conf[3]), Cardinality(conf[4]), 
-                   currentTerm[s], leadershipState[s], commitIndex[s], Len(log[s]), s
-                   >>,
-                CSVFile))
 =============================================================================
+---- CONFIG SIMCoverageccfraft ----
+INIT Init
+NEXT Next
+CHECK_DEADLOCK FALSE
+====
diff --git a/tla/consensus/SIMccfraft.cfg b/tla/consensus/SIMccfraft.cfg
@@ -42,6 +42,7 @@ CONSTANTS
     Timeout <- SIMTimeout
     ChangeConfigurationInt <-SIMChangeConfigurationInt
     CheckQuorum <- SIMCheckQuorum
+    ClientRequest <- SIMClientRequest
 
     Fairness <- SIMFairness
 
@@ -50,8 +51,8 @@ CONSTANTS
     Extend <- [abs]ABSExtend
     CopyMaxAndExtend <- [abs]ABSCopyMaxAndExtend
 
-CONSTRAINT
-    StopAfter
+_PERIODIC
+    Periodically
 
 CHECK_DEADLOCK
     FALSE

diff --git a/tla/consensus/SIMccfraft.tla b/tla/consensus/SIMccfraft.tla
@@ -1,5 +1,5 @@
 ---------- MODULE SIMccfraft ----------
-EXTENDS ccfraft, TLC, Integers, IOUtils, MCAliases
+EXTENDS ccfraft, TLC, Integers, IOUtils
 
 CONSTANTS
     NodeOne, NodeTwo, NodeThree, NodeFour, NodeFive
@@ -16,16 +16,32 @@ SIMInitReconfigurationVars ==
     \* Start with any subset of servers in the active configuration.
     \/ CCF!InitReconfigurationVars
 
+LOCAL R ==
+    1..IF "R" \in DOMAIN IOEnv THEN atoi(IOEnv.R) ELSE 10
+
+SIMClientRequest(i) ==
+    /\ 1 = RandomElement(R)
+    /\ CCF!ClientRequest(i)
+
+LOCAL Q ==
+    1..IF "Q" \in DOMAIN IOEnv THEN atoi(IOEnv.Q) ELSE 10
+
 SIMCheckQuorum(i) ==
-    /\ 1 = RandomElement(1..10)
+    /\ 1 = RandomElement(Q)
     /\ CCF!CheckQuorum(i)
 
+LOCAL C ==
+    1..IF "C" \in DOMAIN IOEnv THEN atoi(IOEnv.C) ELSE 10
+
 SIMChangeConfigurationInt(i, newConfiguration) ==
-    /\ 1 = RandomElement(1..100)
+    /\ 1 = RandomElement(C)
     /\ CCF!ChangeConfigurationInt(i, newConfiguration)
 
+LOCAL T ==
+    1..IF "T" \in DOMAIN IOEnv THEN atoi(IOEnv.T) ELSE 1000
+
 SIMTimeout(i) ==
-    /\ \/ 1 = RandomElement(1..100)
+    /\ \/ 1 = RandomElement(T)
        \* Always allow Timeout if no messages are in the network
        \* and no node is a candidate or leader.  Otherwise, the system
        \* will deadlock if 1 # RandomElement(...).
@@ -58,13 +74,26 @@ SIMFairness ==
         \E newConfiguration \in SUBSET(Servers) \ {{}}:
             WF_vars(CCF!ChangeConfigurationInt(s, newConfiguration))
 
-\* The state constraint  StopAfter  stops TLC after the alloted
+----
+
+\* StopAfter  stops TLC after the alloted
 \* time budget is up, unless TLC encounters an error first.
 StopAfter ==
     LET timeout == IF ("SIM_TIMEOUT" \in DOMAIN IOEnv) /\ IOEnv.SIM_TIMEOUT # "" THEN atoi(IOEnv.SIM_TIMEOUT) ELSE 1200
-    (* The smoke test has a time budget of 20 minutes. *)
     IN TLCSet("exit", TLCGet("duration") > timeout)
 
+SerializeFilename ==
+    "SIMccfraft_" \o "R-" \o ToString(R) \o "_T-" \o ToString(T) \o "_Q-" \o ToString(Q) \o "_C-" \o ToString(C) \o "_ts-" \o ToString(JavaTime) \o ".ndjson"
+
+SerializeTLCStats ==
+    Serialize(<<TLCGet("stats")>>, SerializeFilename, [format |-> "NDJSON", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "APPEND">>])
+
+Periodically ==
+    /\ StopAfter
+    /\ SerializeTLCStats
+
+----
+
 DebugInvUpToDepth ==
     \* The following invariant causes TLC to terminate with a counterexample of length
     \* -depth after generating the first trace.