conference_stubborn_stubborn_alleq_0.dot 991 Bytes
Newer Older
Christian Müller's avatar
Christian Müller committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
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())"]
}