conference_stubborn_stubborn_alleq_0.dot 991 Bytes
 Christian Müller committed Jan 22, 2019 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())"] }``````