Commit 21ea460a authored by MARCHE Claude's avatar MARCHE Claude

SW with Ghost monitor: done, thanks to Martin

parent d401433e
......@@ -149,151 +149,157 @@ module SchorrWaite
(** step function for low-level Schorr-Waite algorithm
while L0: (p != NULL || (t != NULL && ! t->m)) {
L1:
L0:
node t = root;
node p = NULL;
while L1: (p != NULL || (t != NULL && ! t->m)) {
L2:
if (t == NULL || t->m) {
if (p->c) { /* pop */
node q = t; t = p; p = p->r; t->r = q;
node q = t; t = p; p = p->r; t->r = q;
}
else { /* swing */
node q = t; t = p->r; p->r = p->l; p->l = q; p->c = 1;
node q = t; t = p->r; p->r = p->l; p->l = q; p->c = 1;
}
}
else { /* push */
node q = p; p = t; t = t->l; p->l = q; p->m = 1; p->c = 0;
}
}
L2:
L3:
*)
(* Extract parameters (including ghosts) of the main monitor
at top-level so that they are visible in step as well
(only [root] need to be extracted, [graph] extracted for uniformity only) *)
val root : loc
val ghost graph : set loc
(* Non-memory internal state *)
val pc : ref int
val t : ref loc
val p : ref loc
(* Step function *)
let step () : unit
requires { 0 <= !pc < 2 }
requires { !pc = 1 -> !p <> null \/ (!t <> null && not memo.mark[!t]) }
writes { pc,t,p,memo }
ensures { old (!pc = 0 /\ (!p <> null \/ (!t <> null && not memo.mark[!t]))) ->
!pc = 1 /\
!t = old !t /\
!p = old !p /\
memo = old memo }
ensures { old (!pc = 0 /\ not (!p <> null \/ (!t <> null && not memo.mark[!t]))) ->
!pc = 2 /\
!t = old !t /\
!p = old !p /\
memo = old memo }
ensures { old (!pc = 1 /\ (!t = null || memo.mark[!t]) /\ memo.color[!p]) -> (* pop *)
(* q = t *) let q = old !t in let o = old !p in
(* t = p *) !t = o /\
(* p = p->r *) !p = old (memo.right[o]) /\
(* t->r = q (t is old p here!) *) memo.right = old (memo.right[o <- q]) /\
!pc = 0 /\
memo.left = old (memo.left) /\
memo.mark = old (memo.mark) /\
memo.color = old (memo.color) }
ensures { old (!pc = 1 /\ (!t = null || memo.mark[!t]) /\ not memo.color[!p]) -> (* swing *)
(* q = t *) let q =old !t in let o = old !p in
(* t = p->r *) !t = old (memo.right[o]) /\
(* p->r = p->l *) memo.right = old (memo.right[o <- memo.left[o]]) /\
(* p->l = q *) memo.left = old (memo.left[o <- q]) /\
(* p->c = 1 *) memo.color = old (memo.color[o <- true]) /\
!pc = 0 /\
memo.mark = old (memo.mark) }
ensures { old (!pc = 1 /\ not (!t = null || memo.mark[!t])) -> (* push *)
(* q = p *) let q = old !p in let o = old !t in
(* p = t *) !p = o /\
(* t = t->l *) !t = old (memo.left[o]) /\
(* p->l = q (p is old t here!) *) memo.left = old (memo.left[o <- q]) /\
(* p->m = 1 *) memo.mark = old (memo.mark[o <- true]) /\
(* p->c = 0 *) memo.color = old (memo.color[o <- false]) /\
!pc = 0 /\
memo.right = old (memo.right) }
requires { 0 <= !pc < 3 }
requires { !pc = 2 -> !p <> null \/ (!t <> null && not memo.mark[!t]) }
writes { pc,t,p,memo }
ensures { old (!pc = 0) -> !pc = 1 /\ !t = root /\ !p = null /\ memo = old memo }
ensures { old (!pc = 1 /\ (!p <> null \/ (!t <> null /\ not memo.mark[!t]))) ->
!pc = 2 /\ !t = old !t /\ !p = old !p /\ memo = old memo }
ensures { old (!pc = 1 /\ not(!p <> null \/ (!t <> null /\ not memo.mark[!t]))) ->
!pc = 3 /\ !t = old !t /\ !p = old !p /\ memo = old memo }
ensures { old (!pc = 2 /\ (!t = null \/ memo.mark[!t]) /\ memo.color[!p]) -> (* pop *)
(* q = t *) let q = old !t in
(* t = p *) !t = old !p /\
(* p = p->r *) !p = old (memo.right[!p]) /\
(* t->r = q (t is old p here!) *) memo.right = old (memo.right[!p <- q]) /\
!pc = 1 /\
memo.left = old (memo.left) /\
memo.mark = old (memo.mark) /\
memo.color = old (memo.color) }
ensures { old (!pc = 2 /\ (!t = null \/ memo.mark[!t]) /\ not memo.color[!p]) -> (* swing *)
(* q = t *) let q = old !t in
(* p unchanged *) !p = old !p /\
(* t = p->r *) !t = old (memo.right[!p]) /\
(* p->r = p->l *) memo.right = old (memo.right[!p <- memo.left[!p]]) /\
(* p->l = q *) memo.left = old (memo.left[!p <- q]) /\
(* p->c = 1 *) memo.color = old (memo.color[!p <- true]) /\
!pc = 1 /\ memo.mark = old (memo.mark) }
ensures { old (!pc = 2 /\ not (!t = null \/ memo.mark[!t])) -> (* push *)
(* q = p *) let q = old !p in
(* p = t *) !p = old !t /\
(* t = t -> l *) !t = old (memo.left[!t]) /\
(* p->l = q (p is old t here!) *) memo.left = old (memo.left[!t <- q]) /\
(* p->m = 1 *) memo.mark = old (memo.mark[!t <- true]) /\
(* p->c = 0 *) memo.color = old (memo.color[!t <- false]) /\
!pc = 1 /\ memo.right = old (memo.right) }
=
if !pc = 0 then
if !p <> null || (!t <> null && not get_m !t) then
pc := 1
else
pc := 2
else
if !pc = 1 then
if !t = null || get_m !t then
if get_c !p then (* pop *)
let q = !t in t := !p; p := get_r !p; set_r !t q; pc := 0
else (* swing *)
let q = !t in t := get_r !p; set_r !p (get_l !p); set_l !p q; set_c !p true; pc := 0
else (* push *)
let q = !p in p := !t; t := get_l !t; set_l !p q; set_m !p true; set_c !p false; pc := 0
else absurd
(* the monitor performs a depth-first search from current node `!t` *)
let rec monitor (ghost initial_memo:memory) (ghost graph: set loc) (ghost gray_nodes:set loc) : unit
requires { !pc = 0 }
if !pc = 0 then (t := root; p := null; pc := 1)
else if !pc = 1 then
if !p <> null || (!t <> null && not(get_m(!t)))
then pc := 2
else pc := 3
else if !pc = 2 then
if !t = null || get_m(!t) then
if get_c !p then (* pop *)
let q = !t in t := !p; p := get_r !p; set_r !t q; pc := 1
else (* swing *)
let q = !t in t := get_r !p; set_r !p (get_l !p); set_l !p q; set_c !p true; pc := 1
else
let q = !p in p := !t; t := get_l !t; set_l !p q; set_m !p true; set_c !p false; pc := 1
else absurd
let schorr_waite () : unit
(** The program begins execution. *)
requires { !pc = 0 }
(** Root belong to graph (note: for simplicity, the graph set may (and likely does)
contain the null pointer. *)
requires { mem root graph }
(** Graph is closed by following edges *)
requires { forall l. mem l graph /\ l <> null ->
mem memo.left[l] graph /\ mem memo.right[l] graph }
writes { memo,pc,t,p }
(** The graph starts fully unmarked. *)
requires { forall x. mem x graph -> not memo.mark[x] }
(** The program is indeed done executing. *)
ensures { !pc = 3 }
(** The graph structure is left unchanged. *)
ensures { unchanged (old memo) memo }
(** Every non-null location reachable from the root is marked. *)
ensures { forall x. path (old memo) root x /\ x <> null ->
memo.mark[x] }
(** Every other location is left with its previous marking. *)
ensures { forall x. not path (old memo) root x /\ x <> null ->
memo.mark[x] = (old memo.mark)[x] }
=
step (); (* Initialize *)
let ghost initial_memo = pure {memo} in (* Copy of initial memory *)
let rec monitor (ghost gray_nodes: set loc) : unit
requires { !pc = 1 }
(* DFS invariant *)
requires { well_colored_on graph gray_nodes initial_memo memo.mark }
requires { mem !t graph }
(* Non-marked nodes have unchanged structure with
respect to the initial one. *)
(* Non-marked nodes have unchanged structure with respect to the initial one.
Cause: specification refer the graph in initial memory. *)
requires { forall x. x <> null /\ not memo.mark[x] ->
memo.left[x] = initial_memo.left[x] /\ memo.right[x] = initial_memo.right[x]
}
ensures { !pc = 0 }
(* 'stack frames' are maintained correctly *)
memo.left[x] = initial_memo.left[x] /\ memo.right[x] = initial_memo.right[x] }
ensures { !pc = 1 }
(* 'stack frames' are maintained correctly. *)
ensures { !t = old !t /\ !p = old !p }
(* Pointer buffer is left unchanged *)
(* Pointer buffer is overall left unchanged *)
ensures { unchanged (old memo) memo }
(* Maintain DFS invariant *)
ensures { well_colored_on graph gray_nodes initial_memo memo.mark }
(* The top node get marked *)
ensures { !t <> null -> memo.mark[!t] }
(* May not mark unreachable node, neither change marked node. *)
(* May not mark unreachable node (in any way), neither change marked nodes. *)
ensures { forall x. x <> null ->
not path initial_memo !t x \/ not (old memo.mark[x]) ->
memo.mark[x] = (old memo.mark)[x] }
not path initial_memo !t x \/ old memo.mark[x] ->
memo.mark[x] = (old memo.mark)[x] /\
memo.color[x] = (old memo.color)[x]
}
(* Terminates because there is a limited number of 'grayable' nodes. *)
variant { cardinal graph - cardinal gray_nodes }
= if !t = null || get_m !t then () else
let ghost new_gray = add !t gray_nodes in
step ();
step ();
monitor initial_memo graph new_gray; (* traverse the left child *)
step ();
step ();
monitor initial_memo graph new_gray; (* traverse the right child *)
step ();
step ()
let schorr_waite (root: loc) (ghost graph: set loc) : unit
(** Root belong to graph (note: for simplicity, the graph set
may (and likely does) contain the null pointer. *)
requires { mem root graph }
(** Graph is closed by following edges *)
requires { forall l.
mem l graph /\ l <> null ->
mem memo.left[l] graph /\ mem memo.right[l] graph }
writes { memo,pc,t,p }
(** The graph starts fully unmarked. *)
requires { forall x. mem x graph -> not memo.mark[x] }
(** The graph structure is left unchanged. *)
ensures { unchanged (old memo) memo }
(** Every non-null location reachable from the root is marked black. *)
ensures { forall x. path (old memo) root x /\ x <> null ->
memo.mark[x] }
(** Every other location is left with its previous color. *)
ensures { forall x. not path (old memo) root x /\ x <> null ->
memo.mark[x] = (old memo.mark)[x] }
=
pc := 0;
t := root;
p := null;
monitor (pure {memo}) graph empty
(* Need induction to recover path-based specification. *)
(* assert { forall x y m. m = memo at I /\ x <> null /\ y <> null /\
mem x graph /\ black memo.colors[x] ->
([@induction] path m x y) -> black memo.colors[y] }
*)
(* assert { path initial_memo !t !t }; *)
step (); (* Test *)
step (); (* Push *)
monitor new_gray; (* traverse the left child *)
step (); (* Test *)
step (); (* Swing *)
monitor new_gray; (* traverse the right child *)
step (); (* Test *)
step () (* Pop *)
in
monitor empty;
step (); (* Exit. *)
(* Need induction to recover path-based specification. *)
assert { forall x y. ([@induction] path initial_memo x y) ->
x <> null /\ y <> null /\ mem x graph /\ memo.mark[x] ->
memo.mark[y] }
end
......@@ -2,158 +2,168 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5">
<prover id="0" name="Z3" version="4.7.1" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../schorr_waite_with_ghost_monitor.mlw">
<theory name="SchorrWaite">
<prover id="0" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../schorr_waite_with_ghost_monitor.mlw" proved="true">
<theory name="SchorrWaite" proved="true">
<goal name="VC step" expl="VC for step" proved="true">
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="68"/></proof>
</goal>
<goal name="VC monitor" expl="VC for monitor">
<transf name="split_vc" >
<goal name="VC monitor.0" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<goal name="VC schorr_waite" expl="VC for schorr_waite" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC schorr_waite.0" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="VC schorr_waite.1" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="VC schorr_waite.2" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
<goal name="VC schorr_waite.3" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="20"/></proof>
</goal>
<goal name="VC schorr_waite.4" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="20"/></proof>
</goal>
<goal name="VC schorr_waite.5" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="23"/></proof>
</goal>
<goal name="VC schorr_waite.6" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
<goal name="VC schorr_waite.7" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="26"/></proof>
</goal>
<goal name="VC monitor.1" expl="postcondition" proved="true">
<proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<goal name="VC schorr_waite.8" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="24"/></proof>
</goal>
<goal name="VC monitor.2" expl="postcondition" proved="true">
<proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<goal name="VC schorr_waite.9" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC monitor.3" expl="postcondition" proved="true">
<proof prover="1" obsolete="true"><result status="valid" time="0.04" steps="210"/></proof>
<proof prover="2"><result status="valid" time="0.05"/></proof>
<goal name="VC schorr_waite.10" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC monitor.4" expl="postcondition" proved="true">
<proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<goal name="VC schorr_waite.11" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC monitor.5" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<goal name="VC schorr_waite.12" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC monitor.6" expl="postcondition" proved="true">
<proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<goal name="VC schorr_waite.13" expl="variant decrease" proved="true">
<proof prover="1"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC monitor.7" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
<goal name="VC schorr_waite.14" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC monitor.8" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
<goal name="VC schorr_waite.15" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.04" steps="175"/></proof>
</goal>
<goal name="VC monitor.9" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<goal name="VC schorr_waite.16" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC monitor.10" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.06"/></proof>
<goal name="VC schorr_waite.17" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC monitor.11" expl="variant decrease" proved="true">
<proof prover="2"><result status="valid" time="0.08"/></proof>
<goal name="VC schorr_waite.18" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC monitor.12" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<goal name="VC schorr_waite.19" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC monitor.13" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.42"/></proof>
<goal name="VC schorr_waite.20" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC monitor.14" expl="precondition">
<proof prover="0"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="unknown" time="0.18"/></proof>
<proof prover="2"><result status="timeout" time="1.00"/></proof>
<goal name="VC schorr_waite.21" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC monitor.15" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="63"/></proof>
<proof prover="2"><result status="timeout" time="1.00"/></proof>
<goal name="VC schorr_waite.22" expl="variant decrease" proved="true">
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC monitor.16" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
<goal name="VC schorr_waite.23" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC monitor.17" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<goal name="VC schorr_waite.24" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC monitor.18" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.06"/></proof>
<goal name="VC schorr_waite.25" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC monitor.19" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.06"/></proof>
<goal name="VC schorr_waite.26" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC monitor.20" expl="variant decrease" proved="true">
<proof prover="2"><result status="valid" time="0.09"/></proof>
<goal name="VC schorr_waite.27" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC monitor.21" expl="precondition" proved="true">
<proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="valid" time="0.07"/></proof>
<goal name="VC schorr_waite.28" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC monitor.22" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
<goal name="VC schorr_waite.29" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="VC monitor.23" expl="precondition">
<proof prover="0"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="timeout" time="1.00"/></proof>
<goal name="VC schorr_waite.30" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC monitor.24" expl="precondition">
<proof prover="0"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="timeout" time="1.00"/></proof>
<goal name="VC schorr_waite.31" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC monitor.25" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<goal name="VC schorr_waite.32" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.10" steps="363"/></proof>
</goal>
<goal name="VC monitor.26" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<goal name="VC schorr_waite.33" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.33" steps="1067"/></proof>
</goal>
<goal name="VC monitor.27" expl="precondition">
<proof prover="0"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="timeout" time="1.00"/></proof>
<goal name="VC schorr_waite.34" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.45"/></proof>
</goal>
<goal name="VC monitor.28" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<goal name="VC schorr_waite.35" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="VC monitor.29" expl="postcondition">
<proof prover="0"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="timeout" time="1.00"/></proof>
<goal name="VC schorr_waite.36" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.31" steps="1599"/></proof>
</goal>
<goal name="VC monitor.30" expl="postcondition">
<proof prover="0"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="timeout" time="1.00"/></proof>
<goal name="VC schorr_waite.37" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="VC monitor.31" expl="postcondition">
<proof prover="0"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="timeout" time="1.00"/></proof>
<goal name="VC schorr_waite.38" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="55"/></proof>
</goal>
<goal name="VC monitor.32" expl="postcondition">
<proof prover="0"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="timeout" time="1.00"/></proof>
<goal name="VC schorr_waite.39" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="16"/></proof>
</goal>
<goal name="VC monitor.33" expl="postcondition">
<proof prover="0"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="timeout" time="1.00"/></proof>
<goal name="VC schorr_waite.40" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="0"/></proof>
</goal>
<goal name="VC monitor.34" expl="postcondition">
<proof prover="0"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="timeout" time="1.00"/></proof>
<goal name="VC schorr_waite.41" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="24"/></proof>
</goal>
<goal name="VC schorr_waite.42" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="26"/></proof>
</goal>
<goal name="VC schorr_waite.43" expl="assertion" proved="true">
<transf name="induction_pr" proved="true" >
<goal name="VC schorr_waite.43.0" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC schorr_waite.43.1" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="0.10"/></proof>
</goal>
</transf>
</goal>
<goal name="VC schorr_waite.44" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC schorr_waite.45" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC schorr_waite.46" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC schorr_waite.47" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
<goal name="VC schorr_waite" expl="VC for schorr_waite" proved="true">
<proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
</theory>
</file>
</why3session>
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment