conference_stubborn_stubborn_alleq_9.dot 3.82 KB
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
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]
}