Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Christian Müller
NIWO
Commits
405eec83
Commit
405eec83
authored
Jan 22, 2019
by
Christian Müller
Browse files
fix a few things
parent
9a99c60c
Changes
373
Expand all
Hide whitespace changes
Inline
Side-by-side
examples/nonomitting/conference_stubborn.spec
0 → 100644
View file @
405eec83
Workflow
forallmay x:A,p:P
True → Conf += (x,p)
forallmay x:A,p:P
!Conf(x,p) → Assign += (x,p)
forall x:A,p:P,r:R
(Assign(x,p) ∧ Oracle(x,p,r)) → Review += (x,p,r)
loop {
forall xa:A,xb:A,p:P,r:R (Assign(xa,p) ∧ Review(xb,p,r)) → Read += (xa,xb,p,r)
forallmay x:A,p:P,r:R (Assign(x,p)) → Review += (x,p,r)
}
Declassify
Oracle(x:A,p:P,r:R): ¬ Conf(xat:A,p:P)
Target
Read(xat:A, xbt:A, pt:P, rt:R)
results/nonomitting/conference/conference_causal_alleq.invariants
0 → 100644
View file @
405eec83
This diff is collapsed.
Click to expand it.
results/nonomitting/conference/conference_causal_alleq.metrics
0 → 100644
View file @
405eec83
Name: nonomitting/conference
Description: alleq
Invariant:
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ 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
results/nonomitting/conference/conference_causal_alleq_0.dot
0 → 100644
View file @
405eec83
digraph
"Invariant Labelling"
{
3
[
label
=
"Node 3:
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq())"
]
0
[
label
=
"Node 0:
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
=
red
]
3
->
4
[
label
=
"forall
"
,
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"
]
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())"
]
}
\ No newline at end of file
results/nonomitting/conference/conference_causal_alleq_0.png
0 → 100644
View file @
405eec83
89.2 KB
results/nonomitting/conference/conference_causal_alleq_1.dot
0 → 100644
View file @
405eec83
digraph
"Invariant Labelling"
{
3
[
label
=
"Node 3:
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq())"
]
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
]
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
=
red
]
3
->
4
[
label
=
"forall
"
,
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"
]
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())"
]
}
\ No newline at end of file
results/nonomitting/conference/conference_causal_alleq_1.png
0 → 100644
View file @
405eec83
89.4 KB
results/nonomitting/conference/conference_causal_alleq_10.dot
0 → 100644
View file @
405eec83
digraph
"Invariant Labelling"
{
0
[
label
=
"Node 0:
True"
]
4
[
label
=
"Node 4:
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq())"
]
3
[
label
=
"Node 3:
∀ xat:A,xbt:A,pt:P,rt:R. ((Read(t1)(xat,xbt,pt,rt) ↔ eq()) ∧
((¬ 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)(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"
]
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_10.png
0 → 100644
View file @
405eec83
271 KB
results/nonomitting/conference/conference_causal_alleq_11.dot
0 → 100644
View file @
405eec83
digraph
"Invariant Labelling"
{
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
]
4
[
label
=
"Node 4:
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq())"
]
3
[
label
=
"Node 3:
∀ xat:A,xbt:A,pt:P,rt:R. ((Read(t1)(xat,xbt,pt,rt) ↔ eq()) ∧
((¬ 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)(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"
]
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.png
0 → 100644
View file @
405eec83
273 KB
results/nonomitting/conference/conference_causal_alleq_12.dot
0 → 100644
View file @
405eec83
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) ∧
Oracle(t1)(xbt,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
]
4
[
label
=
"Node 4:
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq())"
]
3
[
label
=
"Node 3:
∀ xat:A,xbt:A,pt:P,rt:R. ((Read(t1)(xat,xbt,pt,rt) ↔ eq()) ∧
((¬ 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)(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"
]
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_12.png
0 → 100644
View file @
405eec83
368 KB
results/nonomitting/conference/conference_causal_alleq_13.dot
0 → 100644
View file @
405eec83
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) ∧
Oracle(t1)(xbt,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)"
]
1
->
2
[
label
=
"forall x:A,p:P may (Some(choice1))
¬ Conf(x,p) → Assign += (x,p);"
,
color
=
green
]
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
]
4
[
label
=
"Node 4:
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq())"
]
3
[
label
=
"Node 3:
∀ xat:A,xbt:A,pt:P,rt:R. ((Read(t1)(xat,xbt,pt,rt) ↔ eq()) ∧
((¬ 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)(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)"
]
1
[
label
=
"Node 1:
∀ xat:A,xbt:A,pt:P,rt:R,xb:A,p:P,r:R. ((Conf(t1)(xat,pt) ∨
¬ choice1(t1)(xat,pt) ∨
Conf(t1)(xbt,pt) ∨
¬ choice1(t1)(xbt,pt) ∨
¬ Oracle(t1)(xbt,pt,rt) ∨
(¬ Conf(t2)(xat,pt) ∧
((¬ informed(t1)(xat) ∧
choice1(t1)(xat,pt)) ∨
(informed(t1)(xat) ∧
choice1(t2)(xat,pt))) ∧
¬ Conf(t2)(xbt,pt) ∧
((¬ informed(t1)(xbt) ∧
choice1(t1)(xbt,pt)) ∨
(informed(t1)(xbt) ∧
choice1(t2)(xbt,pt))))) ∧
(Conf(t2)(xat,pt) ∨
((informed(t1)(xat) ∨
¬ choice1(t1)(xat,pt)) ∧
(¬ informed(t1)(xat) ∨
¬ choice1(t2)(xat,pt))) ∨
Conf(t2)(xbt,pt) ∨
((informed(t1)(xbt) ∨
¬ choice1(t1)(xbt,pt)) ∧
(¬ informed(t1)(xbt) ∨
¬ choice1(t2)(xbt,pt))) ∨
((Conf(t1)(xat,pt) ∨
¬ O...(12836 characters)"
]
2
->
3
[
label
=
"forall x:A,p:P,r:R
Assign(x,p) ∧ Oracle(x,p,r) → Review += (x,p,r);"
,
color
=
green
]
0
->
1
[
label
=
"forall x:A,p:P may (Some(choice0))
True → Conf += (x,p);"
,
color
=
red
]
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.png
0 → 100644
View file @
405eec83
520 KB
results/nonomitting/conference/conference_causal_alleq_2.dot
0 → 100644
View file @
405eec83
digraph
"Invariant Labelling"
{
3
[
label
=
"Node 3:
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq())"
]
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
]
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
=
red
]
3
->
4
[
label
=
"forall
"
,
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"
]
4
->
4
[
label
=
"forall
"
,
color
=
green
]
2
[
label
=
"Node 2:
True"
]
5
[
label
=
"Node 5:
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq())"
]
}
\ No newline at end of file
results/nonomitting/conference/conference_causal_alleq_2.png
0 → 100644
View file @
405eec83
89.4 KB
results/nonomitting/conference/conference_causal_alleq_3.dot
0 → 100644
View file @
405eec83
digraph
"Invariant Labelling"
{
3
[
label
=
"Node 3:
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq())"
]
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
]
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
=
red
]
4
[
label
=
"Node 4:
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq())"
]
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"
]
3
->
4
[
label
=
"forall
"
,
color
=
green
]
4
->
4
[
label
=
"forall
"
,
color
=
green
]
2
[
label
=
"Node 2:
True"
]
5
[
label
=
"Node 5:
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq())"
]
}
\ No newline at end of file
results/nonomitting/conference/conference_causal_alleq_3.png
0 → 100644
View file @
405eec83
89.5 KB
results/nonomitting/conference/conference_causal_alleq_4.dot
0 → 100644
View file @
405eec83
digraph
"Invariant Labelling"
{
0
[
label
=
"Node 0:
True"
]
4
[
label
=
"Node 4:
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq())"
]
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"
]
3
->
4
[
label
=
"forall
"
,
color
=
green
]
4
->
4
[
label
=
"forall
"
,
color
=
green
]
2
[
label
=
"Node 2:
True"
]
3
[
label
=
"Node 3:
∀ xat:A,xbt:A,pt:P,rt:R. ((Read(t1)(xat,xbt,pt,rt) ↔ eq()) ∧
((¬ 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)(xat,pt) ∧
Review(t1)(xbt,pt,rt))))"
]
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
]
5
[
label
=
"Node 5:
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq())"
]
}
\ No newline at end of file
Prev
1
2
3
4
5
…
19
Next
Write
Preview