conference_causal_alleq_11.dot 2.84 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1
digraph "Invariant Labelling" {
Christian Müller's avatar
Christian Müller committed
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
	1 [label = "Node 1:
∀ xt:A,pt:P. (Conf(t1)(xt,pt) ↔ eq())"]
	5 [label = "Node 5:
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P,rt:R. (Review(t1)(xt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P. ((Conf(t1)(xt,pt) ↔ eq()) ∧
  (Assign(t1)(xt,pt) ↔ eq())) ∧
∀ xat:A,xbt:A,pt:P,rt:R,xt:A. ((¬ Read(t1)(xat,xbt,pt,rt) ∨
    Read(t2)(xat,xbt,pt,rt)) ∧
  (¬ Read(t2)(xat,xbt,pt,rt) ∨
    Read(t1)(xat,xbt,pt,rt)) ∧
  ((¬ Review(t1)(xt,pt,rt) ∧
      (¬ Assign(t1)(xt,pt) ∨
        ¬ choice2(t1)(xt,pt,rt))) ∨
    Review(t2)(xt,pt,rt) ∨
    (Assign(t2)(xt,pt) ∧
      ((¬ informed(t1)(xt) ∧
          choice2(t1)(xt,pt,rt)) ∨
        (informed(t1)(xt) ∧
          choice2(t2)(xt,pt,rt))))) ∧
  ((¬ Review(t2)(xt,pt,rt) ∧
      (¬ Assign(t2)(xt,pt) ∨
        ¬ informed(t1)(xt) ∨
        ¬ choice2(t2)(xt,pt,rt))) ∨
    Review(t1)(xt,pt,rt) ∨
    (Assign(t1)(xt,pt) ∧
      choice2...(23593 characters)"]
Christian Müller's avatar
Christian Müller committed
29 30 31 32
	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]
Christian Müller's avatar
Christian Müller committed
33 34 35 36 37 38
	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]
Christian Müller's avatar
Christian Müller committed
39
	4 [label = "Node 4:
Christian Müller's avatar
Christian Müller committed
40 41 42 43
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P,rt:R. (Review(t1)(xt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P. ((Conf(t1)(xt,pt) ↔ eq()) ∧
  (Assign(t1)(xt,pt) ↔ eq()))"]
Christian Müller's avatar
Christian Müller committed
44
	3 [label = "Node 3:
Christian Müller's avatar
Christian Müller committed
45 46 47 48 49 50 51 52
∀ xat:A,xbt:A,pt:P,rt:R. (Read(t1)(xat,xbt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P,rt:R. (Review(t1)(xt,pt,rt) ↔ eq()) ∧
∀ xt:A,pt:P. ((Conf(t1)(xt,pt) ↔ eq()) ∧
  (Assign(t1)(xt,pt) ↔ eq())) ∧
∀ xat:A,xbt:A,pt:P,rt:R,xt:A,xb:A,p:P,r:R. ((¬ Review(t1)(xt,pt,rt) ∨
    Review(t2)(xt,pt,rt)) ∧
  (¬ Review(t2)(xt,pt,rt) ∨
    Review(t1)(xt,pt,rt)) ∧
Christian Müller's avatar
Christian Müller committed
53 54 55 56 57 58 59 60 61 62 63
  ((¬ 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) ∧
Christian Müller's avatar
Christian Müller committed
64 65 66 67 68 69 70
      Review(t1)(xbt,pt,rt))) ∧
  ((¬ Review(t1)(xt,pt,rt) ∧
      (¬ Assign(t1)(xt,pt) ∨
        ¬ choice2(t1)(xt,pt,rt)))...(53090 characters)"]
	2 [label = "Node 2:
∀ xt:A,pt:P. ((Conf(t1)(xt,pt) ↔ eq()) ∧
  (Assign(t1)(xt,pt) ↔ eq()))"]
Christian Müller's avatar
Christian Müller committed
71 72 73 74 75 76 77
	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]
}