From 6a0975a06c43b3971ed51865cb97a01c77b1a16f Mon Sep 17 00:00:00 2001
From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr>
Date: Mon, 11 Oct 2021 11:35:17 +0200
Subject: [PATCH] refactor: rename and document the init state search
---
lib/algo/algo.ml | 8 ++++----
lib/algo/algo.mli | 19 +++++++++++++------
lib/sasacore/genRegister.ml | 4 ++--
lib/sasacore/register.ml | 16 ++++++++--------
lib/sasacore/register.mli | 6 +++---
lib/sasacore/worstInit.ml | 8 ++++----
test/coloring/config.ml | 2 +-
test/dijkstra-ring/config.ml | 2 +-
test/k-clustering/config.ml | 2 +-
test/rsp-tree/config.ml | 2 +-
test/st-KK06-algo1/config.ml | 2 +-
test/toy-example-a5sf/config.ml | 2 +-
test/toy-example-sum/config.ml | 2 +-
13 files changed, 41 insertions(+), 34 deletions(-)
diff --git a/lib/algo/algo.ml b/lib/algo/algo.ml
index f6e7f669..2da5646b 100644
--- a/lib/algo/algo.ml
+++ b/lib/algo/algo.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 17/09/2021 (at 12:09) by Erwan Jahier> *)
+(* Time-stamp: <modified the 11/10/2021 (at 11:11) by Erwan Jahier> *)
open Sasacore
(* Process programmer API *)
@@ -64,7 +64,7 @@ type 's to_register = {
legitimate_function : 's legitimate_fun option;
fault_function : 's fault_fun option;
potential_function: 's potential_fun option;
- for_init_search : 's state_to_nums_fun option (** for sasa --init-search *)
+ init_search_utils : 's state_to_nums_fun option (** for sasa --init-search *)
}
@@ -159,9 +159,9 @@ let (register : 's to_register -> unit) =
| None -> ()
| Some ff -> Register.reg_fault (Some ff)
);
- (match s.for_init_search with
+ (match s.init_search_utils with
| None -> ()
- | Some(s2n,n2s) -> Register.reg_for_init_search (Some (to_reg_s2n s2n, to_reg_n2s n2s))
+ | Some(s2n,n2s) -> Register.reg_init_search_utils (Some (to_reg_s2n s2n, to_reg_n2s n2s))
);
()
diff --git a/lib/algo/algo.mli b/lib/algo/algo.mli
index 85fa4d4d..090179db 100644
--- a/lib/algo/algo.mli
+++ b/lib/algo/algo.mli
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 06/10/2021 (at 17:34) by Erwan Jahier> *)
+(* Time-stamp: <modified the 11/10/2021 (at 11:11) by Erwan Jahier> *)
(** {1 The Algorithm programming Interface}
A SASA process is an instance of an algorithm defined via this
@@ -160,10 +160,17 @@ 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
-(** {3 Finding bad initial state }
+(** {3 Finding bad initial states }
- In order to find a bad initial value, sasa need to be able to transform ['s]
- into [num], and back. Also, the [state_to_string] field should show the whole state.
+ In order to find a bad initial value, sasa needs to be able to
+ transform ['s] into [num], and back (to mutate the nums).
+
+ Note that it is not necessary to expose the whole state to the
+ optimization process. To do that, one just needs to filter some of
+ the state value in the ['s -> num list] function. This is the
+ reason the state reconstruction function ([num list -> 's -> 's])
+ takes a state as argument, to be able to fill the filtered values
+ (that never change during the search).
*)
type num = F of float | I of int | B of bool
type 's state_to_nums_fun = ('s -> num list) * (num list -> 's -> 's)
@@ -186,9 +193,9 @@ type 's to_register = {
copy_state: 's -> 's;
actions : action list (** Mandatory in custom daemon mode, or to use oracles *);
legitimate_function : 's legitimate_fun option;
- fault_function : 's fault_fun option (** called at legitimate configuration *);
+ fault_function : 's fault_fun option (** called at legitimate configuration *);
potential_function: 's potential_fun option (** Mandatory with Evil daemons *);
- for_init_search : 's state_to_nums_fun option (** for sasa --init-search *)
+ init_search_utils : 's state_to_nums_fun option (** for sasa --init-search *)
}
(** - For the [state_to_string] field, the idea is to print the raw
values contained in ['s]. If a value is omitted, one won't see it
diff --git a/lib/sasacore/genRegister.ml b/lib/sasacore/genRegister.ml
index fc01d118..f688fe23 100644
--- a/lib/sasacore/genRegister.ml
+++ b/lib/sasacore/genRegister.ml
@@ -52,7 +52,7 @@ let (f: string list -> string * string * string -> unit) =
potential_function = %s.potential;
legitimate_function = %s.legitimate;
fault_function = %s.fault;
- for_init_search = %s.for_init_search;
+ init_search_utils = %s.init_search_utils;
}
"
(String.concat ";" l)
@@ -90,7 +90,7 @@ let actions = [\"a\"]
let potential = None (* None => only -sd, -cd, -lcd, -dd, or -custd are possible *)
let legitimate = None (* None => only silent configuration are legitimate *)
let fault = None (* None => the simulation stop once a legitimate configuration is reached *)
-let for_init_search = None (* To provide to use --init-search *)
+let init_search_utils = None (* To provide to use --init-search *)
";
flush oc;
close_out oc;
diff --git a/lib/sasacore/register.ml b/lib/sasacore/register.ml
index 65d56e28..0dd7e674 100644
--- a/lib/sasacore/register.ml
+++ b/lib/sasacore/register.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 17/09/2021 (at 12:09) by Erwan Jahier> *)
+(* Time-stamp: <modified the 11/10/2021 (at 11:11) by Erwan Jahier> *)
type 's neighbor = {
state: 's ;
@@ -32,7 +32,7 @@ type 's internal_tables = {
mutable potential: Obj.t;
mutable legitimate: Obj.t;
mutable fault: Obj.t;
- mutable for_init_search: Obj.t;
+ mutable init_search_utils: Obj.t;
mutable actions:action list;
mutable topology : Topology.t option;
mutable card : int option;
@@ -66,7 +66,7 @@ let (tbls:'s internal_tables) = {
potential = (Obj.repr None);
legitimate = (Obj.repr None);
fault = (Obj.repr None);
- for_init_search = (Obj.repr None);
+ init_search_utils = (Obj.repr None);
actions = [];
topology = None;
card = None;
@@ -140,12 +140,12 @@ let (reg_fault : 's fault_fun option -> unit) = fun x ->
let (get_fault : unit -> 's fault_fun option) = fun () ->
Obj.obj tbls.fault
-let (reg_for_init_search : 's state_to_nums_fun option -> unit) = fun x ->
- if !verbose_level > 0 then Printf.eprintf "Registering for_init_search functions\n%!";
- tbls.for_init_search <- (Obj.repr x)
+let (reg_init_search_utils : 's state_to_nums_fun option -> unit) = fun x ->
+ if !verbose_level > 0 then Printf.eprintf "Registering init_search_utils functions\n%!";
+ tbls.init_search_utils <- (Obj.repr x)
-let (get_for_init_search : unit -> 's state_to_nums_fun option) = fun () ->
- Obj.obj tbls.for_init_search
+let (get_init_search_utils : unit -> 's state_to_nums_fun option) = fun () ->
+ Obj.obj tbls.init_search_utils
let (reg_legitimate : 's legitimate_fun option -> unit) = fun x ->
if !verbose_level > 0 then Printf.eprintf "Registering legitimate function\n%!";
diff --git a/lib/sasacore/register.mli b/lib/sasacore/register.mli
index 76c02dbd..98f2ee4c 100644
--- a/lib/sasacore/register.mli
+++ b/lib/sasacore/register.mli
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 17/09/2021 (at 12:09) by Erwan Jahier> *)
+(* Time-stamp: <modified the 11/10/2021 (at 11:11) by Erwan Jahier> *)
(** This module duplicates and extends the Algo module with get_*
functions.
@@ -34,7 +34,7 @@ val reg_init_state : algo_id -> (int -> string -> 's) -> unit
val reg_enable : algo_id -> 's enable_fun -> unit
val reg_step : algo_id -> 's step_fun -> unit
val reg_potential : 's potential_fun option -> unit
-val reg_for_init_search : 's state_to_nums_fun option -> unit
+val reg_init_search_utils : 's state_to_nums_fun option -> unit
val reg_legitimate : 's legitimate_fun option -> unit
val reg_fault : 's fault_fun option -> unit
val reg_actions : action list -> unit
@@ -75,7 +75,7 @@ val get_step : algo_id -> 's step_fun
val get_init_state : algo_id -> int -> string -> 's
val get_actions : unit -> action list
val get_potential : unit -> 's potential_fun option
-val get_for_init_search : unit -> 's state_to_nums_fun option
+val get_init_search_utils : unit -> 's state_to_nums_fun option
val get_legitimate : unit -> 's legitimate_fun option
val get_fault : unit -> 's fault_fun option
val get_value_to_string : unit -> 's -> string
diff --git a/lib/sasacore/worstInit.ml b/lib/sasacore/worstInit.ml
index 61a394ab..ed013455 100644
--- a/lib/sasacore/worstInit.ml
+++ b/lib/sasacore/worstInit.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 08/10/2021 (at 10:05) by Erwan Jahier> *)
+(* Time-stamp: <modified the 11/10/2021 (at 11:11) by Erwan Jahier> *)
open Register
@@ -63,7 +63,7 @@ let (point_to_ss : point -> 'v SimuState.t -> 'v SimuState.t) =
fun point ss ->
let (state_to_nums, nums_to_state :
('v -> Register.num list) * (Register.num list -> 'v -> 'v )) =
- match Register.get_for_init_search () with
+ match Register.get_init_search_utils () with
| None -> assert false
| Some (f, g) -> f, g
in
@@ -100,9 +100,9 @@ let (point_to_ss : point -> 'v SimuState.t -> 'v SimuState.t) =
let (ss_to_point : 'v SimuState.t -> point) =
fun ss ->
let (state_to_nums : ('v -> Register.num list) ) =
- match Register.get_for_init_search () with
+ match Register.get_init_search_utils () with
| None ->
- failwith "the Algo.for_init_search registration field should provide state_to_nums functions"
+ failwith "the Algo.init_search_utils registration field should provide state_to_nums functions"
| Some (f, _) -> f
in
let size =
diff --git a/test/coloring/config.ml b/test/coloring/config.ml
index b0466d31..3bcc6b7d 100644
--- a/test/coloring/config.ml
+++ b/test/coloring/config.ml
@@ -13,4 +13,4 @@ let potential = Some clash_number
(* let potential = None *)
let legitimate = None
let fault = None
-let for_init_search = None
+let init_search_utils = None
diff --git a/test/dijkstra-ring/config.ml b/test/dijkstra-ring/config.ml
index 19f07946..7d7b9473 100644
--- a/test/dijkstra-ring/config.ml
+++ b/test/dijkstra-ring/config.ml
@@ -113,4 +113,4 @@ let n2s nl s =
| [I i] -> { s with v = i }
| _ -> assert false
-let for_init_search = Some (s2n, n2s)
+let init_search_utils = Some (s2n, n2s)
diff --git a/test/k-clustering/config.ml b/test/k-clustering/config.ml
index e2025351..200a63d5 100644
--- a/test/k-clustering/config.ml
+++ b/test/k-clustering/config.ml
@@ -42,4 +42,4 @@ let potential = Some pf
let legitimate = None (* None => only silent configuration are legitimate *)
let fault = None (* None => the simulation stop once a legitimate configuration is reached *)
-let for_init_search = None
+let init_search_utils = None
diff --git a/test/rsp-tree/config.ml b/test/rsp-tree/config.ml
index aa09e93d..b2aa893d 100644
--- a/test/rsp-tree/config.ml
+++ b/test/rsp-tree/config.ml
@@ -6,4 +6,4 @@
let potential = None (* None => only -sd, -cd, -lcd, -dd, or -custd are possible *)
let legitimate = None (* None => only silent configuration are legitimate *)
let fault = None (* None => the simulation stop once a legitimate configuration is reached *)
-let for_init_search = None
+let init_search_utils = None
diff --git a/test/st-KK06-algo1/config.ml b/test/st-KK06-algo1/config.ml
index 0ad60e2f..1d43d76d 100644
--- a/test/st-KK06-algo1/config.ml
+++ b/test/st-KK06-algo1/config.ml
@@ -6,4 +6,4 @@
let potential = None (* None => only -sd, -cd, -lcd, -dd, or -custd are possible *)
let legitimate = None (* None => only silent configuration are legitimate *)
let fault = None (* None => the simulation stop once a legitimate configuration is reached *)
-let for_init_search = None
+let init_search_utils = None
diff --git a/test/toy-example-a5sf/config.ml b/test/toy-example-a5sf/config.ml
index ca8ff2a2..4b0b0af6 100644
--- a/test/toy-example-a5sf/config.ml
+++ b/test/toy-example-a5sf/config.ml
@@ -39,4 +39,4 @@ let potential = Some pf
let legitimate = None (* None => only silent configuration are legitimate *)
let fault = None (* None => the simulation stop once a legitimate configuration is reached *)
-let for_init_search = None
+let init_search_utils = None
diff --git a/test/toy-example-sum/config.ml b/test/toy-example-sum/config.ml
index c4e51f69..de724c19 100644
--- a/test/toy-example-sum/config.ml
+++ b/test/toy-example-sum/config.ml
@@ -52,4 +52,4 @@ let potential_combined: State.t Algo.potential_fun =
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 *)
-let for_init_search = None
+let init_search_utils = None
--
GitLab