WIP

.azure-pipelines-templates/model_checking.yml

@@ -34,12 +34,12 @@ jobs:
         displayName: MCccfraftWithReconfig.cfg
         condition: ne(variables['Build.CronSchedule.DisplayName'], 'Daily build')
 
-      - script: ./tlc.sh -workers auto -config consensus/MCccfraftAtomicReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftAtomicReconfig.trace.tla -dumpTrace json MCccfraftAtomicReconfig.json -coverage 1 -nowarning
+      - script: JVM_OPTIONS=-Dtlc2.TLCGlobals.coverage=3 ./tlc.sh -workers auto -config consensus/MCccfraftAtomicReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftAtomicReconfig.trace.tla -dumpTrace json MCccfraftAtomicReconfig.json -nowarning
         workingDirectory: tla
         displayName: MCccfraftAtomicReconfig.cfg
         condition: eq(variables['Build.CronSchedule.DisplayName'], 'Daily build')
 
-      - script: ./tlc.sh -workers auto -config consensus/MCccfraftWithReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftWithReconfig.trace.tla -dumpTrace json MCccfraftWithReconfig.json -coverage 1 -nowarning
+      - script: JVM_OPTIONS=-Dtlc2.TLCGlobals.coverage=3 ./tlc.sh -workers auto -config consensus/MCccfraftWithReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftWithReconfig.trace.tla -dumpTrace json MCccfraftWithReconfig.json -nowarning
         workingDirectory: tla
         displayName: MCccfraftWithReconfig.cfg
         condition: eq(variables['Build.CronSchedule.DisplayName'], 'Daily build')
@@ -49,10 +49,10 @@ jobs:
           python3 -mvenv env
           source env/bin/activate
           pip install -r requirements.txt
-          ls -tr MCccfraftAtomicReconfig_coverage_*.json | xargs cat | python3 actions.py MCccfraftAtomicReconfig.html
-          rm MCccfraftAtomicReconfig_coverage_*.json
-          ls -tr MCccfraftWithReconfig_coverage_*.json | xargs cat | python3 actions.py MCccfraftWithReconfig.html
-          rm MCccfraftWithReconfig_coverage_*.json
+          ls -tr MCccfraftAtomicReconfig_coverage.json | xargs cat | python3 actions.py MCccfraftAtomicReconfig.html
+          rm MCccfraftAtomicReconfig_coverage.json
+          ls -tr MCccfraftWithReconfig_coverage.json | xargs cat | python3 actions.py MCccfraftWithReconfig.html
+          rm MCccfraftWithReconfig_coverage.json
           deactivate
           rm -rf env
         workingDirectory: tla

tla/StatsFile.tla

@@ -1,13 +1,13 @@
 ---- MODULE StatsFile----
-EXTENDS TLC, Json, Sequences, Naturals
+EXTENDS TLC, Json, Sequences, Naturals, IOUtils
 
 \* Filename to write TLC stats to
 CONSTANT StatsFilename
 ASSUME StatsFilename \in STRING
 
 \* Filename to write TLC coverage to
-CONSTANT CoverageFilenamePrefix
-ASSUME CoverageFilenamePrefix \in STRING
+CONSTANT CoverageFilename
+ASSUME CoverageFilename \in STRING
 
 
 \* Writes TLC stats (such as number of states and duration) to StatsFilename in ndJson format
@@ -16,9 +16,11 @@ WriteStatsFile ==
     /\ PrintT("Writing stats to file: " \o StatsFilename)
     /\ ndJsonSerialize(StatsFilename, <<TLCGet("stats")>>)
 
-\* Writes TLC coverage to CoverageFilenamePrefix_coverage_*.json in ndJson format
+\* Append TLC coverage in ndJson format to file identified by CoverageFilename.  Create CoverageFilename if it does not exist.
 SerialiseCoverageConstraint ==
     LET interval == 500000
-    IN IF TLCGet("distinct") % interval = 0 THEN ndJsonSerialize(CoverageFilenamePrefix \o "_coverage_" \o ToString(TLCGet("distinct") \div interval) \o ".json", <<TLCGet("spec")>>) ELSE TRUE
+    IN IF TLCGet("distinct") % interval = 0 
+       THEN Serialize(<<TLCGet("spec")>>, CoverageFilename, [format |-> "NDJSON", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "APPEND">>])
+       ELSE TRUE
 
-====
+====

tla/actions.py

@@ -11,14 +11,16 @@
 """
 A little script to plot TLC action count
 
-Run TLC with -coverage 1 (or higher), and pip the input in, e.g.:
+Run TLC with -Dtlc2.TLCGlobals.coverage=3, and pip the input in, e.g.:
 ls -tr <spec>_coverage_*.json | xargs cat | python3 actions.py
 
 The spec needs to have constraint like:
 
 SerialiseCoverageConstraint ==
     LET interval == 100000
-    IN IF TLCGet("distinct") % interval = 0 THEN ndJsonSerialize("MCccfraftAtomicReconfig_coverage_" \o ToString(TLCGet("distinct") \div interval) \o ".json", <<TLCGet("spec")>>) ELSE TRUE
+    IN IF TLCGet("distinct") % interval = 0 
+       THEN Serialize(<<TLCGet("spec")>>, CoverageFilename, [format |-> "NDJSON", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "APPEND">>])
+       ELSE TRUE
 """
 
 TOP=5

tla/consensus/MCccfraft.cfg

@@ -8,7 +8,7 @@ CONSTANTS
     RequestLimit = 3
 
     StatsFilename = "MCccfraft_stats.json"
-    CoverageFilenamePrefix = "MCccfraft"
+    CoverageFilename = "MCccfraft_coverage.json"
 
     Timeout <- MCTimeout
     Send <- MCSend

tla/consensus/MCccfraftAtomicReconfig.cfg

@@ -8,7 +8,7 @@ CONSTANTS
     RequestLimit = 1
 
     StatsFilename = "MCccfraftAtomicReconfig_stats.json"
-    CoverageFilenamePrefix = "MCccfraftAtomicReconfig"
+    CoverageFilename = "MCccfraftAtomicReconfig_coverage.json"
 
     Timeout <- MCTimeout
     Send <- MCSend

tla/consensus/MCccfraftWithReconfig.cfg

@@ -8,7 +8,7 @@ CONSTANTS
     RequestLimit = 1
 
     StatsFilename = "MCccfraftWithReconfig_stats.json"
-    CoverageFilenamePrefix = "MCccfraftWithReconfig"
+    CoverageFilename = "MCccfraftWithReconfig_coverage.json"
 
     Timeout <- MCTimeout
     Send <- MCSend

tla/consensus/SIMccfraft.cfg

@@ -40,7 +40,7 @@ CONSTANTS
     NodeFive = n5
 
     StatsFilename = "SIMccfraft_stats.json"
-    CoverageFilenamePrefix = "SIMccraft"
+    CoverageFilename = "SIMccraft_coverage.json"
 
     Timeout <- SIMTimeout
     ChangeConfigurationInt <-SIMChangeConfigurationInt