notebook_causal_alleq_11.dot 2.29 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
digraph "Invariant Labelling" {
	1 -> 3 [label = "forall x:User,i:Info may (Some(choice0))
  Written(i,x) → Read += (x,i);", color = green]
	0 [label = "Node 0:
True"]
	3 [label = "Node 3:
∀ u:User,info:Info. ((Read(t1)(u,info) ↔ eq()) ∧
  (¬ Read(t1)(u,info) ∨
    Read(t2)(u,info)) ∧
  (¬ Read(t2)(u,info) ∨
    Read(t1)(u,info)) ∧
  ((¬ 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)))) ∧
∀ u:User,info:Info,i:Info. ((¬ Read(t1)(u,info) ∨
    Read(t2)(u,info)) ∧
  (¬ Read(t2)(u,info) ∨
    Read(t1)(u,info)...(1795 characters)"]
	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)))) ∧
∀ u:User,info:Info,i:Info. (((¬ 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...(3461 characters)"]
	2 [label = "Node 2:
∀ u:User,info:Info. (Read(t1)(u,info) ↔ eq())"]
	1 -> 2 [label = "forall 
  ", color = green]
	0 -> 1 [label = "forall 
  ", color = red]
	2 -> 2 [label = "forall 
  ", color = green]
	1 -> 1 [label = "forall x:User,i:Info
  Oracle(i,x) → Written += (i,x);", color = green]
	3 -> 1 [label = "forall 
  ", color = green]
}