notebook_causal_alleq_3.dot 1.21 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
	1 -> 3 [label = "forall x:User,i:Info may (Some(choice0))
  Written(i,x) → Read += (x,i);", color = green]
Christian Müller's avatar
Christian Müller committed
4
5
	0 [label = "Node 0:
True"]
Christian Müller's avatar
Christian Müller committed
6
7
8
9
10
11
	3 -> 1 [label = "forall 
  ", color = red]
	3 [label = "Node 3:
∀ u:User,info:Info. (Read(t1)(u,info) ↔ eq())"]
	1 -> 2 [label = "forall 
  ", color = red]
Christian Müller's avatar
Christian Müller committed
12
	2 [label = "Node 2:
Christian Müller's avatar
Christian Müller committed
13
14
15
∀ u:User,info:Info. (Read(t1)(u,info) ↔ eq())"]
	1 -> 1 [label = "forall x:User,i:Info
  Oracle(i,x) → Written += (i,x);", color = red]
Christian Müller's avatar
Christian Müller committed
16
17
	0 -> 1 [label = "forall 
  ", color = red]
Christian Müller's avatar
Christian Müller committed
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
	2 -> 2 [label = "forall 
  ", color = green]
	1 [label = "Node 1:
∀ u:User,info:Info. ((Read(t1)(u,info) ↔ eq()) ∧
  ((¬ Read(t1)(u,info) ∧
      (¬ Written(t1)(info,u) ∨
        ¬ choice0(t1)(u,info))) ∨
    Read(t2)(u,info) ∨
    (Written(t2)(info,u) ∧
      ((¬ informed(t1)(u) ∧
          choice0(t1)(u,info)) ∨
        (informed(t1)(u) ∧
          choice0(t2)(u,info))))) ∧
  ((¬ Read(t2)(u,info) ∧
      (¬ Written(t2)(info,u) ∨
        ((informed(t1)(u) ∨
            ¬ choice0(t1)(u,info)) ∧
          (¬ informed(t1)(u) ∨
            ¬ choice0(t2)(u,info))))) ∨
    Read(t1)(u,info) ∨
    (Written(t1)(info,u) ∧
      choice0(t1)(u,info))))"]
Christian Müller's avatar
Christian Müller committed
40
}