Commit b8e04d9a authored by Mário Pereira's avatar Mário Pereira
Browse files

Schorr-Waite: WIP

parent 8c06d842
......@@ -294,34 +294,9 @@ module SchorrWaite
if !t = null || !m[!t] then begin
if !c[!p] then begin (* pop *)
let q = !t in
assert { forall i. 0 <= i < Seq.length !stackNodes ->
let n = Seq.get !stackNodes i in
if !c[n] then
(!left[n] = (at !left 'Init)[n]) else
(!right[n] = (at !right 'Init)[n]) };
t := !p;
assert { forall i. 0 <= i < Seq.length !stackNodes ->
let n = Seq.get !stackNodes i in
if !c[n] then
(!left[n] = (at !left 'Init)[n]) else
(!right[n] = (at !right 'Init)[n]) };
(* assert { !m[!p] /\ Seq.length !stackNodes <> 0 /\
!p = Seq.get !stackNodes 0 /\
(!left[!p] <> null -> !m[!left[!p]]) /\
(!right[!p] <> null -> !m[!right[!p]]) }; *)
stackNodes := tl_stackNodes !stackNodes;
p := !right[!p];
(* assert { !t <> null /\ not_in_stack !t !stackNodes /\
S.mem !t graph /\
!m[!t] /\ (!left[!t] <> null -> !m[!left[!t]]) /\
(!right[!t] <> null -> !m[!right[!t]]) }; *)
(* assert { forall n : loc. S.mem n graph -> n <> !t ->
n <> null -> !m[n] -> not_in_stack n !stackNodes ->
(!left[n] <> null -> !m[!left[n]]) /\
(!right[n] <> null -> !m[!right[n]]) };*)
assert { not_in_stack !t !stackNodes /\ !t <> null /\
!m[!t] /\ !c[!t] /\ (!left[!t] = (at !left 'Init)[!t]) };
set_right !t q;
pth := get_path_from_root !p;
end else begin (* swing *)
......
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