Commit 64ee83d6 by Christian Müller

### remove results

This source diff could not be displayed because it is too large. You can view the blob instead.
 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
 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

147 KB

 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

247 KB