From 43ae605c633c43267c42c784eb08ef6f743a40ed Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 25 Mar 2024 14:25:12 -0700 Subject: [PATCH] WIP --- .azure-pipelines-templates/model_checking.yml | 12 ++++++------ tla/StatsFile.tla | 14 ++++++++------ tla/actions.py | 6 ++++-- tla/consensus/MCccfraft.cfg | 2 +- tla/consensus/MCccfraftAtomicReconfig.cfg | 2 +- tla/consensus/MCccfraftWithReconfig.cfg | 2 +- tla/consensus/SIMccfraft.cfg | 2 +- 7 files changed, 22 insertions(+), 18 deletions(-) diff --git a/.azure-pipelines-templates/model_checking.yml b/.azure-pipelines-templates/model_checking.yml index 5c6909ecaf1b..f10de4a64008 100644 --- a/.azure-pipelines-templates/model_checking.yml +++ b/.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 diff --git a/tla/StatsFile.tla b/tla/StatsFile.tla index 9e143d63a115..20a0ec8494f1 100644 --- a/tla/StatsFile.tla +++ b/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, <>) -\* 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", <>) ELSE TRUE + IN IF TLCGet("distinct") % interval = 0 + THEN Serialize(<>, CoverageFilename, [format |-> "NDJSON", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "APPEND">>]) + ELSE TRUE -==== \ No newline at end of file +==== diff --git a/tla/actions.py b/tla/actions.py index 8319afa15544..a084c89acb8a 100644 --- a/tla/actions.py +++ b/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 _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", <>) ELSE TRUE + IN IF TLCGet("distinct") % interval = 0 + THEN Serialize(<>, CoverageFilename, [format |-> "NDJSON", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "APPEND">>]) + ELSE TRUE """ TOP=5 diff --git a/tla/consensus/MCccfraft.cfg b/tla/consensus/MCccfraft.cfg index dbe823b0050f..bc368753d8f1 100644 --- a/tla/consensus/MCccfraft.cfg +++ b/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 diff --git a/tla/consensus/MCccfraftAtomicReconfig.cfg b/tla/consensus/MCccfraftAtomicReconfig.cfg index 8486ed392ba5..f230a930dc25 100644 --- a/tla/consensus/MCccfraftAtomicReconfig.cfg +++ b/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 diff --git a/tla/consensus/MCccfraftWithReconfig.cfg b/tla/consensus/MCccfraftWithReconfig.cfg index bea306de9bc6..775bbfdce864 100644 --- a/tla/consensus/MCccfraftWithReconfig.cfg +++ b/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 diff --git a/tla/consensus/SIMccfraft.cfg b/tla/consensus/SIMccfraft.cfg index b469e8da2ab7..626185ff694b 100644 --- a/tla/consensus/SIMccfraft.cfg +++ b/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