Skip to content
Snippets Groups Projects
Commit d994b728 authored by Emile Guillaume's avatar Emile Guillaume
Browse files

test: fix expected property

parent c3dfe95f
No related branches found
No related tags found
No related merge requests found
......@@ -5,7 +5,7 @@ open Algo
(* let m=10 (* max 2 (1+2*diameter ()) *) *)
let diameter = Algo.diameter ()
let m = max 2 (1+2*diameter)
let m = max 2 (2*diameter-1)
let (init_state: int -> string -> 'v) =
fun _ _ ->
......
......@@ -9,7 +9,7 @@ var
let
nb_step = 1 -> pre(nb_step) + 1 ;
All_Acti = all_true<<an,pn>>(Acti);
res = ((max_clock>= (2*diameter-1)) and is_connected)
res = (((2*diameter-1)>= (2*diameter-1)) and is_connected)
=> (nb_step>=(3*diameter-2)) => All_Acti ; -- Theorem 4.11 page 40
tel
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment