Skip to content
GitLab
Commit 34ba7fdf authored by Christian Müller's avatar Christian Müller
Browse files

pres results

parent a650859a
Hide whitespace changes
Inline Side-by-side
examples/omitting/notebook_unsafe.spec 0 → 100644
View file @ 34ba7fdf
Workflow
loop {
choose {
forall x:User, y:User, i:Info
Written(i, y) → Read += (x, i)
} {
forall x:User, i:Info
Oracle(i, x) → Written += (i, x)
}
}
Target
Read(u:User, info:Info)
Causality
ac:User
results/nonomitting/notebook/notebook_causal_alleq.invariants
View file @ 34ba7fdf
......@@ -2,7 +2,183 @@ Node 0:
True
Node 1:
True
∀ u:User,info:Info. ((Read(t1)(u,info) ↔ eq()) ∧
((¬ Read(t1)(u,info) ∧
(¬ Written(t1)(info,u) ∨
¬ choice0(t1)(u,info))) ∨
Read(t2)(u,info) ∨
(Written(t2)(info,u) ∧
((¬ informed(t1)(u) ∧
choice0(t1)(u,info)) ∨
(informed(t1)(u) ∧
choice0(t2)(u,info))))) ∧
((¬ Read(t2)(u,info) ∧
(¬ Written(t2)(info,u) ∨
((informed(t1)(u) ∨
¬ choice0(t1)(u,info)) ∧
(¬ informed(t1)(u) ∨
¬ choice0(t2)(u,info))))) ∨
Read(t1)(u,info) ∨
(Written(t1)(info,u) ∧
choice0(t1)(u,info)))) ∧
∀ u:User,info:Info,i:Info. (((¬ Read(t1)(u,info) ∧
(¬ Written(t1)(info,u) ∨
¬ choice0(t1)(u,info))) ∨
Read(t2)(u,info) ∨
(Written(t2)(info,u) ∧
((¬ informed(t1)(u) ∧
choice0(t1)(u,info)) ∨
(informed(t1)(u) ∧
choice0(t2)(u,info))))) ∧
((¬ Read(t2)(u,info) ∧
(¬ Written(t2)(info,u) ∨
((informed(t1)(u) ∨
¬ choice0(t1)(u,info)) ∧
(¬ informed(t1)(u) ∨
¬ choice0(t2)(u,info))))) ∨
Read(t1)(u,info) ∨
(Written(t1)(info,u) ∧
choice0(t1)(u,info))) ∧
(¬ Written(t2)(info,u) ∨
(((¬ Read(t1)(u,i) ∧
(¬ Written(t1)(i,u) ∨
¬ choice0(t1)(u,i))) ∨
Read(t2)(u,i) ∨
(Written(t2)(i,u) ∧
¬ informed(t1)(u) ∧
choice0(t1)(u,i))) ∧
((¬ Read(t2)(u,i) ∧
(¬ Written(t2)(i,u) ∨
¬ choice0(t1)(u,i))) ∨
Read(t1)(u,i) ∨
(Written(t1)(i,u) ∧
choice0(t1)(u,i)))) ∨
¬ choice0(t2)(u,info) ∨
Read(t1)(u,info) ∨
choice0(t1)(u,info)) ∧
(¬ Read(t1)(u,info) ∨
Read(t2)(u,info)) ∧
(¬ Read(t2)(u,info) ∨
Read(t1)(u,info)) ∧
((¬ Read(t1)(u,info) ∧
((¬ Written(t1)(info,u) ∧
¬ Oracle(t1)(u,info)) ∨
¬ choice0(t1)(u,info))) ∨
Read(t2)(u,info) ∨
((Written(t2)(info,u) ∨
(Written(t1)(info,u) ∧
Oracle(t1)(u,info)) ∨
(¬ Written(t1)(info,u) ∧
Oracle(t2)(u,info))) ∧
((¬ informed(t1)(u) ∧
choice0(t1)(u,info)) ∨
(informed(t1)(u) ∧
choice0(t2)(u,info))))) ∧
((¬ Read(t2)(u,info) ∧
((¬ Written(t2)(info,u) ∧
(¬ Written(t1)(info,u) ∨
¬ Oracle(t1)(u,info)) ∧
(Written(t1)(info,u) ∨
¬ Oracle(t2)(u,info))) ∨
((informed(t1)(u) ∨
¬ choice0(t1)(u,info)) ∧
(¬ informed(t1)(u) ∨
¬ choice0(t2)(u,info))))) ∨
Read(t1)(u,info) ∨
((Written(t1)(info,u) ∨
Oracle(t1)(u,info)) ∧
choice0(t1)(u,info))) ∧
((¬ Written(t2)(info,u) ∧
(¬ Written(t1)(info,u) ∨
¬ Oracle(t1)(u,info)) ∧
(Written(t1)(info,u) ∨
¬ Oracle(t2)(u,info))) ∨
(((¬ Read(t1)(u,i) ∧
((¬ Written(t1)(i,u) ∧
¬ Oracle(t1)(u,i)) ∨
¬ choice0(t1)(u,i))) ∨
Read(t2)(u,i) ∨
((Written(t2)(i,u) ∨
(Written(t1)(i,u) ∧
Oracle(t1)(u,i)) ∨
(¬ Written(t1)(i,u) ∧
Oracle(t2)(u,i))) ∧
choice0(t1)(u,i))) ∧
((¬ Read(t2)(u,i) ∧
((¬ Written(t2)(i,u) ∧
(Written(t1)(i,u) ∨
¬ Oracle(t2)(u,i))) ∨
¬ choice0(t1)(u,i))) ∨
Read(t1)(u,i) ∨
((Written(t1)(i,u) ∨
Oracle(t1)(u,i)) ∧
choice0(t1)(u,i)))) ∨
¬ choice0(t2)(u,info) ∨
Read(t1)(u,info) ∨
choice0(t1)(u,info)))
Node 2:
∀ xt:User,it:Info. (Read(t1)(xt,it) ↔ eq())
∀ u:User,info:Info. (Read(t1)(u,info) ↔ eq())
Node 3:
∀ u:User,info:Info. ((Read(t1)(u,info) ↔ eq()) ∧
(¬ Read(t1)(u,info) ∨
Read(t2)(u,info)) ∧
(¬ Read(t2)(u,info) ∨
Read(t1)(u,info)) ∧
((¬ Read(t1)(u,info) ∧
(¬ Written(t1)(info,u) ∨
¬ choice0(t1)(u,info))) ∨
Read(t2)(u,info) ∨
(Written(t2)(info,u) ∧
((¬ informed(t1)(u) ∧
choice0(t1)(u,info)) ∨
(informed(t1)(u) ∧
choice0(t2)(u,info))))) ∧
((¬ Read(t2)(u,info) ∧
(¬ Written(t2)(info,u) ∨
((informed(t1)(u) ∨
¬ choice0(t1)(u,info)) ∧
(¬ informed(t1)(u) ∨
¬ choice0(t2)(u,info))))) ∨
Read(t1)(u,info) ∨
(Written(t1)(info,u) ∧
choice0(t1)(u,info)))) ∧
∀ u:User,info:Info,i:Info. ((¬ Read(t1)(u,info) ∨
Read(t2)(u,info)) ∧
(¬ Read(t2)(u,info) ∨
Read(t1)(u,info)) ∧
((¬ Read(t1)(u,info) ∧
(¬ Written(t1)(info,u) ∨
¬ choice0(t1)(u,info))) ∨
Read(t2)(u,info) ∨
(Written(t2)(info,u) ∧
((¬ informed(t1)(u) ∧
choice0(t1)(u,info)) ∨
(informed(t1)(u) ∧
choice0(t2)(u,info))))) ∧
((¬ Read(t2)(u,info) ∧
(¬ Written(t2)(info,u) ∨
((informed(t1)(u) ∨
¬ choice0(t1)(u,info)) ∧
(¬ informed(t1)(u) ∨
¬ choice0(t2)(u,info))))) ∨
Read(t1)(u,info) ∨
(Written(t1)(info,u) ∧
choice0(t1)(u,info))) ∧
(¬ Written(t2)(info,u) ∨
(((¬ Read(t1)(u,i) ∧
(¬ Written(t1)(i,u) ∨
¬ choice0(t1)(u,i))) ∨
Read(t2)(u,i) ∨
(Written(t2)(i,u) ∧
choice0(t1)(u,i))) ∧
((¬ Read(t2)(u,i) ∧
(¬ Written(t2)(i,u) ∨
¬ choice0(t1)(u,i))) ∨
Read(t1)(u,i) ∨
(Written(t1)(i,u) ∧
choice0(t1)(u,i)))) ∨
¬ choice0(t2)(u,info) ∨
Read(t1)(u,info) ∨
choice0(t1)(u,info)))
results/nonomitting/notebook/notebook_causal_alleq.metrics
View file @ 34ba7fdf
Name: nonomitting/notebook
Description: alleq
Invariant: ∀ xt:User,it:Info. (Read(t1)(xt,it) ↔ Read(t2)(xt,it))
Invariant: ∀ u:User,info:Info. (Read(t1)(u,info) ↔ Read(t2)(u,info))
Model: causal
Result: inductive
WF size: 4
Time: 60 ms
Proof steps: 6
Strengthenings: 0
Largest Inv: 4
Average Inv: 2
\ No newline at end of file
Result: not inductive
WF size: 5
Time: 458 ms
Proof steps: 12
Strengthenings: 5
Largest Inv: 288
Average Inv: 112
\ No newline at end of file
results/nonomitting/notebook/notebook_causal_alleq_0.dot
View file @ 34ba7fdf
digraph "Invariant Labelling" {
0 [label = "Node 0:
True"]
2 [label = "Node 2:
∀ xt:User,it:Info. (Read(t1)(xt,it) ↔ eq())"]
0 -> 2 [label = "forall x:User,i:Info may (Some(choice0))
1 -> 3 [label = "forall x:User,i:Info may (Some(choice0))
Written(i,x) → Read += (x,i);", color = red]
1 [label = "Node 1:
2 -> 2 [label = "forall
", color = red]
0 [label = "Node 0:
True"]
1 -> 1 [label = "forall
3 -> 1 [label = "forall
", color = red]
0 -> 1 [label = "forall
3 [label = "Node 3:
∀ u:User,info:Info. (Read(t1)(u,info) ↔ eq())"]
1 [label = "Node 1:
∀ u:User,info:Info. (Read(t1)(u,info) ↔ eq())"]
1 -> 2 [label = "forall
", color = red]
0 -> 0 [label = "forall x:User,i:Info
2 [label = "Node 2:
∀ u:User,info:Info. (Read(t1)(u,info) ↔ eq())"]
1 -> 1 [label = "forall x:User,i:Info
Oracle(i,x) → Written += (i,x);", color = red]
2 -> 0 [label = "forall
0 -> 1 [label = "forall
", color = red]
}
\ No newline at end of file
results/nonomitting/notebook/notebook_causal_alleq_1.dot
View file @ 34ba7fdf
digraph "Invariant Labelling" {
1 -> 3 [label = "forall x:User,i:Info may (Some(choice0))
Written(i,x) → Read += (x,i);", color = red]
2 -> 2 [label = "forall
", color = red]
0 [label = "Node 0:
True"]
2 [label = "Node 2:
∀ xt:User,it:Info. (Read(t1)(xt,it) ↔ eq())"]
0 -> 2 [label = "forall x:User,i:Info may (Some(choice0))
Written(i,x) → Read += (x,i);", color = red]
3 [label = "Node 3:
∀ u:User,info:Info. (Read(t1)(u,info) ↔ eq())"]
1 [label = "Node 1:
True"]
1 -> 1 [label = "forall
∀ u:User,info:Info. (Read(t1)(u,info) ↔ eq())"]
1 -> 2 [label = "forall
", color = red]
2 -> 0 [label = "forall
", color = green]
2 [label = "Node 2:
∀ u:User,info:Info. (Read(t1)(u,info) ↔ eq())"]
1 -> 1 [label = "forall x:User,i:Info
Oracle(i,x) → Written += (i,x);", color = red]
0 -> 1 [label = "forall
", color = red]
0 -> 0 [label = "forall x:User,i:Info
Oracle(i,x) → Written += (i,x);", color = red]
3 -> 1 [label = "forall
", color = green]
}
\ No newline at end of file
results/nonomitting/notebook/notebook_causal_alleq_10.dot 0 → 100644
View file @ 34ba7fdf
digraph "Invariant Labelling" {
1 -> 3 [label = "forall x:User,i:Info may (Some(choice0))
Written(i,x) → Read += (x,i);", color = green]
0 [label = "Node 0:
True"]
3 [label = "Node 3:
∀ u:User,info:Info. ((Read(t1)(u,info) ↔ eq()) ∧
(¬ Read(t1)(u,info) ∨
Read(t2)(u,info)) ∧
(¬ Read(t2)(u,info) ∨
Read(t1)(u,info)) ∧
((¬ Read(t1)(u,info) ∧
(¬ Written(t1)(info,u) ∨
¬ choice0(t1)(u,info))) ∨
Read(t2)(u,info) ∨
(Written(t2)(info,u) ∧
((¬ informed(t1)(u) ∧
choice0(t1)(u,info)) ∨
(informed(t1)(u) ∧
choice0(t2)(u,info))))) ∧
((¬ Read(t2)(u,info) ∧
(¬ Written(t2)(info,u) ∨
((informed(t1)(u) ∨
¬ choice0(t1)(u,info)) ∧
(¬ informed(t1)(u) ∨
¬ choice0(t2)(u,info))))) ∨
Read(t1)(u,info) ∨
(Written(t1)(info,u) ∧
choice0(t1)(u,info)))) ∧
∀ u:User,info:Info,i:Info. ((¬ Read(t1)(u,info) ∨
Read(t2)(u,info)) ∧
(¬ Read(t2)(u,info) ∨
Read(t1)(u,info)...(1795 characters)"]
1 -> 2 [label = "forall
", color = red]
1 [label = "Node 1:
∀ u:User,info:Info. ((Read(t1)(u,info) ↔ eq()) ∧
((¬ Read(t1)(u,info) ∧
(¬ Written(t1)(info,u) ∨
¬ choice0(t1)(u,info))) ∨
Read(t2)(u,info) ∨
(Written(t2)(info,u) ∧
((¬ informed(t1)(u) ∧
choice0(t1)(u,info)) ∨
(informed(t1)(u) ∧
choice0(t2)(u,info))))) ∧
((¬ Read(t2)(u,info) ∧
(¬ Written(t2)(info,u) ∨
((informed(t1)(u) ∨
¬ choice0(t1)(u,info)) ∧
(¬ informed(t1)(u) ∨
¬ choice0(t2)(u,info))))) ∨
Read(t1)(u,info) ∨
(Written(t1)(info,u) ∧
choice0(t1)(u,info)))) ∧
∀ u:User,info:Info,i:Info. (((¬ Read(t1)(u,info) ∧
(¬ Written(t1)(info,u) ∨
¬ choice0(t1)(u,info))) ∨
Read(t2)(u,info) ∨
(Written(t2)(info,u) ∧
((¬ informed(t1)(u) ∧
choice0(t1...(3461 characters)"]
2 [label = "Node 2:
∀ u:User,info:Info. (Read(t1)(u,info) ↔ eq())"]
0 -> 1 [label = "forall
", color = red]
2 -> 2 [label = "forall
", color = green]
1 -> 1 [label = "forall x:User,i:Info
Oracle(i,x) → Written += (i,x);", color = green]
3 -> 1 [label = "forall
", color = green]
}
\ No newline at end of file
results/nonomitting/notebook/notebook_causal_alleq_11.dot 0 → 100644
View file @ 34ba7fdf
digraph "Invariant Labelling" {
1 -> 3 [label = "forall x:User,i:Info may (Some(choice0))
Written(i,x) → Read += (x,i);", color = green]
0 [label = "Node 0:
True"]
3 [label = "Node 3:
∀ u:User,info:Info. ((Read(t1)(u,info) ↔ eq()) ∧
(¬ Read(t1)(u,info) ∨
Read(t2)(u,info)) ∧
(¬ Read(t2)(u,info) ∨
Read(t1)(u,info)) ∧
((¬ Read(t1)(u,info) ∧
(¬ Written(t1)(info,u) ∨
¬ choice0(t1)(u,info))) ∨
Read(t2)(u,info) ∨
(Written(t2)(info,u) ∧
((¬ informed(t1)(u) ∧
choice0(t1)(u,info)) ∨
(informed(t1)(u) ∧
choice0(t2)(u,info))))) ∧
((¬ Read(t2)(u,info) ∧
(¬ Written(t2)(info,u) ∨
((informed(t1)(u) ∨
¬ choice0(t1)(u,info)) ∧
(¬ informed(t1)(u) ∨
¬ choice0(t2)(u,info))))) ∨
Read(t1)(u,info) ∨
(Written(t1)(info,u) ∧
choice0(t1)(u,info)))) ∧
∀ u:User,info:Info,i:Info. ((¬ Read(t1)(u,info) ∨
Read(t2)(u,info)) ∧
(¬ Read(t2)(u,info) ∨
Read(t1)(u,info)...(1795 characters)"]
1 [label = "Node 1:
∀ u:User,info:Info. ((Read(t1)(u,info) ↔ eq()) ∧
((¬ Read(t1)(u,info) ∧
(¬ Written(t1)(info,u) ∨
¬ choice0(t1)(u,info))) ∨
Read(t2)(u,info) ∨
(Written(t2)(info,u) ∧
((¬ informed(t1)(u) ∧
choice0(t1)(u,info)) ∨
(informed(t1)(u) ∧
choice0(t2)(u,info))))) ∧
((¬ Read(t2)(u,info) ∧
(¬ Written(t2)(info,u) ∨
((informed(t1)(u) ∨
¬ choice0(t1)(u,info)) ∧
(¬ informed(t1)(u) ∨
¬ choice0(t2)(u,info))))) ∨
Read(t1)(u,info) ∨
(Written(t1)(info,u) ∧
choice0(t1)(u,info)))) ∧
∀ u:User,info:Info,i:Info. (((¬ Read(t1)(u,info) ∧
(¬ Written(t1)(info,u) ∨
¬ choice0(t1)(u,info))) ∨
Read(t2)(u,info) ∨
(Written(t2)(info,u) ∧
((¬ informed(t1)(u) ∧
choice0(t1...(3461 characters)"]
2 [label = "Node 2:
∀ u:User,info:Info. (Read(t1)(u,info) ↔ eq())"]
1 -> 2 [label = "forall
", color = green]
0 -> 1 [label = "forall
", color = red]
2 -> 2 [label = "forall
", color = green]
1 -> 1 [label = "forall x:User,i:Info
Oracle(i,x) → Written += (i,x);", color = green]
3 -> 1 [label = "forall
", color = green]
}
\ No newline at end of file
results/nonomitting/notebook/notebook_causal_alleq_2.dot
View file @ 34ba7fdf
digraph "Invariant Labelling" {
1 -> 3 [label = "forall x:User,i:Info may (Some(choice0))
Written(i,x) → Read += (x,i);", color = red]
0 [label = "Node 0:
True"]
1 -> 1 [label = "forall
", color = green]
2 [label = "Node 2:
∀ xt:User,it:Info. (Read(t1)(xt,it) ↔ eq())"]
0 -> 2 [label = "forall x:User,i:Info may (Some(choice0))
Written(i,x) → Read += (x,i);", color = red]
3 [label = "Node 3:
∀ u:User,info:Info. (Read(t1)(u,info) ↔ eq())"]
1 [label = "Node 1:
True"]
2 -> 0 [label = "forall
", color = green]
0 -> 1 [label = "forall
∀ u:User,info:Info. (Read(t1)(u,info) ↔ eq())"]
1 -> 2 [label = "forall
", color = red]
0 -> 0 [label = "forall x:User,i:Info
2 [label = "Node 2:
∀ u:User,info:Info. (Read(t1)(u,info) ↔ eq())"]
1 -> 1 [label = "forall x:User,i:Info
Oracle(i,x) → Written += (i,x);", color = red]
0 -> 1 [label = "forall
", color = red]
2 -> 2 [label = "forall
", color = green]
3 -> 1 [label = "forall
", color = green]
}
\ No newline at end of file
results/nonomitting/notebook/notebook_causal_alleq_3.dot
View file @ 34ba7fdf
digraph "Invariant Labelling" {
1 -> 3 [label = "forall x:User,i:Info may (Some(choice0))
Written(i,x) → Read += (x,i);", color = green]
0 [label = "Node 0:
True"]
0 -> 0 [label = "forall x:User,i:Info
Oracle(i,x) → Written += (i,x);", color = green]
1 -> 1 [label = "forall
", color = green]
3 -> 1 [label = "forall
", color = red]
3 [label = "Node 3:
∀ u:User,info:Info. (Read(t1)(u,info) ↔ eq())"]
1 -> 2 [label = "forall
", color = red]
2 [label = "Node 2:
∀ xt:User,it:Info. (Read(t1)(xt,it) ↔ eq())"]
0 -> 2 [label = "forall x:User,i:Info may (Some(choice0))
Written(i,x) → Read += (x,i);", color = red]
1 [label = "Node 1:
True"]
2 -> 0 [label = "forall
", color = green]
∀ u:User,info:Info. (Read(t1)(u,info) ↔ eq())"]
1 -> 1 [label = "forall x:User,i:Info
Oracle(i,x) → Written += (i,x);", color = red]
0 -> 1 [label = "forall
", color = red]
2 -> 2 [label = "forall
", color = green]
1 [label = "Node 1:
∀ u:User,info:Info. ((Read(t1)(u,info) ↔ eq()) ∧
((¬ Read(t1)(u,info) ∧
(¬ Written(t1)(info,u) ∨
¬ choice0(t1)(u,info))) ∨
Read(t2)(u,info) ∨
(Written(t2)(info,u) ∧
((¬ informed(t1)(u) ∧
choice0(t1)(u,info)) ∨
(informed(t1)(u) ∧
choice0(t2)(u,info))))) ∧
((¬ Read(t2)(u,info) ∧
(¬ Written(t2)(info,u) ∨
((informed(t1)(u) ∨
¬ choice0(t1)(u,info)) ∧
(¬ informed(t1)(u) ∨
¬ choice0(t2)(u,info))))) ∨
Read(t1)(u,info) ∨
(Written(t1)(info,u) ∧
choice0(t1)(u,info))))"]
}
\ No newline at end of file
results/nonomitting/notebook/notebook_causal_alleq_4.dot
View file @ 34ba7fdf
digraph "Invariant Labelling" {
0 -> 1 [label = "forall
", color = green]
1 -> 3 [label = "forall x:User,i:Info may (Some(choice0))
Written(i,x) → Read += (x,i);", color = red]
0 [label = "Node 0:
True"]
0 -> 0 [label = "forall x:User,i:Info
Oracle(i,x) → Written += (i,x);", color = green]
1 -> 1 [label = "forall
", color = green]
1 -> 2 [label = "forall
", color = red]
3 [label = "Node 3:
∀ u:User,info:Info. ((Read(t1)(u,info) ↔ eq()) ∧
(¬ Read(t1)(u,info) ∨
Read(t2)(u,info)) ∧
(¬ Read(t2)(u,info) ∨
Read(t1)(u,info)) ∧
((¬ Read(t1)(u,info) ∧
(¬ Written(t1)(info,u) ∨
¬ choice0(t1)(u,info))) ∨
Read(t2)(u,info) ∨
(Written(t2)(info,u) ∧
((¬ informed(t1)(u) ∧
choice0(t1)(u,info)) ∨
(informed(t1)(u) ∧
choice0(t2)(u,info))))) ∧
((¬ Read(t2)(u,info) ∧
(¬ Written(t2)(info,u) ∨
((informed(t1)(u) ∨
¬ choice0(t1)(u,info)) ∧
(¬ informed(t1)(u) ∨
¬ choice0(t2)(u,info))))) ∨
Read(t1)(u,info) ∨
(Written(t1)(info,u) ∧
choice0(t1)(u,info))))"]
2 [label = "Node 2:
∀ xt:User,it:Info. (Read(t1)(xt,it) ↔ eq())"]
0 -> 2 [label = "forall x:User,i:Info may (Some(choice0))
Written(i,x) → Read += (x,i);", color = red]
∀ u:User,info:Info. (Read(t1)(u,info) ↔ eq())"]
1 -> 1 [label = "forall x:User,i:Info
Oracle(i,x) → Written += (i,x);", color = red]
0 -> 1 [label = "forall
", color = red]
2 -> 2 [label = "forall
", color = green]