conference_stubborn_stubborn_alleq_9.dot 3.82 KB
 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 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 ``````digraph "Invariant Labelling" { 1 [label = "Node 1: ∀ xat:A,xbt:A,pt:P,rt:R. ((Conf(t2)(xat,pt) ∨ Conf(t2)(xbt,pt) ∨ ¬ Conf(t1)(xbt,pt)) ∧ (Conf(t2)(xat,pt) ∨ Conf(t2)(xbt,pt) ∨ ¬ Conf(t1)(xat,pt) ∨ ¬ Oracle(t2)(xbt,pt,rt)) ∧ (Conf(t1)(xat,pt) ∨ Conf(t1)(xbt,pt) ∨ Oracle(t1)(xbt,pt,rt) ∨ Oracle(t2)(xbt,pt,rt) ∨ ¬ Conf(t2)(xat,pt) ∨ ¬ Conf(t2)(xbt,pt)))"] 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())"] 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 [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))) ∧ ((¬ Read(t1)(xat,xbt,pt,rt) ∧ (¬ Assign(t1)(xat,pt) ∨ ¬ Review(t1)(xbt,pt,rt))) ∨ Read(t2)(xat,xbt,pt,rt) ∨ 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))) ∧ (Assign(t1)(xat,pt) ∨ ...(1705 characters)"] 2 [label = "Node 2: ∀ xat:A,xbt:A,pt:P,rt:R. ((¬ Assign(t1)(xat,pt) ∨ ¬ Assign(t1)(xbt,pt) ∨ ¬ Oracle(t1)(xbt,pt,rt) ∨ (¬ 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) ∧ ((¬ Conf(t1)(xat,pt) ∧ Oracle(t1)(xbt,pt,rt)) ∨ (Conf(t1)(xat,pt) ∧ Oracle(t1)(xbt,pt,rt))))) ∧ (Assign(t1)(xat,pt) ∨ ¬ Assign(t2)(xat,pt) ∨ ¬ Assign(t2)(xbt,pt)) ∧ (Assign(t1)(xbt,pt) ∨ (Assign(t1)(xat,pt) ∧ Assign(t1)(xbt,pt) ∧ ((¬ Conf(t1)(xat,pt) ∧ Oracle(t1)(xbt,pt,rt)) ∨ ...(1413 characters)"] 5 [label = "Node 5: ∀ xat:A,xbt:A,pt:P,rt:R. ((Read(t1)(xat,xbt,pt,rt) ↔ eq()) ∧ (Assign(t1)(xat,pt) ∨ Read(t1)(xat,xbt,pt,rt) ∨ ¬ Assign(t2)(xat,pt) ∨ ¬ Assign(t2)(xbt,pt)) ∧ (Assign(t1)(xat,pt) ∨ Read(t1)(xat,xbt,pt,rt) ∨ ¬ Assign(t2)(xat,pt) ∨ ¬ Review(t2)(xbt,pt,rt)) ∧ (Assign(t1)(xat,pt) ∨ Read(t1)(xat,xbt,pt,rt) ∨ ¬ Read(t2)(xat,xbt,pt,rt)) ∧ (Assign(t1)(xbt,pt) ∨ Read(t1)(xat,xbt,pt,rt) ∨ Review(t1)(xbt,pt,rt) ∨ ¬ Assign(t2)(xat,pt) ∨ ¬ Assign(t2)(xbt,pt)) ∧ (Assign(t1)(xbt,pt) ∨ Read(t1)(xat,xbt,pt,rt) ∨ Review(t1)(xbt,pt,rt) ∨ ¬ Assign(t2)(xat,pt) ∨ ¬ Review(t2)(xbt,pt,rt)) ∧ (Assign(t1)(xbt,pt) ∨ Read(t1)(xat,xbt,pt,rt) ∨ Review(t1)(xbt,pt,rt) ∨ ¬ Read(t2)(xat,xbt,pt,rt)) ∧ (Assign(t2)(xat,pt) ∨ Read(t2)(xa...(1459 characters)"] 3 -> 4 [label = "forall ", color = green] 4 -> 4 [label = "forall ", 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 = green] }``````