search

tlaplus / Examples

A collection of TLA⁺ specifications of varying complexities
Other
1.29k stars 200 forks source link

Record state count info in manifest, check during CI #122

Closed ahelwer closed 8 months ago

ahelwer commented 8 months ago

Quite nice having this data in the manifest actually, there are some interesting numbers in there especially with regard to state depth. Record but temporarily disable state depth/diameter check due to https://github.com/tlaplus/tlaplus/issues/883 Closes #120 Also deactivate macOS CI, ref #119

ahelwer commented 8 months ago

@lemmy is it possible for state depth to vary nondeterministically with TLC or should it always be the same? From the latest CI run:

Both Windows & Linux:

INFO:root:specifications\Paxos\MCVoting.cfg
INFO:root:specifications\Paxos\MCVoting.cfg in 1.7s vs. 1s expected
ERROR:root:Error: recorded state count info differed from actual state counts:
ERROR:root:(distinct/total/depth); expected: (77, 451, 12), actual: (77, 451, 11)

Only Windows (check matches on Linux):

INFO:root:specifications\glowingRaccoon\clean.cfg
INFO:root:specifications\glowingRaccoon\clean.cfg in 1.2s vs. 1s expected
ERROR:root:Error: recorded state count info differed from actual state counts:
ERROR:root:(distinct/total/depth); expected: (63, 99, 10), actual: (63, 99, 12)

specifications\SpanningTree\SpanTreeRandom.cfg of course won't have a deterministic number of states due to its use of the Random module so I'll have to figure out a way to incorporate that.

Edit: on thinking about it I suspect it is normal for the state depth to vary as in multithreaded TLC a state that could be 12 steps away from the initial state could be discovered earlier or later by a different thread only 10 steps away from the initial state. So I don't think I should record state depth.

lemmy commented 8 months ago

Where do I find TLC's output?

ahelwer commented 8 months ago

It is printed out in the CI; here it is for MCVoting.cfg:

