Skip to content
Snippets Groups Projects
Commit 865240d6 authored by erwan's avatar erwan
Browse files

Merge branch 'emile'

parents e2c061c1 3c576535
No related branches found
No related tags found
No related merge requests found
Pipeline #107789 failed
Showing
with 206 additions and 125 deletions
(lang dune 2.0)
(authors "Erwan Jahier")
(maintainers "Erwan Jahier")
- [TL;DR](#org9c9d503)
- [Topology](#orgff582ab)
- [Algorithms](#org5ef8bb4)
- [Examples](#org2fa119a)
- [Batch mode](#orga200c38)
- [Running batch simulations](#orgbcba3e2)
- [Running batch simulations with Built-in daemons](#org6f81e55)
- [Running batch simulations with manual (a.k.a. custom) daemons](#org4c63674)
- [Running batch simulations with `lurette`](#orgd2bc290)
- [Viewing Results](#org2b0799e)
- [The `sasa` CLI](#org3b8d4b3)
- [Interactive mode](#org02bafa4)
- [Example: use `rdbg` from the `test/alea-coloring/` directory](#orgd499f7a)
- [The examples of test directory](#org75ae70f)
- [Running interactive sessions with `rdbg`](#orge4643af)
- [Getting `rdbg` on-line help](#org30c51b6)
- [A `rdbg` `sasa` GUI](#org2b4589f)
- [Useful Modules](#orgd3bfce6)
- [Install](#orgead66ac)
- [TL;DR](#orgb390429)
- [Not strictly mandatory, but useful, third-party software](#orgb4cc09a)
- [Install `sasa` via opam (version >= 2.\*)](#org8290be6)
- [Install `sasa` via `git`](#orgb63c57e)
- [Use `sasa` via docker](#org13c72f7)
- [Use `sasa` via a Virtual Machine](#orgaf70033)
- [Screencasts](#org52c7a2d)
- [More](#org4d55fa9)
- [FAQ](#orge446f5a)
- [Is there a FAQ?](#org1788b9d)
- [I have a compilation error that I don't understand](#org2ea9013)
- [I have the error `Invalid_argument("compare: functional value")`](#orga4555a7)
<a id="org9c9d503"></a>
- [TL;DR](#orgc82f76b)
- [Topology](#orgf1bf668)
- [Algorithms](#org675fb02)
- [Examples](#orgd0a590c)
- [Batch mode](#org7bb68a4)
- [Running batch simulations](#org4b6393c)
- [Running batch simulations with Built-in daemons](#orgfe448db)
- [Running batch simulations with manual (a.k.a. custom) daemons](#orgadfdca2)
- [Running batch simulations with `lurette`](#org347b172)
- [Viewing Results](#orgba27fbc)
- [The `sasa` CLI](#orgae5deb1)
- [Interactive mode](#orga63cb12)
- [Example: use `rdbg` from the `test/alea-coloring/` directory](#org913b4b7)
- [The examples of test directory](#orgeb18210)
- [Running interactive sessions with `rdbg`](#org3a65716)
- [Getting `rdbg` on-line help](#org48fa50d)
- [A `rdbg` `sasa` GUI](#orgad6bf70)
- [Useful Modules](#org9d9173a)
- [Install](#org282e5ca)
- [TL;DR](#org45124dd)
- [Not strictly mandatory, but useful, third-party software](#org8d183f0)
- [Install `sasa` via opam (version >= 2.\*)](#org2504ba4)
- [Install `sasa` via `git`](#orgc5e8c3e)
- [Use `sasa` via docker](#org03256dd)
- [Use `sasa` via a Virtual Machine](#org9f93471)
- [Screencasts](#org57f191d)
- [More](#orgbc6bd0b)
- [FAQ](#org046be58)
- [Is there a FAQ?](#org99b42b5)
- [I have a compilation error that I don't understand](#orgbd579cf)
- [I have the error `Invalid_argument("compare: functional value")`](#org1d85558)
<a id="orgc82f76b"></a>
# TL;DR
<a id="orgab88045"></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="orgc076fc7"></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:
......@@ -61,11 +61,11 @@ sasa ring.dot -l 4 # run a batch simulation for 4 steps
[![img](poster.png)](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/poster.pdf)
<a id="orgff582ab"></a>
<a id="orgf1bf668"></a>
# Topology
<a id="orgbd10083"></a> <a id="orgf20065d"></a> The topology is given via `.dot` files, that should
<a id="orga98bc12"></a> <a id="orge45f409"></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](#org6e26471) 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](#orgd3c4718) to generate such kinds of `dot` graphs: <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/sasa-gg/>
<a id="org5ef8bb4"></a>
<a id="org675fb02"></a>
# Algorithms
<a id="orgd7787ed"></a>
<a id="org7a9490c"></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)
......@@ -140,7 +140,7 @@ The following has been generated from [algo.mli](https://gricad-gitlab.univ-gren
</iframe>
<a id="org2fa119a"></a>
<a id="orgd0a590c"></a>
# Examples
......@@ -180,14 +180,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="orga200c38"></a>
<a id="org7bb68a4"></a>
# Batch mode
![img](./sasabatch.svg)
<a id="orgbcba3e2"></a>
<a id="org4b6393c"></a>
## Running batch simulations
......@@ -229,35 +229,38 @@ All the CLI commands above can be run automatically using a `make` rule containe
```
make: 'ring.cmxs' is up to date.
# Automatically generated by /home/jahier/.opam/4.13.1/bin/sasa version "v4.5.9" ("c9bee55")
# on crevetete the 31/5/2022 at 14:17:11
# Automatically generated by /home/jahier/.opam/4.14.0/bin/sasa version "v4.7.0" ("1f6fd7d")
# on crevetete the 21/7/2022 at 11:05:40
#sasa ring.dot
#seed 273810591
#seed 839491647
#inputs
#outputs "p1_c":int "p2_c":int "p3_c":int "p4_c":int "p5_c":int "p6_c":int "p7_c":int "Enab_p1_conflict":bool "Enab_p2_conflict":bool "Enab_p3_conflict":bool "Enab_p4_conflict":bool "Enab_p5_conflict":bool "Enab_p6_conflict":bool "Enab_p7_conflict":bool "p1_conflict":bool "p2_conflict":bool "p3_conflict":bool "p4_conflict":bool "p5_conflict":bool "p6_conflict":bool "p7_conflict":bool "legitimate":bool potential:real
#outputs "p1_c":int "p2_c":int "p3_c":int "p4_c":int "p5_c":int "p6_c":int "p7_c":int "Enab_p1_conflict":bool "Enab_p2_conflict":bool "Enab_p3_conflict":bool "Enab_p4_conflict":bool "Enab_p5_conflict":bool "Enab_p6_conflict":bool "Enab_p7_conflict":bool "p1_conflict":bool "p2_conflict":bool "p3_conflict":bool "p4_conflict":bool "p5_conflict":bool "p6_conflict":bool "p7_conflict":bool "legitimate":bool potential:real round:bool round_nb:int
#step 0
#outs 0 1 1 1 1 0 0 t t t t t t t f f f t t t f f 10.
#outs 1 1 0 0 1 0 0 t t t t f t t t f f f f t f f 6. f 0
#step 1
#outs 0 1 1 0 2 2 0 t t t f t t t t f f f t f f f 6.
#outs 2 1 0 0 1 2 0 f f t t f f f f f t t f f f f 2. f 1
#step 2
#outs 2 1 1 0 1 2 0 f t t f f f f f f t f f f f f 2.
#outs 2 1 2 2 1 2 0 f f t t f f f f f t t f f f f 2. t 2
#step 3
#outs 2 1 2 0 1 2 0 f f f f f f f f f t f f f f t 0.
#outs 2 1 0 0 1 2 0 f f t t f f f f f f t f f f f 2. t 3
This algo is silent after 6 moves, 3 steps, 1 round.
#step 4
#outs 2 1 0 2 1 2 0 f f f f f f f f f f f f f f t 0. t 3
This algo is silent after 7 moves, 4 steps, 3 rounds.
#quit
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="org6f81e55"></a>
<a id="orgfe448db"></a>
## Running batch simulations with Built-in daemons
......@@ -276,7 +279,7 @@ sasa -h | grep "\-daemon"
--greedy-daemon, -gd
<a id="org4c63674"></a>
<a id="orgadfdca2"></a>
## Running batch simulations with manual (a.k.a. custom) daemons
......@@ -314,7 +317,7 @@ In order to enter such input more easily, one can use (requires [the lustre V4 t
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="orgd2bc290"></a>
<a id="org347b172"></a>
## Running batch simulations with `lurette`
......@@ -339,14 +342,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="org2b0799e"></a>
<a id="orgba27fbc"></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="org3b8d4b3"></a>
<a id="orgae5deb1"></a>
## The `sasa` CLI
......@@ -433,11 +436,11 @@ More `sasa` options:
Display the version ocaml version sasa was compiled with and exit.
<a id="org02bafa4"></a>
<a id="orga63cb12"></a>
# Interactive mode
<a id="org4f9a5e3"></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="org4f2e672"></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.
......@@ -446,7 +449,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="orgd499f7a"></a>
<a id="org913b4b7"></a>
## Example: use `rdbg` from the `test/alea-coloring/` directory
......@@ -489,7 +492,7 @@ rdbg
[q] quit
<a id="org75ae70f"></a>
<a id="orgeb18210"></a>
## The examples of test directory
......@@ -500,7 +503,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="orge4643af"></a>
<a id="org3a65716"></a>
## Running interactive sessions with `rdbg`
......@@ -517,7 +520,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="org30c51b6"></a>
<a id="org48fa50d"></a>
## Getting `rdbg` on-line help
......@@ -613,7 +616,7 @@ Here are 2 useful entry-points to rdbg on-line help:
(rdbg)
<a id="org2b4589f"></a>
<a id="orgad6bf70"></a>
## A `rdbg` `sasa` GUI
......@@ -627,7 +630,7 @@ opam install -y rdbgui4ocaml
To use it: <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/rdbgui4sasa/>
<a id="orgd3bfce6"></a>
<a id="org9d9173a"></a>
## Useful Modules
......@@ -662,14 +665,14 @@ Some modules, used by the sasa core engine, can be useful from `rdbg`.
</iframe>
<a id="orgead66ac"></a>
<a id="org282e5ca"></a>
# Install
<a id="org6e26471"></a> <a id="org5302c2f"></a>
<a id="orgd3c4718"></a> <a id="org61057ff"></a>
<a id="orgb390429"></a>
<a id="org45124dd"></a>
## TL;DR
......@@ -723,7 +726,7 @@ git clone https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa.gi
```
<a id="orgb4cc09a"></a>
<a id="org8d183f0"></a>
## Not strictly mandatory, but useful, third-party software
......@@ -766,7 +769,7 @@ sudo apt install -y wish
Otherwise: <http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v4/distrib/index.html>
<a id="org8290be6"></a>
<a id="org2504ba4"></a>
## Install `sasa` via opam (version >= 2.\*)
......@@ -800,7 +803,7 @@ opam upgrade
```
<a id="orgb63c57e"></a>
<a id="orgc5e8c3e"></a>
## Install `sasa` via `git`
......@@ -828,7 +831,7 @@ And of course you need `ocaml`. And a set of tools installable via [opam](https:
Hence, once `opam` is installed, one just need to:
```sh
opam install dune ocamlgraph ocamlfind rdbg lutin lustre-v6
opam install --deps-only ./sasa.opam
```
And then:
......@@ -844,14 +847,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="org13c72f7"></a>
<a id="org03256dd"></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="orgaf70033"></a>
<a id="org9f93471"></a>
## Use `sasa` via a Virtual Machine
......@@ -861,7 +864,7 @@ cf the Docker Install section of the [Synchrone Reactive Tool Box](http://www-ve
- passwd:sasa
<a id="org52c7a2d"></a>
<a id="org57f191d"></a>
# Screencasts
......@@ -877,7 +880,7 @@ cf the Docker Install section of the [Synchrone Reactive Tool Box](http://www-ve
cf <http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/screencasts/>
<a id="org4d55fa9"></a>
<a id="orgbc6bd0b"></a>
# More
......@@ -886,12 +889,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="orge446f5a"></a>
<a id="org046be58"></a>
# FAQ
<a id="org1788b9d"></a>
<a id="org99b42b5"></a>
## Is there a FAQ?
......@@ -900,7 +903,7 @@ Yes.
Beside, some tutorials are also available here: <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/tags/sasa/>
<a id="org2ea9013"></a>
<a id="orgbd579cf"></a>
## I have a compilation error that I don't understand
......@@ -910,7 +913,7 @@ 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="orga4555a7"></a>
<a id="org1d85558"></a>
## I have the error `Invalid_argument("compare: functional value")`
......
......@@ -932,7 +932,7 @@ And a set of tools installable via [[https://opam.ocaml.org/][opam]]
Hence, once =opam= is installed, one just need to:
#+BEGIN_SRC sh :eval no
opam install dune ocamlgraph ocamlfind rdbg lutin lustre-v6
opam install --deps-only ./sasa.opam
#+END_SRC
And then:
......
......@@ -66,8 +66,7 @@ let (f: Topology.t -> 'v Process.t list -> string) =
let input_enab = ";\n "^(String.concat "," enabl) ^ ":bool" in
let input_decl = input_state^input_enab^input_trig^ ";round:bool; round_nb:int" in
let array_decl =
Printf.sprintf "\tActi:bool^an^pn;\n\tEnab:bool^an^pn;\n\tConfig:%s^%d;\n"
(fst (List.hd vars)) vars_nb
Printf.sprintf "\tActi:bool^an^pn;\n\tEnab:bool^an^pn;\n\tConfig:state^card;\n"
in
let acti_name p a = Printf.sprintf "%s_%s" p.pid (StringOf.action a) in
let enab_name p a = Printf.sprintf "Enab_%s_%s" p.pid (StringOf.action a) in
......@@ -84,7 +83,22 @@ let (f: Topology.t -> 'v Process.t list -> string) =
"["^(String.concat "," (List.map (enab_name p) p.actions))^"]") pl))
in
let array_def_config =
Printf.sprintf "\tConfig = [%s];\n" (String.concat "," (List.map fst vars))
if vars_nb <> n then
let struct_nb_var = vars_nb/n in
let rec struct_string vars_list count =
match vars_list with
| []->""
| e::[]->(Printf.sprintf "%s) " e)
| e::tail-> (if (count mod struct_nb_var) = 0 then
(Printf.sprintf "to_state(%s, " e ) ^ (struct_string tail (count-1))
else if (count mod struct_nb_var) = 1 then
(Printf.sprintf "%s), " e) ^ (struct_string tail (count-1))
else
(Printf.sprintf "%s, " e) ^ (struct_string tail (count-1))
) in
Printf.sprintf "\tConfig = [%s];\n" (struct_string (List.map fst vars) vars_nb)
else
Printf.sprintf "\tConfig = [%s];\n" (String.concat "," (List.map fst vars))
in
let algo = Filename.basename (Sys.getcwd()) in
let algo = StringOf.action algo in
......
......@@ -26,7 +26,8 @@ depends: [
"rdbg" { >= "1.194" }
"lustre-v6"
"lutin"
]
build: ["make" "build"]
"kind2" { < "1.6" }
]
build: [make "build"]
install: ["dune" "install"]
post-messages: ["The last version can be obtained via (opam repo add) http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/opam-repository/ "]
include "../lustre/oracle_utils.lus"
type state = int;
const k = pn * pn + 1;
-- The absolute value of the difference modulo k is <= 1
......
include "../lustre/oracle_utils.lus"
type state = { par:int; d:int };
function to_state( par:int; d:int)
returns(res : state);
let
res = state {par=par; d=d};
tel;
node bfs_spanning_tree_oracle<<const an:int; const pn:int>>
(legitimate: bool; Enab, Acti: bool^an^pn; config:int^(2*pn);round:bool; round_nb:int)
(legitimate: bool; Enab, Acti: bool^an^pn; config:state^pn;round:bool; round_nb:int)
returns (ok:bool);
var
CD_disable:bool;
......
# Automatically generated by /home/jahier/.opam/4.14.0/bin/sasa version "v4.6.0" ("73ebb5e")
# on crevetete the 23/6/2022 at 14:37:03
# Automatically generated by /home/jahier/.opam/4.14.0/bin/sasa version "v4.7.0" ("1f6fd7d")
# on crevetete the 25/7/2022 at 17:12:38
#sasa fig52_kcl.dot -seed 42
#seed 42
#inputs
#outputs "Root_alpha":int "p2_alpha":int "p3_alpha":int "p4_alpha":int "p5_alpha":int "p6_alpha":int "p7_alpha":int "Enab_Root_change_alpha":bool "Enab_p2_change_alpha":bool "Enab_p3_change_alpha":bool "Enab_p4_change_alpha":bool "Enab_p5_change_alpha":bool "Enab_p6_change_alpha":bool "Enab_p7_change_alpha":bool "Root_change_alpha":bool "p2_change_alpha":bool "p3_change_alpha":bool "p4_change_alpha":bool "p5_change_alpha":bool "p6_change_alpha":bool "p7_change_alpha":bool "legitimate":bool potential:real round:bool round_nb:int
#outputs "Root_isRoot":bool "Root_alpha":int "Root_par":int "p2_isRoot":bool "p2_alpha":int "p2_par":int "p3_isRoot":bool "p3_alpha":int "p3_par":int "p4_isRoot":bool "p4_alpha":int "p4_par":int "p5_isRoot":bool "p5_alpha":int "p5_par":int "p6_isRoot":bool "p6_alpha":int "p6_par":int "p7_isRoot":bool "p7_alpha":int "p7_par":int "Enab_Root_change_alpha":bool "Enab_p2_change_alpha":bool "Enab_p3_change_alpha":bool "Enab_p4_change_alpha":bool "Enab_p5_change_alpha":bool "Enab_p6_change_alpha":bool "Enab_p7_change_alpha":bool "Root_change_alpha":bool "p2_change_alpha":bool "p3_change_alpha":bool "p4_change_alpha":bool "p5_change_alpha":bool "p6_change_alpha":bool "p7_change_alpha":bool "legitimate":bool potential:real round:bool round_nb:int
#step 0
#outs 0 0 0 0 0 0 0 t t t t t f f f t f f t f f f 15. f 0
#outs t 0 -1 f 0 0 f 0 0 f 0 0 f 0 0 f 0 0 f 0 0 t t t t t f f f t f f t f f f 15. f 0
#step 1
#outs 0 1 0 0 1 0 0 t f t t f f f t f t t f f f f 8. f 1
#outs t 0 -1 f 1 0 f 0 0 f 0 0 f 1 0 f 0 0 f 0 0 t f t t f f f t f t t f f f f 8. f 1
#step 2
#outs 2 1 1 2 1 0 0 f t t f f f f f f t f f f f f 5. t 2
#outs t 2 -1 f 1 0 f 1 0 f 2 0 f 1 0 f 0 0 f 0 0 f t t f f f f f f t f f f f f 5. t 2
#step 3
#outs 2 1 3 2 1 0 0 f t f f f f f f t f f f f f f 2. f 2
#outs t 2 -1 f 1 0 f 3 0 f 2 0 f 1 0 f 0 0 f 0 0 f t f f f f f f t f f f f f f 2. f 2
#step 4
#outs 2 4 3 2 1 0 0 t f f f f f f t f f f f f f f 1. t 3
#outs t 2 -1 f 4 0 f 3 0 f 2 0 f 1 0 f 0 0 f 0 0 t f f f f f f t f f f f f f f 1. t 3
#step 5
#outs 0 4 3 2 1 0 0 f f f f f f f f f f f f f f t 0. t 3
#outs t 0 -1 f 4 0 f 3 0 f 2 0 f 1 0 f 0 0 f 0 0 f f f f f f f f f f f f f f t 0. t 3
This algo is silent after 8 moves, 5 steps, 3 rounds.
......
# Automatically generated by /home/jahier/.opam/4.14.0/bin/sasa version "v4.6.0" ("73ebb5e")
# on crevetete the 23/6/2022 at 14:37:04
# Automatically generated by /home/jahier/.opam/4.14.0/bin/sasa version "v4.7.0" ("1f6fd7d")
# on crevetete the 25/7/2022 at 17:12:38
#sasa rtree10.dot -seed 42
#seed 42
#inputs
#outputs "Root_alpha":int "p1_alpha":int "p2_alpha":int "p3_alpha":int "p4_alpha":int "p5_alpha":int "p6_alpha":int "p7_alpha":int "p8_alpha":int "p9_alpha":int "Enab_Root_change_alpha":bool "Enab_p1_change_alpha":bool "Enab_p2_change_alpha":bool "Enab_p3_change_alpha":bool "Enab_p4_change_alpha":bool "Enab_p5_change_alpha":bool "Enab_p6_change_alpha":bool "Enab_p7_change_alpha":bool "Enab_p8_change_alpha":bool "Enab_p9_change_alpha":bool "Root_change_alpha":bool "p1_change_alpha":bool "p2_change_alpha":bool "p3_change_alpha":bool "p4_change_alpha":bool "p5_change_alpha":bool "p6_change_alpha":bool "p7_change_alpha":bool "p8_change_alpha":bool "p9_change_alpha":bool "legitimate":bool potential:real round:bool round_nb:int
#outputs "Root_isRoot":bool "Root_alpha":int "Root_par":int "p1_isRoot":bool "p1_alpha":int "p1_par":int "p2_isRoot":bool "p2_alpha":int "p2_par":int "p3_isRoot":bool "p3_alpha":int "p3_par":int "p4_isRoot":bool "p4_alpha":int "p4_par":int "p5_isRoot":bool "p5_alpha":int "p5_par":int "p6_isRoot":bool "p6_alpha":int "p6_par":int "p7_isRoot":bool "p7_alpha":int "p7_par":int "p8_isRoot":bool "p8_alpha":int "p8_par":int "p9_isRoot":bool "p9_alpha":int "p9_par":int "Enab_Root_change_alpha":bool "Enab_p1_change_alpha":bool "Enab_p2_change_alpha":bool "Enab_p3_change_alpha":bool "Enab_p4_change_alpha":bool "Enab_p5_change_alpha":bool "Enab_p6_change_alpha":bool "Enab_p7_change_alpha":bool "Enab_p8_change_alpha":bool "Enab_p9_change_alpha":bool "Root_change_alpha":bool "p1_change_alpha":bool "p2_change_alpha":bool "p3_change_alpha":bool "p4_change_alpha":bool "p5_change_alpha":bool "p6_change_alpha":bool "p7_change_alpha":bool "p8_change_alpha":bool "p9_change_alpha":bool "legitimate":bool potential:real round:bool round_nb:int
#step 0
#outs 4 0 3 3 2 0 4 1 1 3 t f f t f f t t t t t f f f f f f f f f f 16. f 0
#outs t 4 -1 f 0 0 f 3 0 f 3 0 f 2 0 f 0 0 f 4 0 f 1 0 f 1 0 f 3 0 t f f t f f t t t t t f f f f f f f f f f 16. f 0
#step 1
#outs 1 0 3 3 2 0 4 1 1 3 f f f t f f t t t t f f f f f f t t t f f 15. f 1
#outs t 1 -1 f 0 0 f 3 0 f 3 0 f 2 0 f 0 0 f 4 0 f 1 0 f 1 0 f 3 0 f f f t f f t t t t f f f f f f t t t f f 15. f 1
#step 2
#outs 1 0 3 3 2 0 2 0 0 3 t f f t t f t f f t f f f f t f t f f t f 12. f 1
#outs t 1 -1 f 0 0 f 3 0 f 3 0 f 2 0 f 0 0 f 2 0 f 0 0 f 0 0 f 3 0 t f f t t f t f f t f f f f t f t f f t f 12. f 1
#step 3
#outs 1 0 3 3 1 0 1 0 0 0 t f t t f f f f f f t f f f f f f f f f f 6. f 1
#outs t 1 -1 f 0 0 f 3 0 f 3 0 f 1 0 f 0 0 f 1 0 f 0 0 f 0 0 f 0 0 t f t t f f f f f f t f f f f f f f f f f 6. f 1
#step 4
#outs 2 0 3 3 1 0 1 0 0 0 f f t t f f f f f f f f t f f f f f f f f 5. f 1
#outs t 2 -1 f 0 0 f 3 0 f 3 0 f 1 0 f 0 0 f 1 0 f 0 0 f 0 0 f 0 0 f f t t f f f f f f f f t f f f f f f f f 5. f 1
#step 5
#outs 2 0 2 3 1 0 1 0 0 0 f f f t f f f f f f f f f t f f f f f f f 3. f 1
#outs t 2 -1 f 0 0 f 2 0 f 3 0 f 1 0 f 0 0 f 1 0 f 0 0 f 0 0 f 0 0 f f f t f f f f f f f f f t f f f f f f f 3. f 1
#step 6
#outs 2 0 2 0 1 0 1 0 0 0 f f f f f f f f f f f f f f f f f f f f t 0. t 1
#outs t 2 -1 f 0 0 f 2 0 f 0 0 f 1 0 f 0 0 f 1 0 f 0 0 f 0 0 f 0 0 f f f f f f f f f f f f f f f f f f f f t 0. t 1
This algo is silent after 10 moves, 6 steps, 1 round.
......
(* Time-stamp: <2022-07-12 11:01:25 emile> *)
open Algo
let d = max_degree()
......@@ -6,11 +8,14 @@ type t = {
isRoot:bool;
alpha:int;
par:int
}
}
(*let boolVint (b:bool):int =
if b then 1 else 0*)
let (to_string: (t -> string)) =
fun s ->
Printf.sprintf "alpha=%d" s.alpha
Printf.sprintf "isRoot=%b alpha=%d par=%d" s.isRoot s.alpha s.par
let (of_string: (string -> t) option) =
Some (fun s ->
......@@ -21,4 +26,4 @@ let (copy : ('v -> 'v)) = fun x -> x
let actions = ["change_alpha"]
let k = 2
......@@ -37,10 +37,10 @@ tel
-- At the first instant, the round has not begun
-- At the very end, no incr should be done
node round_count (r,silent:bool) returns (res:int);
node round_count (r,legit:bool) returns (res:int);
var cpt : int;
let
cpt = (if r and not silent then 1 else 0) + 1 fby cpt;
cpt = (if r and not legit then 1 else 0) + 1 fby cpt;
res = 0 -> cpt;
tel
......
include "../lustre/oracle_utils.lus"
type status = enum { I, C, EB, EF };
type state = struct { st:status; par:int; d:int };
type string;
node rsp_tree_oracle(legit:bool; Enab, Acti:bool^an^pn; config: int ^(3*pn); round:bool; round_nb:int)
function intVstatus (i:int)
returns(res :status);
let
res = if i = 0 then I
else if i = 1 then C
else if i = 2 then EB
else EF;
tel;
function to_state( d:int; par:int; st:int )
returns(res : state);
let
res = state { st=intVstatus(st); par=par; d=d };
tel;
node rsp_tree_oracle(legit:bool; Enab, Acti:bool^an^pn; config: state^pn; round:bool; round_nb:int)
returns (res:bool);
var
Silent:bool;
......
silence
n
n
n
n
wait 3
print_event !e;;
include "../lustre/utils.lus"
type state = int;
node st_KK06_algo1_oracle<<const an:int; const pn:int>>
(legitimate:bool; Enab,Acti:bool^an^pn; Config: int^pn;round:bool; round_nb:int) returns (ok:bool);
var
......
include "../lustre/utils.lus"
type state = int;
const bigN = 2*card;
node st_KK06_algo2_oracle<<const an:int; const pn:int>>(leg:bool; Enab,Acti:bool^an^pn; Config: int^pn;round:bool; round_nb:int)
......
......@@ -5,6 +5,8 @@ DECO_PATTERN="0-:unison.ml"
-include ../Makefile.inc
-include Makefile.untracked
DAEMON=-sd
##############################################################################
# Non-regression tests
......
......@@ -3,14 +3,14 @@ graph fig4_1 {
p1 [algo="unison.ml" init="clock=7"]
p2 [algo="unison.ml" init="clock=8"]
p3 [algo="unison.ml" init="clock=4"]
p4 [algo="unison.ml" init="clock=3"]
p5 [algo="unison.ml" init="clock=0"]
p6 [algo="unison.ml" init="clock=7"]
p7 [algo="unison.ml" init="clock=2"]
p8 [algo="unison.ml" init="clock=7"]
p1 [algo="unison.ml" init="c=7"]
p2 [algo="unison.ml" init="c=8"]
p3 [algo="unison.ml" init="c=4"]
p4 [algo="unison.ml" init="c=3"]
p5 [algo="unison.ml" init="c=0"]
p6 [algo="unison.ml" init="c=7"]
p7 [algo="unison.ml" init="c=2"]
p8 [algo="unison.ml" init="c=7"]
p1 -- p2 -- p3 -- p4 -- p5 -- p3
p2 -- p7 -- p6 -- p3
......
type t = int
let to_string = (fun s -> Printf.sprintf "c=%i" s)
let of_string = None
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
......
type t = int
let to_string = (fun s -> Printf.sprintf "c=%i" s)
let of_string = None
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
......
type t = int
let to_string = (fun s -> Printf.sprintf "c=%i" s)
let of_string = None
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
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment