Finitizing monotonic systems Take2 #155
Open
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
Closed
lemmy
force-pushed
the
mku-FiniteMonotonic
branch
5 times, most recently
from
373f037 to
c20756d
Compare
|
TLAPS, unlike SANY, doesn’t mind the duplicate |
lemmy
force-pushed
the
mku-FiniteMonotonic
branch
from
c20756d to
b551d53
Compare
|
I'll take a look to see whether we can combine some of the validation checks to all run one after the other to dump as much info as possible instead of needing multiple reversions. The multiple declarations thing seems like a bug in TLAPM. It seems like the CI is failing due to a false assumption: It's hard to see since there is so much debug output, search the logs for |
|
@ahelwer How can we pass JVM properties and additional command-line parameters to TLC in the manifest.json? |
|
Ideally we would not, or rather they would be encoded in a way that is divorced from a specific backend implementation - like how the expected result option is exposed (there is a second finite model-checker now, spectacle/tla-web implements one). This has been manageable for all the specs so far but of course all abstractions will reach their limit somewhere. What do you have in mind? |
|
The assumptions fail because '-Dtlc2.tool.impl.Tool.cdot=true' is not passed to TLC. |
|
Ah! Should we perhaps enable that by default for all models? |
Signed-off-by: Markus Alexander Kuppe <[email protected]>
Signed-off-by: Markus Alexander Kuppe <[email protected]>
```shell
-> % opam exec -- tlapm --version
41d03d4
-> % opam exec -- tlapm CRDT_proof.tla
(* loading fingerprints in ".tlacache/CRDT_proof.tlaps/fingerprints" *)
(* created new ".tlacache/CRDT_proof.tlaps/CRDT_proof.thy" *)
(* fingerprints written in ".tlacache/CRDT_proof.tlaps/fingerprints" *)
File "./CRDT_proof.tla", line 182, characters 5-6:
[ERROR]: Could not prove or check:
ASSUME NEW CONSTANT Node,
NEW VARIABLE counter,
TypeOK == counter \in [Node -> [Node -> Nat]],
Safety == \A n, o \in Node : counter[n][n] >= counter[o][n],
Gossip(n, o) ==
LET Max(a, b) == IF a > b THEN a ELSE b
IN counter'
= [counter EXCEPT
![o] = [nodeView \in Node |->
Max
(counter[n][nodeView],
counter[o][nodeView])]],
NodeAssumption == IsFiniteSet(Node),
DistFun(o) ==
[n \in Node |-> counter[n][n] - counter[o][n]],
TypeOK ,
TypeOK' ,
Safety ,
Safety' ,
[\E n, o \in Node : Gossip(n, o)]_vars ,
NEW CONSTANT v \in Node,
NEW CONSTANT w \in Node,
<1>1
PROVE (DistFun(v)')[w] =< DistFun(v)[w]
File "./CRDT_proof.tla", line 1, character 1 to line 354, character 77:
[ERROR]: 1/210 obligations failed.
There were backend errors processing module `"CRDT_proof"`.
tlapm ending abnormally with Failure("backend errors: there are unproved obligations")
Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
Called from Tlapm_lib.process_module in file "src/tlapm_lib.ml", line 446, characters 12-77
Called from Tlapm_lib.main.f in file "src/tlapm_lib.ml", line 575, characters 23-43
Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
Called from Tlapm_lib.main in file "src/tlapm_lib.ml", line 578, characters 13-40
Called from Tlapm_lib.init in file "src/tlapm_lib.ml", line 590, characters 8-33
-> % opam exec -- tlapm CRDT_proof.tla
(* loading fingerprints in ".tlacache/CRDT_proof.tlaps/fingerprints" *)
(* created new ".tlacache/CRDT_proof.tlaps/CRDT_proof.thy" *)
(* fingerprints written in ".tlacache/CRDT_proof.tlaps/fingerprints" *)
File "./CRDT_proof.tla", line 1, character 1 to line 354, character 77:
[INFO]: All 210 obligations proved.
```
Signed-off-by: Markus Alexander Kuppe <[email protected]>
The property `IsSync` in `DistributedReplicatedLog.tla` does not hold; the node with the longest log may forever append a value before the other nodes can catch up. TLC finds the following (valid) counterexample (for three nodes): ```tla Error: Temporal properties were violated. Error: The following behavior constitutes a counter-example: State 1: <Initial predicate> cLogs = (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>>) State 2: <Extend(n2) line 35, col 5 to line 38, col 49 of module DistributedReplicatedLog> cLogs = (n1 :> <<>> @@ n2 :> <<v>> @@ n3 :> <<>>) State 3: <Extend(n2) line 35, col 5 to line 38, col 49 of module DistributedReplicatedLog> cLogs = (n1 :> <<>> @@ n2 :> <<v, v>> @@ n3 :> <<>>) State 4: <Copy(n3) line 26, col 9 to line 32, col 96 of module DistributedReplicatedLog> cLogs = (n1 :> <<>> @@ n2 :> <<v, v>> @@ n3 :> <<v>>) Back to state 2: <Copy(n1) line 26, col 9 to line 32, col 96 of module DistributedReplicatedLog> ``` Signed-off-by: Markus Alexander Kuppe <[email protected]>
lemmy
force-pushed
the
mku-FiniteMonotonic
branch
from
b551d53 to
d97b414
Compare
It’s better not to enable it globally, considering its known limitations. |
|
All right. If we want to stick with the current way of doing things I would probably add "action composition" as another possible feature of each .tla file in the manifest.json, along with "pluscal" and "proof"; it is a pretty neat feature worth highlighting, after all. This could be enforced with a tree-sitter query to find usage of the The real drawback here is that it won't handle transitivity - like if a non-top-level module for the TLC run uses |
|
This should now work if you put |
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.
Related to #97
Supersedes #153