From 4cab2b972b42d7c9b89a0a1b9966edb2ccbe12e2 Mon Sep 17 00:00:00 2001 From: Guillaume Raffin <guillaume.raffin@grenoble-inp.org> Date: Wed, 26 May 2021 08:56:07 +0000 Subject: [PATCH] Toy example (Guillaume) --- .gitignore | 3 +- lib/algo/algo.ml | 43 ++-- lib/algo/algo.mli | 78 ++++--- lib/sasacore/dune | 4 +- lib/sasacore/register.ml | 138 +++++++------ lib/sasacore/register.mli | 13 +- lib/sasacore/topology.ml | 203 +++++++++++-------- lib/sasacore/topology.mli | 3 +- src/dune | 5 +- test/toy-example-sum/.gitignore | 3 + test/toy-example-sum/Makefile | 43 ++++ test/toy-example-sum/config.ml | 54 +++++ test/toy-example-sum/heuristic-bad-propag.ml | 132 ++++++++++++ test/toy-example-sum/heuristic-explore.ml | 202 ++++++++++++++++++ test/toy-example-sum/my-rdbg-tuning.ml | 7 + test/toy-example-sum/p.ml | 62 ++++++ test/toy-example-sum/rooted3.dot | 17 ++ test/toy-example-sum/state.ml | 22 ++ tools/gg/graphGen.ml | 53 ++--- tools/gg/graphGen_arg.ml | 34 ++-- tools/gg/graphGen_arg.mli | 1 + tools/gg/randomGraph.ml | 29 +-- 22 files changed, 896 insertions(+), 253 deletions(-) create mode 100644 test/toy-example-sum/.gitignore create mode 100644 test/toy-example-sum/Makefile create mode 100644 test/toy-example-sum/config.ml create mode 100644 test/toy-example-sum/heuristic-bad-propag.ml create mode 100644 test/toy-example-sum/heuristic-explore.ml create mode 100644 test/toy-example-sum/my-rdbg-tuning.ml create mode 100644 test/toy-example-sum/p.ml create mode 100644 test/toy-example-sum/rooted3.dot create mode 100644 test/toy-example-sum/state.ml diff --git a/.gitignore b/.gitignore index 206f1243..0f0d168d 100644 --- a/.gitignore +++ b/.gitignore @@ -21,6 +21,8 @@ flymd.html log *.sh test/**/*.ml +!test/**/p.ml +!test/**/state.ml results Makefile.local .ocamldebug @@ -32,7 +34,6 @@ lib/sasacore/sasaVersion.ml ### Code ### .vscode/* -!.vscode/settings.json !.vscode/tasks.json !.vscode/launch.json !.vscode/extensions.json diff --git a/lib/algo/algo.ml b/lib/algo/algo.ml index de8f9607..be7eae4d 100644 --- a/lib/algo/algo.ml +++ b/lib/algo/algo.ml @@ -5,11 +5,11 @@ open Sasacore type action = string (* just a label *) type 's neighbor = { - pid: string; - spid: string; + pid: string; + spid: string; state: 's ; - reply: unit -> int; - weight: unit -> int; + reply: unit -> int; + weight: unit -> int; } let (_compare_neighbor: 's neighbor -> 's neighbor -> int) = @@ -18,12 +18,12 @@ let (_compare_neighbor: 's neighbor -> 's neighbor -> int) = let (print_neighbor: 's neighbor -> unit) = fun n -> Format.print_string n.pid - + let (fmt_print_neighbor: Format.formatter -> 's neighbor -> unit) = fun fmt n -> - Format.pp_print_string fmt n.pid + Format.pp_print_string fmt n.pid -(** processes local state (user defined) *) +(** processes local state (user defined) *) let (state : 's neighbor -> 's) = fun s -> s.state (** Returns the channel number that let this neighbor access to the @@ -32,10 +32,10 @@ let (state : 's neighbor -> 's) = fun s -> s.state directed graphs only. This info is not available in all simulation modes. *) let (reply : 's neighbor -> int) = fun s -> s.reply () - + (** Makes sense in directed graphs only *) let (weight : 's neighbor -> int) = fun s -> s.weight () - + module PidMap = Map.Make(String) type pid = string @@ -60,8 +60,8 @@ type 's to_register = { copy_state: 's -> 's; actions: action list; potential_function: 's potential_fun option; - legitimate_function : 's legitimate_fun option; - fault_function : 's fault_fun option + legitimate_function : 's legitimate_fun option; + fault_function : 's fault_fun option } let (to_reg_neigbor : 's Register.neighbor -> 's neighbor) = @@ -70,24 +70,24 @@ let (to_reg_neigbor : 's Register.neighbor -> 's neighbor) = state = n.Register.state ; pid = n.Register.pid; spid = n.Register.spid; - reply = n.Register.reply; - weight = n.Register.weight; + reply = n.Register.reply; + weight = n.Register.weight; } let (to_reg_info : 's * ('s Register.neighbor * pid) list -> 's * ('s neighbor *pid) list) = fun (s, nl) -> s, List.map (fun (n,pid) -> to_reg_neigbor n, pid) nl - + let (to_reg_enable_fun : 's enable_fun -> 's Register.neighbor list -> 's -> action list) = fun f nl s -> f s (List.map to_reg_neigbor nl) - + let (to_reg_step_fun : 's step_fun -> 's Register.neighbor list -> 's -> action -> 's) = fun f nl s a -> f s (List.map to_reg_neigbor nl) a - + let (to_reg_potential_fun : 's potential_fun -> pid list -> (pid -> 's * ('s Register.neighbor * pid) list) -> float) = fun pf pidl f -> @@ -102,15 +102,15 @@ let (to_reg_legitimate_fun : s, List.map (fun (n,pid) -> to_reg_neigbor n, pid) nl in lf pidl n_from_pid - - + + let (register1 : 's algo_to_register -> unit) = fun s -> Register.reg_enable s.algo_id (to_reg_enable_fun s.enab); Register.reg_step s.algo_id (to_reg_step_fun s.step); Register.reg_init_state s.algo_id s.init_state; () - + let registered = ref false (* exported *) let (register : 's to_register -> unit) = @@ -137,7 +137,8 @@ let (register : 's to_register -> unit) = () let card = Register.card -let get_graph_attribute = Register.get_graph_attribute +let get_graph_attribute = Register.get_graph_attribute +let get_graph_attribute_opt = Register.get_graph_attribute_opt let min_degree = Register.min_degree let mean_degree = Register.mean_degree let max_degree = Register.max_degree @@ -150,7 +151,9 @@ let diameter = Register.diameter let is_tree = Register.is_tree let is_in_tree = Register.is_in_tree let is_out_tree = Register.is_out_tree +let is_rooted_tree = Register.is_rooted_tree let height = Register.height +let level = Register.level let sub_tree_size = Register.sub_tree_size let parent = Register.parent diff --git a/lib/algo/algo.mli b/lib/algo/algo.mli index 4c48f6d2..14c7b661 100644 --- a/lib/algo/algo.mli +++ b/lib/algo/algo.mli @@ -1,10 +1,10 @@ (* Time-stamp: <modified the 09/04/2021 (at 10:39) by Erwan Jahier> *) -(** {1 The Algorithm programming Interface} +(** {1 The Algorithm programming Interface} A SASA process is an instance of an algorithm defined via this - module. + module. *) -(** +(** {2 To be provided by users} In order to define a SASA algorithm, one need to provide an enable @@ -17,7 +17,7 @@ *) type 's neighbor -type action = string +type action = string type 's enable_fun = 's -> 's neighbor list -> action list type 's step_fun = 's -> 's neighbor list -> action -> 's (** [enable_fun] and [step_fun] have the same arguments in input: @@ -26,7 +26,7 @@ type 's step_fun = 's -> 's neighbor list -> action -> 's is polymorphic (['s]), algorithms designers can put anything they need into this state (an integer, a structure, etc.). The only constraint is that all algorithms should use the same type. - + - The second argument holds the process neighbors (its successors in the graph). Note that SASA processes, that live in graph nodes, can only access to their immediate neighbors. From each neighbor, @@ -35,7 +35,7 @@ type 's step_fun = 's -> 's neighbor list -> action -> 's [enable_fun] returns the list of enable actions. - [step_fun], which also takes an action in input, returns the new value + [step_fun], which also takes an action in input, returns the new value of the local state resulting from the execution of the action. *) @@ -47,18 +47,18 @@ type 's state_init_fun = int -> string -> 's (** {2 To be provided optionally} *) -(** {3 Potential function} +(** {3 Potential function} Let the user define what the potential of a configuration is. Used to explore best/worst case daemons (--worst-daemon) *) - + type pid = string type 's potential_fun = pid list -> (pid -> 's * ('s neighbor * pid) list) -> float (** {3 Legitimate Configurations} *) - + type 's legitimate_fun = pid list -> (pid -> 's * ('s neighbor * pid) list) -> bool (** By default, legitimate configurations (i.e., global states) are silent ones. But this is not true for all algorithms. Predicates @@ -67,7 +67,7 @@ type 's legitimate_fun = pid list -> (pid -> 's * ('s neighbor * pid) list) -> b (** {3 Fault Injection } *) - + type 's fault_fun = int -> string -> 's -> 's (** The fault function is called on each node to update their state each time a legitimate configuration is reached. It takes 3 @@ -77,8 +77,8 @@ type 's fault_fun = int -> string -> 's -> 's (** {2 Can be used in algorithms} *) (** {3 Process (local) Information} *) - -(** Returns the neighbor processes local state *) + +(** Returns the neighbor processes local state *) val state : 's neighbor -> 's (** Returns the neighbor channel number, that let this neighbor access @@ -104,7 +104,7 @@ val fmt_print_neighbor: Format.formatter -> 's neighbor -> unit When writing algorithms, one can also have access to topological information (i.e., information that are relative to the graph) *) - + val card : unit -> int val min_degree : unit -> int val mean_degree : unit -> float @@ -120,23 +120,37 @@ val is_tree : unit -> bool val is_in_tree : unit -> bool val is_out_tree : unit -> bool -(** The 3 functions below work for in_tree or out_tree only. *) +(** returns true if the graph is an undirected rooted tree + (i.e. every node has exactly one parent except the root, which has none), + false otherwise *) +val is_rooted_tree : unit -> bool + + +(* The following 4 functions only work on rooted trees + (in-trees and out-trees generated by gg are ok) *) -(* maps each node to the size of the corresponding sub-tree *) +(** maps each node to the size of the corresponding sub-tree *) val sub_tree_size : string (* the node id *) -> int (** maps each node to its height in the tree *) val height : string (* the node id *) -> int +(** maps each node to its level in the tree *) +val level : string (* the node id *) -> int + (** maps each node to the channel number of its parent, and to None for the tree root. *) val parent : string (* the node id *) -> int option + (** It is possible to set some global parameters in the dot file using graph attributes. This function allows one the get their - values. *) + values. Throws an error if the attribute doesn't exist. *) val get_graph_attribute : string -> string - + +(** Get the value of a graph attribute. Returns None if the attribute doesn't exist. *) +val get_graph_attribute_opt : string -> string option + (** {2 Code Registration} The [register: 's to_register -> unit] function must be called once in @@ -155,7 +169,7 @@ type 's to_register = { copy_state: 's -> 's; actions : action list (** Mandatory in custom daemon mode, or to use oracles *); potential_function: 's potential_fun option (** Mandatory with Evil daemons *); - legitimate_function : 's legitimate_fun option; + legitimate_function : 's legitimate_fun option; fault_function : 's fault_fun option (** called at legitimate configuration *) } (** - For the [state_to_string] field, the idea is to print the raw @@ -170,49 +184,49 @@ type 's to_register = { (** To be called once *) val register : 's to_register -> unit - + (** {1 Automatic Code Registration } Once enable and step functions are defined, they need to be registered by calling the register function. - An alternative to writing this registration code is to let sasa + An alternative to writing this registration code is to let sasa generate it with the "--gen-register" (or "-reg") option. - In this case, one needs to follow some naming conventions (w.r.t file + In this case, one needs to follow some naming conventions (w.r.t file and function names): - (1) The internal state (i.e. the 's shared by all algos) should be + (1) The internal state (i.e. the 's shared by all algos) should be defined in a file named "state.ml" that defines the following 5 entities: {[ type t = define_me let (to_string: t -> string) = fun _ -> "define_me" let (of_string: string -> t option) = fun _ -> None let (copy : t -> t) = fun x -> x - let actions = ["action1";"action2"]; + let actions = ["action1";"action2"]; ]} If one does not want/need to provide the of_string state parser, returning None is fine. This is mandatory only if one wants to define initial values - in the dot file. + in the dot file. - Defining a copy that is not the identity is necessary if the state is not + Defining a copy that is not the identity is necessary if the state is not functional (e.g., if it contains an array or an Hashtbl). - In the file "state.ml" does not exist in the current directory, a skeleton + In the file "state.ml" does not exist in the current directory, a skeleton is generated. - - (2) The optional functions relative to the global configuration should be + + (2) The optional functions relative to the global configuration should be defined in a file named "config.ml" that defines the following 5 entities: {[ let potential_function = None (** Mandatory with --worst-daemon (-wd) *); let legitimate_function = None (** if different from silent ones *); - let fault_function = None (** called when a legitimate configuration is - reached *) + let fault_function = None (** called when a legitimate configuration is + reached *) ]} - + (3) All the algos mentioned in the dot file should define the following functions: {[ - let (init_state: int -> string -> State.t) = xxx finishme + let (init_state: int -> string -> State.t) = xxx finishme let (enable_f: State.t neighbor list -> State.t -> action list) = xxx let (step_f : State.t neighbor list -> State.t -> action -> State.t) = xxx ]} diff --git a/lib/sasacore/dune b/lib/sasacore/dune index 658f8dae..0c19b2d1 100644 --- a/lib/sasacore/dune +++ b/lib/sasacore/dune @@ -1,10 +1,10 @@ -;; Time-stamp: <modified the 07/02/2020 (at 13:30) by Erwan Jahier> +;; Time-stamp: <modified the 02/05/2021 (at 13:38) by Erwan Jahier> (library (name sasacore) (public_name sasacore) (libraries dynlink ocamlgraph lutils) - + (flags -noassert) ;; ; (wrapped false) (library_flags -linkall) diff --git a/lib/sasacore/register.ml b/lib/sasacore/register.ml index af989bd6..4e670b64 100644 --- a/lib/sasacore/register.ml +++ b/lib/sasacore/register.ml @@ -2,14 +2,14 @@ type 's neighbor = { state: 's ; - pid: string; - spid: string; - reply: unit -> int; - weight: unit -> int; + pid: string; + spid: string; + reply: unit -> int; + weight: unit -> int; } type algo_id = string -type action = string +type action = string type 's enable_fun = 's neighbor list -> 's -> action list type 's step_fun = 's neighbor list -> 's -> action -> 's @@ -33,18 +33,19 @@ type 's internal_tables = { mutable topology : Topology.t option; mutable card : int option; mutable min_deg : int option; - mutable mean_deg : float option; + mutable mean_deg : float option; mutable max_deg : int option; mutable is_cyclic : bool option; mutable is_connected : bool option; mutable is_tree : bool option; - mutable is_in_tree : bool option; - mutable is_out_tree : bool option; + mutable is_in_tree : bool option; + mutable is_out_tree : bool option; mutable is_directed : bool option; + mutable level : (string -> int) option; mutable height : (string -> int) option; mutable sub_tree_size: (string -> int) option; mutable parent : (string -> int option) option; - mutable links_number : int option; + mutable links_number : int option; mutable diameter : int option; } @@ -73,9 +74,10 @@ let (tbls:'s internal_tables) = { is_in_tree = None; is_out_tree = None; is_directed = None; + level = None; height = None; parent = None; - sub_tree_size =None; + sub_tree_size= None; links_number = None; diameter = None } @@ -100,77 +102,77 @@ let (get_init_state : algo_id -> int -> string -> 's) = print_table "init_state" tbls.init_state; raise (Unregistred ("init_state", algo_id)) -let (reg_enable : algo_id -> 's enable_fun -> unit) = fun algo_id x -> +let (reg_enable : algo_id -> 's enable_fun -> unit) = fun algo_id x -> if !verbose_level > 0 then Printf.eprintf "Registering %s enable\n%!" algo_id; Hashtbl.replace tbls.enable algo_id (Obj.repr x) -let (get_enable : algo_id -> 's enable_fun) = fun algo_id -> +let (get_enable : algo_id -> 's enable_fun) = fun algo_id -> try Obj.obj (Hashtbl.find tbls.enable algo_id) with Not_found -> print_table "enable" tbls.enable; raise (Unregistred ("enable", algo_id)) -let (reg_step : algo_id -> 's step_fun -> unit) = fun algo_id x -> +let (reg_step : algo_id -> 's step_fun -> unit) = fun algo_id x -> if !verbose_level > 0 then Printf.eprintf "Registering %s step\n%!" algo_id; Hashtbl.replace tbls.step algo_id (Obj.repr x) - -let (get_step : algo_id -> 's step_fun) = fun algo_id -> + +let (get_step : algo_id -> 's step_fun) = fun algo_id -> try Obj.obj (Hashtbl.find tbls.step algo_id) with Not_found -> print_table "step" tbls.step; raise (Unregistred ("step", algo_id)) -let (reg_potential : 's potential_fun option -> unit) = fun x -> +let (reg_potential : 's potential_fun option -> unit) = fun x -> if !verbose_level > 0 then Printf.eprintf "Registering potential\n%!"; tbls.potential <- (Obj.repr x) - -let (get_potential : unit -> 's potential_fun option) = fun () -> + +let (get_potential : unit -> 's potential_fun option) = fun () -> Obj.obj tbls.potential - -let (reg_fault : 's fault_fun option -> unit) = fun x -> + +let (reg_fault : 's fault_fun option -> unit) = fun x -> if !verbose_level > 0 then Printf.eprintf "Registering fault function\n%!"; tbls.fault <- (Obj.repr x) - -let (get_fault : unit -> 's fault_fun option) = fun () -> + +let (get_fault : unit -> 's fault_fun option) = fun () -> Obj.obj tbls.fault -let (reg_legitimate : 's legitimate_fun option -> unit) = fun x -> +let (reg_legitimate : 's legitimate_fun option -> unit) = fun x -> if !verbose_level > 0 then Printf.eprintf "Registering legitimate function\n%!"; tbls.legitimate <- (Obj.repr x) - -let (get_legitimate : unit -> 's legitimate_fun option) = fun () -> + +let (get_legitimate : unit -> 's legitimate_fun option) = fun () -> Obj.obj tbls.legitimate let (reg_actions : action list -> unit) = - fun x -> + fun x -> if !verbose_level > 0 then Printf.eprintf "Registering actions\n%!"; tbls.actions <- x -let (get_actions : unit -> action list) = fun () -> - tbls.actions +let (get_actions : unit -> action list) = fun () -> + tbls.actions let (reg_value_to_string : ('s -> string) -> unit) = - fun f -> + fun f -> if !verbose_level > 0 then Printf.eprintf "Registering value_to_string\n%!"; Hashtbl.replace tbls.value_to_string "_global" (Obj.repr f) -let (get_value_to_string : unit -> 's -> string) = fun () -> +let (get_value_to_string : unit -> 's -> string) = fun () -> try Obj.obj (Hashtbl.find tbls.value_to_string "_global") with Not_found -> print_table "value_to_string" tbls.value_to_string; raise (Unregistred ("value_to_string", "_global")) let (reg_value_of_string : (string -> 's) -> unit) = - fun f -> + fun f -> if !verbose_level > 0 then Printf.eprintf "Registering value_of_string\n%!"; Hashtbl.replace tbls.value_of_string "_global" (Obj.repr f) -let (get_value_of_string : unit -> (string -> 's) option) = fun () -> +let (get_value_of_string : unit -> (string -> 's) option) = fun () -> try Some (Obj.obj (Hashtbl.find tbls.value_of_string "_global")) with Not_found -> None let (reg_copy_value : ('s -> 's) -> unit) = - fun f -> + fun f -> if !verbose_level > 0 then Printf.eprintf "Registering copy_value\n%!"; Hashtbl.replace tbls.copy_value "_global" (Obj.repr f) - -let (get_copy_value : unit -> ('s -> 's)) = fun () -> + +let (get_copy_value : unit -> ('s -> 's)) = fun () -> try Obj.obj (Hashtbl.find tbls.copy_value "_global") with Not_found -> print_table "copy_value" tbls.copy_value; @@ -181,9 +183,9 @@ let set_topology g = tbls.topology <- Some g let get_topology () = match tbls.topology with | None -> assert false (* SNO if set_topology is called in Main *) | Some g -> g - + let (card : unit -> int) = fun () -> - match tbls.card with + match tbls.card with | None -> let x = List.length (get_topology()).nodes in tbls.card <- Some x; @@ -191,15 +193,15 @@ let (card : unit -> int) = fun () -> | Some b -> b let (is_directed : unit -> bool) = fun () -> - match tbls.is_directed with + match tbls.is_directed with | None -> let x = (get_topology()).directed in tbls.is_directed <- Some x; x | Some b -> b - + let (mean_degree : unit -> float) = fun () -> - match tbls.mean_deg with + match tbls.mean_deg with | None -> let x = Topology.get_mean_degree (get_topology()) in tbls.mean_deg <- Some x; @@ -207,7 +209,7 @@ let (mean_degree : unit -> float) = fun () -> | Some b -> b let (min_degree : unit -> int) = fun () -> - match tbls.min_deg with + match tbls.min_deg with | None -> let mind,maxd = Topology.get_degree (get_topology()) in tbls.max_deg <- Some maxd; @@ -216,7 +218,7 @@ let (min_degree : unit -> int) = fun () -> | Some b -> b let (max_degree : unit -> int) = fun () -> - match tbls.max_deg with + match tbls.max_deg with | None -> let mind,maxd = Topology.get_degree (get_topology()) in tbls.max_deg <- Some maxd; @@ -225,7 +227,7 @@ let (max_degree : unit -> int) = fun () -> | Some b -> b let (is_cyclic : unit -> bool) = fun () -> - match tbls.is_cyclic with + match tbls.is_cyclic with | None -> let cyclic = Topology.is_cyclic (get_topology()) in tbls.is_cyclic <- Some cyclic; @@ -233,15 +235,15 @@ let (is_cyclic : unit -> bool) = fun () -> | Some b -> b let (is_connected : unit -> bool) = fun () -> - match tbls.is_connected with + match tbls.is_connected with | None -> let connect = Topology.is_connected (get_topology()) in tbls.is_connected <- Some connect; connect | Some b -> b - + let (is_tree : unit -> bool) = fun () -> - match tbls.is_tree with + match tbls.is_tree with | None -> let b = Topology.is_tree (get_topology()) in tbls.is_tree <- Some b; @@ -249,7 +251,7 @@ let (is_tree : unit -> bool) = fun () -> | Some b -> b let (is_in_tree : unit -> bool) = fun () -> - match tbls.is_in_tree with + match tbls.is_in_tree with | None -> let b = Topology.is_in_tree (get_topology()) in tbls.is_in_tree <- Some b; @@ -257,7 +259,7 @@ let (is_in_tree : unit -> bool) = fun () -> | Some b -> b let (is_out_tree : unit -> bool) = fun () -> - match tbls.is_out_tree with + match tbls.is_out_tree with | None -> let b = Topology.is_out_tree (get_topology()) in tbls.is_out_tree <- Some b; @@ -267,7 +269,7 @@ let (is_out_tree : unit -> bool) = fun () -> let not_a_tree () = failwith "The graph is not a tree" let height : (string -> int) = - fun pid -> + fun pid -> if is_tree () then ( match tbls.height with | Some h -> h pid @@ -277,19 +279,30 @@ let height : (string -> int) = ) else not_a_tree () +let level: (string -> int) = + fun pid -> + if is_tree () then ( + match tbls.level with + | Some l -> l pid + | None -> + let l = Topology.get_level (get_topology ()) in + tbls.level <- Some l; l pid + ) + else not_a_tree () + let sub_tree_size : (string -> int) = - fun pid -> + fun pid -> if is_tree () then ( match tbls.sub_tree_size with | Some s -> s pid | None -> - let s = Topology.get_sub_tree_size (get_topology ()) in + let s = Topology.get_subtree_size (get_topology ()) in tbls.sub_tree_size <- Some s; s pid ) else not_a_tree () let parent : (string -> int option) = - fun pid -> + fun pid -> match tbls.parent with | Some p -> p pid | None -> @@ -297,7 +310,7 @@ let parent : (string -> int option) = tbls.parent <- Some p; p pid -let (links_number : unit -> int) = +let (links_number : unit -> int) = fun () -> match tbls.links_number with | Some x -> x @@ -306,28 +319,37 @@ let (links_number : unit -> int) = tbls.links_number <- Some x; x -let (diameter : unit -> int) = - fun () -> +let (diameter : unit -> int) = + fun () -> match tbls.diameter with | Some x -> x | None -> let x = Diameter.get (get_topology ()) in tbls.diameter <- Some x; x - + let (to_string : 's -> string) = fun v -> (get_value_to_string ()) v let (get_graph_attribute : string -> string) = fun str -> - try Hashtbl.find tbls.graph_attributes str + try Hashtbl.find tbls.graph_attributes str with Not_found -> failwith (Printf.sprintf "The graph attribute %s does not seem to exist" str) +let (get_graph_attribute_opt : string -> string option) = + fun str -> + Hashtbl.find_opt tbls.graph_attributes str + let (set_graph_attribute : string -> string -> unit) = - Hashtbl.replace tbls.graph_attributes + Hashtbl.replace tbls.graph_attributes let (graph_attribute_list: unit -> (string * string) list) = fun () -> Hashtbl.fold (fun n v acc -> (n,v)::acc) tbls.graph_attributes [] + +let (is_rooted_tree : unit -> bool) = fun () -> + match get_graph_attribute_opt "is_rooted" with + | None -> false + | Some str -> bool_of_string str diff --git a/lib/sasacore/register.mli b/lib/sasacore/register.mli index b33fed0e..2076c3b0 100644 --- a/lib/sasacore/register.mli +++ b/lib/sasacore/register.mli @@ -10,14 +10,14 @@ type 's neighbor = { state: 's ; - pid: string; - spid: string; - reply: unit -> int; - weight: unit -> int; + pid: string; + spid: string; + reply: unit -> int; + weight: unit -> int; } type algo_id = string -type action = string +type action = string type 's enable_fun = 's neighbor list -> 's -> action list type 's step_fun = 's neighbor list -> 's -> action -> 's type 's fault_fun = int -> string -> 's -> 's @@ -49,13 +49,16 @@ val diameter : unit -> int val is_tree : unit -> bool val is_in_tree : unit -> bool val is_out_tree : unit -> bool +val is_rooted_tree : unit -> bool val sub_tree_size : string -> int val parent : string -> int option val is_directed : unit -> bool +val level : string -> int val height : string -> int val verbose_level: int ref val get_graph_attribute : string -> string +val get_graph_attribute_opt : string -> string option (* All the remaining functions are used only by the sasa Engine, while diff --git a/lib/sasacore/topology.ml b/lib/sasacore/topology.ml index 4ad1c28c..1f149e4c 100644 --- a/lib/sasacore/topology.ml +++ b/lib/sasacore/topology.ml @@ -7,14 +7,14 @@ type node_id = string type node = { id: node_id; file: string; - init: string; + init: string; } type t = { nodes: node list; succ: node_id -> (int * node_id) list; - pred: node_id -> node_id list; + pred: node_id -> node_id list; of_id: node_id -> node; directed:bool; attributes: (string * string) list; @@ -28,11 +28,11 @@ let node_succ:node_succ_t = Hashtbl.create 100 type node_pred_t = (string, node_id) Hashtbl.t let node_pred:node_pred_t = Hashtbl.create 100 -let clean_tbl () = +let clean_tbl () = Hashtbl.clear node_info; Hashtbl.clear node_succ; Hashtbl.clear node_pred - + let (of_id:Dot_ast.id -> string) = function Ident str | Html str | Number str | String str -> str @@ -49,7 +49,7 @@ let (get_file: Dot_ast.node_id -> Dot_ast.attr list -> string) = match List.assoc (Ident "algo") attrs with None -> assert false | Some id -> of_id id - ) + ) with Not_found -> failwith ((of_node_id node_id)^" should have an algo attribute") let (get_init: Dot_ast.attr list -> string) = @@ -60,7 +60,7 @@ let (get_init: Dot_ast.attr list -> string) = (fun acc (id,idopt) -> if id <> Ident "init" then acc else match idopt with - | Some (String id) -> id + | Some (String id) -> id | _ -> acc ) "" @@ -70,7 +70,7 @@ let (get_init: Dot_ast.attr list -> string) = let rec (get_weight: Dot_ast.attr -> int) = function - | (Ident "weight", Some Number n)::_ + | (Ident "weight", Some Number n)::_ | (Ident "weight", Some String n)::_ -> (try (int_of_string n) with _ -> 1) | _::tail -> get_weight tail | [] -> 1 @@ -78,7 +78,7 @@ let rec (get_weight: Dot_ast.attr -> int) = type attrs = (string * string) list let (do_graph_attr : attrs -> (Dot_ast.id * Dot_ast.id option) list -> attrs) = - fun acc l -> + fun acc l -> let f acc = function | id, Some v -> (of_id id, of_id v)::acc | _, None -> acc @@ -105,7 +105,7 @@ let (do_stmt: bool -> node list * attrs -> Dot_ast.stmt -> node list * attrs) = c -- d " Graph.Dot.parse_dot_ast returns the pair a,[b,c,d] - which is weird IMHO. + which is weird IMHO. The code below add the missing edges: *) let dot_attrs = List.flatten dot_attrs in (* XXX why a list of list ? *) @@ -127,7 +127,7 @@ let (do_stmt: bool -> node list * attrs -> Dot_ast.stmt -> node list * attrs) = | Attr_graph dot_attrs -> let attrs = do_graph_attr attrs (List.flatten dot_attrs) in n, attrs - | Attr_node _attrs -> n, attrs + | Attr_node _attrs -> n, attrs | Attr_edge _attrs -> n, attrs | Equal (_id1, _id2) -> assert false | Subgraph _subgraph -> assert false @@ -182,7 +182,7 @@ let (get_degree: t -> int*int) = if t.directed then List.length (t.succ (n.id)) + List.length (t.pred (n.id)) else - List.length (t.succ (n.id)) + List.length (t.succ (n.id)) in let d0 = node_deg n in let dmin, dmax = List.fold_left @@ -201,11 +201,11 @@ let (get_nb_link: t -> int) = (* let succ = String.concat "," (List.map snd (t.succ n.id)) in *) (* Printf.printf "%s->%s\n%!" n.id succ; *) ((List.length (t.succ n.id))) + acc) 0 t.nodes - in + in if t.directed then res else res/2 -let (get_mean_degree : t -> float) = - fun t -> +let (get_mean_degree : t -> float) = + fun t -> 2.0 *. (float_of_int (get_nb_link t)) /. (float_of_int (List.length t.nodes)) type color = W | G | B @@ -244,7 +244,7 @@ let is_connected : t -> bool = let accessible = f [] (List.hd g.nodes).id in List.length accessible = List.length g.nodes -let bfs : (t -> string -> bool * string list) = +let bfs : (t -> string -> bool * string list) = fun t n -> let q = Queue.create () in let discovered = ref [n] and parent = ref (function _ -> "") in @@ -252,15 +252,15 @@ let bfs : (t -> string -> bool * string list) = Queue.add n q; while not (Queue.is_empty q) do let node = Queue.take q in - parent := List.fold_left (fun parents (_,suc) -> - if List.for_all (fun disc -> disc <> suc) !discovered + parent := List.fold_left (fun parents (_,suc) -> + if List.for_all (fun disc -> disc <> suc) !discovered then ( Queue.add suc q; discovered := (suc)::!discovered; function a -> if a = suc then node else parents a ) else (( - if suc <> (parents node) - then + if suc <> (parents node) + then cyclic := true); parents ) @@ -315,73 +315,114 @@ let is_out_tree g = (is_tree g) && (List.for_all (fun n -> List.length (g.succ n.id) <= 1) g.nodes) -let not_a_io_tree () = failwith "The graph is not an in-tree nor an out-tree" +let is_root_node _ pid = + pid = "root" + +(* Donne les enfants d'un noeud dans un in-tree (liens partent de la racine) *) +let children_in g pid = + List.map snd (g.succ pid) + +(* Donne les enfants d'un noeud dans un out-tree (liens vers la racine) *) +let children_out g pid = + g.pred pid + +(* Donne les enfants d'un noeud dans un in-out-tree *) +let children_in_out g pid = + let succ = List.map snd (g.succ pid) in + if is_root_node g pid then succ + else List.tl succ + (* pour tous les noeuds sauf la racine, le parent est la tête de succ + ici on veut juste les enfants donc on enlève le premier *) + +let parent_in g pid = + match g.pred pid with + | [] -> None + | id::_ -> Some id + +let parent_out g pid = + match g.succ pid with + | [] -> None + | (_,id)::_ -> Some (id) + +let parent_in_out g pid = + if is_root_node g pid then None + else Some (snd (List.hd (g.succ pid))) + (* Le parent est le premier dans la liste succ pour un in-out-tree ou un rooted-tree *) let get_parent = fun g pid -> + assert (is_tree g); let in_tree = is_in_tree g in let out_tree = is_out_tree g in - if not in_tree && not out_tree then - not_a_io_tree () - else - let succ,reply = - if out_tree then - (fun pid -> List.map snd (g.succ pid)), reply_pred - else - (fun pid -> g.pred pid), reply - in - match succ pid with - | [] -> None - | [par] -> Some (reply g pid par) - | l -> - Printf.printf "%s->%s\n%!" pid (String.concat "," l); - assert false - -let get_sub_tree_size g pid = + let get_parent, rep = + if out_tree then + parent_out, reply_pred + else if in_tree then + parent_in, reply + else + parent_in_out, reply + in + Option.map (fun par -> rep g par pid) (get_parent g pid) + (* on renvoie le numéro de canal du parent *) + +(* Calcule la hauteur d'un noeud. + Hauteur(feuille) = 0 + Hauteur(noeud) = 1 + max(hauteurs des enfants) +*) +let get_height g pid: int = + assert (is_tree g); let in_tree = is_in_tree g in let out_tree = is_out_tree g in - if not in_tree && not out_tree then - not_a_io_tree () - else - let succ = - if in_tree then - (fun pid -> List.map snd (g.succ pid)) - else - (fun pid -> g.pred pid) - in - let visited = Hashtbl.create 0 in - let rec f acc pid = - if Hashtbl.mem visited pid then acc else - (Hashtbl.add visited pid pid; - List.fold_left - (fun acc pid -> f acc pid) - (acc+1) - (succ pid) - ) - in - f 0 pid - -let rec height : (string -> string list) -> string list -> string -> int = - fun succ parents n -> - (List.fold_left - (fun h pid -> - if List.mem pid parents then h else - max h (height succ (n::parents) pid) - ) - (-1) - (succ n) - ) + 1 - -let get_height : t -> string -> int = - fun g -> + let get_children = + if in_tree then children_in + else if out_tree then children_out + else children_in_out + in + let rec height children g pid = + match children g pid with + | [] -> 0 + | x::xs -> + let hx = height children g x in + let hxs = List.map (height children g) xs in + 1 + List.fold_left max hx hxs + in + height get_children g pid + +(* Calcule le niveau/la profondeur d'un noeud + Niveau(racine) = 0 + Niveau(noeud) = Niveau(noeud.parent) + 1 +*) +let get_level g pid: int = + assert (is_tree g); let in_tree = is_in_tree g in let out_tree = is_out_tree g in - if not in_tree && not out_tree then - not_a_io_tree () - else - let succ = - if out_tree then - (fun pid -> List.map snd (g.succ pid)) - else - (fun pid -> g.pred pid) - in - height succ [] + let get_parent = + if in_tree then parent_in + else if out_tree then parent_out + else parent_in_out + in + let rec level parent g pid = + match parent g pid with + | None -> 0 + | Some par -> 1 + (level parent g par) + in + level get_parent g pid + +(* Calcule la taille du sous-arbre partant du noeud donné + taille = 1 + somme des tailles des enfants +*) +let get_subtree_size g pid: int = + assert (is_tree g); + let in_tree = is_in_tree g in + let out_tree = is_out_tree g in + let get_children = + if in_tree then children_in + else if out_tree then children_out + else children_in_out + in + let rec tree_size children g pid = + 1 + (match children g pid with + | [] -> 0 + | l -> List.fold_left (+) 0 (List.map (tree_size children g) l) + ) + in + tree_size get_children g pid diff --git a/lib/sasacore/topology.mli b/lib/sasacore/topology.mli index e37cbf4c..13fb5179 100644 --- a/lib/sasacore/topology.mli +++ b/lib/sasacore/topology.mli @@ -33,8 +33,9 @@ val is_tree : t -> bool val is_in_tree : t -> bool val is_out_tree : t -> bool val get_height : t -> string -> int +val get_level : t -> string -> int val get_parent : t -> string -> int option -val get_sub_tree_size : t -> string -> int +val get_subtree_size : t -> string -> int val get_degree: t -> int * int (** [reply g p p_neighbor] returns the channel number that let diff --git a/src/dune b/src/dune index 2d043061..543ea36c 100644 --- a/src/dune +++ b/src/dune @@ -1,8 +1,9 @@ -;; Time-stamp: <modified the 18/09/2019 (at 15:07) by Erwan Jahier> +;; Time-stamp: <modified the 02/05/2021 (at 13:38) by Erwan Jahier> (executable (name sasaMain) - (link_flags (-linkall)) + (flags -noassert) + (link_flags (-linkall)) (libraries dynlink ocamlgraph lutils sasacore algo) ) diff --git a/test/toy-example-sum/.gitignore b/test/toy-example-sum/.gitignore new file mode 100644 index 00000000..649fbb6b --- /dev/null +++ b/test/toy-example-sum/.gitignore @@ -0,0 +1,3 @@ +!config.ml +!rooted3.dot +!heuristic-*.ml diff --git a/test/toy-example-sum/Makefile b/test/toy-example-sum/Makefile new file mode 100644 index 00000000..d613561b --- /dev/null +++ b/test/toy-example-sum/Makefile @@ -0,0 +1,43 @@ +# Time-stamp: <modified the 18/05/2021 (at 18:08) by Erwan Jahier> + + +test: test1 test2 +test1: rooted3.cmxs + sasa rooted3.dot + +test2: rooted3.cmxs + sasa -gcd rooted3.dot + +DECO_PATTERN="0-:p.ml" +-include ../Makefile.dot + +sim2chrogtk: rooted3.rif + sim2chrogtk -ecran -in $< > /dev/null + +gnuplot: rooted3.rif + gnuplot-rif $< + +explore : heuristic-explore.ml rooted3.ml + echo "(* Do not edit me ; edit mv_hook.ml instead! *)" > include.ml + cat $< >> include.ml + ledit rdbg --sasa --missing-vars-last -env "sasa rooted3.dot -custd" + +bad-propag : heuristic-bad-propag.ml rooted3.ml + echo "(* Do not edit me ; edit mv_hook.ml instead! *)" > include.ml + cat $< >> include.ml + ledit rdbg --sasa --missing-vars-last -env "sasa rooted3.dot -custd" + +gui: rooted3.ml + echo "(* Do not edit me ; edit mv_hook.ml instead! *)" > include.ml + ledit rdbguoi4sasa -sut "sasa rooted3.dot -custd" + + +rdbg: rooted3.ml + rdbg -o rooted3.rif -env "$(sasa) rooted3.dot -gcd" + +clean: genclean + rm -f rooted3.ml + +-include ../Makefile.inc +-include Makefile.untracked + diff --git a/test/toy-example-sum/config.ml b/test/toy-example-sum/config.ml new file mode 100644 index 00000000..ae53180b --- /dev/null +++ b/test/toy-example-sum/config.ml @@ -0,0 +1,54 @@ +open Algo +open P + +let is_enabled_S p nl = + P.enable_f p nl = ["S"] + +let is_enabled_R p nl = + let action = P.enable_f p nl in + action = ["Rp"] || action = ["Rr"] + +(** Potentiel d'un noeud, pour la règle R *) +let pot_r (p: State.t) (nl: State.t neighbor list) = + if is_enabled_R p nl then Algo.sub_tree_size p.pid + else 0 + +(** potentiel pour l'action "R" top-down: + somme des tailles des sous-arbres des activables *) +let potential_r: State.t Algo.potential_fun = + fun pidl get -> + let potentials = List.map (fun pid -> + match get pid with + | (p, l) -> + pot_r p (List.map fst l) + ) pidl in + float_of_int (List.fold_left (+) 0 potentials) + +(** potentiel pour l'action S bottom-up + somme des profondeurs des noeuds activables *) +let rec potential_s: State.t Algo.potential_fun = + fun pidl get -> + let levels = List.filter_map (fun pid -> + match get pid with + | (p, l) -> + let nl = List.map fst l in + if is_enabled_S p nl then + Some (1 + Algo.level pid) (* 1 + niveau du noeud, pour que la racine ait une valeur de 1 *) + else + None + ) pidl in + float_of_int (List.fold_left (+) 0 levels) + +let potential_combined: State.t Algo.potential_fun = + fun pidl get -> + let potR = potential_r pidl get in + let potS = potential_s pidl get in + (* Printf.printf "potR = %f; potS = %f\n" potR potS; *) + let n = float_of_int (Algo.card ()) in + let pot = (n**2.0 +. 1.0) *. potS +. potR in + (* Printf.printf "potTotal = %f\n" pot; *) + pot + +let potential = Some potential_combined +let legitimate = None (* None => only silent configuration are legitimate *) +let fault = None (* None => the simulation stop once a legitimate configuration is reached *) diff --git a/test/toy-example-sum/heuristic-bad-propag.ml b/test/toy-example-sum/heuristic-bad-propag.ml new file mode 100644 index 00000000..31ac490e --- /dev/null +++ b/test/toy-example-sum/heuristic-bad-propag.ml @@ -0,0 +1,132 @@ + +(* Heuristique : pour aller vers le pire cas du Toy Example, on cherche à maximiser le nombre + de propagations (action top-down) d'un résultat erroné. Pour un noeud que l'action top-down R + n'est pas possible si l'action bottom-up S est possible, il faut donc faire S lorsque + c'est nécessaire afin de continuer à avancer, mais le moins souvent possible. *) + +open RdbgRun + +let daemon_i = ref 0 + +type node_info = { + lvl: int; + s: bool; + r: bool +} + +(* Entrée : le contenu de !e.data + Sortie : tuples ("n_S", activate) avec n le nom du noeud et S le nom de l'état, activate un booléen + Attention, les noms ne doivent contenir que des lettres à cause du Data.type_to_string dans rdbgRun.ml:37 *) +let custom_daemon (data: Data.subst list): Data.subst list option = + (* liste des noeuds-états *) + let sl = List.filter (fun (n,v) -> String.length n > 5 && String.sub n 0 5 = "Enab_") data in + + (* regroupe les états par noeud *) + let nodes = Hashtbl.create (List.length sl / 3) in + List.iter (fun (n,v) -> + let split = String.split_on_char '_' n in + let enabled = match v with + | Data.B b -> b + | _ -> assert false + in + + match split with + | _::pid::state::[] -> (* Enab_pid_state *) + let combine_info info = + match state with + | "S" -> {info with s=enabled} + | "Rr" -> if info.lvl=0 then {info with r=enabled} else info + | "Rp" -> if info.lvl>0 then {info with r=enabled} else info + | _ -> assert false + in + (match Hashtbl.find_opt nodes pid with + | None -> Hashtbl.add nodes pid (combine_info {lvl=Algo.level pid; s=false; r=false}); + | Some x -> Hashtbl.replace nodes pid (combine_info x); + ) + | _ -> assert false + ) sl; + (* liste des états triés par niveau croissant (la racine en 1er) *) + let nl = List.of_seq (Hashtbl.to_seq nodes) in + let from_top = List.sort (fun (k1,v1) (k2,v2) -> Stdlib.compare v1.lvl v2.lvl) nl in + + (* Maximise le nombre de propagations en activant les noeuds tour à tour depuis la racine, + à l'aide de la variable globale i *) + let ni = !daemon_i in + let n = List.length from_top in + let res = List.flatten (List.mapi (fun i (k,v) -> + let str_s = Printf.sprintf "%s_S" k in + let str_rr = Printf.sprintf "%s_Rr" k in + let str_rp = Printf.sprintf "%s_Rp" k in + let s,rr,rp = + if i = ni then + (* c'est ce noeud-là qu'il faut activer, de préférence avec l'action R, sinon avec S puis R *) + if v.r then ( + (* R maintenant *) + daemon_i := (!daemon_i + 1) mod n; + if v.lvl = 0 then + false, true, false + else + false, false, true + ) else ( + (* S au prochain coup *) + assert v.s; + true, false, false + ) + else + false, false, false + in + [(str_s, Data.B s); (str_rr, Data.B rr); (str_rp, Data.B rp)] + ) from_top) in + + (* Simule le greedy daemon pour la fonction de potentiel du toy example : *) + (* on fait R le + bas possible, sinon on fait S le + haut possible *) + (* + let from_bottom = List.sort (fun (k1,v1) (k2,v2) -> Stdlib.compare v2.lvl v1.lvl) nl in + let activate_r = List.find_opt (fun (_,info) -> info.r) from_bottom in + let activate_s = List.find_opt (fun (_,info) -> info.s) from_top in + + (* résultat du démon *) + let res = List.map (fun (n,v) -> + let split = String.split_on_char '_' n in + match split with + | "Enab"::pid::state::[] -> + let activate = g + if v = Data.B true then + if state <> "S" then + match activate_r with + | Some (node,info) -> node=pid + | None -> false + else if activate_r = None then + match activate_s with + | Some (node,info) -> node=pid + | None -> false + else + false + else + false + in + let str = Printf.sprintf "%s_%s" pid state in + (str, Data.B activate) + | _ -> assert false + ) sl + in *) + Some res + +let is_end (e: RdbgEvent.t) = + match (List.assoc_opt "potential" e.data) with + | Some (Data.F 0.0) -> true + | Some (Data.F x) -> false + | _ -> assert false + +let auto () = + let stop = ref false in + while not !stop do + e := next_cond !e (fun e -> e.lang = "sasa"); + pe (); + stop := is_end !e; + done; + Printf.printf "done in %d moves\n" (!e.step - 1); + () + +let _ = + rdbg_mv_hook := Some custom_daemon; diff --git a/test/toy-example-sum/heuristic-explore.ml b/test/toy-example-sum/heuristic-explore.ml new file mode 100644 index 00000000..740b6331 --- /dev/null +++ b/test/toy-example-sum/heuristic-explore.ml @@ -0,0 +1,202 @@ + +(* Heuristique : pour aller vers le pire cas, on va simplement tester tous les coups + possibles (ou presque) et choisir le scénario qui maximise le temps de stabilisation. *) + +open RdbgRun +open RdbgStdLib + +type node_info = { + lvl: int; + s: bool; + r: bool +} + +let computed_moves: (string * string) list option ref = ref None + +let daemon_choice = ref ("", "") + +let set_daemon_choice (node: string) (state: string) = + daemon_choice := node, state + +(* Liste des activables sous forme de couples (noeud,état) *) +let enabled (e: RdbgEvent.t): (string * string) list = + List.filter_map (fun (n,v) -> + match v with + | Data.B true -> ( + match String.split_on_char '_' n with + | "Enab"::pid::state::[] -> Some (pid, state) + | _ -> None + ) + | _ -> None + ) e.data + +(* Heuristique qui élimine des coups lors de l'exploration, pour en réduire le coût. +Comme la fonction de potentiel ne mène pas toujours au pire cas sur le Toy Exemple, +on se base sur les noeuds activables en essayant de faire l'action de propagation "R" +en priorité. On pourrait aussi changer la fonction de potentiel et l'utiliser ici, ce +qui rendrait la méthode beaucoup plus générale. *) +let exploration_hint (enabled_list: (string * string) list) = + let l = List.filter (fun (_, state) -> state = "Rp" || state = "Rr") enabled_list in + if l = [] then enabled_list else l + + +(* Explore un coup, donne le nombre de coups total qu'il engendre (pour aller jusqu'à la fin) *) +let rec explore_count e i moves: int = + let possible_choices = enabled e in + match possible_choices with + | [] -> + moves (* fini *) + | l -> + e.save_state i; + (* tout explorer coûte trop cher, on élimine les coups les moins intéressants *) + let filtered = exploration_hint l in + + (* calcule le score de tous les coups sélectionnés *) + let score = List.map (fun (node, st) -> + set_daemon_choice node st; + let next = next_cond e (fun x -> x.lang = "sasa") in + let to_end = explore_count next (i+1) (moves+1) in + e.restore_state i; + to_end + ) filtered in + + (* sélectionne le pire cas *) + match score with + | [] -> assert false + | x::xs -> + let worst_score = List.fold_left max x xs in + worst_score + + +(* Table des états déjà explorés, pour éviter de recalculer pour rien. +On stocke les data des outputs en clé et les coups suivants en valeur. *) +let explored = Hashtbl.create 64 + +(* Donne la partie "outputs" de e.data *) +let event_outputs (e: RdbgEvent.t) = + (* On utilise le fait que les inputs viennent toujours en premier, puis les outputs *) + let ins = (List.length e.inputs) + 3 in (* +3 pour enlever silent,legitimate,potential *) + (List.filteri (fun i _ -> i >= ins) e.data) + + (* Autre méthode : filtrer par nom de variable et ne prendre que l'état des noeuds *) + (* let states = ["input"; "sub"; "res"] in + let res = List.filter_map (fun (n,v) -> + let s = String.split_on_char '_' n in + match s with + | _::x::[] when List.mem x states -> Some (x,v) + | _ -> None + ) e.data + in + res *) + + +(* Explore un état, donne le pire cas qu'il engendre +(liste tous les coups suivants menant au pire cas possible à partir de cette configuration) *) +let rec explore e i: (string * string) list = + (* si on a déjà été dans la même situation avant, on réutilise le résultat *) + let outputs = event_outputs e in + match Hashtbl.find_opt explored outputs with + | Some x -> x + | None -> + ( + let possible_choices = enabled e in + match possible_choices with + | [] -> [] (* fini: rien ensuite *) + | l -> + e.save_state i; + (* tout explorer coûte trop cher, on élimine les coups les moins intéressants *) + let filtered = exploration_hint l in + + (* calcule les coups suivants pour tous les coups sélectionnés *) + let all_moves = List.map (fun (node, st) -> + set_daemon_choice node st; + let next = next_cond e (fun x -> x.lang = "sasa") in + (* calcule jusqu'à la fin et choisit la pire suite de coups à partir d'ici *) + let to_end = explore next (i+1) in + (* restore l'évènement originel *) + e.restore_state i; + (* renvoie ce coup-là avec la pire suite, dans l'ordre chronologique (prepend pour + de perf) *) + let elem = (node,st) in + elem::to_end + ) filtered in + + (* sélectionne le pire cas *) + match all_moves with + | [] -> assert false + | x::xs -> + let compare a b = + let na = List.length a in + let nb = List.length b in + if nb > na then b else a + in + let worst_case = List.fold_left compare x xs in + (* stocke le résultat pour éviter de le recalculer si on retombe sur cette config *) + Hashtbl.add explored outputs worst_case; + worst_case + ) + + +(* Entrée : le contenu de !e.data + Sortie : tuples ("n_S", activate) avec n le nom du noeud et S le nom de l'état, activate un booléen + Attention, les noms ne doivent contenir que des lettres à cause du Data.type_to_string dans rdbgRun.ml:37 *) +let custom_daemon (data: Data.subst list): Data.subst list option = + (* liste des noeuds-états *) + let sl = List.filter (fun (n,v) -> String.length n > 5 && String.sub n 0 5 = "Enab_") data in + + (* évènement sasa courant *) + let evt = !e in + + (* sortie du démon : active le noeud sélectionné *) + let get_daemon_choice : string * string = + match !computed_moves with + | None -> + (* lance l'exploration si elle n'est pas déjà en cours *) + let a,b = !daemon_choice in + if a = "" && b = "" then ( + Printf.printf "computing worst case...\n"; + let worst_case = explore evt 0 in + let moves = worst_case in + Printf.printf "found worst case: %d moves\n" (List.length moves); + let first_move = List.hd moves in + computed_moves := Some (List.tl moves); + first_move + ) + else + a,b + | Some (next_move::rest) -> + computed_moves := Some rest; + next_move + | Some [] -> + Printf.printf "no event left\n"; + assert false + in + + let sel_pid, sel_state = get_daemon_choice in + let res = List.map (fun (n,v) -> + match String.split_on_char '_' n with + | _::pid::state::[] -> + let str = Printf.sprintf "%s_%s" pid state in + let activate = (pid = sel_pid) && (sel_state = state) in + (str, Data.B activate) + | _ -> assert false + ) sl in + + Some res + +let is_end (e: RdbgEvent.t) = + match (List.assoc_opt "potential" e.data) with + | Some (Data.F 0.0) -> true + | _ -> false + +let auto () = + let stop = ref false in + while not !stop do + e := next_cond !e (fun e -> e.lang = "sasa"); + pe (); + stop := is_end !e; + done; + Printf.printf "done in %d moves\n" (!e.step - 1); + () + +let _ = + rdbg_mv_hook := Some custom_daemon; diff --git a/test/toy-example-sum/my-rdbg-tuning.ml b/test/toy-example-sum/my-rdbg-tuning.ml new file mode 100644 index 00000000..3214875d --- /dev/null +++ b/test/toy-example-sum/my-rdbg-tuning.ml @@ -0,0 +1,7 @@ + + (* Generated by rdbg because not existing *) +#use "rdbg-cmds.ml";; + +#use "sasa-rdbg-cmds.ml";; + +#use "include.ml";; diff --git a/test/toy-example-sum/p.ml b/test/toy-example-sum/p.ml new file mode 100644 index 00000000..f59dfdb2 --- /dev/null +++ b/test/toy-example-sum/p.ml @@ -0,0 +1,62 @@ +(* from "Acyclic Strategy for Silent Self-Stabilization in Spanning + Forests" Karine Altisen, SteÌphane Devismes, and Anaı̈s Durand, + SSS 2018 + +https://hal.archives-ouvertes.fr/hal-01938671 *) + +open Algo +open State + +let init_state (i: int) (id: string): State.t = + { + pid = id; + input = 0; + sub = 0; + res = 0 + } + +let children_states pid (neighbors: 'st neighbor list): 'st list = + let n = + match Algo.parent pid with + | None -> neighbors + | Some par -> List.filteri (fun i _ -> i <> par) neighbors + in + List.map state n + +let parent_opt pid (nl: State.t neighbor list): State.t option = + let parent_i = Algo.parent pid in + Option.map (fun par -> state (List.nth nl par)) parent_i + +let parent_state (s: State.t) (nl: State.t neighbor list): State.t = + match parent_opt s.pid nl with + | Some par -> par + | None -> + let nls = String.concat " " (List.map (fun s -> (state s).pid) nl) in + Printf.eprintf "No parent found for pid=%s, nl=%s\n" s.pid nls; + assert false + +let enable_f (p: State.t) (nl: State.t neighbor list): action list = + let children = children_states p.pid nl in + let sum_subs = List.fold_left (+) 0 (List.map (fun s -> s.sub) children) in + if p.sub <> p.input + sum_subs then ["S"] + else + if p.pid = "root" then + if (p.res <> p.sub) then ["Rr"] else [] + else + if p.res <> (max p.sub (parent_state p nl).res) then ["Rp"] else [] + +let step_f (p: State.t) (nl: State.t neighbor list) (a: action): State.t = + match a with + | "S" -> + let children = children_states p.pid nl in + let sum_subs = List.fold_left (+) 0 (List.map (fun s -> s.sub) children) in + {p with sub = p.input + sum_subs} + + | "Rr" -> + {p with res = p.sub} + + | "Rp" -> + {p with res = max p.sub (parent_state p nl).res} + + | _ -> + assert false diff --git a/test/toy-example-sum/rooted3.dot b/test/toy-example-sum/rooted3.dot new file mode 100644 index 00000000..9d922051 --- /dev/null +++ b/test/toy-example-sum/rooted3.dot @@ -0,0 +1,17 @@ +graph rooted3 { +graph [min_deg=1 + mean_deg=1.33333333333 + max_deg=2 + is_connected=true + is_cyclic=false + is_tree=true + links_number=2 + is_rooted=true] + + root [algo="p.ml" init="{pid=root ; input=1}"] + p1 [algo="p.ml" init="{pid=p1 ; input=1}"] + p2 [algo="p.ml" init="{pid=p2 ; input=1}"] + + p1 -- root + p2 -- root +} diff --git a/test/toy-example-sum/state.ml b/test/toy-example-sum/state.ml new file mode 100644 index 00000000..522a32ef --- /dev/null +++ b/test/toy-example-sum/state.ml @@ -0,0 +1,22 @@ + +open Algo + +type t = { + pid:string; + input:int; + sub:int; + res:int +} + +let (to_string: (t -> string)) = + fun s -> + Printf.sprintf "input=%d sub=%d res=%d" s.input s.sub s.res + +let of_string: (string -> t) option = + Some (fun s -> + Scanf.sscanf s "{pid=%s ; input=%d}" + (fun pid input -> {pid = pid; input = input; sub = 0; res = 0}) + ) + +let (copy : ('v -> 'v)) = fun x -> x +let actions = ["S";"Rr";"Rp"] diff --git a/tools/gg/graphGen.ml b/tools/gg/graphGen.ml index c7f17aff..c2fabb58 100644 --- a/tools/gg/graphGen.ml +++ b/tools/gg/graphGen.ml @@ -9,7 +9,7 @@ open Sasacore exception Incorrect_attribute -let min_max = ref None +let min_max = ref None let connected = ref None let cyclic = ref None let tree = ref None @@ -20,16 +20,16 @@ let generate_du_dur graph plan_udg t : unit = make_dot_udg_qudg graph plan_udg (t.qudg.width,t.qudg.height) (t.dotUDGrad)); if (t.dotUDGrad <> "") then ( make_dot_udg_qudg graph plan_udg (t.qudg.width,t.qudg.height) ~r0:(t.qudg.radius) - ~r1:(t.qudg.r1) (t.dotUDGrad); + ~r1:(t.qudg.r1) (t.dotUDGrad); Printf.printf "%f -- %f" t.qudg.radius t.qudg.r1 ) -(* Deadcode: +(* Deadcode: let compute_attr : (Topology.t -> string list -> (string * string) list) = fun g -> List.map - (fun attr -> + (fun attr -> Printf.eprintf "Computing %s\n" attr; flush stderr; attr,match attr with @@ -82,9 +82,9 @@ let compute_attr : (Topology.t -> string list -> (string * string) list) = else raise Incorrect_attribute) ) *) - -let all_attr : bool -> (Topology.t -> (string * string) list) = - fun diameter g -> + +let all_attr : bool -> bool -> (Topology.t -> (string * string) list) = + fun rooted diameter g -> [ "min_deg", string_of_int (match !min_max with | None -> ( @@ -137,13 +137,14 @@ let all_attr : bool -> (Topology.t -> (string * string) list) = Printf.eprintf "Computing the link_number...\n"; flush stderr; Topology.get_nb_link g); - ] @ (if not diameter then [] else + "is_rooted", string_of_bool rooted; + ] @ (if not diameter then [] else ["diameter", string_of_int ( Printf.eprintf "Computing the diameter...\n"; flush stderr; - Diameter.get g) + Diameter.get g) ]) - + let to_dot_string : (Topology.t -> string -> (string * string) list -> string) = fun g name attrs -> @@ -167,12 +168,12 @@ let to_dot_string : (Topology.t -> string -> (string * string) list -> string) (match w with | 1 -> assert (n.Topology.id <> neighbour); - if n.Topology.id < neighbour || g.directed then + if n.Topology.id < neighbour || g.directed then Printf.sprintf (" %s %s %s") n.Topology.id link_kind neighbour - else - Printf.sprintf (" %s %s %s") neighbour link_kind n.Topology.id + else + Printf.sprintf (" %s %s %s") neighbour link_kind n.Topology.id | x -> - if n.Topology.id < neighbour || g.directed then + if n.Topology.id < neighbour || g.directed then Printf.sprintf (" %s %s %s [weight=%d]") n.Topology.id link_kind neighbour x else Printf.sprintf (" %s %s %s [weight=%d]") neighbour link_kind n.Topology.id x @@ -184,11 +185,11 @@ let to_dot_string : (Topology.t -> string -> (string * string) list -> string) in let links = List.map node_to_link_string g.nodes in let links = List.flatten links in - let links = List.sort_uniq compare links in + let links = List.sort_uniq compare links in let links = String.concat "\n" links in Printf.sprintf "%s %s {\n%s\n%s\n\n%s\n}\n" (if g.directed then "digraph" else "graph") - name graph_attr nodes links + name graph_attr nodes links let trials = ref 0 @@ -202,7 +203,7 @@ let make_dot : (Topology.t -> string -> (string * string) list -> unit) = else ( name := Filename.basename file_name; name:= Str.global_replace (Str.regexp "[-,]") "" !name ; - (try ( (* remove all extensions. So if name = ref "tt.dot.dot" + (try ( (* remove all extensions. So if name = ref "tt.dot.dot" at the beginning, at the end name = ref "tt". *) while true do name := Filename.chop_extension !name; @@ -220,7 +221,7 @@ let () = ( if (t.n < 0) then ( let msg = match t.action with | "void" | "grid" -> "" - | "HC" -> ( + | "HC" -> ( t.n <- 3; "=========================================================================\n"^ "Caution : the dimension is not defined or negative. It has been set to 3.\n"^ @@ -234,12 +235,12 @@ let () = ( ) in if (not t.silent) then Printf.fprintf stderr "%s" msg ); - if (t.outputFile <> "" && not t.silent) + if (t.outputFile <> "" && not t.silent) then Printf.eprintf "Generating a %s graph...\n" t.action; flush stderr; - let dir = t.directed in + let dir = t.directed in let rec gen_graph () = - let g = + let g = match t.action with | "void" -> exit 0 | "clique" -> (gen_clique dir t.n) @@ -250,7 +251,7 @@ let () = ( | "ER" -> (gen_ER dir t.n t.er) | "BA" -> (gen_BA dir t.n t.ba) | "tree" -> (rand_tree t.tree_edge dir t.n) - | "UDG" -> + | "UDG" -> let (graph, plan) = gen_udg dir t.n t.qudg.width t.qudg.height t.qudg.radius in @@ -263,7 +264,7 @@ let () = ( in generate_du_dur graph plan t; graph - | _ -> (Printf.fprintf stderr "Unexpected outcome. Command line : %s\n" + | _ -> (Printf.fprintf stderr "Unexpected outcome. Command line : %s\n" (String.concat " " (Array.to_list Sys.argv)); assert false) in if t.connected && not (Topology.is_connected g) then @@ -271,14 +272,14 @@ let () = ( else Some g in - let g = + let g = match gen_graph () with | None -> Printf.printf "[gg] failed to generate a connected graph after %d trials.\n%!" max_trials; exit 2 | Some g -> g in - make_dot g t.outputFile (all_attr t.diameter g); - if (t.outputFile <> "" && not t.silent) + make_dot g t.outputFile (all_attr t.rooted t.diameter g); + if (t.outputFile <> "" && not t.silent) then Printf.printf "Done.\nOutput file : '%s'\n" t.outputFile ) diff --git a/tools/gg/graphGen_arg.ml b/tools/gg/graphGen_arg.ml index ee7b3ec2..381cdd39 100644 --- a/tools/gg/graphGen_arg.ml +++ b/tools/gg/graphGen_arg.ml @@ -36,6 +36,7 @@ type t = { mutable connected : bool; mutable directed : bool; mutable diameter : bool; + mutable rooted : bool; mutable _args : (string * Arg.spec * string) list; mutable _man : (string * (string list * action) list) list; @@ -46,15 +47,15 @@ type t = { let usage_msg do_print_command tool = "gg is an experimental graph generator.\n"^ - (if do_print_command then + (if do_print_command then ("usage: " ^ tool ^ " <graph-kind> [<option>]*\n") else ("usage: "^tool^" [option]*\n")) -let print_usage output do_print_command tool = +let print_usage output do_print_command tool = Printf.fprintf output "%s%s" (usage_msg do_print_command tool) ( - if (do_print_command) then - "use -h to see the available <graph-kind>.\n\n" + if (do_print_command) then + "use -h to see the available <graph-kind>.\n\n" else "use -h to see available <option>.\n" ) @@ -88,6 +89,7 @@ let (make_args : unit -> t) = connected = false; directed = false; diameter = false; + rooted = false; _args = []; _man = []; @@ -110,7 +112,7 @@ let unexpected s = ( let printSpec args outChannel action (c, messageList) = ( List.iter (fun (ml,action_type) -> - if (action = action_type) then + if (action = action_type) then let (m1, oth) = match ml with | h::t -> (h,t) | _ -> ("",[]) @@ -159,7 +161,7 @@ let help args tool = ( ) ); Printf.printf "\n"; - exit 0 + exit 0 ) @@ -205,6 +207,12 @@ let (mkoptab : string array -> t -> unit) = | _ -> unexpected "--in-out-tree")) [(["Generate directed in-out-trees (downward+upward edges) "],"tree")]; + mkopt args ["--rooted-tree"] + (Arg.Unit (fun () -> match args.action with + | "tree" -> args.tree_edge <- InTree; args.directed <- false; args.rooted <- true + | _ -> unexpected "--rooted-tree")) + [(["Generate undirected rooted tree "],"tree")]; + mkopt args ["--dimension";"-d"] ~arg:" <int>" (Arg.Int (fun n -> match args.action with | "HC"-> args.n <- n @@ -272,9 +280,9 @@ let (mkoptab : string array -> t -> unit) = "inside the second"; "radius, but not the first one.\n" ], "QUDG")]; - + let msg = ["Create a DOT file to visualize the UDG plan."; - "When it transformed into a PDF that takes the positioning tags into account"; + "When it transformed into a PDF that takes the positioning tags into account"; "(like 'neato' command from GraphViz), each node is visible at the coordinates"; "where they were placed during execution.\n"] in mkopt args ["--dot-udg";"-du"]~arg:" <file>" @@ -292,7 +300,7 @@ let (mkoptab : string array -> t -> unit) = (["Create a DOT file to visualize the UDG plan."; "Same as the option '-du', but with the two radiuses being "; "also displayed.\n"],"QUDG")]; - + mkopt args ["--silent";"-s"] (Arg.Unit (fun () -> args.silent <- true)) [(["be quiet"],"void")]; @@ -312,7 +320,7 @@ let (mkoptab : string array -> t -> unit) = [(["Generate a directed graph"],"ring")]; mkopt args ["--help";"-h"] - (Arg.Unit (fun () -> help args ((argv.(0))^(if args.action = "void" then "" + (Arg.Unit (fun () -> help args ((argv.(0))^(if args.action = "void" then "" else " "^args.action)))) [(["Print this help\n"],"void")]; ) @@ -354,8 +362,8 @@ let parse argv = ( with | Arg.Bad msg -> Printf.fprintf stderr "*** Error when calling '%s': %s\n" (argv.(0)) - (first_line msg); - (print_usage stderr true argv.(0)); exit 3 (* bad argument *); - | Arg.Help _msg -> + (first_line msg); + (print_usage stderr true argv.(0)); exit 3 (* bad argument *); + | Arg.Help _msg -> help args argv.(0) ) diff --git a/tools/gg/graphGen_arg.mli b/tools/gg/graphGen_arg.mli index 9fda7860..f2a88d74 100644 --- a/tools/gg/graphGen_arg.mli +++ b/tools/gg/graphGen_arg.mli @@ -34,6 +34,7 @@ type t = { mutable connected : bool; mutable directed : bool; mutable diameter : bool; + mutable rooted : bool; mutable _args : (string * Arg.spec * string) list; mutable _man : (string * (string list * action) list) list; diff --git a/tools/gg/randomGraph.ml b/tools/gg/randomGraph.ml index 1f766262..38403a65 100644 --- a/tools/gg/randomGraph.ml +++ b/tools/gg/randomGraph.ml @@ -32,7 +32,7 @@ let gen_ER : (bool -> int -> probability -> Topology.t) = let pred n = Hashtbl.find_all node_pred n in let add_succ n m = Hashtbl.add node_succ n (1,m); - Hashtbl.add node_pred m n + Hashtbl.add node_pred m n in iteri (fun i n -> iteri (fun j m -> @@ -45,7 +45,7 @@ let gen_ER : (bool -> int -> probability -> Topology.t) = ) nodes; let nl = id_to_empty_nodes nodes in - update_tbl directed node_succ node_pred; + update_tbl directed node_succ node_pred; { nodes = nl; succ = succ; @@ -60,7 +60,7 @@ let get_m_nodes m nodes = let rec f i acc nodes = match nodes with | [] -> assert false - | (node::tail) -> + | (node::tail) -> if i > 0 then f (i-1) (node::acc) tail else @@ -85,9 +85,9 @@ let (neighbours_BA : node_id list -> int -> node_succ_t -> node_pred_t -> Hashtbl.add node_succ n (1,head); Hashtbl.add node_succ head (1,n); Hashtbl.add node_pred head n ; - Hashtbl.add node_pred n head + Hashtbl.add node_pred n head ) - m_nodes; + m_nodes; (*init terminée. On a un graph connexe pour les m premiers points, nodes ne contient que les points non ajoutés*) ignore ( @@ -107,7 +107,7 @@ let (neighbours_BA : node_id list -> int -> node_succ_t -> node_pred_t -> if (r >= 0 && not skip) then ( let n_succ = Hashtbl.find_all node_succ n_id in let d_n_id = length n_succ in - let r = r - d_n_id in + let r = r - d_n_id in if r < 0 && not skip then ( succ := (1,n_id)::!succ; deg_ref := !deg_ref - d_n_id @@ -124,7 +124,7 @@ let (neighbours_BA : node_id list -> int -> node_succ_t -> node_pred_t -> Hashtbl.add node_succ node s; Hashtbl.add node_succ (snd s) (1,node); Hashtbl.add node_pred (snd s) node ; - Hashtbl.add node_pred node (snd s) + Hashtbl.add node_pred node (snd s) ) !succ; (deg_tot + (2 * m)) @@ -144,7 +144,7 @@ let gen_BA : (bool -> int -> int -> Topology.t) = let (node_succ:node_succ_t) = Hashtbl.create nb in let (node_pred:node_pred_t) = Hashtbl.create nb in let nodes = create_nodes "p" (0,nb) in - if nb < m + 1 then + if nb < m + 1 then (Printf.eprintf "Error: with -m %d, the node number needs to be at least %d (it is %d).\n%!" m (m+1) nb; @@ -169,18 +169,23 @@ let (pre_rand_tree : bool -> GraphGen_arg.tree_edge -> node_succ_t -> | [] -> failwith "Tree Error : You need at least one nodes in your tree" | h::t -> ignore (List.fold_left (fun acc elem -> + (* choose a random node *) let no = (List.nth acc (Random.int (List.length acc))) in - (* add an option to control whether to add + (* add an option to control whether to add - down edges - up edges - both *) if tree_edge <> GraphGen_arg.OutTree then ( + (* add elem as a successor of node *) Hashtbl.add node_succ no (1,elem); + (* add node as a predecessor of elem *) Hashtbl.add node_pred elem no ); if tree_edge <> GraphGen_arg.InTree then ( + (* add node as a successor of elem *) Hashtbl.add node_succ elem (1,no); + (* add elem as a predecessor of node *) Hashtbl.add node_pred no elem ); (elem::acc) @@ -193,7 +198,7 @@ let (rand_tree: GraphGen_arg.tree_edge -> bool -> int -> Topology.t) = fun tree_edge directed nb -> let (node_succ:node_succ_t) = Hashtbl.create nb in let (node_pred:node_pred_t) = Hashtbl.create nb in - let nodes = "root"::(create_nodes "p" (1,nb-1)) in + let nodes = "root"::(create_nodes "p" (1,nb)) in let nl = id_to_empty_nodes nodes in let succ, pred = pre_rand_tree directed tree_edge node_succ node_pred nodes in { @@ -230,8 +235,8 @@ let gen_qudg : (bool -> int -> float -> float -> float -> float -> float -> List.iter (fun elem -> let (n,_,_) = elem and dist = dist_udg n_udg elem in if node <> n && - (dist <= r0 || (dist <= r1 && Random.float 1. <= p)) - (* e.g. if the node is : (within the radius r0) + (dist <= r0 || (dist <= r1 && Random.float 1. <= p)) + (* e.g. if the node is : (within the radius r0) or : (within the radius r1, with a probability of p) *) then ( Hashtbl.add node_succ node (1,n); -- GitLab