Commit 30613090 authored by erwan's avatar erwan
Browse files

Merge branch 'master' of gricad-gitlab.univ-grenoble-alpes.fr:verimag/synchrone/sasa

parents 72e6c596 b50e8aba
Pipeline #67724 failed with stages
in 1 minute and 30 seconds
......@@ -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
......
......@@ -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
......
(* 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
]}
......
;; 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)
......
......@@ -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