From 7a49c8bbd0a88616db5b99564624091ce11d345e Mon Sep 17 00:00:00 2001 From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr> Date: Tue, 5 Oct 2021 15:54:42 +0200 Subject: [PATCH] feat: implement a --init-search option to find the best initial state using local search --- .gitignore | 1 + .gitlab-ci.yml | 2 +- guides/users/README.md | 150 +++++++++++++++--------------- guides/users/README.org | 10 +- lib/algo/algo.ml | 35 ++++++- lib/algo/algo.mli | 15 +-- lib/sasacore/diameter.ml | 12 +-- lib/sasacore/dune | 4 +- lib/sasacore/genRegister.ml | 5 +- lib/sasacore/register.ml | 14 ++- lib/sasacore/register.mli | 9 +- lib/sasacore/sasArg.ml | 17 +++- lib/sasacore/sasArg.mli | 6 +- lib/sasacore/simuState.ml | 54 ++++++++++- lib/sasacore/simuState.mli | 4 +- lib/sasacore/topology.mli | 4 +- lib/sasacore/worstInit.ml | 177 ++++++++++++++++++------------------ 17 files changed, 320 insertions(+), 199 deletions(-) diff --git a/.gitignore b/.gitignore index 0f0d168d..ff68d410 100644 --- a/.gitignore +++ b/.gitignore @@ -155,3 +155,4 @@ tags /toto /tools/simca/xxx /tools/simca/x +tk& diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index d5f97d3a..102934e1 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -48,7 +48,7 @@ test_opam_test: # automating version numbering release: - image: node:12-buster-slim + image: node:14-buster-slim stage: release before_script: - apt-get update && apt-get install -y --no-install-recommends git-core ca-certificates diff --git a/guides/users/README.md b/guides/users/README.md index 269c0ca5..312cef9a 100644 --- a/guides/users/README.md +++ b/guides/users/README.md @@ -1,42 +1,42 @@ -- [TL;DR](#org03fdb32) -- [Topology](#org6bce3a3) -- [Algorithms](#org4ebc979) -- [Examples](#orgbc8bb97) -- [Batch mode](#org5e2df1b) - - [Running batch simulations](#orgb1110c6) - - [Running batch simulations with Built-in daemons](#orgdaa4528) - - [Running batch simulations with manual (a.k.a. custom) daemons](#org0600fb4) - - [Running batch simulations with `lurette`](#orgc2124a4) - - [Viewing Results](#org352ec48) - - [The `sasa` CLI](#org065842a) -- [Interactive mode](#org8cabb77) - - [Example: use `rdbg` from the `test/alea-coloring/` directory](#org940a545) - - [The examples of test directory](#orga8bb93c) - - [Running interactive sessions with `rdbg`](#orgc1677b8) - - [Getting `rdbg` on-line help](#org45312ba) - - [A `rdbg` `sasa` GUI](#orgc050bc9) - - [Useful Modules](#org68ddece) -- [Install](#org870ae55) - - [TL;DR](#org6a2be30) - - [Not strictly mandatory, but useful, third-party software](#orgc778fb2) - - [Install `sasa` via opam (version >= 2.\*)](#orge389556) - - [Install `sasa` via `git`](#org375da8e) - - [Use `sasa` via docker](#org8634d7f) - - [Use `sasa` via a Virtual Machine](#orgfca4398) -- [Screencasts](#org1965004) -- [More](#orgb10647d) -- [FAQ](#org45ee1b0) - - [Is there a FAQ?](#orgcdd1fda) - - [I have a compilation error that I don't understand](#org1a4026e) - - [I have the error `Invalid_argument("compare: functional value")`](#org59935ae) - - - -<a id="org03fdb32"></a> +- [TL;DR](#org7d8f7c0) +- [Topology](#orgb740b40) +- [Algorithms](#org8dcf853) +- [Examples](#org4a3e28a) +- [Batch mode](#org45900d7) + - [Running batch simulations](#org5e6aabd) + - [Running batch simulations with Built-in daemons](#org688c49a) + - [Running batch simulations with manual (a.k.a. custom) daemons](#orge126295) + - [Running batch simulations with `lurette`](#org5e351b7) + - [Viewing Results](#org5a16c11) + - [The `sasa` CLI](#org787969e) +- [Interactive mode](#org578208a) + - [Example: use `rdbg` from the `test/alea-coloring/` directory](#org7d9fb4e) + - [The examples of test directory](#org646483c) + - [Running interactive sessions with `rdbg`](#org4538175) + - [Getting `rdbg` on-line help](#org8bb16ba) + - [A `rdbg` `sasa` GUI](#org69bf58c) + - [Useful Modules](#org5781218) +- [Install](#orgccc7e98) + - [TL;DR](#orgf88e099) + - [Not strictly mandatory, but useful, third-party software](#orge18cbad) + - [Install `sasa` via opam (version >= 2.\*)](#orgb522bdb) + - [Install `sasa` via `git`](#orgb3bb93b) + - [Use `sasa` via docker](#orgbdfd166) + - [Use `sasa` via a Virtual Machine](#org8a3c22b) +- [Screencasts](#orgcb02048) +- [More](#org020d69e) +- [FAQ](#org4be25b7) + - [Is there a FAQ?](#orgb84f441) + - [I have a compilation error that I don't understand](#orgc8ed449) + - [I have the error `Invalid_argument("compare: functional value")`](#org0f6d260) + + + +<a id="org7d8f7c0"></a> # TL;DR -<a id="org7b6382e"></a> SASA is a **Self-stabilizing Algorithms SimulAtor**, based on the so-called **Atomic State model** (ASM) introduced by <span class="underline">Dijkstra</span> in its seminal article on [Self-stabilizing distributed algorithms](http://www.cs.utexas.edu/~EWD/ewd04xx/EWD426.PDF). This model is also sometimes named "locally shared memory model with composite atomicity" +<a id="org7c817e9"></a> SASA is a **Self-stabilizing Algorithms SimulAtor**, based on the so-called **Atomic State model** (ASM) introduced by <span class="underline">Dijkstra</span> in its seminal article on [Self-stabilizing distributed algorithms](http://www.cs.utexas.edu/~EWD/ewd04xx/EWD426.PDF). This model is also sometimes named "locally shared memory model with composite atomicity" Basically, one needs to provide: @@ -49,8 +49,8 @@ The fastest way to get started is to copy the files provided in the `test/skelet cd test cp -rf skeleton my_algo # copy a simple example cd my_algo # one may want to edit "p.ml" and "ring.dot" -make ring.cmxs # compile anything that needs to be compiled -sasa ring.dot -l 4 # run a batch simulation for 4 steps +make ring7.cmxs # compile anything that needs to be compiled +sasa ring7.dot -l 4 # run a batch simulation for 4 steps ``` - [SASA source code](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa) @@ -61,11 +61,11 @@ sasa ring.dot -l 4 # run a batch simulation for 4 steps [](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/poster.pdf) -<a id="org6bce3a3"></a> +<a id="orgb740b40"></a> # Topology -<a id="org965f693"></a> <a id="orged45ab6"></a> The topology is given via `.dot` files, that should +<a id="orgf00d97c"></a> <a id="org5857dc1"></a> The topology is given via `.dot` files, that should 1. follow the [graphviz/dot format](https://en.wikipedia.org/wiki/DOT_(graph_description_language)) 2. have nodes **labeled** by the `algo` field @@ -121,14 +121,14 @@ graph ring { Such parameters can be retrieved in algorithms using the `Algo.get_graph_attribute : string -> string` function. For example, if you know the graph diameter, you can define it as a graph attribute (a `Algo.diameter: unit -> int` function is provided, but it can be expensive to use for large graphs). -Some tools are provided in the `sasa` [distributions](#org5572cc7) to generate such kinds of `dot` graphs: <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/sasa-gg/> +Some tools are provided in the `sasa` [distributions](#org366a559) to generate such kinds of `dot` graphs: <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/sasa-gg/> -<a id="org4ebc979"></a> +<a id="org8dcf853"></a> # Algorithms -<a id="org0148ed7"></a> +<a id="orga43fd68"></a> The following has been generated from [algo.mli](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/blob/master/lib/algo/algo.mli) @@ -138,7 +138,7 @@ The following has been generated from [algo.mli](https://gricad-gitlab.univ-gren </div> -<a id="orgbc8bb97"></a> +<a id="org4a3e28a"></a> # Examples @@ -178,14 +178,14 @@ The `test` directory also contains sub-directories which gathers programs shared - `test/*/my-rdbg-tuning.ml`: includes `test/my-rdbg-tuning.ml` and defines commands specific to the example of the directory. Indeed, `rdbg`, once launched, first tries to read the content of the file name `my-rdbg-tuning.ml` (if it exists). -<a id="org5e2df1b"></a> +<a id="org45900d7"></a> # Batch mode  -<a id="orgb1110c6"></a> +<a id="org5e6aabd"></a> ## Running batch simulations @@ -252,7 +252,7 @@ sasa ring.dot # launch the simulation nb: the simulation output (in the green frame) follows the [RIF](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-orga43b00b) conventions. -<a id="orgdaa4528"></a> +<a id="org688c49a"></a> ## Running batch simulations with Built-in daemons @@ -271,7 +271,7 @@ sasa -h | grep "\-daemon" --greedy-daemon, -gd -<a id="org0600fb4"></a> +<a id="orge126295"></a> ## Running batch simulations with manual (a.k.a. custom) daemons @@ -309,7 +309,7 @@ luciole-rif sasa ring.dot --custom-daemon Daemons can also by simulated by [`lutin`](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-sec-4) programs via the use of [`lurette`](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-sec-9) (for batch executions) or [`rdbg`](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-sec-10) (for interactive sessions). -<a id="orgc2124a4"></a> +<a id="org5e351b7"></a> ## Running batch simulations with `lurette` @@ -334,14 +334,14 @@ Note that for `lurette`, the role of the SUT (System Under Test) and the one of For more information on this topic: <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/sasa-daemons/> -<a id="org352ec48"></a> +<a id="org5a16c11"></a> ## Viewing Results `sasa -rif` and `lurette` generates `.rif` files that can be viewed with `gnuplot-rif` or `sim2chro`; cf <http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/reactive-toolbox/> -<a id="org065842a"></a> +<a id="org787969e"></a> ## The `sasa` CLI @@ -411,11 +411,11 @@ sasa --more Display the version ocaml version sasa was compiled with and exit. -<a id="org8cabb77"></a> +<a id="org578208a"></a> # Interactive mode -<a id="orga7c8b81"></a> If you want to perform step-by-step simulations, you can use the `-custd` option. But if you want to perform step-by-step simulations without the burden of playing the role of the daemon, you can launch `sasa` under the control of [rdbg](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/rdbg/). +<a id="org1e0f245"></a> If you want to perform step-by-step simulations, you can use the `-custd` option. But if you want to perform step-by-step simulations without the burden of playing the role of the daemon, you can launch `sasa` under the control of [rdbg](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/rdbg/). Another advantage of [rdbg](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/rdbg/) is its ability to display a graphical view of the current configuration during the simulation, to move step by step, or round by round, forward or backwards. @@ -424,7 +424,7 @@ cf <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/rdbg-sasa/> Before reading this section, please read at least the [Basic usage Section if the rdbg documentation](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/rdbg/README.html#outline-container-sec-3). -<a id="org940a545"></a> +<a id="org7d9fb4e"></a> ## Example: use `rdbg` from the `test/alea-coloring/` directory @@ -467,7 +467,7 @@ rdbg [q] quit -<a id="orga8bb93c"></a> +<a id="org646483c"></a> ## The examples of test directory @@ -478,7 +478,7 @@ The [test](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/t - `test/*/my-rdbg-tuning.ml`: includes `test/my-rdbg-tuning.ml` and defines commands specific to the example of the directory. Indeed, `rdbg`, once launched, first tries to read the content of the file name `my-rdbg-tuning.ml` (it it exists). -<a id="orgc1677b8"></a> +<a id="org4538175"></a> ## Running interactive sessions with `rdbg` @@ -495,7 +495,7 @@ The [test](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/t All those commands are defined in (the common) [test/my-rdbg-tuning.ml](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test/my-rdbg-tuning.ml) that is included in (locals) `test/*/my-rdbg-tuning.ml` that are included in (generated) `test/*/rdbg-session.ml` files. `my-rdbg-tuning.ml` contains straigthforward `ocaml` code that defines various `rdbg` shortcuts to ease the simulation of `sasa` systems. Feel free to tailor those command to yours needs by modyfying the local `my-rdbg-tuning.ml`! -<a id="org45312ba"></a> +<a id="org8bb16ba"></a> ## Getting `rdbg` on-line help @@ -591,7 +591,7 @@ Here are 2 useful entry-points to rdbg on-line help: (rdbg) -<a id="orgc050bc9"></a> +<a id="org69bf58c"></a> ## A `rdbg` `sasa` GUI @@ -605,7 +605,7 @@ opam install -y rdbgui4ocaml To use it: <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/rdbgui4sasa/> -<a id="org68ddece"></a> +<a id="org5781218"></a> ## Useful Modules @@ -632,14 +632,14 @@ Some modules, used by the sasa core engine, can be useful from `rdbg`. </div> -<a id="org870ae55"></a> +<a id="orgccc7e98"></a> # Install -<a id="org5572cc7"></a> <a id="org29e3b1b"></a> +<a id="org366a559"></a> <a id="org4c1c8c8"></a> -<a id="org6a2be30"></a> +<a id="orgf88e099"></a> ## TL;DR @@ -693,7 +693,7 @@ git clone https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa.gi ``` -<a id="orgc778fb2"></a> +<a id="orge18cbad"></a> ## Not strictly mandatory, but useful, third-party software @@ -736,7 +736,7 @@ sudo apt install -y wish Otherwise: <http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v4/distrib/index.html> -<a id="orge389556"></a> +<a id="orgb522bdb"></a> ## Install `sasa` via opam (version >= 2.\*) @@ -770,7 +770,7 @@ opam upgrade ``` -<a id="org375da8e"></a> +<a id="orgb3bb93b"></a> ## Install `sasa` via `git` @@ -814,14 +814,14 @@ make test One can also mimic the content of the `test` job in the project [.gitlab-ci.yml Gitlab CI script](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/.gitlab-ci.yml). -<a id="org8634d7f"></a> +<a id="orgbdfd166"></a> ## Use `sasa` via docker cf the Docker Install section of the [Synchrone Reactive Tool Box](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#docker). This docker image contains all the tools mentioned in this section (`sasa`, `lustre`, `opam`, `ocaml`, emacs, graphviz, etc.). -<a id="orgfca4398"></a> +<a id="org8a3c22b"></a> ## Use `sasa` via a Virtual Machine @@ -831,7 +831,7 @@ cf the Docker Install section of the [Synchrone Reactive Tool Box](http://www-ve - passwd:sasa -<a id="org1965004"></a> +<a id="orgcb02048"></a> # Screencasts @@ -841,13 +841,13 @@ cf the Docker Install section of the [Synchrone Reactive Tool Box](http://www-ve - Create a xubuntu 20.4 VM: [2 minutes video (20 min of real time)](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/screencasts/vbox-x2.avi) - Clone that VM and install sasa via opam [2:39 minutes video (37 min of real time)](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/screencasts/sasa-install-x2.avi) - Sasa demos (done on the VM build above, which is [available here](https://cloud.univ-grenoble-alpes.fr/index.php/s/ekAbtizPFNYPSaf): - - demo 1: write and execute an algo (Dijkstra ring) [[<http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/screencasts/first-demo.avi>][first-demo.avi] + - demo 1: write and execute an algo (Dijkstra ring) [first-demo.avi](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/screencasts/first-demo.avi) - demo 2: re-define what a legitimate configuration is (Dijkstra ring) [legitimate-demo.avi](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/screencasts/legitimate-demo.avi) cf <http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/screencasts/> -<a id="orgb10647d"></a> +<a id="org020d69e"></a> # More @@ -856,12 +856,12 @@ cf <http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/screencasts/> - Tutorials: <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt//tags/sasa/> -<a id="org45ee1b0"></a> +<a id="org4be25b7"></a> # FAQ -<a id="orgcdd1fda"></a> +<a id="orgb84f441"></a> ## Is there a FAQ? @@ -870,7 +870,7 @@ Yes. Beside, some tutorials are also available here: <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/tags/sasa/> -<a id="org1a4026e"></a> +<a id="orgc8ed449"></a> ## I have a compilation error that I don't understand @@ -880,8 +880,8 @@ Beside, some tutorials are also available here: <https://verimag.gricad-pages.un - If the message is totally useless, please feel free to add an issue here <https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/issues> -<a id="org59935ae"></a> +<a id="org0f6d260"></a> ## I have the error `Invalid_argument("compare: functional value")` -Most probably you a try to compare 2 `'s Algo.neighbor`. It's an abstract type, hence you cannot compare them, i.e., you cannot use `Stdlib.compare`, nor its twins (`<>`, `>`, `<`, etc.), nor functions that use them (`min`, `max`, `List.sort`, etc.). You should compare their `pid` instead (if the network is not anonymous). +Most probably you a try to compare 2 `'s Algo.neighbor`. It's an abstract type, hence you cannot compare them, i.e., you cannot use `Stdlib.compare`, nor its twins (`<>`, `>`, `<`, etc.), nor functions that use them (`min`, `max`, `List.sort`, etc.). You should compare their `pid` instead (if the network is not anonymous). \ No newline at end of file diff --git a/guides/users/README.org b/guides/users/README.org index b679f2db..8af41139 100644 --- a/guides/users/README.org +++ b/guides/users/README.org @@ -51,17 +51,17 @@ make clean cd test cp -rf skeleton my_algo # copy a simple example cd my_algo # one may want to edit "p.ml" and "ring.dot" -make ring.cmxs # compile anything that needs to be compiled -sasa ring.dot -l 4 # run a batch simulation for 4 steps +make ring7.cmxs # compile anything that needs to be compiled +sasa ring7.dot -l 4 # run a batch simulation for 4 steps #+END_SRC #+RESULTS[13cc60a20b534115483ffd7ae0f22f6bcc52a8dd]: #+begin_example -sasa -reg ring.dot -ocamlfind ocamlopt -package algo -shared state.ml p.ml config.ml ring.ml -o ring.cmxs +sasa -reg ring7.dot +ocamlfind ocamlopt -package algo -shared state.ml p.ml config.ml ring7.ml -o ring7.cmxs # Automatically generated by /home/jahier/.opam/4.10.0/bin/sasa version "4.3.5" ("a6897fa") # on crevetete the 4/11/2020 at 8:28:38 -#sasa ring.dot -l 4 +#sasa ring7.dot -l 4 #seed 194528744 #inputs diff --git a/lib/algo/algo.ml b/lib/algo/algo.ml index be7eae4d..f6e7f669 100644 --- a/lib/algo/algo.ml +++ b/lib/algo/algo.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 09/04/2021 (at 10:04) by Erwan Jahier> *) +(* Time-stamp: <modified the 17/09/2021 (at 12:09) by Erwan Jahier> *) open Sasacore (* Process programmer API *) @@ -46,6 +46,8 @@ type 's fault_fun = int -> string -> 's -> 's type 's legitimate_fun = pid list -> (pid -> 's * ('s neighbor * pid) list) -> bool type 's potential_fun = pid list -> (pid -> 's * ('s neighbor * pid) list) -> float +type num = F of float | I of int | B of bool +type 's state_to_nums_fun = ('s -> num list) * (num list -> 's -> 's) type 's algo_to_register = { algo_id: string; @@ -59,9 +61,11 @@ type 's to_register = { state_of_string: (string -> 's) option; 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 + 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 *) + } let (to_reg_neigbor : 's Register.neighbor -> 's neighbor) = @@ -103,6 +107,27 @@ let (to_reg_legitimate_fun : in lf pidl n_from_pid +let (to_reg_s2n: ('s -> num list) -> 's -> Register.num list) = + fun f s -> + List.map + (function + | F x -> Register.F x + | I x -> Register.I x + | B x -> Register.B x + ) + (f s) + +let (to_reg_n2s: (num list -> 's -> 's) -> Register.num list -> 's -> 's) = + fun f nl s -> + f (List.map + (function + | Register.F x -> (F x) + | Register.I x -> (I x) + | Register.B x -> (B x) + ) + nl + ) + s let (register1 : 's algo_to_register -> unit) = fun s -> @@ -134,6 +159,10 @@ let (register : 's to_register -> unit) = | None -> () | Some ff -> Register.reg_fault (Some ff) ); + (match s.for_init_search with + | None -> () + | Some(s2n,n2s) -> Register.reg_for_init_search (Some (to_reg_s2n s2n, to_reg_n2s n2s)) + ); () let card = Register.card diff --git a/lib/algo/algo.mli b/lib/algo/algo.mli index d1ecc103..b7f1109d 100644 --- a/lib/algo/algo.mli +++ b/lib/algo/algo.mli @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 14/09/2021 (at 16:12) by Erwan Jahier> *) +(* Time-stamp: <modified the 17/09/2021 (at 12:08) by Erwan Jahier> *) (** {1 The Algorithm programming Interface} A SASA process is an instance of an algorithm defined via this @@ -160,9 +160,13 @@ 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 state } + + 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. +*) type num = F of float | I of int | B of bool -type 's state_of_nums : num list -> 's +type 's state_to_nums_fun = ('s -> num list) * (num list -> 's -> 's) (** {2 Code Registration} @@ -182,10 +186,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 *); potential_function: 's potential_fun option (** Mandatory with Evil daemons *); - fault_function : 's fault_fun option (** called at legitimate configuration *) - - state_of_nums : 's state_of_nums option; + for_init_search : '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/diameter.ml b/lib/sasacore/diameter.ml index 15408355..27a85cf4 100644 --- a/lib/sasacore/diameter.ml +++ b/lib/sasacore/diameter.ml @@ -49,12 +49,12 @@ let (max_mat: int array array -> int) = fun mat -> let n = (Array.length mat) and m = (Array.length mat.(0)) in let maxi = ref (-1) in - for i=0 to (n - 1) do - for j=0 to (m - 1) do - maxi := max !maxi mat.(i).(j) - done; - done; - !maxi + for i=0 to (n - 1) do + for j=0 to (m - 1) do + maxi := max !maxi mat.(i).(j) + done; + done; + !maxi (* takes a graph t in argument and returns the diameter *) let (get: Topology.t -> int ) = diff --git a/lib/sasacore/dune b/lib/sasacore/dune index c3e52b8e..460dd67f 100644 --- a/lib/sasacore/dune +++ b/lib/sasacore/dune @@ -1,9 +1,9 @@ -;; Time-stamp: <modified the 09/06/2021 (at 15:07) by Erwan Jahier> +;; Time-stamp: <modified the 05/10/2021 (at 09:59) by Erwan Jahier> (library (name sasacore) (public_name sasacore) - (libraries dynlink ocamlgraph lutils) + (libraries dynlink ocamlgraph lutils psq functory) ; (flags -noassert) ;; ; (wrapped false) diff --git a/lib/sasacore/genRegister.ml b/lib/sasacore/genRegister.ml index e74fddb5..fc01d118 100644 --- a/lib/sasacore/genRegister.ml +++ b/lib/sasacore/genRegister.ml @@ -52,10 +52,12 @@ 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; } " (String.concat ";" l) - state_module state_module state_module state_module config_module config_module config_module; + state_module state_module state_module state_module config_module config_module + config_module config_module; flush oc; close_out oc; Printf.eprintf " [sasa] The file %s has been generated\n" register_file; @@ -88,6 +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 *) "; flush oc; close_out oc; diff --git a/lib/sasacore/register.ml b/lib/sasacore/register.ml index 63e2c955..65d56e28 100644 --- a/lib/sasacore/register.ml +++ b/lib/sasacore/register.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 27/08/2021 (at 14:21) by Erwan Jahier> *) +(* Time-stamp: <modified the 17/09/2021 (at 12:09) by Erwan Jahier> *) type 's neighbor = { state: 's ; @@ -18,6 +18,9 @@ type 's potential_fun = pid list -> (pid -> 's * ('s neighbor * pid) list) -> fl type 's fault_fun = int -> string -> 's -> 's type 's legitimate_fun = string list -> (string -> 's * ('s neighbor * pid) list) -> bool +type num = F of float | I of int | B of bool +type 's state_to_nums_fun = ('s -> num list) * (num list -> 's -> 's) + type 's internal_tables = { init_state: (string, Obj.t) Hashtbl.t; enable : (string, Obj.t) Hashtbl.t; @@ -29,6 +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 actions:action list; mutable topology : Topology.t option; mutable card : int option; @@ -62,6 +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); actions = []; topology = None; card = None; @@ -135,6 +140,13 @@ 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 (get_for_init_search : unit -> 's state_to_nums_fun option) = fun () -> + Obj.obj tbls.for_init_search + 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) diff --git a/lib/sasacore/register.mli b/lib/sasacore/register.mli index 2076c3b0..76c02dbd 100644 --- a/lib/sasacore/register.mli +++ b/lib/sasacore/register.mli @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 08/04/2021 (at 21:55) by Erwan Jahier> *) +(* Time-stamp: <modified the 17/09/2021 (at 12:09) by Erwan Jahier> *) (** This module duplicates and extends the Algo module with get_* functions. @@ -23,6 +23,10 @@ type 's step_fun = 's neighbor list -> 's -> action -> 's type 's fault_fun = int -> string -> 's -> 's type pid = string + +type num = F of float | I of int | B of bool +type 's state_to_nums_fun = ('s -> num list) * (num list -> 's -> 's) + type 's potential_fun = pid list -> (pid -> 's * ('s neighbor * pid) list) -> float type 's legitimate_fun = string list -> (string -> 's * ('s neighbor * pid) list) -> bool @@ -30,6 +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_legitimate : 's legitimate_fun option -> unit val reg_fault : 's fault_fun option -> unit val reg_actions : action list -> unit @@ -70,6 +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_legitimate : unit -> 's legitimate_fun option val get_fault : unit -> 's fault_fun option val get_value_to_string : unit -> 's -> string @@ -83,4 +89,3 @@ type node_id = string (* cf topology.mli *) val set_graph_attribute : string -> string -> unit val graph_attribute_list: unit -> (string * string) list - diff --git a/lib/sasacore/sasArg.ml b/lib/sasacore/sasArg.ml index 2019e823..b11adaad 100644 --- a/lib/sasacore/sasArg.ml +++ b/lib/sasacore/sasArg.ml @@ -1,9 +1,10 @@ -(* Time-stamp: <modified the 17/06/2021 (at 11:10) by Erwan Jahier> *) +(* Time-stamp: <modified the 05/10/2021 (at 10:15) by Erwan Jahier> *) type t = { mutable topo: string; mutable length: int; + mutable cores_nb: int; mutable verbose: int; mutable daemon: DaemonType.t; mutable rif: bool; @@ -15,6 +16,7 @@ type t = { mutable dummy_input: bool; mutable output_algos: bool; mutable gen_register: bool; + mutable init_search_max_trials: int option; mutable _args : (string * Arg.spec * string) list; mutable _user_man : (string * string list) list; @@ -35,6 +37,7 @@ let (make_args : unit -> t) = { topo = ""; length = 10000; + cores_nb = 1; verbose = 0; daemon = DaemonType.Distributed; rif = false; @@ -46,6 +49,7 @@ let (make_args : unit -> t) = dummy_input = false; output_algos = false; gen_register = false; + init_search_max_trials = None; _args = []; _user_man = []; _hidden_man = []; @@ -131,6 +135,15 @@ let (mkoptab : string array -> t -> unit) = (* (Arg.Int (fun i -> args.daemon <- DaemonType.Bad i)) *) (* ["Use a daemon that tries to maximize the potential function, "; *) (* "considering sub-graphs of a given maximal size"]; *) + mkopt args ["--init-search";"-is"] + (Arg.Int(fun i -> args.init_search_max_trials <- Some i)) + ["Use local search algorithms to find an initial configuration that pessimize "; + "the step number. The argument is the maximum number of trials to do the search. "; + "Require the state_to_nums Algo.to_register field to be defined."] ~arg:" <int>"; + + mkopt args ["--cores-nb";"-cn"] + (Arg.Int(fun i -> args.cores_nb <- i)) + ["Number of cores to use during the simulation (default is 1)"]; mkopt args ~hide:true ["--rif";"-rif"] (Arg.Unit(fun () -> args.rif <- true)) @@ -141,7 +154,7 @@ let (mkoptab : string array -> t -> unit) = ["Do not generate any data file"]; mkopt args ["--seed";"-seed"] - (Arg.Int(fun i -> Seed.set i)) + (Arg.Int(fun i -> Seed.set i)) ~arg:" <int>" ["Set the pseudo-random generator seed of build-in daemons (wins over --replay)"]; mkopt args ["--replay";"-replay"] diff --git a/lib/sasacore/sasArg.mli b/lib/sasacore/sasArg.mli index 8dd6466b..d97784ef 100644 --- a/lib/sasacore/sasArg.mli +++ b/lib/sasacore/sasArg.mli @@ -1,8 +1,9 @@ -(* Time-stamp: <modified the 17/06/2021 (at 11:09) by Erwan Jahier> *) +(* Time-stamp: <modified the 05/10/2021 (at 10:15) by Erwan Jahier> *) type t = { mutable topo: string; mutable length: int; + mutable cores_nb: int; mutable verbose: int; mutable daemon: DaemonType.t; mutable rif: bool; @@ -14,7 +15,8 @@ type t = { mutable dummy_input: bool; mutable output_algos: bool; mutable gen_register: bool; - + mutable init_search_max_trials: int option; + mutable _args : (string * Arg.spec * string) list; mutable _user_man : (string * string list) list; mutable _hidden_man: (string * string list) list; diff --git a/lib/sasacore/simuState.ml b/lib/sasacore/simuState.ml index 0f49939f..486fcebd 100644 --- a/lib/sasacore/simuState.ml +++ b/lib/sasacore/simuState.ml @@ -1,6 +1,7 @@ -(* Time-stamp: <modified the 27/08/2021 (at 15:10) by Erwan Jahier> *) +(* Time-stamp: <modified the 28/09/2021 (at 14:08) by Erwan Jahier> *) open Register +open Topology let (update_env_with_init : 'v Env.t -> 'v Process.t list -> 'v Env.t) = fun e pl -> @@ -247,6 +248,7 @@ let (make : bool -> string array -> 'v t) = let algo_id = Filename.chop_suffix n.Topology.file ".ml" in let value_of_string_opt = Register.get_value_of_string () in if value_of_string_opt = None || n.Topology.init = "" then + (* Use the init functions if initial values are not in the dot *) Register.get_init_state algo_id (List.length (g.succ n.id)) n.id else match value_of_string_opt with @@ -338,3 +340,53 @@ let (make : bool -> string array -> 'v t) = Printf.eprintf " [sasa] Error (Sasacore.make): %s\n%!" (Printexc.to_string e); flush_all(); exit 2 + + + +let (to_dot : 'v t -> string) = + fun ss -> + let dot_file = ss.sasarg.topo in + let g = Topology.read dot_file in + let nodes_decl = + String.concat "\n" + (List.map + (fun node -> + Printf.sprintf " %s [algo=\"%s\" init=\"%s\"]" node.id node.file + (Register.to_string (Env.get ss.config node.id)) + ) + g.nodes) + in + let trans = + if g.directed then + List.flatten + (List.map + (fun n -> + List.map + (fun t -> Printf.sprintf "%s -> %s" t n.id) + (g.succ n.id) + ) + g.nodes + ) + else + List.flatten + (List.map + (fun n -> + let l = g.succ n.id in + List.map (fun t -> + if n.id < t then + Printf.sprintf "%s -- %s" n.id t + else + Printf.sprintf "%s -- %s" t n.id + ) + l + ) + g.nodes + ) + in + let trans = List.sort_uniq compare trans in + let trans_str = String.concat "\n" trans in + let attributes = String.concat " " (List.map (fun (n,v) -> n^"="^v) g.attributes) in + Printf.sprintf + "%sgraph %s {\n graph [%s]\n\n%s\n\n%s\n}\n" + (if g.directed then "di" else "") "g" + attributes nodes_decl trans_str; diff --git a/lib/sasacore/simuState.mli b/lib/sasacore/simuState.mli index 7946f3be..d25b26dd 100644 --- a/lib/sasacore/simuState.mli +++ b/lib/sasacore/simuState.mli @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 17/06/2021 (at 15:29) by Erwan Jahier> *) +(* Time-stamp: <modified the 19/09/2021 (at 23:06) by Erwan Jahier> *) (** The module is used by - the main sasa simulation loop (in ../../src/sasaMain.ml) @@ -33,3 +33,5 @@ val neigbors_of_pid : 'v t -> string -> 'v * ('v Register.neighbor * string) lis (* For SasaRun *) val get_inputs_rif_decl : SasArg.t -> 'v Process.t list -> (string * string) list val get_outputs_rif_decl: SasArg.t -> 'v Process.t list -> (string * string) list + +val to_dot : 'v t -> string diff --git a/lib/sasacore/topology.mli b/lib/sasacore/topology.mli index cb31a7c0..4c711ae0 100644 --- a/lib/sasacore/topology.mli +++ b/lib/sasacore/topology.mli @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 27/08/2021 (at 15:35) by Erwan Jahier> *) +(* Time-stamp: <modified the 20/09/2021 (at 09:45) by Erwan Jahier> *) (** {1 Topology: internal representation of Graphs } *) @@ -41,6 +41,6 @@ val get_degree: t -> int * int (** [reply g p p_neighbor] returns the channel number that let [p_neighbor] access to the content of [p], if [p] is a neighbor of - [p_neighbor]. Returns -1 if [p] is not a neighbor of [p_neigbor], + [p_neighbor]. Returns -1 if [p] is not a neighbor of [p_neighbor], which can happen in directed graphs. *) val reply: t -> string -> string -> int diff --git a/lib/sasacore/worstInit.ml b/lib/sasacore/worstInit.ml index 08c08330..8704d3ba 100644 --- a/lib/sasacore/worstInit.ml +++ b/lib/sasacore/worstInit.ml @@ -1,21 +1,21 @@ -(* Time-stamp: <modified the 01/10/2021 (at 11:58) by Erwan Jahier> *) +(* Time-stamp: <modified the 05/10/2021 (at 16:28) by Erwan Jahier> *) open Register -type 's node = { st : 's ; d : int } +type 's node = { st : 's ; d : int ; cost : int ; cpt : int } type point = num Array.t let debug = false -type succ_heuristic = (* Various heuristic to choose the neighbor *) - | OneDim (* only move one value at a time *) - | RanDim (* move a value or not at random *) - | AllDim (* move all values *) + (* type succ_heuristic = (* Various heuristic to choose the neighbor *) *) + (* | OneDim (* only move one value at a time *) *) + (* | RanDim (* move a value or not at random *) *) +(* | AllDim (* move all values *) *) -let succ_heuristic_nb = 3 -let int_of_succ_heuristic = function OneDim -> 0 | RanDim -> 1 | AllDim -> 2 -let succ_heuristic_of_int = function 0 -> OneDim | 1 -> RanDim | 2 -> AllDim - | _ -> assert false +(* let succ_heuristic_nb = 3 *) +(* let int_of_succ_heuristic = function OneDim -> 0 | RanDim -> 1 | AllDim -> 2 *) + (* let succ_heuristic_of_int = function 0 -> OneDim | 1 -> RanDim | 2 -> AllDim *) +(* | _ -> assert false *) let mutate_num = function | F f -> F(f+.(Random.float 2.0) -. 1.0) @@ -23,66 +23,37 @@ let mutate_num = function | B b -> B (not b) -let (one_dim_succ : point -> point) = fun p -> +let one_dim_succ n = + let p = Array.copy n in let j = Random.int (Array.length p) in p.(j) <- mutate_num p.(j); p -let ran_dim_succ p = + +let ran_dim_succ n = + let p = Array.copy n in for j=0 to Array.length p - 1 do if Random.bool () then p.(j) <- mutate_num p.(j) done; p -let all_dim_succ p = + +let all_dim_succ n = + let p = Array.copy n in for j=0 to Array.length p - 1 do p.(j) <- mutate_num p.(j) done; p -let succ_heuristic_to_succ = function - OneDim -> one_dim_succ | RanDim -> ran_dim_succ | AllDim -> all_dim_succ - -(* each succ_heuristic has a weight between 1 and 100, initialized at 50 *) -let hw = Array.make succ_heuristic_nb 50 -let decr_w log i = - Printf.fprintf log "Decrementing heuristic %d\n%!" i; - try hw.(i) <- max 1 (hw.(i)-1) with _ -> assert false -let incr_w log i = - Printf.fprintf log "Incrementing heuristic %d\n%!" i; - try hw.(i) <- min 100 (hw.(i)+1) with _ -> assert false -let tf = float_of_int - -let (choose_succ_heuristic : unit -> succ_heuristic) = - fun () -> (* Choose one succ_heuristic with a probability defined by their weights in hw *) - let sum = tf(Array.fold_left (+) 0 hw) in - let r = ref (sum *. Random.float 1.0) in - let ri = ref (-1) in - assert(sum>0.0); - assert(!r>0.0); - while !r>0.0 do - incr ri; - assert (!ri<Array.length hw); - r := !r -. (tf hw.(!ri)); - done; - if debug then Printf.printf "choose heuristics %d, %!" !ri; - succ_heuristic_of_int !ri - -let h = ref (choose_succ_heuristic ()) -let choose_succ s = - let s_st = Array.copy s.st in - let ns = (succ_heuristic_to_succ !h) s_st in - (* update heuristic weights depending on their success at the previous step *) - (*if ns = pre_s then decr_w else incr_w) (int_of_succ_heuristic !h*) - h := choose_succ_heuristic (); - { st = ns ; d = s.d+1 } - - -let print_stat log = - Printf.fprintf log " ===> heuristic array: [|%s|]\n%!" - (Array.fold_left (fun acc d -> Printf.sprintf "%s,%d" acc d) "" hw); - - +(* let tf = float_of_int *) + +let (choose : int -> point -> (point -> point) -> point list) = + fun n p heuristic -> + (*choose n successors of p using heuristic *) + assert (n>=0); + let rec f acc i = if i <= 0 then acc else f ((heuristic p)::acc) (i-1) in + f [] n + (*****************************************************************************) (* XXX a ranger ailleurs !!! *) @@ -90,7 +61,6 @@ open Process 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 @@ -157,7 +127,18 @@ let (ss_to_point : 'v SimuState.t -> point) = open LocalSearch +module NumArrayNode = struct + type t = num array node + let compare n1 n2 = compare n2.cost n1.cost +end + +let _ = Functory.Cores.set_number_of_cores 4 + +(* open Functory.Sequential *) +open Functory.Cores +module Q = Psq.Make (Int) (NumArrayNode) + (* First Choice Hill Climbing: a successor is chosen at random (using some heuristics), and became the current state if its cost is better. @@ -167,53 +148,71 @@ open LocalSearch never null. *) let (fchc : out_channel -> ('v SimuState.t -> int) -> 'v SimuState.t -> int -> 'v SimuState.t) = fun log run ss_init dmax -> + let cpt = ref 0 in let cost p = run (point_to_ss p ss_init) in - + let pinit = ss_to_point ss_init in let g = { - init = ({ st = ss_to_point ss_init ; d = 0 }, None, ()); - succ = (fun n -> [choose_succ n]); - stop = (fun _ _n -> false); + init = ({ st = pinit ; d = 0 ; cost = cost pinit ; cpt = 0 }, Q.empty, ()); + succ = (fun n -> + let m = min 50 (max 1 (dmax / 10)) in + let pl = (choose m n.st one_dim_succ) @ + (choose 1 n.st ran_dim_succ) @ + (choose 1 n.st all_dim_succ) + in + Printf.fprintf log "fchc: %d+2=%d points have been drawn\n " m (List.length pl); + (* List.map (fun p -> *) + (* Functory.Cores.map ~f: (fun p -> *) + let new_cpt, res = + map_local_fold + ~f: (fun p -> cost p, p) + ~fold:(fun (cpt,nl) (c,p) -> + Printf.fprintf log "At depth %d, cost=%d\n" (n.d+1) c; + cpt+1,{ d=n.d+1; cost=c; st=p ; cpt = cpt}::nl + ) + (!cpt, []) + pl + in + cpt:=new_cpt; + res + ); + stop = (fun _ _n -> !cpt > dmax); is_goal = (fun _n -> true); - push = (fun _tv n -> Some n); - pop = (fun tv -> Some(Option.get tv, None)); + push = (fun tv n -> + Printf.fprintf log "Pushing a point of cost %d (queue size=%d)\n" (n.cost) (Q.size tv); + Q.add n.cpt n tv); + pop = (fun tv -> match Q.pop tv with None -> None | Some((i,x),t) -> + Printf.fprintf log "Poping a point of cost %d (simu #%d)\n" x.cost i; + Some(x, t)); visiting = (fun _ x -> x); visited = (fun _ _ -> false); - cut = (fun _ _ -> false); + cut = (fun pn n -> if pn.cost > n.cost then ( + Printf.fprintf log "%d: cut a point at depth %d of cost %d < %d\n%!" + !cpt n.d n.cost pn.cost; + true) + else false ); } in - let cpt = ref 0 in - let av_cost = ref 0 in - let rec run_more pcost psol more = - print_stat log; - incr cpt; - if !cpt < dmax then + let rec run_more psol more = ( match more (Some psol) with - | LocalSearch.Stopped -> assert false (* SNO *) - | LocalSearch.NoMore-> assert false (* SNO *) + | LocalSearch.Stopped + | LocalSearch.NoMore-> + Printf.printf "The worst initial configuration, which costs %d, is " psol.cost; + point_to_ss psol.st ss_init | LocalSearch.Sol (nsol, more) -> - av_cost := (!av_cost * (!cpt-1) + pcost) / !cpt; - let ncost = cost nsol.st in - Printf.fprintf log "%d > %d? " ncost pcost; - if ncost > pcost then - incr_w log (int_of_succ_heuristic !h) - else - decr_w log (int_of_succ_heuristic !h); - if ncost > pcost then ( - run_more ncost nsol more + + if nsol.cost > psol.cost then ( + Printf.printf "Hey, I've found a configuration cost %d! (simu #%d, depth %d)\n" + nsol.cost nsol.cpt nsol.d; + run_more nsol more ) else ( - run_more pcost psol more + run_more psol more ) ) - else ( - Printf.printf "The worst initial configuration, which costs %d, is " pcost; - point_to_ss psol.st ss_init - (* XXX generate a dot file using this initialisation *) - - ) + in match LocalSearch.run g None with | LocalSearch.Stopped -> assert false (* SNO *) | LocalSearch.NoMore-> assert false (* SNO *) - | LocalSearch.Sol (sol, more) -> run_more (cost sol.st) sol more + | LocalSearch.Sol (sol, more) -> run_more sol more -- GitLab