Commits (7)
......@@ -104,7 +104,7 @@ let (make_do: string array -> 'v SimuState.t -> RdbgPlugin.t) =
(* 2: read the actions from the outside process, i.e., from sl_in *)
let _, pnal = Daemon.f st.sasarg.dummy_input
(st.sasarg.verbose > 0) st.sasarg.daemon st.network
(SimuState.neigbors_of_pid st) st pre_pnall pre_enab_ll
SimuState.neigbors_of_pid st pre_pnall pre_enab_ll
(get_action_value sl_in) Step.f
in
(* 3: Do the steps *)
......@@ -143,7 +143,7 @@ let (make_do: string array -> 'v SimuState.t -> RdbgPlugin.t) =
let activate_val, pnal =
Daemon.f st.sasarg.dummy_input
(st.sasarg.verbose > 0) st.sasarg.daemon st.network
(SimuState.neigbors_of_pid st) st pnall enab_ll
SimuState.neigbors_of_pid st pnall enab_ll
(get_action_value sl_in) Step.f
in
(* 3: Do the steps *)
......
(* Time-stamp: <modified the 18/06/2021 (at 16:23) by Erwan Jahier> *)
(* Time-stamp: <modified the 31/07/2021 (at 09:15) by Erwan Jahier> *)
(* Enabled processes (with its enabling action + neighbors) *)
type 'v pna = 'v Process.t * 'v Register.neighbor list * Register.action
......@@ -134,7 +134,8 @@ let (get_activate_val: 'v triggered -> 'v Process.t list -> bool list list)=
List.map (List.map (fun a -> List.mem a al)) actions
let (f: bool -> bool -> DaemonType.t -> 'v Process.t list ->
(string -> 'v * ('v Register.neighbor * string) list) -> 'v SimuState.t ->
('v SimuState.t -> string -> 'v * ('v Register.neighbor * string) list) ->
'v SimuState.t ->
'v enabled -> bool list list -> (string -> string -> bool) -> 'v step ->
bool list list * 'v triggered) =
fun dummy_in verbose_mode daemon pl neigbors_of_pid st all enab get_action_value step ->
......
(* Time-stamp: <modified the 18/06/2021 (at 16:22) by Erwan Jahier> *)
(* Time-stamp: <modified the 31/07/2021 (at 09:15) by Erwan Jahier> *)
type 'v pna = 'v Process.t * 'v Register.neighbor list * Register.action
type 'v enabled = 'v pna list list
......@@ -33,7 +33,7 @@ nb: it is possible that we read on stdin that an action should be
type 'v step = 'v triggered -> 'v SimuState.t -> 'v SimuState.t
val f : bool -> bool -> DaemonType.t -> 'v Process.t list ->
(string -> 'v * ('v Register.neighbor * string) list) ->
('v SimuState.t -> string -> 'v * ('v Register.neighbor * string) list) ->
'v SimuState.t -> 'v enabled -> bool list list ->
(string -> string -> bool) -> 'v step -> bool list list * 'v triggered
......
(* Time-stamp: <modified the 18/06/2021 (at 16:25) by Erwan Jahier> *)
(* Time-stamp: <modified the 31/07/2021 (at 09:15) by Erwan Jahier> *)
type 'v pna = 'v Process.t * 'v Register.neighbor list * Register.action
type 'v enabled = 'v pna list list
......@@ -122,7 +122,7 @@ let time3 verb lbl f x y z =
fxy
let (greedy: bool -> 'v SimuState.t -> 'v Process.t list ->
(string -> 'v * ('v Register.neighbor * string) list) ->
('v SimuState.t -> string -> 'v * ('v Register.neighbor * string) list) ->
'v step -> 'v pna list list -> 'v pna list) =
fun verb st pl neigbors_of_pid step all ->
assert (all<>[]);
......@@ -133,7 +133,7 @@ let (greedy: bool -> 'v SimuState.t -> 'v Process.t list ->
let pidl = List.map (fun p -> p.Process.pid) pl in
let nst = step pnal st in
let get_info pid =
let _, nl = neigbors_of_pid pid in
let _, nl = neigbors_of_pid nst pid in
Env.get nst.config pid, nl
in
user_pf pidl get_info
......@@ -167,7 +167,7 @@ let (greedy: bool -> 'v SimuState.t -> 'v Process.t list ->
(* val greedy_central: bool -> 'v Env.t -> ('v Process.t * 'v Register.neighbor list) list -> *)
let (greedy_central: bool -> 'v SimuState.t -> 'v Process.t list ->
(string -> 'v * ('v Register.neighbor * string) list) ->
('v SimuState.t -> string -> 'v * ('v Register.neighbor * string) list) ->
'v step -> 'v pna list list -> 'v pna list) =
fun verb st pl neigbors_of_pid step all ->
assert (all<>[]);
......@@ -178,7 +178,7 @@ let (greedy_central: bool -> 'v SimuState.t -> 'v Process.t list ->
let pidl = List.map (fun p -> p.Process.pid) pl in
let nst = step [pna] st in
let get_info pid =
let _, nl = neigbors_of_pid pid in
let _, nl = neigbors_of_pid nst pid in
Env.get nst.config pid, nl
in
user_pf pidl get_info
......
(* Time-stamp: <modified the 18/06/2021 (at 16:25) by Erwan Jahier> *)
(* Time-stamp: <modified the 31/07/2021 (at 09:15) by Erwan Jahier> *)
(** This module gathers daemons that tries to reach the worst case with
......@@ -13,13 +13,13 @@ type 'v step = 'v triggered -> 'v SimuState.t -> 'v SimuState.t
among the combinations of length 1, i.e., O(2^n) where n is the
number of enabled processes (|all|) *)
val greedy: bool -> 'v SimuState.t -> 'v Process.t list ->
(string -> 'v * ('v Register.neighbor * string) list) ->
('v SimuState.t -> string -> 'v * ('v Register.neighbor * string) list) ->
'v step -> 'v enabled -> 'v triggered
(** Ditto, but for central daemons (of a connected component) *)
val greedy_central:
bool -> 'v SimuState.t -> 'v Process.t list ->
(string -> 'v * ('v Register.neighbor * string) list) ->
('v SimuState.t -> string -> 'v * ('v Register.neighbor * string) list) ->
'v step -> 'v enabled -> 'v triggered
(** Returns the worst case among the combinations of length 1 for
......
(* Time-stamp: <modified the 11/03/2020 (at 14:13) by Erwan Jahier> *)
(* Time-stamp: <modified the 28/07/2021 (at 11:23) by Erwan Jahier> *)
open Process
......@@ -96,11 +96,11 @@ const f=false;
const t=true;
const adjacency=%s;
%s
node oracle(%s) \nreturns (ok:bool);
node oracle(legitimate:bool; %s) \nreturns (ok:bool);
var
%slet
%s %s
ok = %s_oracle(Enab,Acti);
ok = %s_oracle(legitimate, Enab, Acti);
tel
"
(Mypervasives.entete "--" SasaVersion.str SasaVersion.sha)
......
(* Time-stamp: <modified the 27/07/2021 (at 09:19) by Erwan Jahier> *)
(* Time-stamp: <modified the 28/07/2021 (at 11:37) by Erwan Jahier> *)
open Register
......@@ -304,7 +304,7 @@ let (make : bool -> string array -> 'v t) =
in
if !Register.verbose_level > 0 then
Printf.eprintf "==> get output var names...\n%!";
Printf.printf "#outputs %s %s\n" (env_rif_decl args pl) pot;
Printf.printf "#outputs %s \"legitimate\":bool %s\n" (env_rif_decl args pl) pot;
Printf.printf "\n%!";
flush_all()
);
......
open Sasacore
let (print_step : int -> int -> string -> SasArg.t -> 'v Env.t -> 'v Process.t list
-> string -> bool list list -> unit) =
fun n i pot args e pl activate_val enab_ll ->
let (print_step : int -> int -> string -> string -> SasArg.t -> 'v Env.t ->
'v Process.t list -> string -> bool list list -> unit) =
fun n i legitimate pot args e pl activate_val enab_ll ->
let enable_val =
String.concat " " (List.map (fun b -> if b then "t" else "f")
(List.flatten enab_ll))
......@@ -18,16 +18,16 @@ let (print_step : int -> int -> string -> SasArg.t -> 'v Env.t -> 'v Process.t l
Printf.eprintf "\n#step %s\n" (string_of_int (n-i)) ;
Printf.eprintf "%s #outs " activate_val; flush stderr
);
Printf.printf "%s %s %s\n%!" (StringOf.env_rif e pl) enable_val pot;
Printf.printf "%s %s %s %s\n%!" (StringOf.env_rif e pl) enable_val legitimate pot;
) else (
(* rif mode, internal daemons *)
if args.rif then
Printf.printf " %s %s %s %s\n%!" (StringOf.env_rif e pl) enable_val activate_val pot
Printf.printf " %s %s %s %s %s\n%!" (StringOf.env_rif e pl) enable_val activate_val legitimate pot
else (
Printf.printf "\n#step %s\n" (string_of_int (n-i));
Printf.printf "%s%s %s %s %s\n%!"
Printf.printf "%s%s %s %s %s %s\n%!"
(if args.rif then "" else "#outs ")
(StringOf.env_rif e pl) enable_val activate_val pot
(StringOf.env_rif e pl) enable_val activate_val legitimate pot
);
);
flush stderr;
......@@ -97,6 +97,7 @@ let (simustep: int -> int -> string -> 'v SimuState.t -> 'v SimuState.t * string
let all, enab_ll = Sasacore.SimuState.get_enable_processes st in
let pot = compute_potentiel st in
let pl = st.network in
let leg = legitimate st in
let st, all, enab_ll =
if
(* not (args.rif) && *)
......@@ -104,11 +105,11 @@ let (simustep: int -> int -> string -> 'v SimuState.t -> 'v SimuState.t * string
then (
match Register.get_fault () with
| None ->
print_step n i pot st.sasarg st.config pl activate_val enab_ll;
print_step n i "t" pot st.sasarg st.config pl activate_val enab_ll;
incr rounds;
raise (Silent (n-i))
| Some ff ->
print_step n i pot st.sasarg st.config pl activate_val enab_ll;
print_step n i "t" pot st.sasarg st.config pl activate_val enab_ll;
let str = if st.sasarg.rif then "#" else "" in
Printf.eprintf "\n%sThis algo is silent after %i move%s, %i step%s, %i round%s.\n"
str !moves (plur !moves) (n-i) (plur (n-i)) !rounds (plur !rounds);
......@@ -117,13 +118,13 @@ let (simustep: int -> int -> string -> 'v SimuState.t -> 'v SimuState.t * string
let all, enab_ll = Sasacore.SimuState.get_enable_processes st in
st, all, enab_ll
)
else if legitimate st then (
else if leg then (
match Register.get_fault () with
| None ->
print_step n i pot st.sasarg st.config pl activate_val enab_ll;
print_step n i "t" pot st.sasarg st.config pl activate_val enab_ll;
raise (Legitimate (n-i))
| Some ff ->
print_step n i pot st.sasarg st.config pl activate_val enab_ll;
print_step n i "t" pot st.sasarg st.config pl activate_val enab_ll;
let str = if st.sasarg.rif then "#" else "#" in
Printf.eprintf
"\n%sThis algo reached a legitimate configuration after %i move%s, %i step%s, %i round%s.\n"
......@@ -136,13 +137,14 @@ let (simustep: int -> int -> string -> 'v SimuState.t -> 'v SimuState.t * string
else
st, all, enab_ll
in
let leg_str = if leg then "t" else "f" in
if st.sasarg.daemon = DaemonType.Custom then
print_step n i pot st.sasarg st.config pl activate_val enab_ll;
print_step n i leg_str pot st.sasarg st.config pl activate_val enab_ll;
(* 2: read the actions *)
if verb then Printf.eprintf "==> SasaSimuState.simustep : 2: read the actions\n%!";
let get_action_value = RifRead.bool (st.sasarg.verbose > 1) in
let next_activate_val, pnal = Daemon.f st.sasarg.dummy_input
(st.sasarg.verbose >= 1) st.sasarg.daemon st.network (SimuState.neigbors_of_pid st)
(st.sasarg.verbose >= 1) st.sasarg.daemon st.network SimuState.neigbors_of_pid
st all enab_ll get_action_value Step.f
in
List.iter (List.iter (fun b -> if b then incr moves)) next_activate_val;
......@@ -151,7 +153,7 @@ let (simustep: int -> int -> string -> 'v SimuState.t -> 'v SimuState.t * string
(* 3: Do the steps *)
if verb then Printf.eprintf "==> SasaSimuState.simustep : 3: Do the steps\n%!";
if st.sasarg.daemon <> DaemonType.Custom then
print_step n i pot st.sasarg st.config pl next_activate_val enab_ll;
print_step n i leg_str pot st.sasarg st.config pl next_activate_val enab_ll;
let st = Sasacore.Step.f pnal st in
st, next_activate_val
......
# Time-stamp: <modified the 05/05/2021 (at 13:20) by Erwan Jahier>
# Time-stamp: <modified the 27/07/2021 (at 10:44) by Erwan Jahier>
# Rules to generate various dot files.
# The DECO_PATTERN variable should be defined
......@@ -32,6 +32,10 @@ ring%.dot:
gg ring -n $* -o $@
gg-deco $(DECO_PATTERN) $@ -o $@
diring%.dot:
gg ring -dir -n $* -o $@
gg-deco $(DECO_PATTERN) $@ -o $@
tree%.dot:
gg tree -n $* -o $@
gg-deco $(DECO_PATTERN) $@ -o $@
......
This diff is collapsed.
#inputs
#outputs "root_d":int "root_par":int "p1_d":int "p1_par":int "p2_d":int "p2_par":int "p3_d":int "p3_par":int "p4_d":int "p4_par":int "p5_d":int "p5_par":int "p6_d":int "p6_par":int "p7_d":int "p7_par":int "Enab_root_CD":bool "Enab_root_CP":bool "Enab_p1_CD":bool "Enab_p1_CP":bool "Enab_p2_CD":bool "Enab_p2_CP":bool "Enab_p3_CD":bool "Enab_p3_CP":bool "Enab_p4_CD":bool "Enab_p4_CP":bool "Enab_p5_CD":bool "Enab_p5_CP":bool "Enab_p6_CD":bool "Enab_p6_CP":bool "Enab_p7_CD":bool "Enab_p7_CP":bool "root_CD":bool "root_CP":bool "p1_CD":bool "p1_CP":bool "p2_CD":bool "p2_CP":bool "p3_CD":bool "p3_CP":bool "p4_CD":bool "p4_CP":bool "p5_CD":bool "p5_CP":bool "p6_CD":bool "p6_CP":bool "p7_CD":bool "p7_CP":bool
#outputs "root_d":int "root_par":int "p1_d":int "p1_par":int "p2_d":int "p2_par":int "p3_d":int "p3_par":int "p4_d":int "p4_par":int "p5_d":int "p5_par":int "p6_d":int "p6_par":int "p7_d":int "p7_par":int "Enab_root_CD":bool "Enab_root_CP":bool "Enab_p1_CD":bool "Enab_p1_CP":bool "Enab_p2_CD":bool "Enab_p2_CP":bool "Enab_p3_CD":bool "Enab_p3_CP":bool "Enab_p4_CD":bool "Enab_p4_CP":bool "Enab_p5_CD":bool "Enab_p5_CP":bool "Enab_p6_CD":bool "Enab_p6_CP":bool "Enab_p7_CD":bool "Enab_p7_CP":bool "root_CD":bool "root_CP":bool "p1_CD":bool "p1_CP":bool "p2_CD":bool "p2_CP":bool "p3_CD":bool "p3_CP":bool "p4_CD":bool "p4_CP":bool "p5_CD":bool "p5_CP":bool "p6_CD":bool "p6_CP":bool "p7_CD":bool "p7_CP":bool "legitimate":bool
0 -1 0 1 0 0 0 1 2 1 0 0 0 1 1 0 f f t f t f t f t f t f t f f f f f t f t f t f t f t f t f f f
0 -1 1 1 1 0 1 1 1 1 1 0 1 1 1 0 f f f f t f t f t f t f t f f f f f f f t f t f t f t f t f f f
0 -1 1 1 2 0 2 1 2 1 2 0 2 1 1 0 f f f f f t t f t f t f f f f f f f f f f t t f t f t f f f f f
0 -1 1 1 2 2 3 1 3 1 3 0 2 1 1 0 f f f f f f f f f f f f f f f f f f f f f t t f t f t f f f f f
0 -1 0 1 0 0 0 1 2 1 0 0 0 1 1 0 f f t f t f t f t f t f t f f f f f t f t f t f t f t f t f f f f
0 -1 1 1 1 0 1 1 1 1 1 0 1 1 1 0 f f f f t f t f t f t f t f f f f f f f t f t f t f t f t f f f f
0 -1 1 1 2 0 2 1 2 1 2 0 2 1 1 0 f f f f f t t f t f t f f f f f f f f f f t t f t f t f f f f f f
0 -1 1 1 2 2 3 1 3 1 3 0 2 1 1 0 f f f f f f f f f f f f f f f f f f f f f t t f t f t f f f f f t
#This algo is silent after 15 moves, 3 steps, 4 rounds.
......
# Automatically generated by /home/jahier/.opam/4.10.0/bin/sasa version "4.3.27-1-g4eb78d9" ("4eb78d9")
# on crevetete the 4/5/2021 at 10:04:50
# Automatically generated by /home/jahier/.opam/4.12.0/bin/sasa version "v4.5.2" ("6122a58")
# on crevetete the 28/7/2021 at 11:30:02
#sasa -l 200 ring.dot -seed 42
#seed 42
#inputs
#outputs "p1_c":int "p2_c":int "p3_c":int "p4_c":int "p5_c":int "p6_c":int "p7_c":int "Enab_p1_conflict":bool "Enab_p2_conflict":bool "Enab_p3_conflict":bool "Enab_p4_conflict":bool "Enab_p5_conflict":bool "Enab_p6_conflict":bool "Enab_p7_conflict":bool "p1_conflict":bool "p2_conflict":bool "p3_conflict":bool "p4_conflict":bool "p5_conflict":bool "p6_conflict":bool "p7_conflict":bool potential:real
#outputs "p1_c":int "p2_c":int "p3_c":int "p4_c":int "p5_c":int "p6_c":int "p7_c":int "Enab_p1_conflict":bool "Enab_p2_conflict":bool "Enab_p3_conflict":bool "Enab_p4_conflict":bool "Enab_p5_conflict":bool "Enab_p6_conflict":bool "Enab_p7_conflict":bool "p1_conflict":bool "p2_conflict":bool "p3_conflict":bool "p4_conflict":bool "p5_conflict":bool "p6_conflict":bool "p7_conflict":bool "legitimate":bool potential:real
#step 0
#outs 0 1 1 1 1 1 0 t t t t t t t t t t f f f f 10.
#outs 0 1 1 1 1 1 0 t t t t t t t t t t f f f f f 10.
#step 1
#outs 2 2 0 1 1 1 0 t t f t t t f f f f t t t f 6.
#outs 2 2 0 1 1 1 0 t t f t t t f f f f t t t f f 6.
#step 2
#outs 2 2 0 2 0 2 0 t t f f f f f t t f f f f f 2.
#outs 2 2 0 2 0 2 0 t t f f f f f t t f f f f f f 2.
#step 3
#outs 1 1 0 2 0 2 0 t t f f f f f t f f f f f f 2.
#outs 1 1 0 2 0 2 0 t t f f f f f t f f f f f f f 2.
#step 4
#outs 2 1 0 2 0 2 0 f f f f f f f t f f f f f f 0.
#outs 2 1 0 2 0 2 0 f f f f f f f t f f f f f f t 0.
This algo is silent after 9 moves, 4 steps, 3 rounds.
......
# Automatically generated by /home/jahier/.opam/4.10.0/bin/sasa version "4.3.27-1-g4eb78d9" ("4eb78d9")
# on crevetete the 4/5/2021 at 10:04:50
# Automatically generated by /home/jahier/.opam/4.12.0/bin/sasa version "v4.5.2" ("6122a58")
# on crevetete the 28/7/2021 at 11:30:02
#sasa -l 200 grid4.dot -seed 42
#seed 42
#inputs
#outputs "p0_c":int "p1_c":int "p2_c":int "p3_c":int "p4_c":int "p5_c":int "p6_c":int "p7_c":int "p8_c":int "p9_c":int "p10_c":int "p11_c":int "p12_c":int "p13_c":int "p14_c":int "p15_c":int "Enab_p0_conflict":bool "Enab_p1_conflict":bool "Enab_p2_conflict":bool "Enab_p3_conflict":bool "Enab_p4_conflict":bool "Enab_p5_conflict":bool "Enab_p6_conflict":bool "Enab_p7_conflict":bool "Enab_p8_conflict":bool "Enab_p9_conflict":bool "Enab_p10_conflict":bool "Enab_p11_conflict":bool "Enab_p12_conflict":bool "Enab_p13_conflict":bool "Enab_p14_conflict":bool "Enab_p15_conflict":bool "p0_conflict":bool "p1_conflict":bool "p2_conflict":bool "p3_conflict":bool "p4_conflict":bool "p5_conflict":bool "p6_conflict":bool "p7_conflict":bool "p8_conflict":bool "p9_conflict":bool "p10_conflict":bool "p11_conflict":bool "p12_conflict":bool "p13_conflict":bool "p14_conflict":bool "p15_conflict":bool potential:real
#outputs "p0_c":int "p1_c":int "p2_c":int "p3_c":int "p4_c":int "p5_c":int "p6_c":int "p7_c":int "p8_c":int "p9_c":int "p10_c":int "p11_c":int "p12_c":int "p13_c":int "p14_c":int "p15_c":int "Enab_p0_conflict":bool "Enab_p1_conflict":bool "Enab_p2_conflict":bool "Enab_p3_conflict":bool "Enab_p4_conflict":bool "Enab_p5_conflict":bool "Enab_p6_conflict":bool "Enab_p7_conflict":bool "Enab_p8_conflict":bool "Enab_p9_conflict":bool "Enab_p10_conflict":bool "Enab_p11_conflict":bool "Enab_p12_conflict":bool "Enab_p13_conflict":bool "Enab_p14_conflict":bool "Enab_p15_conflict":bool "p0_conflict":bool "p1_conflict":bool "p2_conflict":bool "p3_conflict":bool "p4_conflict":bool "p5_conflict":bool "p6_conflict":bool "p7_conflict":bool "p8_conflict":bool "p9_conflict":bool "p10_conflict":bool "p11_conflict":bool "p12_conflict":bool "p13_conflict":bool "p14_conflict":bool "p15_conflict":bool "legitimate":bool potential:real
#step 0
#outs 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 t t t t t t t t t t t t t t t t t f f f f f f t f f f f t t t f 48.
#outs 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 t t t t t t t t t t t t t t t t t f f f f f f t f f f f t t t f f 48.
#step 1
#outs 1 0 0 0 0 0 0 1 0 0 0 0 1 1 1 0 f t t t t t t f t t t t t t t t f f f f t t f f f f f t t f f t 30.
#outs 1 0 0 0 0 0 0 1 0 0 0 0 1 1 1 0 f t t t t t t f t t t t t t t t f f f f t t f f f f f t t f f t f 30.
#step 2
#outs 1 0 0 0 2 1 0 1 0 0 0 2 2 1 1 2 f t t t f f t f t t t t f t t t f t f t f f f f t t f f f f f f 16.
#outs 1 0 0 0 2 1 0 1 0 0 0 2 2 1 1 2 f t t t f f t f t t t t f t t t f t f t f f f f t t f f f f f f f 16.
#step 3
#outs 1 2 0 2 2 1 0 1 1 2 0 2 2 1 1 2 f f t f f f t f f f t t f t t t f f f f f f t f f f f f f t t f 8.
#outs 1 2 0 2 2 1 0 1 1 2 0 2 2 1 1 2 f f t f f f t f f f t t f t t t f f f f f f t f f f f f f t t f f 8.
#step 4
#outs 1 2 0 2 2 1 2 1 1 2 0 2 2 0 3 2 f f f f f f f f f f f t f f f t f f f f f f f f f f f t f f f t 2.
#outs 1 2 0 2 2 1 2 1 1 2 0 2 2 0 3 2 f f f f f f f f f f f t f f f t f f f f f f f f f f f t f f f t f 2.
#step 5
#outs 1 2 0 2 2 1 2 1 1 2 0 3 2 0 3 0 f f f f f f f f f f f f f f f f f f f f f f f f f f f t f f f t 0.
#outs 1 2 0 2 2 1 2 1 1 2 0 3 2 0 3 0 f f f f f f f f f f f f f f f f f f f f f f f f f f f t f f f t t 0.
This algo is silent after 19 moves, 5 steps, 2 rounds.
......
(* Time-stamp: <modified the 02/09/2020 (at 10:37) by Erwan Jahier> *)
(* Time-stamp: <modified the 28/07/2021 (at 09:01) by Erwan Jahier> *)
(* This is algo 3.1 in the book *)
open Algo
let k=max_degree () + 1
let k = if is_directed () then
failwith "this algo is for non-directed graphs!" card()+1
else
max_degree () + 1
let (init_state: int -> string -> 'v) = fun i _ -> Random.int i
......
#inputs
#outputs "p1_path0":int "p1_path1":int "p1_path2":int "p1_path3":int "p1_path4":int "p1_path5":int "p1_path6":int "p1_path7":int "p1_path8":int "p1_path9":int "p1_par":int "p2_path0":int "p2_path1":int "p2_path2":int "p2_path3":int "p2_path4":int "p2_path5":int "p2_path6":int "p2_path7":int "p2_path8":int "p2_path9":int "p2_par":int "p3_path0":int "p3_path1":int "p3_path2":int "p3_path3":int "p3_path4":int "p3_path5":int "p3_path6":int "p3_path7":int "p3_path8":int "p3_path9":int "p3_par":int "p4_path0":int "p4_path1":int "p4_path2":int "p4_path3":int "p4_path4":int "p4_path5":int "p4_path6":int "p4_path7":int "p4_path8":int "p4_path9":int "p4_par":int "p5_path0":int "p5_path1":int "p5_path2":int "p5_path3":int "p5_path4":int "p5_path5":int "p5_path6":int "p5_path7":int "p5_path8":int "p5_path9":int "p5_par":int "p6_path0":int "p6_path1":int "p6_path2":int "p6_path3":int "p6_path4":int "p6_path5":int "p6_path6":int "p6_path7":int "p6_path8":int "p6_path9":int "p6_par":int "p7_path0":int "p7_path1":int "p7_path2":int "p7_path3":int "p7_path4":int "p7_path5":int "p7_path6":int "p7_path7":int "p7_path8":int "p7_path9":int "p7_par":int "p8_path0":int "p8_path1":int "p8_path2":int "p8_path3":int "p8_path4":int "p8_path5":int "p8_path6":int "p8_path7":int "p8_path8":int "p8_path9":int "p8_par":int "p9_path0":int "p9_path1":int "p9_path2":int "p9_path3":int "p9_path4":int "p9_path5":int "p9_path6":int "p9_path7":int "p9_path8":int "p9_path9":int "p9_par":int "p10_path0":int "p10_path1":int "p10_path2":int "p10_path3":int "p10_path4":int "p10_path5":int "p10_path6":int "p10_path7":int "p10_path8":int "p10_path9":int "p10_par":int "Enab_p1_update_path":bool "Enab_p1_compute_parent":bool "Enab_p2_update_path":bool "Enab_p2_compute_parent":bool "Enab_p3_update_path":bool "Enab_p3_compute_parent":bool "Enab_p4_update_path":bool "Enab_p4_compute_parent":bool "Enab_p5_update_path":bool "Enab_p5_compute_parent":bool "Enab_p6_update_path":bool "Enab_p6_compute_parent":bool "Enab_p7_update_path":bool "Enab_p7_compute_parent":bool "Enab_p8_update_path":bool "Enab_p8_compute_parent":bool "Enab_p9_update_path":bool "Enab_p9_compute_parent":bool "Enab_p10_update_path":bool "Enab_p10_compute_parent":bool "p1_update_path":bool "p1_compute_parent":bool "p2_update_path":bool "p2_compute_parent":bool "p3_update_path":bool "p3_compute_parent":bool "p4_update_path":bool "p4_compute_parent":bool "p5_update_path":bool "p5_compute_parent":bool "p6_update_path":bool "p6_compute_parent":bool "p7_update_path":bool "p7_compute_parent":bool "p8_update_path":bool "p8_compute_parent":bool "p9_update_path":bool "p9_compute_parent":bool "p10_update_path":bool "p10_compute_parent":bool
#outputs "p1_path0":int "p1_path1":int "p1_path2":int "p1_path3":int "p1_path4":int "p1_path5":int "p1_path6":int "p1_path7":int "p1_path8":int "p1_path9":int "p1_par":int "p2_path0":int "p2_path1":int "p2_path2":int "p2_path3":int "p2_path4":int "p2_path5":int "p2_path6":int "p2_path7":int "p2_path8":int "p2_path9":int "p2_par":int "p3_path0":int "p3_path1":int "p3_path2":int "p3_path3":int "p3_path4":int "p3_path5":int "p3_path6":int "p3_path7":int "p3_path8":int "p3_path9":int "p3_par":int "p4_path0":int "p4_path1":int "p4_path2":int "p4_path3":int "p4_path4":int "p4_path5":int "p4_path6":int "p4_path7":int "p4_path8":int "p4_path9":int "p4_par":int "p5_path0":int "p5_path1":int "p5_path2":int "p5_path3":int "p5_path4":int "p5_path5":int "p5_path6":int "p5_path7":int "p5_path8":int "p5_path9":int "p5_par":int "p6_path0":int "p6_path1":int "p6_path2":int "p6_path3":int "p6_path4":int "p6_path5":int "p6_path6":int "p6_path7":int "p6_path8":int "p6_path9":int "p6_par":int "p7_path0":int "p7_path1":int "p7_path2":int "p7_path3":int "p7_path4":int "p7_path5":int "p7_path6":int "p7_path7":int "p7_path8":int "p7_path9":int "p7_par":int "p8_path0":int "p8_path1":int "p8_path2":int "p8_path3":int "p8_path4":int "p8_path5":int "p8_path6":int "p8_path7":int "p8_path8":int "p8_path9":int "p8_par":int "p9_path0":int "p9_path1":int "p9_path2":int "p9_path3":int "p9_path4":int "p9_path5":int "p9_path6":int "p9_path7":int "p9_path8":int "p9_path9":int "p9_par":int "p10_path0":int "p10_path1":int "p10_path2":int "p10_path3":int "p10_path4":int "p10_path5":int "p10_path6":int "p10_path7":int "p10_path8":int "p10_path9":int "p10_par":int "Enab_p1_update_path":bool "Enab_p1_compute_parent":bool "Enab_p2_update_path":bool "Enab_p2_compute_parent":bool "Enab_p3_update_path":bool "Enab_p3_compute_parent":bool "Enab_p4_update_path":bool "Enab_p4_compute_parent":bool "Enab_p5_update_path":bool "Enab_p5_compute_parent":bool "Enab_p6_update_path":bool "Enab_p6_compute_parent":bool "Enab_p7_update_path":bool "Enab_p7_compute_parent":bool "Enab_p8_update_path":bool "Enab_p8_compute_parent":bool "Enab_p9_update_path":bool "Enab_p9_compute_parent":bool "Enab_p10_update_path":bool "Enab_p10_compute_parent":bool "p1_update_path":bool "p1_compute_parent":bool "p2_update_path":bool "p2_compute_parent":bool "p3_update_path":bool "p3_compute_parent":bool "p4_update_path":bool "p4_compute_parent":bool "p5_update_path":bool "p5_compute_parent":bool "p6_update_path":bool "p6_compute_parent":bool "p7_update_path":bool "p7_compute_parent":bool "p8_update_path":bool "p8_compute_parent":bool "p9_update_path":bool "p9_compute_parent":bool "p10_update_path":bool "p10_compute_parent":bool "legitimate":bool
-1 -1 -1 -1 -1 -1 -1 -1 -1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 3 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -10 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 1 t f t f f f t f t f t f t f t f t f t f t f t f f f t f t f t f t f t f t f t f
-1 3 -1 -1 -1 -1 -1 -1 -1 -1 0 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 3 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -10 -1 1 -1 -1 -1 -1 -1 -1 -1 -1 0 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 0 -1 1 -1 -1 -1 -1 -1 -1 -1 -1 1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 0 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 1 t f t f f f t f t f f t t f t f t f t f t f t f f f t f t f f t t f t f t f t f
-1 0 3 -1 -1 -1 -1 -1 -1 -1 0 -1 0 0 -1 -1 -1 -1 -1 -1 -1 3 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -10 -1 0 1 -1 -1 -1 -1 -1 -1 -1 0 -1 0 0 -1 -1 -1 -1 -1 -1 -1 1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 2 -1 0 1 -1 -1 -1 -1 -1 -1 -1 1 -1 0 1 -1 -1 -1 -1 -1 -1 -1 0 -1 0 0 -1 -1 -1 -1 -1 -1 -1 1 -1 0 0 -1 -1 -1 -1 -1 -1 -1 1 t f t f f f t f t f f f f f t f t f f t t f t f f f t f t f f f f f t f t f f t
-1 0 0 3 -1 -1 -1 -1 -1 -1 0 -1 0 0 0 -1 -1 -1 -1 -1 -1 3 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -10 -1 0 0 1 -1 -1 -1 -1 -1 -1 0 -1 0 0 0 -1 -1 -1 -1 -1 -1 1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 2 -1 0 1 -1 -1 -1 -1 -1 -1 -1 1 -1 0 0 1 -1 -1 -1 -1 -1 -1 0 -1 0 0 1 -1 -1 -1 -1 -1 -1 1 -1 0 0 -1 -1 -1 -1 -1 -1 -1 0 t f t f f f t f t f f f t f t f f t f f t f t f f f t f t f f f t f t f f t f f
-1 0 0 0 3 -1 -1 -1 -1 -1 0 -1 0 0 0 0 -1 -1 -1 -1 -1 3 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -10 -1 0 0 0 1 -1 -1 -1 -1 -1 0 -1 0 0 0 0 -1 -1 -1 -1 -1 1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 2 -1 0 0 1 1 -1 -1 -1 -1 -1 1 -1 0 0 1 1 -1 -1 -1 -1 -1 0 -1 0 0 1 -1 -1 -1 -1 -1 -1 0 -1 0 0 -1 -1 -1 -1 -1 -1 -1 0 t f t f f f t f t f f f t f f f f f f f t f t f f f t f t f f f t f f f f f f f
-1 0 0 0 0 3 -1 -1 -1 -1 0 -1 0 0 0 0 0 -1 -1 -1 -1 3 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -10 -1 0 0 0 0 1 -1 -1 -1 -1 0 -1 0 0 0 0 0 -1 -1 -1 -1 1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 2 -1 0 0 1 1 1 -1 -1 -1 -1 1 -1 0 0 1 1 -1 -1 -1 -1 -1 0 -1 0 0 1 -1 -1 -1 -1 -1 -1 0 -1 0 0 -1 -1 -1 -1 -1 -1 -1 0 t f t f f f t f t f f f f t f f f f f f t f t f f f t f t f f f f t f f f f f f
-1 0 0 0 0 0 3 -1 -1 -1 0 -1 0 0 0 0 0 0 -1 -1 -1 3 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -10 -1 0 0 0 0 0 1 -1 -1 -1 0 -1 0 0 0 0 0 0 -1 -1 -1 1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 2 -1 0 0 1 1 1 -1 -1 -1 -1 0 -1 0 0 1 1 -1 -1 -1 -1 -1 0 -1 0 0 1 -1 -1 -1 -1 -1 -1 0 -1 0 0 -1 -1 -1 -1 -1 -1 -1 0 t f t f f f t f t f f f f f f f f f f f t f t f f f t f t f f f f f f f f f f f
-1 0 0 0 0 0 0 3 -1 -1 0 -1 0 0 0 0 0 0 0 -1 -1 3 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -10 -1 0 0 0 0 0 0 1 -1 -1 0 -1 0 0 0 0 0 0 0 -1 -1 1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 2 -1 0 0 1 1 1 -1 -1 -1 -1 0 -1 0 0 1 1 -1 -1 -1 -1 -1 0 -1 0 0 1 -1 -1 -1 -1 -1 -1 0 -1 0 0 -1 -1 -1 -1 -1 -1 -1 0 t f t f f f t f t f f f f f f f f f f f t f t f f f t f t f f f f f f f f f f f
-1 0 0 0 0 0 0 0 3 -1 0 -1 0 0 0 0 0 0 0 0 -1 3 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -10 -1 0 0 0 0 0 0 0 1 -1 0 -1 0 0 0 0 0 0 0 0 -1 1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 2 -1 0 0 1 1 1 -1 -1 -1 -1 0 -1 0 0 1 1 -1 -1 -1 -1 -1 0 -1 0 0 1 -1 -1 -1 -1 -1 -1 0 -1 0 0 -1 -1 -1 -1 -1 -1 -1 0 t f t f f f t f t f f f f f f f f f f f t f t f f f t f t f f f f f f f f f f f
-1 0 0 0 0 0 0 0 0 3 0 -1 0 0 0 0 0 0 0 0 0 3 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -10 -1 0 0 0 0 0 0 0 0 1 0 -1 0 0 0 0 0 0 0 0 0 1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 2 -1 0 0 1 1 1 -1 -1 -1 -1 0 -1 0 0 1 1 -1 -1 -1 -1 -1 0 -1 0 0 1 -1 -1 -1 -1 -1 -1 0 -1 0 0 -1 -1 -1 -1 -1 -1 -1 0 t f t f f f t f t f f f f f f f f f f f t f t f f f t f t f f f f f f f f f f f
0 0 0 0 0 0 0 0 0 3 0 -1 2 -1 -1 -1 -1 -1 -1 -1 -1 3 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -10 -1 1 -1 -1 -1 -1 -1 -1 -1 -1 0 0 0 0 0 0 0 0 0 0 0 1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 2 -1 0 0 1 1 1 -1 -1 -1 -1 0 -1 0 0 1 1 -1 -1 -1 -1 -1 0 -1 0 0 1 -1 -1 -1 -1 -1 -1 0 -1 0 0 -1 -1 -1 -1 -1 -1 -1 0 t f t f f f f t t f f f f f f f f f f f t f t f f f f t t f f f f f f f f f f f
-1 2 3 -1 -1 -1 -1 -1 -1 -1 0 -1 1 1 -1 -1 -1 -1 -1 -1 -1 3 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -10 -1 1 -1 -1 -1 -1 -1 -1 -1 -1 2 -1 1 0 -1 -1 -1 -1 -1 -1 -1 1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 2 -1 0 0 1 1 1 -1 -1 -1 -1 0 -1 0 0 1 1 -1 -1 -1 -1 -1 0 -1 0 0 1 -1 -1 -1 -1 -1 -1 0 -1 0 0 -1 -1 -1 -1 -1 -1 -1 0 t f t f f f f f f f f f f f f f f f f f t f t f f f f f f f f f f f f f f f f f
-1 1 1 3 -1 -1 -1 -1 -1 -1 0 -1 1 0 0 -1 -1 -1 -1 -1 -1 3 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -10 -1 1 -1 -1 -1 -1 -1 -1 -1 -1 2 -1 1 0 -1 -1 -1 -1 -1 -1 -1 1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 2 -1 0 0 1 1 1 -1 -1 -1 -1 0 -1 0 0 1 1 -1 -1 -1 -1 -1 0 -1 0 0 1 -1 -1 -1 -1 -1 -1 0 -1 0 0 -1 -1 -1 -1 -1 -1 -1 0 t f f t f f f f f f f f f f f f f f f f t f f t f f f f f f f f f f f f f f f f
-1 1 0 0 3 -1 -1 -1 -1 -1 0 -1 1 0 0 -1 -1 -1 -1 -1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -10 -1 1 -1 -1 -1 -1 -1 -1 -1 -1 2 -1 1 0 -1 -1 -1 -1 -1 -1 -1 1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 2 -1 0 0 1 1 1 -1 -1 -1 -1 0 -1 0 0 1 1 -1 -1 -1 -1 -1 0 -1 0 0 1 -1 -1 -1 -1 -1 -1 0 -1 0 0 -1 -1 -1 -1 -1 -1 -1 0 f f f f f f f f f f f f f f f f f f f f t f f t f f f f f f f f f f f f f f f f
-1 -1 -1 -1 -1 -1 -1 -1 -1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 3 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -10 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 1 t f t f f f t f t f t f t f t f t f t f t f t f f f t f t f t f t f t f t f t f f
-1 3 -1 -1 -1 -1 -1 -1 -1 -1 0 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 3 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -10 -1 1 -1 -1 -1 -1 -1 -1 -1 -1 0 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 0 -1 1 -1 -1 -1 -1 -1 -1 -1 -1 1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 0 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 1 t f t f f f t f t f f t t f t f t f t f t f t f f f t f t f f t t f t f t f t f f
-1 0 3 -1 -1 -1 -1 -1 -1 -1 0 -1 0 0 -1 -1 -1 -1 -1 -1 -1 3 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -10 -1 0 1 -1 -1 -1 -1 -1 -1 -1 0 -1 0 0 -1 -1 -1 -1 -1 -1 -1 1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 2 -1 0 1 -1 -1 -1 -1 -1 -1 -1 1 -1 0 1 -1 -1 -1 -1 -1 -1 -1 0 -1 0 0 -1 -1 -1 -1 -1 -1 -1 1 -1 0 0 -1 -1 -1 -1 -1 -1 -1 1 t f t f f f t f t f f f f f t f t f f t t f t f f f t f t f f f f f t f t f f t f
-1 0 0 3 -1 -1 -1 -1 -1 -1 0 -1 0 0 0 -1 -1 -1 -1 -1 -1 3 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -10 -1 0 0 1 -1 -1 -1 -1 -1 -1 0 -1 0 0 0 -1 -1 -1 -1 -1 -1 1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 2 -1 0 1 -1 -1 -1 -1 -1 -1 -1 1 -1 0 0 1 -1 -1 -1 -1 -1 -1 0 -1 0 0 1 -1 -1 -1 -1 -1 -1 1 -1 0 0 -1 -1 -1 -1 -1 -1 -1 0 t f t f f f t f t f f f t f t f f t f f t f t f f f t f t f f f t f t f f t f f f
-1 0 0 0 3 -1 -1 -1 -1 -1 0 -1 0 0 0 0 -1 -1 -1 -1 -1 3 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -10 -1 0 0 0 1 -1 -1 -1 -1 -1 0 -1 0 0 0 0 -1 -1 -1 -1 -1 1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 2 -1 0 0 1 1 -1 -1 -1 -1 -1 1 -1 0 0 1 1 -1 -1 -1 -1 -1 0 -1 0 0 1 -1 -1 -1 -1 -1 -1 0 -1 0 0 -1 -1 -1 -1 -1 -1 -1 0 t f t f f f t f t f f f t f f f f f f f t f t f f f t f t f f f t f f f f f f f f
-1 0 0 0 0 3 -1 -1 -1 -1 0 -1 0 0 0 0 0 -1 -1 -1 -1 3 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -10 -1 0 0 0 0 1 -1 -1 -1 -1 0 -1 0 0 0 0 0 -1 -1 -1 -1 1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 2 -1 0 0 1 1 1 -1 -1 -1 -1 1 -1 0 0 1 1 -1 -1 -1 -1 -1 0 -1 0 0 1 -1 -1 -1 -1 -1 -1 0 -1 0 0 -1 -1 -1 -1 -1 -1 -1 0 t f t f f f t f t f f f f t f f f f f f t f t f f f t f t f f f f t f f f f f f f
-1 0 0 0 0 0 3 -1 -1 -1 0 -1 0 0 0 0 0 0 -1 -1 -1 3 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -10 -1 0 0 0 0 0 1 -1 -1 -1 0 -1 0 0 0 0 0 0 -1 -1 -1 1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 2 -1 0 0 1 1 1 -1 -1 -1 -1 0 -1 0 0 1 1 -1 -1 -1 -1 -1 0 -1 0 0 1 -1 -1 -1 -1 -1 -1 0 -1 0 0 -1 -1 -1 -1 -1 -1 -1 0 t f t f f f t f t f f f f f f f f f f f t f t f f f t f t f f f f f f f f f f f f
-1 0 0 0 0 0 0 3 -1 -1 0 -1 0 0 0 0 0 0 0 -1 -1 3 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -10 -1 0 0 0 0 0 0 1 -1 -1 0 -1 0 0 0 0 0 0 0 -1 -1 1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 2 -1 0 0 1 1 1 -1 -1 -1 -1 0 -1 0 0 1 1 -1 -1 -1 -1 -1 0 -1 0 0 1 -1 -1 -1 -1 -1 -1 0 -1 0 0 -1 -1 -1 -1 -1 -1 -1 0 t f t f f f t f t f f f f f f f f f f f t f t f f f t f t f f f f f f f f f f f f
-1 0 0 0 0 0 0 0 3 -1 0 -1 0 0 0 0 0 0 0 0 -1 3 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -10 -1 0 0 0 0 0 0 0 1 -1 0 -1 0 0 0 0 0 0 0 0 -1 1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 2 -1 0 0 1 1 1 -1 -1 -1 -1 0 -1 0 0 1 1 -1 -1 -1 -1 -1 0 -1 0 0 1 -1 -1 -1 -1 -1 -1 0 -1 0 0 -1 -1 -1 -1 -1 -1 -1 0 t f t f f f t f t f f f f f f f f f f f t f t f f f t f t f f f f f f f f f f f f
-1 0 0 0 0 0 0 0 0 3 0 -1 0 0 0 0 0 0 0 0 0 3 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -10 -1 0 0 0 0 0 0 0 0 1 0 -1 0 0 0 0 0 0 0 0 0 1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 2 -1 0 0 1 1 1 -1 -1 -1 -1 0 -1 0 0 1 1 -1 -1 -1 -1 -1 0 -1 0 0 1 -1 -1 -1 -1 -1 -1 0 -1 0 0 -1 -1 -1 -1 -1 -1 -1 0 t f t f f f t f t f f f f f f f f f f f t f t f f f t f t f f f f f f f f f f f f
0 0 0 0 0 0 0 0 0 3 0 -1 2 -1 -1 -1 -1 -1 -1 -1 -1 3 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -10 -1 1 -1 -1 -1 -1 -1 -1 -1 -1 0 0 0 0 0 0 0 0 0 0 0 1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 2 -1 0 0 1 1 1 -1 -1 -1 -1 0 -1 0 0 1 1 -1 -1 -1 -1 -1 0 -1 0 0 1 -1 -1 -1 -1 -1 -1 0 -1 0 0 -1 -1 -1 -1 -1 -1 -1 0 t f t f f f f t t f f f f f f f f f f f t f t f f f f t t f f f f f f f f f f f f
-1 2 3 -1 -1 -1 -1 -1 -1 -1 0 -1 1 1 -1 -1 -1 -1 -1 -1 -1 3 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -10 -1 1 -1 -1 -1 -1 -1 -1 -1 -1 2 -1 1 0 -1 -1 -1 -1 -1 -1 -1 1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 2 -1 0 0 1 1 1 -1 -1 -1 -1 0 -1 0 0 1 1 -1 -1 -1 -1 -1 0 -1 0 0 1 -1 -1 -1 -1 -1 -1 0 -1 0 0 -1 -1 -1 -1 -1 -1 -1 0 t f t f f f f f f f f f f f f f f f f f t f t f f f f f f f f f f f f f f f f f f
-1 1 1 3 -1 -1 -1 -1 -1 -1 0 -1 1 0 0 -1 -1 -1 -1 -1 -1 3 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -10 -1 1 -1 -1 -1 -1 -1 -1 -1 -1 2 -1 1 0 -1 -1 -1 -1 -1 -1 -1 1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 2 -1 0 0 1 1 1 -1 -1 -1 -1 0 -1 0 0 1 1 -1 -1 -1 -1 -1 0 -1 0 0 1 -1 -1 -1 -1 -1 -1 0 -1 0 0 -1 -1 -1 -1 -1 -1 -1 0 t f f t f f f f f f f f f f f f f f f f t f f t f f f f f f f f f f f f f f f f f
-1 1 0 0 3 -1 -1 -1 -1 -1 0 -1 1 0 0 -1 -1 -1 -1 -1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -10 -1 1 -1 -1 -1 -1 -1 -1 -1 -1 2 -1 1 0 -1 -1 -1 -1 -1 -1 -1 1 -1 0 -1 -1 -1 -1 -1 -1 -1 -1 2 -1 0 0 1 1 1 -1 -1 -1 -1 0 -1 0 0 1 1 -1 -1 -1 -1 -1 0 -1 0 0 1 -1 -1 -1 -1 -1 -1 0 -1 0 0 -1 -1 -1 -1 -1 -1 -1 0 f f f f f f f f f f f f f f f f f f f f t f f t f f f f f f f f f f f f f f f f t
#This algo is silent after 66 moves, 13 steps, 14 rounds.
......
This diff is collapsed.
# Time-stamp: <modified the 11/05/2021 (at 16:46) by Erwan Jahier>
# Time-stamp: <modified the 28/07/2021 (at 11:44) by Erwan Jahier>
test: ring.cmxs lurette1 rdbg_test
......@@ -52,4 +52,4 @@ lurette1: ring.lut ring_oracle.lus
-include Makefile.untracked
clean: genclean
rm -f ring_oracle.lus ring.ml
rm -f ring.ml
open Algo
open State
let potential = None
(** Computes the value Z of the book, that is 0 if the values are convex,
* and the minimum number of incrementations the root has to do so that its value
* is different to every other value of the ring.
*
* A disposition is convex if there is no value that is the same than the root seperated from the
* root with another value.
* 2 2 2 3 0 1 3 -> convex
* 2 4 5 3 0 1 3 -> convex
* 2 2 2 3 0 2 3 -> not convex
*)
let compute_Z root root_st (get: Algo.pid -> State.t * (State.t Algo.neighbor * Algo.pid) list) =
let v = root_st.v in
let used = Array.make (card () + 1) false in
let rec convex pid encountered res =
(* Printf.eprintf (if encountered then "<" else "|"); *)
(* Printf.eprintf (if res then ">" else "|"); *)
let next_st, next =
match get pid with
(_, [s,n]) -> state s, n | _ -> failwith "Can't compute the cost of a topology that is not a directed ring"
in
if next = root then res
else
let next_v = next_st.v in
(* Printf.eprintf "%s %d" next next_v; *)
used.(next_v) <- true;
convex next (encountered || next_v = v) (res && (not encountered || next_v = v))
in
if convex root false true
then 0
else
let rec get_min_free cur_val dist =
if cur_val = v then assert false;
if not used.(cur_val) then dist
else
get_min_free ((cur_val + 1) mod (card () + 1)) (dist + 1)
in
get_min_free (v+1) 1
;;
(* Computes the sum_dist as described in the book. It is the sum of the distance
from each token to the root *)
let compute_sd (root: pid) (get: Algo.pid -> State.t * (State.t Algo.neighbor * Algo.pid) list) =
let rec compute pid total rang =
if pid = root then total
else
let st, ((n_state, neighbor): 's * pid) =
match get pid with
(st, [n]) -> st, n | _ -> failwith "Can't compute the cost of a topology that is not a directed ring"
in
let total = if (P.enable_f st [n_state]) <> [] then total + rang else total in
compute neighbor total (rang+1)
in
let succ: pid =
match get root with
(_, [_, n]) -> n | _ -> failwith "Can't compute the cost of a topology that is not a directed ring"
in
compute succ 0 1
;;
(* Computes the cost (it's the regular cost not the tighter_cost) *)
let cost : pid list -> (pid -> t * (t neighbor * pid) list) -> float =
fun pidl get ->
let root = List.find (fun p -> (fst (get p)).root) pidl in
let root_st = fst (get root) in
let n = card() in
let z = compute_Z root root_st get in
let c = if z = (n - 1)
then (3 * n * (n - 1) / 2) - n - 1
else
let sum_dist = compute_sd root get in
let res = z * n + sum_dist - 2 in
if res < 0 then 0 else res
in
float_of_int c
;;
let potential = Some cost
let fault = None
(* For the Dijkstra ring, a configuration is legitimate iff there is
......
include "../lustre/oracle_utils.lus"
-----------------------------------------------------------------------------
node theorem_6_29<<const m : int; const n: int>> (Enab, Acti: bool^m^n) returns (res:bool);
node theorem_6_29<<const m : int; const n: int>> (legitimate:bool; Acti: bool^m^n)
returns (res:bool);
var
Silent:bool;
MoveNb:int ;
let
Silent = silent<<m,n>>(Enab);
MoveNb = 1 -> pre(MoveNb) + 1;
res = (k>=n)=>((((3*n*(n-1))/2)<MoveNb)=>Silent) ; -- Theorem 6.29
MoveNb = move_count(Acti);
res = (k>=n)=>(( (3*n*(n-1))/2 < MoveNb) => legitimate) ; -- Theorem 6.29
tel
-----------------------------------------------------------------------------
node lemma_6_28<<const m : int; const n: int>> (Enab, Acti: bool^m^n) returns (res:bool);
node lemma_6_28<<const m : int; const n: int>>
(legitimate:bool; Acti: bool^m^n) returns (res:bool);
var
Xn:int;
Silent:bool;
MoveNb:int;
let
Xn = 0 -> if(Acti[0][0]) then pre(Xn) + 1 else pre(Xn) ;
Silent = silent<<m,n>>(Enab);
MoveNb = move_count(Acti);
res = (((n*(n-1)/2) + Xn*n)<MoveNb) => Silent ; -- Lemma 6.28
res = (((n*(n-1)/2) + Xn*n)<MoveNb) => legitimate ; -- Lemma 6.28
tel
-----------------------------------------------------------------------------
node dijkstra_ring_oracle<<const an:int; const pn:int>> (Enab, Acti: bool^an^pn)
returns (ok:bool);
node dijkstra_ring_oracle<<const an:int; const pn:int>>
(legitimate:bool; Enab, Acti: bool^an^pn) returns (ok:bool);
let
ok = lemma_6_28 <<an,pn>> (legitimate, Acti) and
theorem_6_29<<an,pn>> (legitimate, Acti);
tel
node dijkstra_ring_oracle_cov<<const an:int; const pn:int>>
(legitimate:bool; Enab, Acti: bool^an^pn) returns (ok:bool; WortCaseReached : bool);
var
WortCase : int;
MoveNb:int;
let
MoveNb = move_count(Acti);
WortCase=(3*pn*(pn-1))/2;
WortCaseReached = (WortCase = MoveNb);
ok = lemma_6_28 <<an,pn>> (Enab, Acti) and
theorem_6_29<<an,pn>> (Enab, Acti);
ok = dijkstra_ring_oracle <<an,pn>> (legitimate, Enab, Acti);
tel
# Automatically generated by /home/jahier/.opam/4.10.0/bin/sasa version "4.3.27-1-g4eb78d9" ("4eb78d9")
# on crevetete the 4/5/2021 at 10:27:26
# Automatically generated by /home/jahier/.opam/4.12.0/bin/sasa version "v4.5.2" ("6122a58")
# on crevetete the 31/7/2021 at 9:17:22
#sasa ring.dot -seed 42
#seed 42
#inputs
#outputs "root_c":int "p2_c":int "p3_c":int "p4_c":int "p5_c":int "p6_c":int "p7_c":int "p8_c":int "Enab_root_T":bool "Enab_p2_T":bool "Enab_p3_T":bool "Enab_p4_T":bool "Enab_p5_T":bool "Enab_p6_T":bool "Enab_p7_T":bool "Enab_p8_T":bool "root_T":bool "p2_T":bool "p3_T":bool "p4_T":bool "p5_T":bool "p6_T":bool "p7_T":bool "p8_T":bool
#outputs "root_c":int "p2_c":int "p3_c":int "p4_c":int "p5_c":int "p6_c":int "p7_c":int "p8_c":int "Enab_root_T":bool "Enab_p2_T":bool "Enab_p3_T":bool "Enab_p4_T":bool "Enab_p5_T":bool "Enab_p6_T":bool "Enab_p7_T":bool "Enab_p8_T":bool "root_T":bool "p2_T":bool "p3_T":bool "p4_T":bool "p5_T":bool "p6_T":bool "p7_T":bool "p8_T":bool "legitimate":bool potential:real
#step 0
#outs 1 3 3 2 2 1 1 0 f f t f t f t t f f f f f f t f
#outs 1 3 3 2 2 1 1 0 f f t f t f t t f f f f f f t f f 41.
#step 1
#outs 1 3 3 2 2 1 0 0 f f t f t t f t f f f f t t f t
#outs 1 3 3 2 2 1 0 0 f f t f t t f t f f f f t t f t f 40.
#step 2
#outs 1 3 3 2 1 0 0 1 f f t t t f t f f f f f f f t f
#outs 1 3 3 2 1 0 0 1 f f t t t f t f f f f f f f t f f 37.
#step 3
#outs 1 3 3 2 1 0 1 1 f f t t t t f f f f t t t f f f
#outs 1 3 3 2 1 0 1 1 f f t t t t f f f f t t t f f f f 36.
#step 4
#outs 1 3 2 1 0 0 1 1 f t t t f t f f f f f f f t f f
#outs 1 3 2 1 0 0 1 1 f t t t f t f f f f f f f t f f f 33.
#step 5
#outs 1 3 2 1 0 1 1 1 f t t t t f f f f t t f f f f f
#outs 1 3 2 1 0 1 1 1 f t t t t f f f f t t f f f f f f 32.
#step 6
#outs 1 2 1 1 0 1 1 1 f t f t t f f f f f f f t f f f
#outs 1 2 1 1 0 1 1 1 f t f t t f f f f f f f t f f f f 22.
#step 7
#outs 1 2 1 1 1 1 1 1 f t f f f f f f f f f f t f f f
#outs 1 2 1 1 1 1 1 1 f t f f f f f f f f f f t f f f t 0.
#This algo reached a legitimate configuration after 12 moves, 7 steps, 1 round.
......