From ff80522caeb280a3084955bb0025d552abba1a8c Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 28 Oct 2024 10:31:49 -0700 Subject: [PATCH] As expect, AllSyncing is not a theorem of the spec: ```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: cLogs = (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>>) State 2: cLogs = (n1 :> <<3, 2>> @@ n2 :> <<>> @@ n3 :> <<>>) State 3: cLogs = (n1 :> <<3, 2>> @@ n2 :> <<3, 2>> @@ n3 :> <<>>) Back to state 1: 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 --- tla/consensus/MCabs.cfg | 1 + tla/consensus/abs.tla | 4 ++++ 2 files changed, 5 insertions(+) diff --git a/tla/consensus/MCabs.cfg b/tla/consensus/MCabs.cfg index 8ef524eba5f3..4e275454c56f 100644 --- a/tla/consensus/MCabs.cfg +++ b/tla/consensus/MCabs.cfg @@ -17,6 +17,7 @@ INVARIANTS PROPERTIES InSync Syncing + AllSyncing AppendOnlyProp \* EquivExtendProp \* EquivCopyMaxAndExtendProp diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla index dd4e2abb4021..f76a14891666 100644 --- a/tla/consensus/abs.tla +++ b/tla/consensus/abs.tla @@ -135,6 +135,10 @@ Syncing == THEOREM MachineClosedFairSpec => Syncing +AllSyncing == + []<><<\A s \in Servers: IsStrictPrefix(cLogs[s], cLogs'[s])>>_cLogs + +\* NOT A THEOREM: MachineClosedFairSpec => AllSyncing ---- \* abs models ccfraft's logs up to the commitIndex and the extension of the