Merge branch 'master' of versioncontrolseidl.in.tum.de:mueller/loopingworkflows

examples/nonomitting/conference_stubborn.spec

+Workflow
+
+forallmay x:A,p:P
+    True → Conf += (x,p)
+forallmay x:A,p:P
+    !Conf(x,p) → Assign += (x,p)
+forall x:A,p:P,r:R
+    (Assign(x,p) ∧ Oracle(x,p,r)) → Review += (x,p,r)
+loop {
+    forall xa:A,xb:A,p:P,r:R (Assign(xa,p) ∧ Review(xb,p,r)) → Read += (xa,xb,p,r)
+    forallmay x:A,p:P,r:R (Assign(x,p)) → Review += (x,p,r)
+}
+
+Declassify
+
+Oracle(x:A,p:P,r:R): ¬ Conf(xat:A,p:P)
+
+Target
+
+Read(xat:A, xbt:A, pt:P, rt:R)

examples/nonomitting/notebook.spec

@@ -5,15 +5,11 @@ loop {
 		forallmay x:User, i:Info
 			Written(i, x) → Read += (x, i)
 	} {
-		forall x:User, i:Info
-			Oracle(i, x) → Written += (i, x)
+		forallmay x:User, i:Info
+			True → Written += (i, x)
 	}
 }
 
-Declassify
-
-Oracle(i:Info,x:User): Written(i:Info, u:User)
-
 Target
 
 Read(u:User, info:Info)

examples/nonomitting/notebook_stubborn.spec

@@ -5,15 +5,11 @@ loop {
 		forallmay x:User, i:Info
 			Written(i, x) → Read += (x, i)
 	} {
-		forall x:User, i:Info
-			Oracle(i, x) → Written += (i, x)
+		forallmay x:User, i:Info
+			True → Written += (i, x)
 	}
 }
 
-Declassify
-
-Oracle(i:Info,x:User): Written(i:Info, u:User)
-
 Target
 
 Read(u:User, info:Info)

results/nonomitting/conference/conference_causal_alleq.metrics

+Name: nonomitting/conference
+         Description: alleq
+         Invariant:
+            ∀ 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()) ∧
+            ∀ xt:A,pt:P. (Assign(t1)(xt,pt) ↔ eq())
+         Model: causal
+         Result: not inductive
+         WF size: 6
+         Time: 6822 ms
+         Proof steps: 15
+         Strengthenings: 11
+         Largest Inv: 3544
+         Average Inv: 1546
\ No newline at end of file

results/nonomitting/conference/conference_causal_alleq_0.dot

+digraph "Invariant Labelling" {
+	1 [label = "Node 1:
+∀ xt:A,pt:P. (Conf(t1)(xt,pt) ↔ eq())"]
+	0 [label = "Node 0:
+True"]
+	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 = red]
+	3 -> 4 [label = "forall 
+  ", color = red]
+	2 -> 3 [label = "forall x:A,p:P,r:R
+  Assign(x,p) ∧ Oracle(x,p,r) → Review += (x,p,r);", color = red]
+	5 -> 3 [label = "forall x:A,p:P,r:R may (Some(choice2))
+  Assign(x,p) → 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]
+	3 [label = "Node 3:
+∀ 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()))"]
+	4 [label = "Node 4:
+∀ 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()))"]
+	2 [label = "Node 2:
+∀ xt:A,pt:P. ((Conf(t1)(xt,pt) ↔ eq()) ∧
+  (Assign(t1)(xt,pt) ↔ eq()))"]
+	4 -> 4 [label = "forall 
+  ", color = red]
+	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()))"]
+}
\ No newline at end of file

results/nonomitting/conference/conference_causal_alleq_1.dot

+digraph "Invariant Labelling" {
+	1 [label = "Node 1:
+∀ xt:A,pt:P. (Conf(t1)(xt,pt) ↔ eq())"]
+	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]
+	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 = red]
+	3 -> 4 [label = "forall 
+  ", color = red]
+	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]
+	3 [label = "Node 3:
+∀ 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()))"]
+	4 [label = "Node 4:
+∀ 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()))"]
+	2 [label = "Node 2:
+∀ xt:A,pt:P. ((Conf(t1)(xt,pt) ↔ eq()) ∧
+  (Assign(t1)(xt,pt) ↔ eq()))"]
+	4 -> 4 [label = "forall 
+  ", color = red]
+	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...(1009 characters)"]
+}
\ No newline at end of file

results/nonomitting/conference/conference_causal_alleq_10.dot

+digraph "Invariant Labelling" {
+	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)"]
+	0 [label = "Node 0:
+True"]
+	2 -> 3 [label = "forall x:A,p:P,r:R
+  Assign(x,p) ∧ Oracle(x,p,r) → Review += (x,p,r);", color = red]
+	5 -> 3 [label = "forall x:A,p:P,r:R may (Some(choice2))
+  Assign(x,p) → 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]
+	4 [label = "Node 4:
+∀ 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()))"]
+	3 [label = "Node 3:
+∀ 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)) ∧
+  ((¬ 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))) ∧
+  ((¬ 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()))"]
+	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]
+}
\ No newline at end of file

results/nonomitting/conference/conference_causal_alleq_11.dot

+digraph "Invariant Labelling" {
+	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)"]
+	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]
+	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]
+	4 [label = "Node 4:
+∀ 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()))"]
+	3 [label = "Node 3:
+∀ 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)) ∧
+  ((¬ 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))) ∧
+  ((¬ 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()))"]
+	3 -> 4 [label = "forall 
+  ", color = green]
+	4 -> 4 [label = "forall 
+  ", color = green]
+	3 -> 5 [label = "forall xa:A,xb:A,p:P,r:R