Commit ce18173c authored by Benoit Barbot's avatar Benoit Barbot
Browse files

progress

parent 72565b58
Pipeline #1694 passed with stages
in 31 seconds
pta
module m
s : [0..1] init 0;
x : clock;
y : clock;
invariant
true
endinvariant
[a] (s=0)&(y<1) -> (y'=0);
[b] (s=1)&(x<1) -> (x'=0);
[c] (s=0) & (x>4) -> (x'=0) & (s'=1);
[c] (s=1) & (y>4) -> (y'=0) & (s'=0);
endmodule
......@@ -105,7 +105,7 @@ let _ =
print_flush ()
);
let w,rgp = FunIt.iterate_functionnal ~update:(fun () ->if !verbose >0 then (printf "|"; print_flush ()))
rg !npoly in
rg !npoly in
if !verbose>0 then printf "] [%.2fs]@." (check_time ());
w,rgp
| _, Some rg, false -> FunIt.iterate_functionnal rg 0
......
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