TLC2 Version 2.18 of Day Month 20?? (rev: 2576f2c)
Running breadth-first search Model-Checking with fp 65 and seed -7659071396622026425 with 4 workers on 4 cores with 3641MB heap and 64MB offheap memory [pid: 1444] (Windows Server 2022 10.0 amd64, Eclipse Adoptium 17.0.10 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file D:\a\Examples\Examples\specifications\Paxos\MCVoting.tla
Parsing file D:\a\Examples\Examples\specifications\Paxos\Voting.tla
Parsing file C:\Users\runneradmin\AppData\Local\Temp\tlc-10456697468897371051\TLC.tla (jar:file:/D:/a/Examples/Examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file C:\Users\runneradmin\AppData\Local\Temp\tlc-10456697468897371051\_TLCTrace.tla (jar:file:/D:/a/Examples/Examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/_TLCTrace.tla)
Parsing file C:\Users\runneradmin\AppData\Local\Temp\tlc-10456697468897371051\Integers.tla (jar:file:/D:/a/Examples/Examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file C:\Users\runneradmin\AppData\Local\Temp\tlc-10456697468897371051\TLAPS.tla (file:/D:/a/Examples/Examples/deps/tlapm/library/TLAPS.tla)
Parsing file C:\Users\runneradmin\AppData\Local\Temp\tlc-10456697468897371051\Naturals.tla (jar:file:/D:/a/Examples/Examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file D:\a\Examples\Examples\specifications\Paxos\Consensus.tla
Parsing file C:\Users\runneradmin\AppData\Local\Temp\tlc-10456697468897371051\FiniteSets.tla (jar:file:/D:/a/Examples/Examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file C:\Users\runneradmin\AppData\Local\Temp\tlc-10456697468897371051\FiniteSetTheorems.tla (file:/D:/a/Examples/Examples/deps/tlapm/library/FiniteSetTheorems.tla)
Parsing file C:\Users\runneradmin\AppData\Local\Temp\tlc-10456697468897371051\Functions.tla (jar:file:/D:/a/Examples/Examples/deps/community/modules.jar!/Functions.tla)
Parsing file C:\Users\runneradmin\AppData\Local\Temp\tlc-10456697468897371051\WellFoundedInduction.tla (file:/D:/a/Examples/Examples/deps/tlapm/library/WellFoundedInduction.tla)
Parsing file C:\Users\runneradmin\AppData\Local\Temp\tlc-10456697468897371051\NaturalsInduction.tla (file:/D:/a/Examples/Examples/deps/tlapm/library/NaturalsInduction.tla)
Parsing file C:\Users\runneradmin\AppData\Local\Temp\tlc-10456697468897371051\Sequences.tla (jar:file:/D:/a/Examples/Examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file C:\Users\runneradmin\AppData\Local\Temp\tlc-10456697468897371051\Folds.tla (jar:file:/D:/a/Examples/Examples/deps/community/modules.jar!/Folds.tla)
Parsing file C:\Users\runneradmin\AppData\Local\Temp\tlc-10456697468897371051\TLCExt.tla (jar:file:/D:/a/Examples/Examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/TLCExt.tla)
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module TLAPS
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module Folds
Semantic processing of module Functions
Semantic processing of module NaturalsInduction
Semantic processing of module WellFoundedInduction
Semantic processing of module FiniteSetTheorems
Semantic processing of module Consensus
Semantic processing of module Voting
Semantic processing of module TLC
Semantic processing of module TLCExt
Semantic processing of module _TLCTrace
Semantic processing of module MCVoting
Starting... (2024-02-21 21:07:57)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2024-02-21 21:07:57.
Model checking completed. No error has been found.
  Estimates of the probability that TLC did not check all reachable states
  because two distinct states had the same fingerprint:
  calculated (optimistic):  val = 1.6E-15
451 states generated, 77 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 11.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 5 and the 95th percentile is 4).
Finished in 01s at (2024-02-21 21:07:57)

Here it is for glowingRaccoon/clean.cfg:

TLC2 Version 2.18 of Day Month 20?? (rev: 2576f2c)
Running breadth-first search Model-Checking with fp 4 and seed -7826053100054716445 with 4 workers on 4 cores with 3641MB heap and 64MB offheap memory [pid: 2432] (Windows Server 2022 10.0 amd64, Eclipse Adoptium 17.0.10 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file D:\a\Examples\Examples\specifications\glowingRaccoon\clean.tla
Parsing file C:\Users\runneradmin\AppData\Local\Temp\tlc-13607610376821900184\Naturals.tla (jar:file:/D:/a/Examples/Examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file C:\Users\runneradmin\AppData\Local\Temp\tlc-13607610376821900184\_TLCTrace.tla (jar:file:/D:/a/Examples/Examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/_TLCTrace.tla)
Parsing file C:\Users\runneradmin\AppData\Local\Temp\tlc-13607610376821900184\TLC.tla (jar:file:/D:/a/Examples/Examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file C:\Users\runneradmin\AppData\Local\Temp\tlc-13607610376821900184\TLCExt.tla (jar:file:/D:/a/Examples/Examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/TLCExt.tla)
Parsing file C:\Users\runneradmin\AppData\Local\Temp\tlc-13607610376821900184\Sequences.tla (jar:file:/D:/a/Examples/Examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file C:\Users\runneradmin\AppData\Local\Temp\tlc-13607610376821900184\FiniteSets.tla (jar:file:/D:/a/Examples/Examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file C:\Users\runneradmin\AppData\Local\Temp\tlc-13607610376821900184\Integers.tla (jar:file:/D:/a/Examples/Examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module Integers
Semantic processing of module TLCExt
Semantic processing of module _TLCTrace
Semantic processing of module clean
Starting... (2024-02-21 21:09:23)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2024-02-21 21:09:23.
Model checking completed. No error has been found.
  Estimates of the probability that TLC did not check all reachable states
  because two distinct states had the same fingerprint:
  calculated (optimistic):  val = 1.2E-16
99 states generated, 63 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 12.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 5 and the 95th percentile is 4).
Finished in 00s at (2024-02-21 21:09:23)

I derived all the state numbers on my local workstation using TLC2 Version 2.18 of Day Month 20?? (rev: 6849026)

lemmy commented 8 months ago

The diameter should be deterministic:

https://github.com/tlaplus/tlaplus/blob/2576f2c1bf7110a8a0747b7e8f6dcddf59ca5904/tlatools/org.lamport.tlatools/src/tlc2/tool/ConcurrentTLCTrace.java#L75-L80

https://github.com/tlaplus/tlaplus/blob/2576f2c1bf7110a8a0747b7e8f6dcddf59ca5904/tlatools/org.lamport.tlatools/src/tlc2/tool/Worker.java#L62