[Proof-of-Concept] Liveness checking ccfraft #6587
Draft
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
lemmy
changed the title
* Add FairSpec and InSync property * Comment TypeOK because violated by (non-axiom) Spec (TLC checks invariants even for states that are excluded by a state constraint) The liveness property `InSync` should be violated because the fairness constraint is too weak. However, TLC won't find the violation because of the naive state constraint. ```shell -> % tlc -note MCabs.tla TLC2 Version 2.20 of Day Month 20?? (rev: cc65eef) Running breadth-first search Model-Checking with fp 47 and seed 8464703399013400155 with 1 worker on 10 cores with 7282MB heap and 64MB offheap memory [pid: 58100] (Mac OS X 15.0.1 aarch64, Homebrew 11.0.25 x86_64, MSBDiskFPSet, DiskStateQueue). Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/MCabs.tla Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/abs.tla Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-14783782376297602783/TLC.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/TLC.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-14783782376297602783/SequencesExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/SequencesExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-14783782376297602783/FiniteSetsExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/FiniteSetsExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-14783782376297602783/Sequences.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-14783782376297602783/Naturals.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-14783782376297602783/FiniteSets.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-14783782376297602783/Relation.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Relation.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-14783782376297602783/Folds.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Folds.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-14783782376297602783/Functions.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Functions.tla) Semantic processing of module Naturals Semantic processing of module Sequences Semantic processing of module FiniteSets Semantic processing of module Folds Semantic processing of module Functions Semantic processing of module FiniteSetsExt Semantic processing of module TLC Semantic processing of module SequencesExt Semantic processing of module Relation Semantic processing of module abs Semantic processing of module MCabs Starting... (2024-10-22 17:44:30) Implied-temporal checking--satisfiability problem has 1 branches. Computing initial states... Computed 2 initial states... Computed 4 initial states... Computed 8 initial states... Computed 16 initial states... Finished computing initial states: 27 distinct states generated at 2024-10-22 17:44:30. Checking temporal properties for the current state space with 1698 total distinct states at (2024-10-22 17:44:33) Finished checking temporal properties in 00s at 2024-10-22 17:44:33 Progress(4) at 2024-10-22 17:44:33: 292,065 states generated (292,065 s/min), 33,113 distinct states found (33,113 ds/min), 31,441 states left on queue. Checking temporal properties for the current state space with 69444 total distinct states at (2024-10-22 17:45:33) Finished checking temporal properties in 00s at 2024-10-22 17:45:33 Progress(5) at 2024-10-22 17:45:33: 12,119,265 states generated (11,827,200 s/min), 372,262 distinct states found (339,149 ds/min), 302,817 states left on queue. Checking temporal properties for the current state space with 154698 total distinct states at (2024-10-22 17:46:33) Finished checking temporal properties in 01s at 2024-10-22 17:46:35 Progress(5) at 2024-10-22 17:46:35: 27,220,596 states generated (15,101,331 s/min), 467,752 distinct states found (95,490 ds/min), 313,053 states left on queue. Checking temporal properties for the current state space with 244201 total distinct states at (2024-10-22 17:47:35) Finished checking temporal properties in 02s at 2024-10-22 17:47:38 Progress(5) at 2024-10-22 17:47:38: 42,968,607 states generated (15,748,011 s/min), 487,462 distinct states found (19,710 ds/min), 243,260 states left on queue. Checking temporal properties for the current state space with 345878 total distinct states at (2024-10-22 17:48:38) Finished checking temporal properties in 03s at 2024-10-22 17:48:42 Progress(6) at 2024-10-22 17:48:42: 63,237,877 states generated (20,269,270 s/min), 490,432 distinct states found (2,970 ds/min), 144,553 states left on queue. Checking temporal properties for the current state space with 451165 total distinct states at (2024-10-22 17:49:42) Finished checking temporal properties in 05s at 2024-10-22 17:49:47 Progress(6) at 2024-10-22 17:49:47: 84,563,041 states generated (21,325,164 s/min), 490,432 distinct states found (0 ds/min), 39,266 states left on queue. Progress(6) at 2024-10-22 17:50:16: 94,419,147 states generated, 490,432 distinct states found, 0 states left on queue. Checking temporal properties for the complete state space with 490432 total distinct states at (2024-10-22 17:50:16) Finished checking temporal properties in 05s at 2024-10-22 17:50:22 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 = 2.5E-6 based on the actual fingerprints: val = 2.6E-8 94419147 states generated, 490432 distinct states found, 0 states left on queue. The depth of the complete state graph search is 6. The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 31 and the 95th percentile is 4). Finished in 05min 52s at (2024-10-22 17:50:22) ``` Signed-off-by: Markus Alexander Kuppe <[email protected]>
* Add the MonotonicReduction disjunct to Next that reduces the infinite state space to a finite one As expected, the action property AppendOnlyProp is immediately violated: ```shell -> % tlc -note MCabs.tla TLC2 Version 2.20 of Day Month 20?? (rev: cc65eef) Running breadth-first search Model-Checking with fp 46 and seed 9013274278368943051 with 1 worker on 10 cores with 7282MB heap and 64MB offheap memory [pid: 60575] (Mac OS X 15.0.1 aarch64, Homebrew 11.0.25 x86_64, MSBDiskFPSet, DiskStateQueue). Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/MCabs.tla Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/abs.tla Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-17957423033042532951/TLC.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/TLC.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-17957423033042532951/SequencesExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/SequencesExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-17957423033042532951/FiniteSetsExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/FiniteSetsExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-17957423033042532951/Integers.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Integers.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-17957423033042532951/Sequences.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-17957423033042532951/Naturals.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-17957423033042532951/FiniteSets.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-17957423033042532951/Relation.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Relation.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-17957423033042532951/Folds.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Folds.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-17957423033042532951/Functions.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Functions.tla) Semantic processing of module Naturals Semantic processing of module Sequences Semantic processing of module FiniteSets Semantic processing of module Folds Semantic processing of module Functions Semantic processing of module FiniteSetsExt Semantic processing of module TLC Semantic processing of module SequencesExt Semantic processing of module Relation Semantic processing of module abs Semantic processing of module Integers Semantic processing of module MCabs Starting... (2024-10-22 18:02:23) Implied-temporal checking--satisfiability problem has 1 branches. Computing initial states... Computed 2 initial states... Computed 4 initial states... Computed 8 initial states... Computed 16 initial states... Finished computing initial states: 27 states generated, with 15 of them distinct at 2024-10-22 18:02:23. Error: Action property AppendOnlyProp is violated. Error: The behavior up to this point is: State 1: <Initial predicate> cLogs = (n1 :> <<2, 2>> @@ n2 :> <<2, 2>> @@ n3 :> <<2, 2>>) State 2: <MonotonicReduction line 110, col 9 to line 113, col 21 of module abs> cLogs = (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>>) 2153 states generated, 90 distinct states found, 82 states left on queue. The depth of the complete state graph search is 2. Finished in 00s at (2024-10-22 18:02:23) ``` Signed-off-by: Markus Alexander Kuppe <[email protected]>
```tla -> % tlc -note MCabs.tla TLC2 Version 2.20 of Day Month 20?? (rev: cc65eef) Running breadth-first search Model-Checking with fp 40 and seed 2933531752807036538 with 1 worker on 10 cores with 7282MB heap and 64MB offheap memory [pid: 61862] (Mac OS X 15.0.1 aarch64, Homebrew 11.0.25 x86_64, MSBDiskFPSet, DiskStateQueue). Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/MCabs.tla Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/abs.tla Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13148651527763708847/TLC.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/TLC.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13148651527763708847/SequencesExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/SequencesExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13148651527763708847/FiniteSetsExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/FiniteSetsExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13148651527763708847/Integers.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Integers.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13148651527763708847/Sequences.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13148651527763708847/Naturals.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13148651527763708847/FiniteSets.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13148651527763708847/Relation.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Relation.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13148651527763708847/Folds.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Folds.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13148651527763708847/Functions.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Functions.tla) Semantic processing of module Naturals Semantic processing of module Sequences Semantic processing of module FiniteSets Semantic processing of module Folds Semantic processing of module Functions Semantic processing of module FiniteSetsExt Semantic processing of module TLC Semantic processing of module SequencesExt Semantic processing of module Relation Semantic processing of module abs Semantic processing of module Integers Semantic processing of module MCabs Starting... (2024-10-22 18:07:45) Implied-temporal checking--satisfiability problem has 1 branches. Computing initial states... Computed 2 initial states... Computed 4 initial states... Computed 8 initial states... Computed 16 initial states... Finished computing initial states: 27 states generated, with 15 of them distinct at 2024-10-22 18:07:45. Checking temporal properties for the current state space with 2979 total distinct states at (2024-10-22 18:07:48) Error: Temporal properties were violated. Error: The following behavior constitutes a counter-example: State 1: <Initial predicate> cLogs = (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<2, 2>>) State 2: <Copy(n1) line 35, col 9 to line 37, col 92 of module abs> cLogs = (n1 :> <<2, 2>> @@ n2 :> <<>> @@ n3 :> <<2, 2>>) State 3: <CopyMaxAndExtend(n2) line 72, col 9 to line 74, col 56 of module abs> cLogs = (n1 :> <<2, 2>> @@ n2 :> <<2, 2, 4, 4>> @@ n3 :> <<2, 2>>) State 4: <Copy(n1) line 35, col 9 to line 37, col 92 of module abs> cLogs = (n1 :> <<2, 2, 4, 4>> @@ n2 :> <<2, 2, 4, 4>> @@ n3 :> <<2, 2>>) State 5: <CopyMaxAndExtend(n3) line 72, col 9 to line 74, col 56 of module abs> cLogs = (n1 :> <<2, 2, 4, 4>> @@ n2 :> <<2, 2, 4, 4>> @@ n3 :> <<2, 2, 4, 4, 2, 2>>) Back to state 1: <MonotonicReduction line 110, col 9 to line 113, col 21 of module abs> Finished checking temporal properties in 00s at 2024-10-22 18:07:48 614674 states generated, 9999 distinct states found, 7020 states left on queue. The depth of the complete state graph search is 6. Finished in 03s at (2024-10-22 18:07:48) ``` Signed-off-by: Markus Alexander Kuppe <[email protected]>
…constraint: ```tla -> % tlc -note MCabs.tla TLC2 Version 2.20 of Day Month 20?? (rev: cc65eef) Running breadth-first search Model-Checking with fp 112 and seed -8448579411904421790 with 1 worker on 10 cores with 7282MB heap and 64MB offheap memory [pid: 62776] (Mac OS X 15.0.1 aarch64, Homebrew 11.0.25 x86_64, MSBDiskFPSet, DiskStateQueue). Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/MCabs.tla Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/abs.tla Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-11473022655680028070/TLC.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/TLC.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-11473022655680028070/SequencesExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/SequencesExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-11473022655680028070/FiniteSetsExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/FiniteSetsExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-11473022655680028070/Integers.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Integers.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-11473022655680028070/Sequences.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-11473022655680028070/Naturals.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-11473022655680028070/FiniteSets.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-11473022655680028070/Relation.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Relation.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-11473022655680028070/Folds.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Folds.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-11473022655680028070/Functions.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Functions.tla) Semantic processing of module Naturals Semantic processing of module Sequences Semantic processing of module FiniteSets Semantic processing of module Folds Semantic processing of module Functions Semantic processing of module FiniteSetsExt Semantic processing of module TLC Semantic processing of module SequencesExt Semantic processing of module Relation Semantic processing of module abs Semantic processing of module Integers Semantic processing of module MCabs Starting... (2024-10-22 18:13:27) Implied-temporal checking--satisfiability problem has 1 branches. Computing initial states... Computed 2 initial states... Computed 4 initial states... Computed 8 initial states... Computed 16 initial states... Finished computing initial states: 27 states generated, with 15 of them distinct at 2024-10-22 18:13:27. Checking temporal properties for the current state space with 2633 total distinct states at (2024-10-22 18:13:30) Error: Temporal properties were violated. Error: The following behavior constitutes a counter-example: State 1: <Initial predicate> cLogs = (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<2, 2>>) State 2: <Copy(n1) line 35, col 9 to line 37, col 92 of module abs> cLogs = (n1 :> <<2, 2>> @@ n2 :> <<>> @@ n3 :> <<2, 2>>) State 3: <CopyMaxAndExtend(n2) line 72, col 9 to line 74, col 56 of module abs> cLogs = (n1 :> <<2, 2>> @@ n2 :> <<2, 2, 2, 4>> @@ n3 :> <<2, 2>>) State 4: <Copy(n3) line 35, col 9 to line 37, col 92 of module abs> cLogs = (n1 :> <<2, 2>> @@ n2 :> <<2, 2, 2, 4>> @@ n3 :> <<2, 2, 2, 4>>) State 5: <CopyMaxAndExtend(n1) line 72, col 9 to line 74, col 56 of module abs> cLogs = (n1 :> <<2, 2, 2, 4, 4, 3>> @@ n2 :> <<2, 2, 2, 4>> @@ n3 :> <<2, 2, 2, 4>>) State 6: <MonotonicReduction line 110, col 9 to line 113, col 21 of module abs> cLogs = (n1 :> <<4, 3>> @@ n2 :> <<>> @@ n3 :> <<>>) State 7: <Copy(n2) line 35, col 9 to line 37, col 92 of module abs> cLogs = (n1 :> <<4, 3>> @@ n2 :> <<4, 3>> @@ n3 :> <<>>) State 8: <CopyMaxAndExtend(n3) line 72, col 9 to line 74, col 56 of module abs> cLogs = (n1 :> <<4, 3>> @@ n2 :> <<4, 3>> @@ n3 :> <<4, 3, 2, 2>>) Back to state 1: <MonotonicReduction line 110, col 9 to line 113, col 21 of module abs> Finished checking temporal properties in 00s at 2024-10-22 18:13:30 530896 states generated, 7831 distinct states found, 5198 states left on queue. The depth of the complete state graph search is 6. Finished in 03s at (2024-10-22 18:13:30) ``` Signed-off-by: Markus Alexander Kuppe <[email protected]>
lemmy
force-pushed
the
mku-abslive
branch
2 times, most recently
from
ccece6d to
5eff00c
Compare
…fy AppendOnlyProp. However, TLC produces a bogus counterexample for InSync: ```tla -> % tlc -note MCabs.tla TLC2 Version 2.20 of Day Month 20?? (rev: cc65eef) Running breadth-first search Model-Checking with fp 40 and seed -6940681262185035164 with 1 worker on 10 cores with 7282MB heap and 64MB offheap memory [pid: 63895] (Mac OS X 15.0.1 aarch64, Homebrew 11.0.25 x86_64, MSBDiskFPSet, DiskStateQueue). Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/MCabs.tla Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/abs.tla Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4426784817192118700/TLC.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/TLC.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4426784817192118700/SequencesExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/SequencesExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4426784817192118700/FiniteSetsExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/FiniteSetsExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4426784817192118700/Integers.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Integers.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4426784817192118700/Sequences.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4426784817192118700/Naturals.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4426784817192118700/FiniteSets.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4426784817192118700/Relation.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Relation.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4426784817192118700/Folds.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Folds.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4426784817192118700/Functions.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Functions.tla) Semantic processing of module Naturals Semantic processing of module Sequences Semantic processing of module FiniteSets Semantic processing of module Folds Semantic processing of module Functions Semantic processing of module FiniteSetsExt Semantic processing of module TLC Semantic processing of module SequencesExt Semantic processing of module Relation Semantic processing of module abs Semantic processing of module Integers Semantic processing of module MCabs Starting... (2024-10-22 18:18:47) Implied-temporal checking--satisfiability problem has 1 branches. Computing initial states... Computed 2 initial states... Computed 4 initial states... Computed 8 initial states... Computed 16 initial states... Finished computing initial states: 27 states generated, with 7 of them distinct at 2024-10-22 18:18:47. Progress(3) at 2024-10-22 18:18:47: 26,895 states generated, 127 distinct states found, 0 states left on queue. Checking temporal properties for the complete state space with 127 total distinct states at (2024-10-22 18:18:47) Error: Temporal properties were violated. Error: The following behavior constitutes a counter-example: State 1: <Initial predicate> cLogs = (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<2, 2>>) State 2: <Copy(n1) line 35, col 9 to line 37, col 92 of module abs> cLogs = (n1 :> <<2, 2>> @@ n2 :> <<>> @@ n3 :> <<2, 2>>) State 3: <CopyMaxAndExtend(n2) line 72, col 9 to line 74, col 56 of module abs> cLogs = (n1 :> <<2, 2>> @@ n2 :> <<2, 2, 2, 3>> @@ n3 :> <<2, 2>>) State 4: <Copy(n3) line 35, col 9 to line 37, col 92 of module abs> cLogs = (n1 :> <<2, 2>> @@ n2 :> <<2, 2, 2, 3>> @@ n3 :> <<2, 2, 2, 3>>) State 5: <CopyMaxAndExtend(n1) line 72, col 9 to line 74, col 56 of module abs> cLogs = (n1 :> <<2, 2, 2, 3, 2, 3>> @@ n2 :> <<2, 2, 2, 3>> @@ n3 :> <<2, 2, 2, 3>>) State 6: <Copy(n2) line 35, col 9 to line 37, col 92 of module abs> cLogs = (n1 :> <<2, 2, 2, 3, 2, 3>> @@ n2 :> <<2, 2, 2, 3, 2, 3>> @@ n3 :> <<2, 2, 2, 3>>) Back to state 1: <CopyMaxAndExtend(n3) line 72, col 9 to line 74, col 56 of module abs> Finished checking temporal properties in 00s at 2024-10-22 18:18:47 26895 states generated, 127 distinct states found, 0 states left on queue. The depth of the complete state graph search is 3. Finished in 00s at (2024-10-22 18:18:47) ``` Related: * tlaplus/tlaplus#1045 * tlaplus/tlaplus#854 Signed-off-by: Markus Alexander Kuppe <[email protected]>
```tla -> % tlc -note MCabs.tla TLC2 Version 2.20 of Day Month 20?? (rev: cc65eef) Running breadth-first search Model-Checking with fp 69 and seed 7965754324960689978 with 1 worker on 10 cores with 7282MB heap and 64MB offheap memory [pid: 65817] (Mac OS X 15.0.1 aarch64, Homebrew 11.0.25 x86_64, MSBDiskFPSet, DiskStateQueue). Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/MCabs.tla Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/abs.tla Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-5146248408337384612/TLC.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/TLC.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-5146248408337384612/SequencesExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/SequencesExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-5146248408337384612/FiniteSetsExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/FiniteSetsExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-5146248408337384612/Integers.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Integers.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-5146248408337384612/Sequences.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-5146248408337384612/Naturals.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-5146248408337384612/FiniteSets.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-5146248408337384612/Relation.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Relation.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-5146248408337384612/Folds.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Folds.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-5146248408337384612/Functions.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Functions.tla) Semantic processing of module Naturals Semantic processing of module Sequences Semantic processing of module FiniteSets Semantic processing of module Folds Semantic processing of module Functions Semantic processing of module FiniteSetsExt Semantic processing of module TLC Semantic processing of module SequencesExt Semantic processing of module Relation Semantic processing of module abs Semantic processing of module Integers Semantic processing of module MCabs Starting... (2024-10-22 18:24:24) Computing initial states... Computed 2 initial states... Computed 4 initial states... Computed 8 initial states... Computed 16 initial states... Finished computing initial states: 27 states generated, with 7 of them distinct at 2024-10-22 18:24:24. Error: Action property AppendOnlyProp is violated. Error: The behavior up to this point is: State 1: <Initial predicate> cLogs = (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<2, 2>>) State 2: <CopyMaxAndExtend(n3) line 75, col 9 to line 77, col 63 of module abs> cLogs = (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<2>>) 632 states generated, 46 distinct states found, 44 states left on queue. The depth of the complete state graph search is 2. Finished in 00s at (2024-10-22 18:24:24) ``` Signed-off-by: Markus Alexander Kuppe <[email protected]>
```tla -> % tlc -note MCabs.tla TLC2 Version 2.20 of Day Month 20?? (rev: cc65eef) Running breadth-first search Model-Checking with fp 51 and seed -2425574771500255732 with 1 worker on 10 cores with 7282MB heap and 64MB offheap memory [pid: 67342] (Mac OS X 15.0.1 aarch64, Homebrew 11.0.25 x86_64, MSBDiskFPSet, DiskStateQueue). Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/MCabs.tla Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/abs.tla Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13080965223161871241/TLC.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/TLC.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13080965223161871241/SequencesExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/SequencesExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13080965223161871241/FiniteSetsExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/FiniteSetsExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13080965223161871241/Integers.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Integers.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13080965223161871241/Sequences.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13080965223161871241/Naturals.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13080965223161871241/FiniteSets.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13080965223161871241/Relation.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Relation.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13080965223161871241/Folds.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Folds.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-13080965223161871241/Functions.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Functions.tla) Semantic processing of module Naturals Semantic processing of module Sequences Semantic processing of module FiniteSets Semantic processing of module Folds Semantic processing of module Functions Semantic processing of module FiniteSetsExt Semantic processing of module TLC Semantic processing of module SequencesExt Semantic processing of module Relation Semantic processing of module abs Semantic processing of module Integers Semantic processing of module MCabs Starting... (2024-10-22 18:30:15) Implied-temporal checking--satisfiability problem has 1 branches. Computing initial states... Computed 2 initial states... Computed 4 initial states... Computed 8 initial states... Computed 16 initial states... Finished computing initial states: 27 states generated, with 7 of them distinct at 2024-10-22 18:30:15. Progress(3) at 2024-10-22 18:30:16: 26,895 states generated, 127 distinct states found, 0 states left on queue. Checking temporal properties for the complete state space with 127 total distinct states at (2024-10-22 18:30:16) Finished checking temporal properties in 00s at 2024-10-22 18:30:16 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.8E-13 26895 states generated, 127 distinct states found, 0 states left on queue. The depth of the complete state graph search is 3. The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 31 and the 95th percentile is 4). Finished in 00s at (2024-10-22 18:30:16) ``` Signed-off-by: Markus Alexander Kuppe <[email protected]>
…ology into a sufficient constraint that is not a tautology. However, the fairness constraint is not machine closed, and it is stronger than it has to be. In fact, we only need "long enough" sequences of Copy actions, but we cannot express "long enough". Signed-off-by: Markus Alexander Kuppe <[email protected]>
…ndOnlyProp. Signed-off-by: Markus Alexander Kuppe <[email protected]>
constraint because it requires the leader to let followers to catch up. However, the leader cannot know how far a follower is behind, unless it can atomically access/read that follower's state. ```tla -> % tlc -note MCabs.tla TLC2 Version 2.20 of Day Month 20?? (rev: cc65eef) Running breadth-first search Model-Checking with fp 128 and seed -4337590855307700118 with 1 worker on 10 cores with 7282MB heap and 64MB offheap memory [pid: 20380] (Mac OS X 15.0.1 aarch64, Homebrew 11.0.25 x86_64, MSBDiskFPSet, DiskStateQueue). Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/MCabs.tla Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/abs.tla Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-15636453091352892932/TLC.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/TLC.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-15636453091352892932/SequencesExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/SequencesExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-15636453091352892932/FiniteSetsExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/FiniteSetsExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-15636453091352892932/Integers.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Integers.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-15636453091352892932/Sequences.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-15636453091352892932/Naturals.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-15636453091352892932/FiniteSets.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-15636453091352892932/Relation.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Relation.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-15636453091352892932/Folds.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Folds.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-15636453091352892932/Functions.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Functions.tla) Semantic processing of module Naturals Semantic processing of module Sequences Semantic processing of module FiniteSets Semantic processing of module Folds Semantic processing of module Functions Semantic processing of module FiniteSetsExt Semantic processing of module TLC Semantic processing of module SequencesExt Semantic processing of module Relation Semantic processing of module abs Semantic processing of module Integers Semantic processing of module MCabs Starting... (2024-10-28 09:56:39) Implied-temporal checking--satisfiability problem has 1 branches. Computing initial states... Computed 2 initial states... Computed 4 initial states... Computed 8 initial states... Computed 16 initial states... Finished computing initial states: 27 states generated, with 7 of them distinct at 2024-10-28 09:56:39. Progress(3) at 2024-10-28 09:56:40: 26,895 states generated, 127 distinct states found, 0 states left on queue. Checking temporal properties for the complete state space with 127 total distinct states at (2024-10-28 09:56:40) Error: Temporal properties were violated. Error: The following behavior constitutes a counter-example: State 1: <Initial predicate> cLogs = (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<2, 2>>) State 2: <Copy(n1) line 35, col 9 to line 37, col 92 of module abs> cLogs = (n1 :> <<2, 2>> @@ n2 :> <<>> @@ n3 :> <<2, 2>>) State 3: <CopyMaxAndExtend(n2) line 72, col 9 to line 74, col 56 of module abs> cLogs = (n1 :> <<2, 2>> @@ n2 :> <<2, 2, 2, 2>> @@ n3 :> <<2, 2>>) State 4: <Copy(n1) line 35, col 9 to line 37, col 92 of module abs> cLogs = (n1 :> <<2, 2, 2, 2>> @@ n2 :> <<2, 2, 2, 2>> @@ n3 :> <<2, 2>>) Back to state 1: <CopyMaxAndExtend(n3) line 72, col 9 to line 74, col 56 of module abs> Finished checking temporal properties in 00s at 2024-10-28 09:56:40 26895 states generated, 127 distinct states found, 0 states left on queue. The depth of the complete state graph search is 3. Finished in 01s at (2024-10-28 09:56:40) ``` Signed-off-by: Markus Alexander Kuppe <[email protected]>
Signed-off-by: Markus Alexander Kuppe <[email protected]>
of at least one server is repeatedly extended. With InSync commented in MCabs.cfg. ```tla -> % tlc -note MCabs.tla TLC2 Version 2.20 of Day Month 20?? (rev: cc65eef) Running breadth-first search Model-Checking with fp 121 and seed -4916710017190118041 with 1 worker on 10 cores with 7282MB heap and 64MB offheap memory [pid: 26014] (Mac OS X 15.0.1 aarch64, Homebrew 11.0.25 x86_64, MSBDiskFPSet, DiskStateQueue). Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/MCabs.tla Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/abs.tla Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-974701093072543730/TLC.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/TLC.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-974701093072543730/SequencesExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/SequencesExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-974701093072543730/FiniteSetsExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/FiniteSetsExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-974701093072543730/Integers.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Integers.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-974701093072543730/Sequences.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-974701093072543730/Naturals.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-974701093072543730/FiniteSets.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-974701093072543730/Relation.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Relation.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-974701093072543730/Folds.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Folds.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-974701093072543730/Functions.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Functions.tla) Semantic processing of module Naturals Semantic processing of module Sequences Semantic processing of module FiniteSets Semantic processing of module Folds Semantic processing of module Functions Semantic processing of module FiniteSetsExt Semantic processing of module TLC Semantic processing of module SequencesExt Semantic processing of module Relation Semantic processing of module abs Semantic processing of module Integers Semantic processing of module MCabs Starting... (2024-10-28 10:16:11) Implied-temporal checking--satisfiability problem has 1 branches. Computing initial states... Computed 2 initial states... Computed 4 initial states... Computed 8 initial states... Computed 16 initial states... Finished computing initial states: 27 states generated, with 7 of them distinct at 2024-10-28 10:16:11. Progress(3) at 2024-10-28 10:16:12: 26,895 states generated, 127 distinct states found, 0 states left on queue. Checking temporal properties for the complete state space with 127 total distinct states at (2024-10-28 10:16:12) Finished checking temporal properties in 00s at 2024-10-28 10:16:12 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.8E-13 26895 states generated, 127 distinct states found, 0 states left on queue. The depth of the complete state graph search is 3. The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 31 and the 95th percentile is 4). Finished in 00s at (2024-10-28 10:16:12) ``` Signed-off-by: Markus Alexander Kuppe <[email protected]>
```tla -> % tlc -note MCabs.tla TLC2 Version 2.20 of Day Month 20?? (rev: cc65eef) Running breadth-first search Model-Checking with fp 8 and seed -6640873860738991250 with 1 worker on 10 cores with 7282MB heap and 64MB offheap memory [pid: 28225] (Mac OS X 15.0.1 aarch64, Homebrew 11.0.25 x86_64, MSBDiskFPSet, DiskStateQueue). Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/MCabs.tla Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/abs.tla Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4226323038874662463/TLC.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/TLC.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4226323038874662463/SequencesExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/SequencesExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4226323038874662463/FiniteSetsExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/FiniteSetsExt.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4226323038874662463/Integers.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Integers.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4226323038874662463/Sequences.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4226323038874662463/Naturals.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4226323038874662463/FiniteSets.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4226323038874662463/Relation.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Relation.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4226323038874662463/Folds.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Folds.tla) Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4226323038874662463/Functions.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Functions.tla) Semantic processing of module Naturals Semantic processing of module Sequences Semantic processing of module FiniteSets Semantic processing of module Folds Semantic processing of module Functions Semantic processing of module FiniteSetsExt Semantic processing of module TLC Semantic processing of module SequencesExt Semantic processing of module Relation Semantic processing of module abs Semantic processing of module Integers Semantic processing of module MCabs Starting... (2024-10-28 10:30:27) Implied-temporal checking--satisfiability problem has 1 branches. Computing initial states... Computed 2 initial states... Computed 4 initial states... Computed 8 initial states... Computed 16 initial states... Finished computing initial states: 27 states generated, with 7 of them distinct at 2024-10-28 10:30:27. Progress(3) at 2024-10-28 10:30:28: 26,895 states generated, 127 distinct states found, 0 states left on queue. Checking temporal properties for the complete state space with 127 total distinct states at (2024-10-28 10:30:28) Error: Temporal properties were violated. Error: The following behavior constitutes a counter-example: State 1: <Initial predicate> cLogs = (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>>) State 2: <Extend(n1) line 44, col 5 to line 46, col 49 of module abs> cLogs = (n1 :> <<3, 2>> @@ n2 :> <<>> @@ n3 :> <<>>) State 3: <Copy(n2) line 35, col 9 to line 37, col 92 of module abs> cLogs = (n1 :> <<3, 2>> @@ n2 :> <<3, 2>> @@ n3 :> <<>>) Back to state 1: <Copy(n3) line 35, col 9 to line 37, col 92 of module abs> Finished checking temporal properties in 00s at 2024-10-28 10:30:28 26895 states generated, 127 distinct states found, 0 states left on queue. The depth of the complete state graph search is 3. Finished in 00s at (2024-10-28 10:30:28) ``` Signed-off-by: Markus Alexander Kuppe <[email protected]>
Proved with TLAPS built from git commit ffb8846ff3c49d53ee6eeedfc4c8c4c409306ae3 tlaplus/tlapm@ffb8846 Signed-off-by: Markus Alexander Kuppe <[email protected]>
…hineClosedFairSpec. Signed-off-by: Markus Alexander Kuppe <[email protected]>
…ence. Signed-off-by: Markus Alexander Kuppe <[email protected]>
Signed-off-by: Markus Alexander Kuppe <[email protected]>
Signed-off-by: Markus Alexander Kuppe <[email protected]>
More formally: LongestCommonPrefix({log}) = log
Signed-off-by: Markus Alexander Kuppe <[email protected]>
…t makes the state space finite. Signed-off-by: Markus Alexander Kuppe <[email protected]>
This was referenced Oct 31, 2024
…ommon prefix but leaves the Terms untouched. Signed-off-by: Markus Alexander Kuppe <[email protected]>
to be equivalent (...AndTerms always substracts 0). Signed-off-by: Markus Alexander Kuppe <[email protected]>
…ck under the MonotonicReduction view. Signed-off-by: Markus Alexander Kuppe <[email protected]>
… limitations of the MonotonicReduction view. ```tla Starting... (2024-10-31 11:22:03) Implied-temporal checking--satisfiability problem has 7 branches. Computing initial states... Computed 2 initial states... Computed 4 initial states... Computed 8 initial states... Computed 16 initial states... Finished computing initial states: 27 states generated, with 7 of them distinct at 2024-10-31 11:22:03. Progress(3) at 2024-10-31 11:22:05: 26,895 states generated, 127 distinct states found, 0 states left on queue. Checking 7 branches of temporal properties for the complete state space with 889 total distinct states at (2024-10-31 11:22:05) Error: Temporal properties were violated. Error: The following behavior constitutes a counter-example: State 1: <Initial predicate> cLogs = (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>>) State 2: <Extend(n3) line 45, col 5 to line 47, col 49 of module abs> cLogs = (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<3, 4>>) State 3: <Copy(n2) line 36, col 9 to line 38, col 92 of module abs> cLogs = (n1 :> <<>> @@ n2 :> <<3, 4>> @@ n3 :> <<3, 4>>) State 4: <Copy(n1) line 36, col 9 to line 38, col 92 of module abs> cLogs = (n1 :> <<3, 4>> @@ n2 :> <<3, 4>> @@ n3 :> <<3, 4>>) Back to state 2: <Extend(n3) line 45, col 5 to line 47, col 49 of module abs> Finished checking temporal properties in 00s at 2024-10-31 11:22:05 26895 states generated, 127 distinct states found, 0 states left on queue. The depth of the complete state graph search is 3. Finished in 02s at (2024-10-31 11:22:05) ``` Signed-off-by: Markus Alexander Kuppe <[email protected]>
…s as sanity checks. Signed-off-by: Markus Alexander Kuppe <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
TBD