diff --git a/test/dijkstra-ring/config.ml b/test/dijkstra-ring/config.ml index 98b279bf7700e80367b8fc9a39381a363e0a217b..d017e2e0521bea78c6111c70c35ac980ab9786cb 100644 --- a/test/dijkstra-ring/config.ml +++ b/test/dijkstra-ring/config.ml @@ -1,20 +1,26 @@ - open Algo open State let potential = None let fault = None +(* For the Dijkstra ring, a configuration is legitimate iff there is + exactly one token. + + nb: there are as many tokens as enabled nodes. So let's count enable nodes! + *) let (legitimate: pid list -> (pid -> t * (t neighbor * pid) list) -> bool) = fun pidl get -> - (* only one node is enabled *) + (* increment the token number i if pid is enabled *) let incr_token i pid = let s, nl = get pid in let nl = List.map fst nl in let have_token = (if s.root then Root.enable_f s nl else P.enable_f s nl) <> [] in if have_token then i+1 else i in + (* Now let's iterate on all the nodes starting from |tokens|=0 *) let token_nb = List.fold_left incr_token 0 pidl in + (* if there is 1 token, returns true *) token_nb = 1 let legitimate = Some legitimate