search

tlaplus / Examples

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

Finite Monotonic #153

Open lemmy opened 1 month ago

lemmy commented 1 month ago

Related to https://github.com/tlaplus/Examples/pull/97

-> % tlc -note SCCRDT.tla -config SCCRDT.tla                     
TLC2 Version 2.20 of Day Month 20?? (rev: 2360829)
Running breadth-first search Model-Checking with fp 55 and seed 1802278425399457922 with 1 worker on 10 cores with 7282MB heap and 64MB offheap memory [pid: 41282] (Mac OS X 15.0.1 aarch64, Homebrew 11.0.24 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /Users/markus/src/TLA/_specs/examples/specifications/FiniteMonotonic/SCCRDT.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-11431439590268313249/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-11431439590268313249/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-11431439590268313249/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-11431439590268313249/IOUtils.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/IOUtils.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-11431439590268313249/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-11431439590268313249/Integers.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/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 IOUtils
Semantic processing of module SCCRDT
Starting... (2024-10-17 06:45:34)
<<"conf", [D |-> 0, F |-> 0, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 0, F |-> 0, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 0, F |-> 0, G |-> TRUE, C |-> FALSE], 0>>
<<"conf", [D |-> 0, F |-> 0, G |-> TRUE, C |-> TRUE], 0>>
<<"conf", [D |-> 0, F |-> 1, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 0, F |-> 1, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 0, F |-> 1, G |-> TRUE, C |-> FALSE], 0>>
<<"conf", [D |-> 0, F |-> 1, G |-> TRUE, C |-> TRUE], 0>>
<<"conf", [D |-> 0, F |-> 2, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 0, F |-> 2, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 0, F |-> 2, G |-> TRUE, C |-> FALSE], 0>>
<<"conf", [D |-> 0, F |-> 2, G |-> TRUE, C |-> TRUE], 0>>
<<"conf", [D |-> 0, F |-> 3, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 0, F |-> 3, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 0, F |-> 3, G |-> TRUE, C |-> FALSE], 0>>
<<"conf", [D |-> 0, F |-> 3, G |-> TRUE, C |-> TRUE], 0>>
<<"conf", [D |-> 0, F |-> 4, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 0, F |-> 4, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 0, F |-> 4, G |-> TRUE, C |-> FALSE], 0>>
<<"conf", [D |-> 0, F |-> 4, G |-> TRUE, C |-> TRUE], 0>>
<<"conf", [D |-> 0, F |-> 5, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 0, F |-> 5, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 0, F |-> 5, G |-> TRUE, C |-> FALSE], 0>>
<<"conf", [D |-> 0, F |-> 5, G |-> TRUE, C |-> TRUE], 0>>
<<"conf", [D |-> 0, F |-> 6, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 0, F |-> 6, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 0, F |-> 6, G |-> TRUE, C |-> FALSE], 0>>
<<"conf", [D |-> 0, F |-> 6, G |-> TRUE, C |-> TRUE], 0>>
<<"conf", [D |-> 1, F |-> 0, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 1, F |-> 0, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 1, F |-> 0, G |-> TRUE, C |-> FALSE], 0>>
<<"conf", [D |-> 1, F |-> 0, G |-> TRUE, C |-> TRUE], 0>>
<<"conf", [D |-> 1, F |-> 1, G |-> FALSE, C |-> FALSE], 13>>
<<"conf", [D |-> 1, F |-> 1, G |-> FALSE, C |-> TRUE], 13>>
<<"conf", [D |-> 1, F |-> 1, G |-> TRUE, C |-> FALSE], 13>>
<<"conf", [D |-> 1, F |-> 1, G |-> TRUE, C |-> TRUE], 13>>
<<"conf", [D |-> 1, F |-> 2, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 1, F |-> 2, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 1, F |-> 2, G |-> TRUE, C |-> FALSE], 0>>
<<"conf", [D |-> 1, F |-> 2, G |-> TRUE, C |-> TRUE], 0>>
<<"conf", [D |-> 1, F |-> 3, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 1, F |-> 3, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 1, F |-> 3, G |-> TRUE, C |-> FALSE], 0>>
<<"conf", [D |-> 1, F |-> 3, G |-> TRUE, C |-> TRUE], 0>>
<<"conf", [D |-> 1, F |-> 4, G |-> FALSE, C |-> FALSE], 13>>
<<"conf", [D |-> 1, F |-> 4, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 1, F |-> 4, G |-> TRUE, C |-> FALSE], 13>>
<<"conf", [D |-> 1, F |-> 4, G |-> TRUE, C |-> TRUE], 0>>
<<"conf", [D |-> 1, F |-> 5, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 1, F |-> 5, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 1, F |-> 5, G |-> TRUE, C |-> FALSE], 0>>
<<"conf", [D |-> 1, F |-> 5, G |-> TRUE, C |-> TRUE], 0>>
<<"conf", [D |-> 1, F |-> 6, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 1, F |-> 6, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 1, F |-> 6, G |-> TRUE, C |-> FALSE], 0>>
<<"conf", [D |-> 1, F |-> 6, G |-> TRUE, C |-> TRUE], 0>>
<<"conf", [D |-> 2, F |-> 0, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 2, F |-> 0, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 2, F |-> 0, G |-> TRUE, C |-> FALSE], 13>>
<<"conf", [D |-> 2, F |-> 0, G |-> TRUE, C |-> TRUE], 13>>
<<"conf", [D |-> 2, F |-> 1, G |-> FALSE, C |-> FALSE], 13>>
<<"conf", [D |-> 2, F |-> 1, G |-> FALSE, C |-> TRUE], 13>>
<<"conf", [D |-> 2, F |-> 1, G |-> TRUE, C |-> FALSE], 13>>
<<"conf", [D |-> 2, F |-> 1, G |-> TRUE, C |-> TRUE], 13>>
<<"conf", [D |-> 2, F |-> 2, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 2, F |-> 2, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 2, F |-> 2, G |-> TRUE, C |-> FALSE], 13>>
<<"conf", [D |-> 2, F |-> 2, G |-> TRUE, C |-> TRUE], 13>>
<<"conf", [D |-> 2, F |-> 3, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 2, F |-> 3, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 2, F |-> 3, G |-> TRUE, C |-> FALSE], 13>>
<<"conf", [D |-> 2, F |-> 3, G |-> TRUE, C |-> TRUE], 13>>
<<"conf", [D |-> 2, F |-> 4, G |-> FALSE, C |-> FALSE], 13>>
<<"conf", [D |-> 2, F |-> 4, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 2, F |-> 4, G |-> TRUE, C |-> FALSE], 13>>
<<"conf", [D |-> 2, F |-> 4, G |-> TRUE, C |-> TRUE], 13>>
<<"conf", [D |-> 2, F |-> 5, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 2, F |-> 5, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 2, F |-> 5, G |-> TRUE, C |-> FALSE], 0>>
<<"conf", [D |-> 2, F |-> 5, G |-> TRUE, C |-> TRUE], 0>>
<<"conf", [D |-> 2, F |-> 6, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 2, F |-> 6, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 2, F |-> 6, G |-> TRUE, C |-> FALSE], 0>>
<<"conf", [D |-> 2, F |-> 6, G |-> TRUE, C |-> TRUE], 0>>
<<"conf", [D |-> 3, F |-> 0, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 3, F |-> 0, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 3, F |-> 0, G |-> TRUE, C |-> FALSE], 13>>
<<"conf", [D |-> 3, F |-> 0, G |-> TRUE, C |-> TRUE], 13>>
<<"conf", [D |-> 3, F |-> 1, G |-> FALSE, C |-> FALSE], 13>>
<<"conf", [D |-> 3, F |-> 1, G |-> FALSE, C |-> TRUE], 13>>
<<"conf", [D |-> 3, F |-> 1, G |-> TRUE, C |-> FALSE], 13>>
<<"conf", [D |-> 3, F |-> 1, G |-> TRUE, C |-> TRUE], 13>>
<<"conf", [D |-> 3, F |-> 2, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 3, F |-> 2, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 3, F |-> 2, G |-> TRUE, C |-> FALSE], 13>>
<<"conf", [D |-> 3, F |-> 2, G |-> TRUE, C |-> TRUE], 13>>
<<"conf", [D |-> 3, F |-> 3, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 3, F |-> 3, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 3, F |-> 3, G |-> TRUE, C |-> FALSE], 13>>
<<"conf", [D |-> 3, F |-> 3, G |-> TRUE, C |-> TRUE], 13>>
<<"conf", [D |-> 3, F |-> 4, G |-> FALSE, C |-> FALSE], 13>>
<<"conf", [D |-> 3, F |-> 4, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 3, F |-> 4, G |-> TRUE, C |-> FALSE], 13>>
<<"conf", [D |-> 3, F |-> 4, G |-> TRUE, C |-> TRUE], 13>>
<<"conf", [D |-> 3, F |-> 5, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 3, F |-> 5, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 3, F |-> 5, G |-> TRUE, C |-> FALSE], 0>>
<<"conf", [D |-> 3, F |-> 5, G |-> TRUE, C |-> TRUE], 0>>
<<"conf", [D |-> 3, F |-> 6, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 3, F |-> 6, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 3, F |-> 6, G |-> TRUE, C |-> FALSE], 0>>
<<"conf", [D |-> 3, F |-> 6, G |-> TRUE, C |-> TRUE], 0>>
Computing initial states...
Finished computing initial states: 0 distinct states generated at 2024-10-17 06:47:24.
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 = 0.0
0 states generated, 0 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 0.
Finished in 01min 50s at (2024-10-17 06:47:24)

Better exit values: https://github.com/tlaplus/tlaplus/issues/1041

-> % D=3 F=4 G=TRUE C=FALSE tlc -note MCCRDT.tla -config MCCRDT.cfg
TLC2 Version 2.20 of Day Month 20?? (rev: 2360829)
Running breadth-first search Model-Checking with fp 130 and seed 4584290592961789553 with 1 worker on 10 cores with 7282MB heap and 64MB offheap memory [pid: 42208] (Mac OS X 15.0.1 aarch64, Homebrew 11.0.24 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /Users/markus/src/TLA/_specs/examples/specifications/FiniteMonotonic/MCCRDT.tla
Parsing file /Users/markus/src/TLA/_specs/examples/specifications/FiniteMonotonic/CRDT.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-14565095515634353915/IOUtils.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/IOUtils.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-14565095515634353915/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-14565095515634353915/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-14565095515634353915/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-14565095515634353915/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-14565095515634353915/FiniteSets.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Semantic processing of module Naturals
Semantic processing of module CRDT
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module Integers
Semantic processing of module IOUtils
Semantic processing of module MCCRDT
Starting... (2024-10-17 06:52:34)
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2024-10-17 06:52:34.
Progress(9) at 2024-10-17 06:52:34: 621 states generated, 100 distinct states found, 0 states left on queue.
Checking temporal properties for the complete state space with 100 total distinct states at (2024-10-17 06:52:34)
Error: Temporal properties were violated.

Error: The following behavior constitutes a counter-example:

State 1: <Initial predicate>
counter = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))

