diff --git a/salut/test/dijkstra-ring/dune-project b/salut/test/dijkstra-ring/dune-project deleted file mode 120000 index f539fb462993123645b56b6670732a7198c756a4..0000000000000000000000000000000000000000 --- a/salut/test/dijkstra-ring/dune-project +++ /dev/null @@ -1 +0,0 @@ -../../../test/dune-project2copy \ No newline at end of file diff --git a/salut/test/dijkstra-ring/dune-project b/salut/test/dijkstra-ring/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..37f995d6492934bb2174bfbda93670ac438e5844 --- /dev/null +++ b/salut/test/dijkstra-ring/dune-project @@ -0,0 +1 @@ +(lang dune 3.0) diff --git a/test/bfs-spanning-tree/config.ml b/test/bfs-spanning-tree/config.ml index ae8110f558f0005e01ebe0fc03e37993a895d3b7..b509d17f2a9adf9dbb23b932b629f1f0a41cbed7 100644 --- a/test/bfs-spanning-tree/config.ml +++ b/test/bfs-spanning-tree/config.ml @@ -5,5 +5,11 @@ 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 *) + +open State +let fault = Some (fun i _ _ -> + { + d = Random.int State.d; + par = Random.int i + }) let init_search_utils = None diff --git a/test/coloring/config.ml b/test/coloring/config.ml index 7284ba4364f0c4a2eab51e0823b071ff35d5ba6a..dd548501c5e84f470040723360d1983f0c43e95f 100644 --- a/test/coloring/config.ml +++ b/test/coloring/config.ml @@ -12,7 +12,7 @@ let clash_number pidl get = let potential = Some clash_number (* let potential = None *) let legitimate = None -let fault = None +let fault = Some (fun d _pid _st -> Random.int d) let md = max_degree () diff --git a/test/coloring/p.ml b/test/coloring/p.ml index 0dd95de9674a157e6c2b4c0226486c292a7b2cb4..b5102c0e7f101400318c3638dbd62f96da5038a6 100644 --- a/test/coloring/p.ml +++ b/test/coloring/p.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 14/04/2022 (at 17:17) by Erwan Jahier> *) +(* Time-stamp: <modified the 31/01/2024 (at 16:34) by Erwan Jahier> *) (* This is algo 3.1 in the book *) open Algo @@ -7,9 +7,9 @@ let k = if is_directed () then else max_degree () + 1 -let (init_state: int -> string -> 'v) = fun i _ -> Random.int i +let (init_state: int -> string -> 'v) = fun i _ -> Random.int i -let (colors : 'v neighbor list -> 'v list) = fun nl -> +let (colors : 'v neighbor list -> 'v list) = fun nl -> List.map (fun n -> state n) nl (* Returns the free colors is ascending order (n.log(n)) @@ -32,10 +32,10 @@ let (free : 'v neighbor list -> 'v list) = fun nl -> in aux [] n_colors (k-1) -let (enable_f: 'v -> 'v neighbor list -> action list) = +let (enable_f: int -> int neighbor list -> action list) = fun c nl -> if List.exists (fun n -> state n = c) nl then ["conflict"] else [] - -let (step_f : 'v -> 'v neighbor list -> action -> 'v) = + +let (step_f : int -> int neighbor list -> action -> int) = fun _ nl _ -> List.hd (free nl) (* Returns the smallest possible color *) diff --git a/test/dijkstra-ring/config.ml b/test/dijkstra-ring/config.ml index 4db94dcdf31886857d7bd140cf4b5516bd887e91..ce0d4ba432971fbc0f4474c78f341baad82fec8f 100644 --- a/test/dijkstra-ring/config.ml +++ b/test/dijkstra-ring/config.ml @@ -100,7 +100,7 @@ let cost : pid list -> (pid -> t * (t neighbor * pid) list) -> float = let potential = Some cost -let fault = None +let fault = Some (fun _d _pid st -> { st with v = Random.int (card())} ) (* For the Dijkstra ring, a configuration is legitimate iff there is exactly one token. diff --git a/test/ghosh/config.ml b/test/ghosh/config.ml index e82eec4b1094f490a400d1f5ef1bbd9dcaf4289a..3972313b887d9787142e7c283fdf5c9b8738f470 100644 --- a/test/ghosh/config.ml +++ b/test/ghosh/config.ml @@ -23,7 +23,7 @@ let (legitimate: pid list -> (pid -> t * (t neighbor * pid) list) -> bool) = let legitimate = Some legitimate let potential = None -let fault = None (* None => the simulation stop once a legitimate configuration is reached *) +let fault = Some(fun _ _ st -> { st with s = (Random.bool ()) }) open Algo diff --git a/test/k-clustering/config.ml b/test/k-clustering/config.ml index 02fc2c075d57d4468c2a27b02fa110322cb7dcc5..c9845771ca34d2e4c955e64b22998b9e8da2e31a 100644 --- a/test/k-clustering/config.ml +++ b/test/k-clustering/config.ml @@ -79,7 +79,12 @@ let (pf: pid list -> (pid -> ('a * ('a neighbor * pid) list)) -> float) = let potential = Some pf let legitimate = None (* None => only silent configuration are legitimate *) -let fault = None +let fault = Some(fun _ pid _ -> + { + isRoot = pid = "Root"; (* ZZZ: The root of the tree should be named "Root"! *) + alpha = Random.int (2*k+1); + par = if pid="Root" then -1 else 0 (* the input tree should be sorted alphabetically (wrt a bf traversal) *) + }) open State let maxi = 2*k+1 diff --git a/test/ring-orientation/config.ml b/test/ring-orientation/config.ml index 54c8032ff65f5ee19a6ad8e3818cb08657afaf94..e15c41069a0161b9e58aef2c21199a410c94a541 100644 --- a/test/ring-orientation/config.ml +++ b/test/ring-orientation/config.ml @@ -1,6 +1,10 @@ let potential = None (* None => only -sd, -cd, -lcd, -dd, or -custd are possible *) -let fault = None (* None => the simulation stop once a legitimate configuration is reached *) let init_search_utils = None (* To provide to use --init-search *) let legitimate = None (* XXX this is wrong: FIXME *) + +open State +let fault = Some (fun _nl _ _ -> + { color_0 = Random.bool () ; phase_pos = Random.bool () ; orient_left = Random.bool () } +) diff --git a/test/ring-orientation/p.ml b/test/ring-orientation/p.ml index fbbc86c2a30bd24ab5fe115b580ed5d654debfe4..2df2dbad26163969e672b099555212ccac36bcc3 100644 --- a/test/ring-orientation/p.ml +++ b/test/ring-orientation/p.ml @@ -1,8 +1,9 @@ -(* Time-stamp: <modified the 07/07/2023 (at 15:24) by Erwan Jahier> *) +(* Time-stamp: <modified the 18/10/2023 (at 17:07) by Erwan Jahier> *) (* Uniform deterministic self-stabilizing ring-orientation on odd-length rings Hoepman, Jaap-Henk WDAG'1994 + https://core.ac.uk/download/pdf/301654088.pdf hyp: central daemon *) diff --git a/test/ring-orientation/ring_orientation_oracle.lus b/test/ring-orientation/ring_orientation_oracle.lus index 8241f5cc9db2989e4e41e1931bfc6ebcfdcd0172..80212ecacb4bf8de3526640018a22136fd00d498 100644 --- a/test/ring-orientation/ring_orientation_oracle.lus +++ b/test/ring-orientation/ring_orientation_oracle.lus @@ -1,8 +1,9 @@ -- include "../lustre/oracle_utils.lus" include "../../salut/lib/utils.lus" +include "../../salut/test/ring-orientation/state.lus" -type state = { color_0 : bool ; phase_pos : bool ; orient_left : bool }; +-- type state = { color_0 : bool ; phase_pos : bool ; orient_left : bool }; function to_state( color_0 : bool ; phase_pos : bool ; orient_left : bool ) returns(res : state); @@ -12,6 +13,8 @@ tel; +-- This oracle checks th 5.5 (via lurette) + node ring_orientation_oracle<<const an:int; const pn:int>> (legitimate:bool; Enab, Acti: bool^an^pn; Config:state^card ; round:bool; round_nb:int) returns (ok:bool); diff --git a/test/unison/Makefile b/test/unison/Makefile index bb681c3fd2ad3ebb38ffc933744e90eb05da97b6..0fde985f11286130a9f4bd80cce1a752be78aabd 100644 --- a/test/unison/Makefile +++ b/test/unison/Makefile @@ -1,4 +1,4 @@ -# Time-stamp: <modified the 17/01/2023 (at 14:22) by Erwan Jahier> +# Time-stamp: <modified the 13/02/2024 (at 21:04) by Erwan Jahier> DECO_PATTERN="0-:unison.ml" -include ./Makefile.dot @@ -20,11 +20,9 @@ test2: ring.cmxs $(sasa) -l 50 ring.dot -rif test3: - cp state_with_fault.ml state.ml rm fig41.cmxs make fig41.cmxs $(sasa) -l 5 fig41.dot -sd -rif - cp state_no_fault.ml state.ml rm fig41.cmxs sasaopt=-sd diff --git a/test/unison/config.ml b/test/unison/config.ml index e76247170e1347fe916a1d9f02b7b30abda40e23..2ad7944cfcc7b30be1fc2b5081b621e32b19a64e 100644 --- a/test/unison/config.ml +++ b/test/unison/config.ml @@ -1,6 +1,6 @@ -let fault = None (* None => the simulation stop once a legitimate configuration is reached *) +let fault = Some(fun _ _ _ -> Random.int State.m) let legitimate pidl from_pid = (* a legitimate configuration is reached when all states have the same values *) diff --git a/test/unison/state.ml b/test/unison/state.ml index 36fa4acebfa26dcfeaee2fb9346cc74429d557aa..0ca6ec321a910f2aae5018547cf86b61254fa50b 100644 --- a/test/unison/state.ml +++ b/test/unison/state.ml @@ -2,6 +2,10 @@ type t = int let to_string = (fun s -> Printf.sprintf "c=%i" s) +(* let m=10 (* max 2 (1+2*diameter ()) *) *) +let diameter = Algo.diameter () +let m = max 2 (2*diameter-1) + let (of_string: (string -> t) option) = Some (fun s -> let res = Scanf.sscanf s "c=%d" (fun i -> i ) in @@ -13,8 +17,6 @@ let copy x = x let actions = ["g"] let potential = None -let fault = None - let legitimate pidl from_pid = (* a legitimate configuration is reached when all states have the same values *) let v = fst(from_pid (List.hd pidl)) in @@ -22,8 +24,6 @@ let legitimate pidl from_pid = (fun acc pid -> acc && fst(from_pid pid) = v) true (List.tl pidl) - - + + let legitimate = Some legitimate - - diff --git a/test/unison/state_no_fault.ml b/test/unison/state_no_fault.ml deleted file mode 100644 index 36fa4acebfa26dcfeaee2fb9346cc74429d557aa..0000000000000000000000000000000000000000 --- a/test/unison/state_no_fault.ml +++ /dev/null @@ -1,29 +0,0 @@ - -type t = int -let to_string = (fun s -> Printf.sprintf "c=%i" s) - -let (of_string: (string -> t) option) = - Some (fun s -> - let res = Scanf.sscanf s "c=%d" (fun i -> i ) in - res - ) - - -let copy x = x -let actions = ["g"] -let potential = None - -let fault = None - -let legitimate pidl from_pid = - (* a legitimate configuration is reached when all states have the same values *) - let v = fst(from_pid (List.hd pidl)) in - List.fold_left - (fun acc pid -> acc && fst(from_pid pid) = v) - true - (List.tl pidl) - - -let legitimate = Some legitimate - - diff --git a/test/unison/state_with_fault.ml b/test/unison/state_with_fault.ml deleted file mode 100644 index 888253f228e95729e6b3491078428ca8a55092f0..0000000000000000000000000000000000000000 --- a/test/unison/state_with_fault.ml +++ /dev/null @@ -1,32 +0,0 @@ - -type t = int -let to_string = (fun s -> Printf.sprintf "c=%i" s) -let (of_string: (string -> t) option) = - Some (fun s -> - let res = Scanf.sscanf s "c=%d" (fun i -> i ) in - res - ) - -let copy x = x -let actions = ["g"] -let potential = None - - -let fault m _ e = - if Random.bool () then Random.int m else e - - -let fault = Some fault - -let legitimate pidl from_pid = - (* a legitimate configuration is reached when all states have the same values *) - let v = fst(from_pid (List.hd pidl)) in - List.fold_left - (fun acc pid -> acc && fst(from_pid pid) = v) - true - (List.tl pidl) - - -let legitimate = Some legitimate - - diff --git a/test/unison/unison.ml b/test/unison/unison.ml index 3dd47d238bb1f6fa2517a22dfef3ddc09b992d94..4f63535b383fd4667e17cc49cf0fc5274c4580a7 100644 --- a/test/unison/unison.ml +++ b/test/unison/unison.ml @@ -1,11 +1,8 @@ -(* Time-stamp: <modified the 22/11/2022 (at 13:59) by Erwan Jahier> *) +(* Time-stamp: <modified the 13/02/2024 (at 20:55) by Erwan Jahier> *) open Algo -(* let m=10 (* max 2 (1+2*diameter ()) *) *) -let diameter = Algo.diameter () - -let m = max 2 (2*diameter-1) +let m = State.m let (init_state: int -> string -> 'v) = fun _ _ -> @@ -15,17 +12,14 @@ let (init_state: int -> string -> 'v) = let new_clock_value nl clock = let cl = List.map (fun n -> state n) nl in let min_clock = List.fold_left min clock cl in - (min_clock + 1) mod m + (min_clock + 1) mod m let (enable_f: 'v -> 'v neighbor list -> action list) = fun clock nl -> if (new_clock_value nl clock) <> clock then ["g"] else [] - + let (step_f : 'v -> 'v neighbor list -> action -> 'v) = fun clock nl a -> let v = new_clock_value nl clock in match a with | _ -> v - - - diff --git a/tools/simca/nonreg_test_campaign.ml b/tools/simca/nonreg_test_campaign.ml index bc24c4c6c8530eb40288334dbd2db0025dcf4b99..179e0d3fa5e0a752448e7ada03c6c3b7f9e0b607 100644 --- a/tools/simca/nonreg_test_campaign.ml +++ b/tools/simca/nonreg_test_campaign.ml @@ -1,6 +1,6 @@ #use "genExpeMakefiles.ml";; precision := 0.1;; -(* 0.1 means that we simulate until the onfidence Interval size of +(* 0.1 means that we simulate until the confidence Interval size of the 3 complexity numbers under estimation is smaller than 10% of their current estimation. @@ -11,7 +11,7 @@ timeout_in_sec := 60;; (* ditto *) let algos = ["../../test/alea-coloring-alt"; "../../test/alea-coloring-unif"; "../../test/alea-coloring"] -let daemons = ["-sd";"-lcd";"-dd"] +let daemons = ["-sd";"-lcd";"-dd"] let cliques = List.init 5 (fun n -> Clique (10*(n+1))) (* [10; 20; ...; 50] *) let rings = List.init 5 (fun n -> Ring (100*(n+1))) (* [100; 200; ...; 500] *) let er = List.init 5 (fun n -> ER (20*(n+1), 0.4)) (* [20; 40; ...; 100] *) @@ -22,7 +22,7 @@ let gen_make_rules () = gen_makefile "Makefile.expe-rules" daemons algos network #use "parseLog.ml";; let gen_pdf () = let gl = ["clique"; "ring"; "er"] in - List.iter (fun n -> sh ("rm -f "^n^".data")) gl; (* because parse_log appends data *) + List.iter (fun n -> sh ("rm -f "^n^".data")) gl; (* because parse_log appends data *) parse_log ["Uniform When Activated", "alea-coloring-unif"] gl daemons; parse_log ["Smallest When Activated","alea-coloring"] gl daemons; parse_log ["Always the Biggest", "alea-coloring-alt"] gl daemons;