Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Finite Monotonic #153

Draft
wants to merge 7 commits into
base: master
Choose a base branch
from
Draft

Finite Monotonic #153

wants to merge 7 commits into from

Conversation

lemmy
Copy link
Member

@lemmy lemmy commented Oct 17, 2024 •
edited
Loading

Related to #97

  • Violations of Convergence are missed without GarbageCollect (regardless of state constraint or conjunct to disable Increment)
  • Conjunct to disable Increment causes spurious liveness violation that ends in stuttering (see bottom)
-> % 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: tlaplus/tlaplus#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 added 3 commits October 17, 2024 06:43
@lemmy
Turn Convergence from a state predicate that is true or false of th…
8034c04 
…e initial states into a liveness property.

Signed-off-by: Markus Alexander Kuppe <[email protected]>
@lemmy
Add a fairness constraint (not machine-closed) that asserts there are…
7c7576b 
… only finitely many Increment actions. A sufficient but weaker fairness constraint would be one that guarantees a sufficient number of uninterrupted Gossip steps.

Signed-off-by: Markus Alexander Kuppe <[email protected]>
@lemmy
Add script and model spec to explore diferent fairness constraints wi…
3debf30 
…th and without the `GarbageCollect` action, a state constraint or a conjunct to disable `Increment`, and different bounds for the divergence.

Signed-off-by: Markus Alexander Kuppe <[email protected]>
@lemmy

This comment was marked as duplicate.

Sign in to view
lemmy added 4 commits October 18, 2024 11:18
@lemmy
Add TRUE, i.e., no fairness as a possible fairness constraint.
8e9dc07 
Signed-off-by: Markus Alexander Kuppe <[email protected]>
@lemmy
Do not switch between GarbageCollect and no GarbageCollect conjoi…
f3763ac 
…ned to `Next.` Instead, toggle between `GarbageCollect` conjoined to `Next` and `GarbageCollect` as a separate VIEW.

Signed-off-by: Markus Alexander Kuppe <[email protected]>
@lemmy
Assert the shape of the counterexamples under all configuration. Log …
45443ef 
…to a CSV file is violated.

Depends on pending PR tlaplus/tlaplus#1042

Signed-off-by: Markus Alexander Kuppe <[email protected]>
@lemmy
Ensure that the exit/return value of nested TLC runs is either
d8bdb00 
a successful run with no counterexample, a run that detected
a liveness violation, or a postcondition violation.

Signed-off-by: Markus Alexander Kuppe <[email protected]>
@lemmy lemmy mentioned this pull request Oct 21, 2024
Merged
@lemmy
Copy link
Member Author

lemmy commented Jan 6, 2025

@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

@muenchnerkindl
Copy link
Collaborator

muenchnerkindl commented Jan 7, 2025 •
edited by lemmy
Loading

Interesting challenge! I believe that TLAPS should be able to prove the property but I think the specification is not the one you want. Since <<Increment(n)>>_vars is always enabled, so is <<Next>>_vars, and therefore the spec implies that there must be infinitely many non-stuttering steps. On the other hand the conjunct \A n,o \in Node : <>[][Gossip(n,o)]_vars implies eventual stuttering, so the spec is just equivalent to FALSE. (Ah, yes, the joy of not machine-closed specifications!) I think you want the fairness condition

/\ \A n,o \in Node : WF_vars(Gossip(n,o))
/\ <>[][\E n,o \in Node : Gossip(n,o)]_vars

(Alternatively, you can leave the second conjunct as it is, but I find the above a little easier to understand.)

I'll try to find some time to prove the property for the modified spec.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ahelwer ahelwer ahelwer left review comments

Assignees
No one assigned
Labels
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@lemmy @muenchnerkindl @ahelwer