search

lbinria / TwoPhase

MIT License
3 stars 3 forks source link

Checking any trace in BenchMarks/ fails with `The variable rmState was changed while it is specified as UNCHANGED at` #1

Open lemmy opened 7 months ago

lemmy commented 7 months ago 
-> % tlc -note TwoPhaseTrace.tla 
TLC2 Version 2.18 of Day Month 20?? (rev: 6fb13e9)
Running breadth-first search Model-Checking with fp 108 and seed -7209979154559774580 with 1 worker on 10 cores with 7282MB heap and 64MB offheap memory [pid: 66065] (Mac OS X 13.6.6 aarch64, Homebrew 11.0.23 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /Users/markus/src/TLA/_specs/TwoPhase/spec/TwoPhaseTrace.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-16088740289159181284/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-16088740289159181284/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-16088740289159181284/SequencesExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/SequencesExt.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-16088740289159181284/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-16088740289159181284/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-16088740289159181284/Bags.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Bags.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-16088740289159181284/Json.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Json.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-16088740289159181284/IOUtils.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/IOUtils.tla)
Parsing file /Users/markus/src/TLA/_specs/TwoPhase/spec/TwoPhase.tla
Parsing file /Users/markus/src/TLA/_specs/TwoPhase/spec/TVOperators.tla
Parsing file /Users/markus/src/TLA/_specs/TwoPhase/spec/TraceSpec.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-16088740289159181284/FiniteSetsExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/FiniteSetsExt.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-16088740289159181284/Folds.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Folds.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-16088740289159181284/Functions.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Functions.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-16088740289159181284/Integers.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /Users/markus/src/TLA/_specs/TwoPhase/spec/TCommit.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 Folds
Semantic processing of module Functions
Semantic processing of module FiniteSetsExt
Semantic processing of module SequencesExt
Semantic processing of module Bags
Semantic processing of module Json
Semantic processing of module Integers
Semantic processing of module IOUtils
Semantic processing of module TCommit
Semantic processing of module TwoPhase
Semantic processing of module TVOperators
Semantic processing of module TraceSpec
Semantic processing of module TwoPhaseTrace
Starting... (2024-04-17 20:50:48)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2024-04-17 20:50:48.
Error: TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.RuntimeException
: The variable rmState was changed while it is specified as UNCHANGED at
line 107, col 18 to line 107, col 24 of module TwoPhase
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ l = 1
/\ tmPrepared = {}
/\ msgs = {}
/\ rmState = ("rm-0" :> "working" @@ "rm-1" :> "working" @@ "rm-2" :> "working" @@ "rm-3" :> "working")
/\ tmState = "init"

State 2: <IsRMPrepare line 61, col 5 to line 66, col 38 of module TwoPhaseTrace>
/\ l = 2
/\ tmPrepared = {}
/\ msgs = {[type |-> "Prepared", rm |-> "rm-0"]}
/\ rmState = ("rm-0" :> "prepared" @@ "rm-1" :> "working" @@ "rm-2" :> "working" @@ "rm-3" :> "working")
/\ tmState = "init"

Error: The error occurred when TLC was evaluating the nested
expressions at the following positions:
0. Line 49, column 5 to line 50, column 14 in TwoPhaseTrace
1. Line 49, column 8 to line 49, column 25 in TwoPhaseTrace
2. Line 34, column 5 to line 37, column 31 in TraceSpec
3. Line 34, column 8 to line 34, column 26 in TraceSpec
4. Line 35, column 8 to line 35, column 69 in TraceSpec
5. Line 35, column 66 to line 35, column 69 in TraceSpec
6. Line 36, column 8 to line 36, column 17 in TraceSpec
7. Line 37, column 8 to line 37, column 31 in TraceSpec
8. Line 26, column 5 to line 41, column 17 in TwoPhaseTrace
9. Line 27, column 9 to line 29, column 17 in TwoPhaseTrace
10. Line 28, column 14 to line 28, column 61 in TwoPhaseTrace
11. Line 31, column 9 to line 33, column 17 in TwoPhaseTrace
12. Line 33, column 14 to line 33, column 17 in TwoPhaseTrace
13. Line 35, column 9 to line 37, column 17 in TwoPhaseTrace
14. Line 37, column 14 to line 37, column 17 in TwoPhaseTrace
15. Line 39, column 9 to line 41, column 17 in TwoPhaseTrace
16. Line 41, column 14 to line 41, column 17 in TwoPhaseTrace
17. Line 50, column 8 to line 50, column 14 in TwoPhaseTrace
18. Line 104, column 3 to line 107, column 38 in TwoPhase
19. Line 104, column 6 to line 104, column 21 in TwoPhase
20. Line 105, column 6 to line 105, column 22 in TwoPhase
21. Line 106, column 6 to line 106, column 43 in TwoPhase
22. Line 107, column 6 to line 107, column 38 in TwoPhase
23. Line 107, column 16 to line 107, column 38 in TwoPhase
24. Line 107, column 18 to line 107, column 24 in TwoPhase

10 states generated, 10 distinct states found, 8 states left on queue.
The depth of the complete state graph search is 2.
Finished in 00s at (2024-04-17 20:50:48)

TLC validates the trace successfully if one manually deletes what seems to be initialization logging: https://github.com/lbinria/TwoPhase/blob/d95a2282ba44a8753551e349b75edbba1a4fb389/BenchMarks/trace.ndjson.4RM.E#L1-L5

The two-state counterexample above suggested that TLC matches those lines arbitrarily (IsRMPrepare), which was traced to https://github.com/lbinria/TwoPhase/blob/d95a2282ba44a8753551e349b75edbba1a4fb389/spec/TraceSpec.tla#L41 being vacuously true.

hcirstea commented 7 months ago

The initialization logging was experimental, it's no longer done and the corresponding lines removed from the trace files.

There are still warnings for some traces, like TwoPhase/BenchMarks/trace.ndjson.4RM.VpEA:

Warning: The variable rmState was changed while it is specified as UNCHANGED at line 41, col 11 to line 41, col 17 of module TwoPhase