Skip to content

GitLab

Commit c9d7928e authored by Christian Müller's avatar Christian Müller
Browse files

examples

parent 99485abb
Expand all Hide whitespace changes
Inline Side-by-side
results/nonomitting/conference/conference_causal_alleq.metrics
View file @ c9d7928e
Name: nonomitting/conference
Description: alleq
Invariant:
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq())
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P,rt:R. (Review(t1)(xt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P. (Conf(t1)(xt,pt) ↔ eq()) ∧
∀ xt:A,pt:P. (Assign(t1)(xt,pt) ↔ eq())
Model: causal
Result: not inductive
WF size: 6
Time: 3813 ms
Proof steps: 14
Strengthenings: 9
Largest Inv: 1455
Average Inv: 599
\ No newline at end of file
Time: 6822 ms
Proof steps: 15
Strengthenings: 11
Largest Inv: 3544
Average Inv: 1546
\ No newline at end of file
results/nonomitting/conference/conference_causal_alleq_0.dot
View file @ c9d7928e
digraph "Invariant Labelling" {
3 [label = "Node 3:
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq())"]
1 [label = "Node 1:
∀ xt:A,pt:P. (Conf(t1)(xt,pt) ↔ eq())"]
0 [label = "Node 0:
True"]
3 -> 5 [label = "forall xa:A,xb:A,p:P,r:R
......@@ -9,20 +9,30 @@ True"]
", color = red]
2 -> 3 [label = "forall x:A,p:P,r:R
Assign(x,p) ∧ Oracle(x,p,r) → Review += (x,p,r);", color = red]
4 [label = "Node 4:
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq())"]
5 -> 3 [label = "forall x:A,p:P,r:R may (Some(choice2))
Assign(x,p) → Review += (x,p,r);", color = red]
1 -> 2 [label = "forall x:A,p:P may (Some(choice1))
¬ Conf(x,p) → Assign += (x,p);", color = red]
0 -> 1 [label = "forall x:A,p:P may (Some(choice0))
True → Conf += (x,p);", color = red]
1 [label = "Node 1:
True"]
3 [label = "Node 3:
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P,rt:R. (Review(t1)(xt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P. ((Conf(t1)(xt,pt) ↔ eq()) ∧
(Assign(t1)(xt,pt) ↔ eq()))"]
4 [label = "Node 4:
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P,rt:R. (Review(t1)(xt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P. ((Conf(t1)(xt,pt) ↔ eq()) ∧
(Assign(t1)(xt,pt) ↔ eq()))"]
2 [label = "Node 2:
∀ xt:A,pt:P. ((Conf(t1)(xt,pt) ↔ eq()) ∧
(Assign(t1)(xt,pt) ↔ eq()))"]
4 -> 4 [label = "forall
", color = red]
2 [label = "Node 2:
True"]
5 [label = "Node 5:
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq())"]
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P,rt:R. (Review(t1)(xt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P. ((Conf(t1)(xt,pt) ↔ eq()) ∧
(Assign(t1)(xt,pt) ↔ eq()))"]
}
\ No newline at end of file
results/nonomitting/conference/conference_causal_alleq_1.dot
View file @ c9d7928e
digraph "Invariant Labelling" {
3 [label = "Node 3:
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq())"]
1 [label = "Node 1:
∀ xt:A,pt:P. (Conf(t1)(xt,pt) ↔ eq())"]
0 [label = "Node 0:
True"]
5 -> 3 [label = "forall x:A,p:P,r:R may (Some(choice2))
......@@ -11,18 +11,48 @@ True"]
", color = red]
2 -> 3 [label = "forall x:A,p:P,r:R
Assign(x,p) ∧ Oracle(x,p,r) → Review += (x,p,r);", color = red]
4 [label = "Node 4:
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq())"]
1 -> 2 [label = "forall x:A,p:P may (Some(choice1))
¬ Conf(x,p) → Assign += (x,p);", color = red]
0 -> 1 [label = "forall x:A,p:P may (Some(choice0))
True → Conf += (x,p);", color = red]
1 [label = "Node 1:
True"]
3 [label = "Node 3:
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P,rt:R. (Review(t1)(xt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P. ((Conf(t1)(xt,pt) ↔ eq()) ∧
(Assign(t1)(xt,pt) ↔ eq()))"]
4 [label = "Node 4:
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P,rt:R. (Review(t1)(xt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P. ((Conf(t1)(xt,pt) ↔ eq()) ∧
(Assign(t1)(xt,pt) ↔ eq()))"]
2 [label = "Node 2:
∀ xt:A,pt:P. ((Conf(t1)(xt,pt) ↔ eq()) ∧
(Assign(t1)(xt,pt) ↔ eq()))"]
4 -> 4 [label = "forall
", color = red]
2 [label = "Node 2:
True"]
5 [label = "Node 5:
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq())"]
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P,rt:R. (Review(t1)(xt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P. ((Conf(t1)(xt,pt) ↔ eq()) ∧
(Assign(t1)(xt,pt) ↔ eq())) ∧
∀ xat:A,xbt:A,pt:P,rt:R,xt:A. ((¬ Read(t1)(xat,xbt,pt,rt) ∨
Read(t2)(xat,xbt,pt,rt)) ∧
(¬ Read(t2)(xat,xbt,pt,rt) ∨
Read(t1)(xat,xbt,pt,rt)) ∧
((¬ Review(t1)(xt,pt,rt) ∧
(¬ Assign(t1)(xt,pt) ∨
¬ choice2(t1)(xt,pt,rt))) ∨
Review(t2)(xt,pt,rt) ∨
(Assign(t2)(xt,pt) ∧
((¬ informed(t1)(xt) ∧
choice2(t1)(xt,pt,rt)) ∨
(informed(t1)(xt) ∧
choice2(t2)(xt,pt,rt))))) ∧
((¬ Review(t2)(xt,pt,rt) ∧
(¬ Assign(t2)(xt,pt) ∨
¬ informed(t1)(xt) ∨
¬ choice2(t2)(xt,pt,rt))) ∨
Review(t1)(xt,pt,rt) ∨
(Assign(t1)(xt,pt) ∧
choice2...(1009 characters)"]
}
\ No newline at end of file
results/nonomitting/conference/conference_causal_alleq_10.dot
View file @ c9d7928e
digraph "Invariant Labelling" {
1 [label = "Node 1:
∀ xt:A,pt:P. (Conf(t1)(xt,pt) ↔ eq())"]
5 [label = "Node 5:
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P,rt:R. (Review(t1)(xt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P. ((Conf(t1)(xt,pt) ↔ eq()) ∧
(Assign(t1)(xt,pt) ↔ eq())) ∧
∀ xat:A,xbt:A,pt:P,rt:R,xt:A. ((¬ Read(t1)(xat,xbt,pt,rt) ∨
Read(t2)(xat,xbt,pt,rt)) ∧
(¬ Read(t2)(xat,xbt,pt,rt) ∨
Read(t1)(xat,xbt,pt,rt)) ∧
((¬ Review(t1)(xt,pt,rt) ∧
(¬ Assign(t1)(xt,pt) ∨
¬ choice2(t1)(xt,pt,rt))) ∨
Review(t2)(xt,pt,rt) ∨
(Assign(t2)(xt,pt) ∧
((¬ informed(t1)(xt) ∧
choice2(t1)(xt,pt,rt)) ∨
(informed(t1)(xt) ∧
choice2(t2)(xt,pt,rt))))) ∧
((¬ Review(t2)(xt,pt,rt) ∧
(¬ Assign(t2)(xt,pt) ∨
¬ informed(t1)(xt) ∨
¬ choice2(t2)(xt,pt,rt))) ∨
Review(t1)(xt,pt,rt) ∨
(Assign(t1)(xt,pt) ∧
choice2...(23593 characters)"]
0 [label = "Node 0:
True"]
2 -> 3 [label = "forall x:A,p:P,r:R
Assign(x,p) ∧ Oracle(x,p,r) → Review += (x,p,r);", color = red]
5 -> 3 [label = "forall x:A,p:P,r:R may (Some(choice2))
Assign(x,p) → Review += (x,p,r);", color = red]
1 -> 2 [label = "forall x:A,p:P may (Some(choice1))
¬ Conf(x,p) → Assign += (x,p);", color = red]
0 -> 1 [label = "forall x:A,p:P may (Some(choice0))
True → Conf += (x,p);", color = red]
4 [label = "Node 4:
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq())"]
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P,rt:R. (Review(t1)(xt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P. ((Conf(t1)(xt,pt) ↔ eq()) ∧
(Assign(t1)(xt,pt) ↔ eq()))"]
3 [label = "Node 3:
∀ xat:A,xbt:A,pt:P,rt:R. ((Read(t1)(xat,xbt,pt,rt) ↔ eq()) ∧
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P,rt:R. (Review(t1)(xt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P. ((Conf(t1)(xt,pt) ↔ eq()) ∧
(Assign(t1)(xt,pt) ↔ eq())) ∧
∀ xat:A,xbt:A,pt:P,rt:R,xt:A,xb:A,p:P,r:R. ((¬ Review(t1)(xt,pt,rt) ∨
Review(t2)(xt,pt,rt)) ∧
(¬ Review(t2)(xt,pt,rt) ∨
Review(t1)(xt,pt,rt)) ∧
((¬ Read(t1)(xat,xbt,pt,rt) ∧
(¬ Assign(t1)(xat,pt) ∨
¬ Review(t1)(xbt,pt,rt))) ∨
......@@ -16,59 +61,17 @@ True"]
¬ Review(t2)(xbt,pt,rt))) ∨
Read(t1)(xat,xbt,pt,rt) ∨
(Assign(t1)(xat,pt) ∧
Review(t1)(xbt,pt,rt)))) ∧
∀ xat:A,xbt:A,pt:P,rt:R,xb:A,p:P,r:R. (((¬ Read(t1)(xat,xbt,pt,rt) ∧
(¬ Assign(t1)(xat,pt) ∨
¬ Review(t1)(xbt,pt,rt))) ∨
Read(t2)(xat,xbt,pt,rt) ∨
(Assign(t2)(xat,pt) ∧
Review(t2)(xbt,pt,rt))) ∧
((¬ Read(t2)(xat,xbt,pt,rt) ∧
(¬ Assign(t2)(xat,pt) ∨
¬ Review(t2)(xbt,pt,rt))) ∨
Read(t1)(xat,xbt,pt,rt) ∨
(Assign(t1)...(21447 characters)"]
2 -> 3 [label = "forall x:A,p:P,r:R
Assign(x,p) ∧ Oracle(x,p,r) → Review += (x,p,r);", color = red]
5 -> 3 [label = "forall x:A,p:P,r:R may (Some(choice2))
Assign(x,p) → Review += (x,p,r);", color = red]
1 -> 2 [label = "forall x:A,p:P may (Some(choice1))
¬ Conf(x,p) → Assign += (x,p);", color = red]
0 -> 1 [label = "forall x:A,p:P may (Some(choice0))
True → Conf += (x,p);", color = red]
1 [label = "Node 1:
True"]
Review(t1)(xbt,pt,rt))) ∧
((¬ Review(t1)(xt,pt,rt) ∧
(¬ Assign(t1)(xt,pt) ∨
¬ choice2(t1)(xt,pt,rt)))...(53090 characters)"]
2 [label = "Node 2:
∀ xt:A,pt:P. ((Conf(t1)(xt,pt) ↔ eq()) ∧
(Assign(t1)(xt,pt) ↔ eq()))"]
3 -> 4 [label = "forall
", color = green]
4 -> 4 [label = "forall
", color = green]
5 [label = "Node 5:
∀ xat:A,xbt:A,pt:P,rt:R. ((Read(t1)(xat,xbt,pt,rt) ↔ eq()) ∧
(¬ Read(t1)(xat,xbt,pt,rt) ∨
Read(t2)(xat,xbt,pt,rt)) ∧
(¬ Read(t2)(xat,xbt,pt,rt) ∨
Read(t1)(xat,xbt,pt,rt)) ∧
((¬ Read(t1)(xat,xbt,pt,rt) ∧
(¬ Assign(t1)(xat,pt) ∨
(¬ Review(t1)(xbt,pt,rt) ∧
(¬ Assign(t1)(xbt,pt) ∨
¬ choice2(t1)(xbt,pt,rt))))) ∨
Read(t2)(xat,xbt,pt,rt) ∨
(Assign(t2)(xat,pt) ∧
(Review(t2)(xbt,pt,rt) ∨
(Assign(t2)(xbt,pt) ∧
((¬ informed(t1)(xbt) ∧
choice2(t1)(xbt,pt,rt)) ∨
(informed(t1)(xbt) ∧
choice2(t2)(xbt,pt,rt))))))) ∧
((¬ Read(t2)(xat,xbt,pt,rt) ∧
(¬ Assign(t2)(xat,pt) ∨
(¬ Review(t2)(xbt,pt,rt) ∧
(¬ Assign(t2)(xbt,pt) ∨
((informed(t1)(xbt) ∨
...(10063 characters)"]
2 [label = "Node 2:
True"]
3 -> 5 [label = "forall xa:A,xb:A,p:P,r:R
Assign(xa,p) ∧ Review(xb,p,r) → Read += (xa,xb,p,r);", color = green]
}
\ No newline at end of file
results/nonomitting/conference/conference_causal_alleq_11.dot
View file @ c9d7928e
digraph "Invariant Labelling" {
1 [label = "Node 1:
∀ xt:A,pt:P. (Conf(t1)(xt,pt) ↔ eq())"]
5 [label = "Node 5:
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P,rt:R. (Review(t1)(xt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P. ((Conf(t1)(xt,pt) ↔ eq()) ∧
(Assign(t1)(xt,pt) ↔ eq())) ∧
∀ xat:A,xbt:A,pt:P,rt:R,xt:A. ((¬ Read(t1)(xat,xbt,pt,rt) ∨
Read(t2)(xat,xbt,pt,rt)) ∧
(¬ Read(t2)(xat,xbt,pt,rt) ∨
Read(t1)(xat,xbt,pt,rt)) ∧
((¬ Review(t1)(xt,pt,rt) ∧
(¬ Assign(t1)(xt,pt) ∨
¬ choice2(t1)(xt,pt,rt))) ∨
Review(t2)(xt,pt,rt) ∨
(Assign(t2)(xt,pt) ∧
((¬ informed(t1)(xt) ∧
choice2(t1)(xt,pt,rt)) ∨
(informed(t1)(xt) ∧
choice2(t2)(xt,pt,rt))))) ∧
((¬ Review(t2)(xt,pt,rt) ∧
(¬ Assign(t2)(xt,pt) ∨
¬ informed(t1)(xt) ∨
¬ choice2(t2)(xt,pt,rt))) ∨
Review(t1)(xt,pt,rt) ∨
(Assign(t1)(xt,pt) ∧
choice2...(23593 characters)"]
0 [label = "Node 0:
True"]
5 -> 3 [label = "forall x:A,p:P,r:R may (Some(choice2))
Assign(x,p) → Review += (x,p,r);", color = green]
2 -> 3 [label = "forall x:A,p:P,r:R
Assign(x,p) ∧ Oracle(x,p,r) → Review += (x,p,r);", color = red]
1 -> 2 [label = "forall x:A,p:P may (Some(choice1))
¬ Conf(x,p) → Assign += (x,p);", color = red]
0 -> 1 [label = "forall x:A,p:P may (Some(choice0))
True → Conf += (x,p);", color = red]
4 [label = "Node 4:
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq())"]
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P,rt:R. (Review(t1)(xt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P. ((Conf(t1)(xt,pt) ↔ eq()) ∧
(Assign(t1)(xt,pt) ↔ eq()))"]
3 [label = "Node 3:
∀ xat:A,xbt:A,pt:P,rt:R. ((Read(t1)(xat,xbt,pt,rt) ↔ eq()) ∧
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P,rt:R. (Review(t1)(xt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P. ((Conf(t1)(xt,pt) ↔ eq()) ∧
(Assign(t1)(xt,pt) ↔ eq())) ∧
∀ xat:A,xbt:A,pt:P,rt:R,xt:A,xb:A,p:P,r:R. ((¬ Review(t1)(xt,pt,rt) ∨
Review(t2)(xt,pt,rt)) ∧
(¬ Review(t2)(xt,pt,rt) ∨
Review(t1)(xt,pt,rt)) ∧
((¬ Read(t1)(xat,xbt,pt,rt) ∧
(¬ Assign(t1)(xat,pt) ∨
¬ Review(t1)(xbt,pt,rt))) ∨
......@@ -18,57 +61,17 @@ True"]
¬ Review(t2)(xbt,pt,rt))) ∨
Read(t1)(xat,xbt,pt,rt) ∨
(Assign(t1)(xat,pt) ∧
Review(t1)(xbt,pt,rt)))) ∧
∀ xat:A,xbt:A,pt:P,rt:R,xb:A,p:P,r:R. (((¬ Read(t1)(xat,xbt,pt,rt) ∧
(¬ Assign(t1)(xat,pt) ∨
¬ Review(t1)(xbt,pt,rt))) ∨
Read(t2)(xat,xbt,pt,rt) ∨
(Assign(t2)(xat,pt) ∧
Review(t2)(xbt,pt,rt))) ∧
((¬ Read(t2)(xat,xbt,pt,rt) ∧
(¬ Assign(t2)(xat,pt) ∨
¬ Review(t2)(xbt,pt,rt))) ∨
Read(t1)(xat,xbt,pt,rt) ∨
(Assign(t1)...(21447 characters)"]
2 -> 3 [label = "forall x:A,p:P,r:R
Assign(x,p) ∧ Oracle(x,p,r) → Review += (x,p,r);", color = red]
1 -> 2 [label = "forall x:A,p:P may (Some(choice1))
¬ Conf(x,p) → Assign += (x,p);", color = red]
0 -> 1 [label = "forall x:A,p:P may (Some(choice0))
True → Conf += (x,p);", color = red]
1 [label = "Node 1:
True"]
Review(t1)(xbt,pt,rt))) ∧
((¬ Review(t1)(xt,pt,rt) ∧
(¬ Assign(t1)(xt,pt) ∨
¬ choice2(t1)(xt,pt,rt)))...(53090 characters)"]
2 [label = "Node 2:
∀ xt:A,pt:P. ((Conf(t1)(xt,pt) ↔ eq()) ∧
(Assign(t1)(xt,pt) ↔ eq()))"]
3 -> 4 [label = "forall
", color = green]
4 -> 4 [label = "forall
", color = green]
5 [label = "Node 5:
∀ xat:A,xbt:A,pt:P,rt:R. ((Read(t1)(xat,xbt,pt,rt) ↔ eq()) ∧
(¬ Read(t1)(xat,xbt,pt,rt) ∨
Read(t2)(xat,xbt,pt,rt)) ∧
(¬ Read(t2)(xat,xbt,pt,rt) ∨
Read(t1)(xat,xbt,pt,rt)) ∧
((¬ Read(t1)(xat,xbt,pt,rt) ∧
(¬ Assign(t1)(xat,pt) ∨
(¬ Review(t1)(xbt,pt,rt) ∧
(¬ Assign(t1)(xbt,pt) ∨
¬ choice2(t1)(xbt,pt,rt))))) ∨
Read(t2)(xat,xbt,pt,rt) ∨
(Assign(t2)(xat,pt) ∧
(Review(t2)(xbt,pt,rt) ∨
(Assign(t2)(xbt,pt) ∧
((¬ informed(t1)(xbt) ∧
choice2(t1)(xbt,pt,rt)) ∨
(informed(t1)(xbt) ∧
choice2(t2)(xbt,pt,rt))))))) ∧
((¬ Read(t2)(xat,xbt,pt,rt) ∧
(¬ Assign(t2)(xat,pt) ∨
(¬ Review(t2)(xbt,pt,rt) ∧
(¬ Assign(t2)(xbt,pt) ∨
((informed(t1)(xbt) ∨
...(10063 characters)"]
2 [label = "Node 2:
True"]
3 -> 5 [label = "forall xa:A,xb:A,p:P,r:R
Assign(xa,p) ∧ Review(xb,p,r) → Read += (xa,xb,p,r);", color = green]
}
\ No newline at end of file
results/nonomitting/conference/conference_causal_alleq_12.dot
View file @ c9d7928e
digraph "Invariant Labelling" {
1 [label = "Node 1:
∀ xt:A,pt:P. (Conf(t1)(xt,pt) ↔ eq())"]
5 [label = "Node 5:
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P,rt:R. (Review(t1)(xt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P. ((Conf(t1)(xt,pt) ↔ eq()) ∧
(Assign(t1)(xt,pt) ↔ eq())) ∧
∀ xat:A,xbt:A,pt:P,rt:R,xt:A. ((¬ Read(t1)(xat,xbt,pt,rt) ∨
Read(t2)(xat,xbt,pt,rt)) ∧
(¬ Read(t2)(xat,xbt,pt,rt) ∨
Read(t1)(xat,xbt,pt,rt)) ∧
((¬ Review(t1)(xt,pt,rt) ∧
(¬ Assign(t1)(xt,pt) ∨
¬ choice2(t1)(xt,pt,rt))) ∨
Review(t2)(xt,pt,rt) ∨
(Assign(t2)(xt,pt) ∧
((¬ informed(t1)(xt) ∧
choice2(t1)(xt,pt,rt)) ∨
(informed(t1)(xt) ∧
choice2(t2)(xt,pt,rt))))) ∧
((¬ Review(t2)(xt,pt,rt) ∧
(¬ Assign(t2)(xt,pt) ∨
¬ informed(t1)(xt) ∨
¬ choice2(t2)(xt,pt,rt))) ∨
Review(t1)(xt,pt,rt) ∨
(Assign(t1)(xt,pt) ∧
choice2...(23593 characters)"]
0 [label = "Node 0:
True"]
5 -> 3 [label = "forall x:A,p:P,r:R may (Some(choice2))
Assign(x,p) → Review += (x,p,r);", color = green]
2 [label = "Node 2:
∀ xat:A,xbt:A,pt:P,rt:R,xb:A,p:P,r:R. ((¬ Assign(t1)(xat,pt) ∨
¬ Assign(t1)(xbt,pt) ∨
¬ Oracle(t1)(xbt,pt,rt) ∨
(Assign(t2)(xat,pt) ∧
Assign(t2)(xbt,pt) ∧
((¬ Conf(t1)(xat,pt) ∧
Oracle(t1)(xbt,pt,rt)) ∨
(Conf(t1)(xat,pt) ∧
Oracle(t2)(xbt,pt,rt))))) ∧
(¬ Assign(t2)(xat,pt) ∨
¬ Assign(t2)(xbt,pt) ∨
∀ xt:A,pt:P. ((Conf(t1)(xt,pt) ↔ eq()) ∧
(Assign(t1)(xt,pt) ↔ eq())) ∧
∀ xat:A,xbt:A,pt:P,rt:R,xt:A,xb:A,p:P,r:R. ((¬ Assign(t2)(xt,pt) ∨
((Conf(t1)(xat,pt) ∨
¬ Oracle(t1)(xbt,pt,rt)) ∧
¬ Oracle(t1)(xt,pt,rt)) ∧
(¬ Conf(t1)(xat,pt) ∨
¬ Oracle(t2)(xbt,pt,rt))) ∨
(Assign(t1)(xat,pt) ∧
Assign(t1)(xbt,pt) ∧
Oracle(t1)(xbt,pt,rt))) ∧
¬ Oracle(t2)(xt,pt,rt))) ∨
(Assign(t1)(xt,pt) ∧
Oracle(t1)(xt,pt,rt))) ∧
(¬ Conf(t1)(xt,pt) ∨
Conf(t2)(xt,pt)) ∧
(¬ Conf(t2)(xt,pt) ∨
Conf(t1)(xt,pt)) ∧
(¬ Assign(t1)(xt,pt) ∨
Assign(t2)(xt,pt)) ∧
(¬ Assign(t2)(xt,pt) ∨
Assign(t1)(xt,pt)) ∧
(¬ Assign(t1)(xt,pt) ∨
¬ Oracle(t1)(xt,pt,rt) ∨
(Assign(t2)(xt,pt) ∧
((¬ Conf(t1)(xat,pt) ∧
Oracle(t1)(xt,pt,rt)) ∨
(Conf(t1)(xat,pt) ∧
Oracle(t2)(xt,pt,rt))))) ∧
(¬ Assign(t1)(xat,pt) ∨
¬ Assign(t1)(xbt,pt) ∨
¬ choice2(t1)(xbt,pt,rt) ∨
(Assign(t2)(xat,pt) ∧
((Assign(t2)(xbt,pt) ∧
((¬ Conf(t1)(xat,pt) ∧
Oracle(t1)(xbt,pt,rt)) ∨
(Conf(t1)(xa...(7281 characters)"]
0 [label = "Node 0:
True"]
5 -> 3 [label = "forall x:A,p:P,r:R may (Some(choice2))
Assign(x,p) → Review += (x,p,r);", color = green]
¬ Oracle(t1)(xbt,pt,rt) ∨
...(25865 characters)"]
2 -> 3 [label = "forall x:A,p:P,r:R
Assign(x,p) ∧ Oracle(x,p,r) → Review += (x,p,r);", color = green]
1 -> 2 [label = "forall x:A,p:P may (Some(choice1))
¬ Conf(x,p) → Assign += (x,p);", color = red]
0 -> 1 [label = "forall x:A,p:P may (Some(choice0))
True → Conf += (x,p);", color = red]
4 [label = "Node 4:
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq())"]
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P,rt:R. (Review(t1)(xt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P. ((Conf(t1)(xt,pt) ↔ eq()) ∧
(Assign(t1)(xt,pt) ↔ eq()))"]
3 [label = "Node 3:
∀ xat:A,xbt:A,pt:P,rt:R. ((Read(t1)(xat,xbt,pt,rt) ↔ eq()) ∧
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P,rt:R. (Review(t1)(xt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P. ((Conf(t1)(xt,pt) ↔ eq()) ∧
(Assign(t1)(xt,pt) ↔ eq())) ∧
∀ xat:A,xbt:A,pt:P,rt:R,xt:A,xb:A,p:P,r:R. ((¬ Review(t1)(xt,pt,rt) ∨
Review(t2)(xt,pt,rt)) ∧
(¬ Review(t2)(xt,pt,rt) ∨
Review(t1)(xt,pt,rt)) ∧
((¬ Read(t1)(xat,xbt,pt,rt) ∧
(¬ Assign(t1)(xat,pt) ∨
¬ Review(t1)(xbt,pt,rt))) ∨
......@@ -45,55 +90,14 @@ True"]
¬ Review(t2)(xbt,pt,rt))) ∨
Read(t1)(xat,xbt,pt,rt) ∨
(Assign(t1)(xat,pt) ∧
Review(t1)(xbt,pt,rt)))) ∧
∀ xat:A,xbt:A,pt:P,rt:R,xb:A,p:P,r:R. (((¬ Read(t1)(xat,xbt,pt,rt) ∧
(¬ Assign(t1)(xat,pt) ∨
¬ Review(t1)(xbt,pt,rt))) ∨
Read(t2)(xat,xbt,pt,rt) ∨
(Assign(t2)(xat,pt) ∧
Review(t2)(xbt,pt,rt))) ∧
((¬ Read(t2)(xat,xbt,pt,rt) ∧
(¬ Assign(t2)(xat,pt) ∨
¬ Review(t2)(xbt,pt,rt))) ∨
Read(t1)(xat,xbt,pt,rt) ∨
(Assign(t1)...(21447 characters)"]
2 -> 3 [label = "forall x:A,p:P,r:R
Assign(x,p) ∧ Oracle(x,p,r) → Review += (x,p,r);", color = green]
1 -> 2 [label = "forall x:A,p:P may (Some(choice1))
¬ Conf(x,p) → Assign += (x,p);", color = red]
0 -> 1 [label = "forall x:A,p:P may (Some(choice0))
True → Conf += (x,p);", color = red]
1 [label = "Node 1:
True"]
Review(t1)(xbt,pt,rt))) ∧
((¬ Review(t1)(xt,pt,rt) ∧
(¬ Assign(t1)(xt,pt) ∨
¬ choice2(t1)(xt,pt,rt)))...(53090 characters)"]
3 -> 4 [label = "forall
", color = green]
4 -> 4 [label = "forall
", color = green]
5 [label = "Node 5:
∀ xat:A,xbt:A,pt:P,rt:R. ((Read(t1)(xat,xbt,pt,rt) ↔ eq()) ∧
(¬ Read(t1)(xat,xbt,pt,rt) ∨
Read(t2)(xat,xbt,pt,rt)) ∧
(¬ Read(t2)(xat,xbt,pt,rt) ∨
Read(t1)(xat,xbt,pt,rt)) ∧
((¬ Read(t1)(xat,xbt,pt,rt) ∧
(¬ Assign(t1)(xat,pt) ∨
(¬ Review(t1)(xbt,pt,rt) ∧
(¬ Assign(t1)(xbt,pt) ∨
¬ choice2(t1)(xbt,pt,rt))))) ∨
Read(t2)(xat,xbt,pt,rt) ∨
(Assign(t2)(xat,pt) ∧
(Review(t2)(xbt,pt,rt) ∨
(Assign(t2)(xbt,pt) ∧
((¬ informed(t1)(xbt) ∧
choice2(t1)(xbt,pt,rt)) ∨
(informed(t1)(xbt) ∧
choice2(t2)(xbt,pt,rt))))))) ∧
((¬ Read(t2)(xat,xbt,pt,rt) ∧
(¬ Assign(t2)(xat,pt) ∨
(¬ Review(t2)(xbt,pt,rt) ∧
(¬ Assign(t2)(xbt,pt) ∨
((informed(t1)(xbt) ∨
...(10063 characters)"]
3 -> 5 [label = "forall xa:A,xb:A,p:P,r:R
Assign(xa,p) ∧ Review(xb,p,r) → Read += (xa,xb,p,r);", color = green]
}
\ No newline at end of file
results/nonomitting/conference/conference_causal_alleq_13.dot
View file @ c9d7928e
digraph "Invariant Labelling" {
2 [label = "Node 2:
∀ xat:A,xbt:A,pt:P,rt:R,xb:A,p:P,r:R. ((¬ Assign(t1)(xat,pt) ∨
¬ Assign(t1)(xbt,pt) ∨
¬ Oracle(t1)(xbt,pt,rt) ∨
(Assign(t2)(xat,pt) ∧
Assign(t2)(xbt,pt) ∧
((¬ Conf(t1)(xat,pt) ∧
Oracle(t1)(xbt,pt,rt)) ∨
(Conf(t1)(xat,pt) ∧
Oracle(t2)(xbt,pt,rt))))) ∧
(¬ Assign(t2)(xat,pt) ∨
¬ Assign(t2)(xbt,pt) ∨
((Conf(t1)(xat,pt) ∨
¬ Oracle(t1)(xbt,pt,rt)) ∧
(¬ Conf(t1)(xat,pt) ∨
¬ Oracle(t2)(xbt,pt,rt))) ∨
(Assign(t1)(xat,pt) ∧
Assign(t1)(xbt,pt) ∧