Commit d401433e authored by MARCHE Claude's avatar MARCHE Claude

WIP S-W with ghost monitor: add the evidently missing calls to step ()

parent 53bd6ca6
......@@ -258,7 +258,11 @@ module SchorrWaite
step ();
step ();
monitor initial_memo graph new_gray; (* traverse the left child *)
monitor initial_memo graph new_gray (* traverse the right 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
......@@ -284,7 +288,7 @@ module SchorrWaite
pc := 0;
t := root;
p := null;
monitor (pure {memo}) graph empty;
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 /\
......
......@@ -55,52 +55,99 @@
<proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC monitor.11" expl="variant decrease" proved="true">
<proof prover="2"><result status="valid" time="0.09"/></proof>
<proof prover="2"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC monitor.12" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC monitor.13" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.44"/></proof>
<proof prover="2"><result status="valid" time="0.42"/></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>
<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>
<goal name="VC monitor.16" expl="variant decrease" proved="true">
<proof prover="2"><result status="valid" time="0.08"/></proof>
<goal name="VC monitor.16" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC monitor.17" 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.04"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC monitor.18" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC monitor.19" expl="precondition">
<goal name="VC monitor.19" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC monitor.20" expl="precondition">
<goal name="VC monitor.20" expl="variant decrease" proved="true">
<proof prover="2"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC monitor.21" expl="postcondition" proved="true">
<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.04"/></proof>
<proof prover="2"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC monitor.22" expl="postcondition">
<goal name="VC monitor.22" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC monitor.23" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.04" steps="210"/></proof>
<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>
<goal name="VC monitor.24" expl="postcondition">
<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>
<goal name="VC monitor.25" expl="postcondition" proved="true">
<goal name="VC monitor.25" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC monitor.26" expl="postcondition">
<goal name="VC monitor.26" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></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>
<goal name="VC monitor.28" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></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>
<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>
<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>
<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>
<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>
<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>
</transf>
</goal>
......
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