State 2: <S!Next line 34, col 1 to line 34, col 18 of module MCCRDT>
counter = (n1 :> (n1 :> 1 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))

State 3: <S!Next line 34, col 1 to line 34, col 18 of module MCCRDT>
counter = (n1 :> (n1 :> 1 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 1))

State 4: <S!Next line 34, col 1 to line 34, col 18 of module MCCRDT>
counter = (n1 :> (n1 :> 1 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 2))

State 5: <S!Next line 34, col 1 to line 34, col 18 of module MCCRDT>
counter = (n1 :> (n1 :> 1 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 3))

State 6: <S!Next line 34, col 1 to line 34, col 18 of module MCCRDT>
counter = (n1 :> (n1 :> 2 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 3))

State 7: <S!Next line 34, col 1 to line 34, col 18 of module MCCRDT>
counter = (n1 :> (n1 :> 3 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 3))

State 8: <S!Next line 34, col 1 to line 34, col 18 of module MCCRDT>
counter = (n1 :> (n1 :> 3 @@ n2 :> 3) @@ n2 :> (n1 :> 0 @@ n2 :> 3))

State 9: Stuttering
Finished checking temporal properties in 00s at 2024-10-17 06:52:34
621 states generated, 100 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 9.
Finished in 00s at (2024-10-17 06:52:34)
lemmy commented 1 month ago

@muenchnerkindl What's your feeling? Can TLAPS (with the enablement branch) prove the liveness property Convergence given the specified fairness constraint?

https://github.com/tlaplus/Examples/blob/3debf309d1d1afe33baca0f20f93821737b0307c/specifications/FiniteMonotonic/CRDT.tla