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

doc: some enhancements

parent 01e4df83
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 740 additions and 835 deletions
guides/users/Makefile
+ 5
− 5
View file @ ff1410f8
all:README.html README.md algo all:README.html algo
# always work via dockver ... # always work via dockver ...
dockver: dockver:
...@@ -9,21 +9,21 @@ algo: ...@@ -9,21 +9,21 @@ algo:
cd ../..; make odoc cd ../..; make odoc
cp -rf ../../_build/default/_doc/_html . cp -rf ../../_build/default/_doc/_html .
%.html:%.org %.html:%.org
emacs --batch --load=emacs-org.el \ emacs --batch --load=emacs-org.el \
--visit=$*.org --funcall org-html-export-to-html --visit=$*.org --funcall org-html-export-to-html
%.md:%.org %.md:%.org
emacs --batch --eval="(add-to-list 'load-path \".\")" --load=emacs-org.el --visit=$*.org --funcall org-md-export-to-markdown emacs --batch --eval="(add-to-list 'load-path \".\")" --load=emacs-org.el --visit=$*.org --funcall org-md-export-to-markdown
%.html3:%.org %.html3:%.org
emacs --batch --eval="(add-to-list 'load-path \".\") (add-to-list 'load-path \"./el\")" --eval="(require 'htmlize)" --load=emacs-org.el \ emacs --batch --eval="(add-to-list 'load-path \".\") (add-to-list 'load-path \"./el\")" --eval="(require 'htmlize)" --load=emacs-org.el \
--visit=$*.org --funcall org-html-export-to-html --visit=$*.org --funcall org-html-export-to-html
EMACS=emacs \ EMACS=emacs \
--load=htmlize.el \ --load=htmlize.el \
--load=el/ob-ocaml.el \ --load=el/ob-ocaml.el \
--load=emacs-org.el --load=emacs-org.el
%.html2: %.html2:
$(EMACS) --visit=$*.org --funcall org-html-export-to-html --eval "(kill-emacs)" -Q $(EMACS) --visit=$*.org --funcall org-html-export-to-html --eval "(kill-emacs)" -Q
......
guides/users/README.md
+ 423
− 584
View file @ ff1410f8
This diff is collapsed.
guides/users/README.org
+ 273
− 161
View file @ ff1410f8
This diff is collapsed.
test/Makefile.inc
+ 2
− 2
View file @ ff1410f8
# Time-stamp: <modified the 23/01/2023 (at 14:31) by Erwan Jahier> # Time-stamp: <modified the 23/01/2023 (at 17:27) by Erwan Jahier>
# #
# Define some default rules that ought to work most of the time # Define some default rules that ought to work most of the time
# #
...@@ -9,7 +9,7 @@ LIB=-package algo ...@@ -9,7 +9,7 @@ LIB=-package algo
ifndef DAEMON ifndef DAEMON
# some rules uses this one # some rules uses this one
DAEMON=-dd DAEMON=
endif endif
......
test/README.md
+ 19
− 15
View file @ ff1410f8
```sh
git clone https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa.git
cd sasa/test
```
The [test](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test) directory contains various examples of self-stabilizing distributed programs taken from the book \`\`Introduction to Distributed Self-Stabilizing Algorithms'' By Altisen, Devismes, Dubois, and Petit. The [test](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test) directory contains various examples of self-stabilizing distributed programs taken from the book \`\`Introduction to Distributed Self-Stabilizing Algorithms'' By Altisen, Devismes, Dubois, and Petit.
1. `test/skeleton/`: a fake algorithm meant to be used as a skeleton 1. `test/skeleton/`: a fake algorithm meant to be used as a skeleton
2. `test/dijkstra-ring/`: Dijkstra token ring 2. `test/dijkstra-ring/`: Dijkstra token ring
3. `test/unison/`: Synchronous unison 3. `test/unison/`: Synchronous unison
4. `test/async-unison/`: Asynchronous unison 4. `test/coloring/`: a graph coloring algorithm
5. `test/coloring/`: a graph coloring algorithm 5. `test/alea-coloring/`: a randomized variant of the previous one
6. `test/alea-coloring/`: a randomized variant of the previous one 6. `test/bfs-spanning-tree/`: a Breadth First Search Spanning tree construction
7. `test/bfs-spanning-tree/`: a Breadth First Search Spanning tree construction
It also contains implementations of algorithms found in the literature: It also contains implementations of algorithms found in the literature:
1. `test/st-CYH91`: another Spanning tree construction ("A self-stabilizing algorithm for constructing spanning trees" by Chen, Yu, and Huang in 1991) 1. `test/async-unison/`: Asynchronous unison ("Asynchronous unison" by Couvreur, J., Francez, N., and Gouda, M. G. in 1992)
2. `test/bfs-st-HC92`: another BFS Spanning tree construction ("A self-stabilizing algorithm for constructing breadth-first trees" by Huang and Chen in 1992) 2. `test/st-CYH91`: another Spanning tree construction ("A self-stabilizing algorithm for constructing spanning trees" by Chen, Yu, and Huang in 1991)
3. `test/st-KK06_algo1` and `test/st-KK06_algo2`: another Spanning tree construction ("A Self-stabilizing Algorithm for Finding a Spanning Tree in a Polynomial Number of Moves" by Kosowski and Kuszner, 2006) 3. `test/bfs-st-HC92`: another BFS Spanning tree construction ("A self-stabilizing algorithm for constructing breadth-first trees" by Huang and Chen in 1992)
4. `test/dfs/`: a Depth First Search using arrays (the \`\`atomic state model'' version of a [Depth First Search algorithm proposed by Collin and Dolev in 1994](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.57.1100&rep=rep1&type=pdf)) 4. `test/st-KK06_algo1` and `test/st-KK06_algo2`: another Spanning tree construction ("A Self-stabilizing Algorithm for Finding a Spanning Tree in a Polynomial Number of Moves" by Kosowski and Kuszner, 2006)
5. `test/dfs-list/`: the same Depth First Search, but using lists instead or arrays 5. `test/dfs/`: a Depth First Search using arrays (the \`\`atomic state model'' version of a [Depth First Search algorithm proposed by Collin and Dolev in 1994](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.57.1100&rep=rep1&type=pdf))
6. `test/dfs-list/`: the same Depth First Search, but using lists instead or arrays
7. `test/rsp-tree/`: The Algorithm 1 of "Self-Stabilizing Disconnected Components Detection and Rooted Shortest-Path Tree Maintenance in Polynomial Steps" by Stéphane Devismes, David Ilcinkas, Colette Johnen.
Each directories contains working examples, which are checked using the Continuous Integration facilities of Gitlab (cf the [.gitlab-ci.yml](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/.gitlab-ci.yml) script and the [CI pipelines](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/pipelines) results). Each directory contains working examples, which are checked using the Continuous Integration facilities of Gitlab (cf the [.gitlab-ci.yml](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/.gitlab-ci.yml) script and the [CI pipelines](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/pipelines) results).
If you want to reproduce or understand what those non-regression tests do, please look at the `test/*/Makefile`, present in each directory (which all include the [test/Makefile.inc](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test/Makefile.inc) one). If you want to reproduce or understand what those non-regression tests do, uo can have a look at the `test/*/Makefile` files, present in each directory (which all include the [test/Makefile.inc](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test/Makefile.inc)and the [test/Makefile.dot](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test/Makefile.dot) ones).
The `test` directory also contains sub-directories which gathers programs shared by all examples: The `test` directory also contains sub-directories which gather programs shared by all examples:
- `test/lustre/`: contains Lustre programs used as (`test/*/*.lus`) oracles - `test/lustre/`: contains Lustre programs used as (`test/*/*.lus`) oracles
- `test/rdbg-utils/`: contains `ocaml` functions that can be used from `rdbg` - `test/rdbg-utils/`: contains `ocaml` functions that can be used from `rdbg`
- `test/my-rdbg-tuning.ml`: contains useful shortcuts/commands that can be used from `rdbg`. \ No newline at end of file
- `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).
test/README.org
+ 7
− 13
View file @ ff1410f8
...@@ -39,24 +39,18 @@ literature: ...@@ -39,24 +39,18 @@ literature:
Johnen. Johnen.
Each directories contains working examples, which are checked using the Each directory contains working examples, which are checked using the
Continuous Integration facilities of Gitlab (cf the [[https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/.gitlab-ci.yml][.gitlab-ci.yml]] Continuous Integration facilities of Gitlab (cf the [[https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/.gitlab-ci.yml][.gitlab-ci.yml]]
script and the [[https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/pipelines][CI pipelines]] results). script and the [[https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/pipelines][CI pipelines]] results).
If you want to reproduce or understand what those non-regression tests If you want to reproduce or understand what those non-regression
do, please look at the =test/*/Makefile=, present in each directory tests do, uo can have a look at the =test/*/Makefile= files, present
(which all include the [[https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test/Makefile.inc][test/Makefile.inc]] one). in each directory (which all include the [[https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test/Makefile.inc][test/Makefile.inc]]and the
[[https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test/Makefile.dot][test/Makefile.dot]] ones).
The =test= directory also contains sub-directories which gathers The =test= directory also contains sub-directories which gather
programs shared by all examples: programs shared by all examples:
- =test/lustre/=: contains Lustre programs used as (=test/*/*.lus=) oracles - =test/lustre/=: contains Lustre programs used as (=test/*/*.lus=) oracles
- =test/rdbg-utils/=: contains =ocaml= functions that can be used from - =test/rdbg-utils/=: contains =ocaml= functions that can be used from
=rdbg= =rdbg=
- =test/my-rdbg-tuning.ml=: contains useful shortcuts/commands that
can be used from =rdbg=.
- =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).
test/alea-coloring-alt/Makefile
+ 2
− 2
View file @ ff1410f8
# Time-stamp: <modified the 17/01/2023 (at 14:41) by Erwan Jahier> # Time-stamp: <modified the 25/01/2023 (at 10:51) by Erwan Jahier>
DECO_PATTERN="0-:algo_331.ml" DECO_PATTERN="0-:algo_331.ml"
DAEMON=-sd DAEMON=
-include ./Makefile.dot -include ./Makefile.dot
-include ./Makefile.inc -include ./Makefile.inc
-include Makefile.untracked -include Makefile.untracked
......
test/alea-coloring/Makefile
+ 2
− 2
View file @ ff1410f8
# Time-stamp: <modified the 21/01/2023 (at 11:44) by Erwan Jahier> # Time-stamp: <modified the 25/01/2023 (at 10:51) by Erwan Jahier>
DECO_PATTERN="0-:p.ml" DECO_PATTERN="0-:p.ml"
DAEMON=-sd DAEMON=
-include ./Makefile.dot -include ./Makefile.dot
-include ./Makefile.inc -include ./Makefile.inc
-include Makefile.untracked -include Makefile.untracked
......
test/alea-coloring/state.ml
+ 2
− 8
View file @ ff1410f8
(* Automatically generated by /home/jahier/sasa/_build/default/src/sasaMain.exe version "2.10.4-1-g9a7f112" ("9a7f112")*) type t = int
(* on crevetete the 12/9/2019 at 10:36:45*)
(*../../_build/install/default/bin/sasa -l 100 -reg ring.dot*)
type t = int (* fixme *)
let to_string = string_of_int let to_string = string_of_int
let of_string = Some int_of_string let of_string = Some int_of_string
let copy = fun x -> x let copy = fun x -> x
let actions = ["conflict"] let actions = ["conflict"]
let potential = None let potential = None
let legitimate = None let legitimate = None
let fault = None let fault = None
test/bfs-spanning-tree/Makefile
+ 3
− 3
View file @ ff1410f8
# Time-stamp: <modified the 17/01/2023 (at 13:46) by Erwan Jahier> # Time-stamp: <modified the 23/01/2023 (at 17:35) by Erwan Jahier>
DECO_PATTERN="0:root.ml 1-:p.ml" DECO_PATTERN="0:root.ml 1-:p.ml"
-include ./Makefile.dot -include ./Makefile.dot
...@@ -64,11 +64,11 @@ lurette: lurette0 ...@@ -64,11 +64,11 @@ lurette: lurette0
sim2chrogtk -ecran -in lurette.rif > /dev/null sim2chrogtk -ecran -in lurette.rif > /dev/null
gnuplot-rif lurette.rif gnuplot-rif lurette.rif
rdbgui: fig51_noinit.ml fig51_noinit.lut fig51_noinit_oracle.lus rdbgui: fig51_noinit.cma fig51_noinit.lut fig51_noinit_oracle.lus
rdbgui4sasa -sut "sasa -seed 42 fig51_noinit.dot -dd " \ rdbgui4sasa -sut "sasa -seed 42 fig51_noinit.dot -dd " \
-oracle-nd "lv6 fig51_noinit_oracle.lus -n oracle" -oracle-nd "lv6 fig51_noinit_oracle.lus -n oracle"
rdbg2: fig51.ml fig51.lut rdbg2: fig51.cma fig51.lut
rdbg --sasa -o lurette.rif \ rdbg --sasa -o lurette.rif \
-env "$(sasa) fig51.dot -custd -rif" \ -env "$(sasa) fig51.dot -custd -rif" \
-sut-nd "lutin fig51.lut -n distributed" -sut-nd "lutin fig51.lut -n distributed"
......
test/coloring/Makefile
+ 2
− 40
View file @ ff1410f8
# Time-stamp: <modified the 16/01/2023 (at 10:43) by Erwan Jahier> # Time-stamp: <modified the 21/01/2023 (at 11:41) by Erwan Jahier>
sasa=$(DIR)/bin/sasa -l 100 sasa=$(DIR)/bin/sasa -l 100
...@@ -40,44 +40,6 @@ rdbg-lurette: ring.cmxs ring_oracle.lus ...@@ -40,44 +40,6 @@ rdbg-lurette: ring.cmxs ring_oracle.lus
-sut "sasa ring.dot -rif -lcd " \ -sut "sasa ring.dot -rif -lcd " \
-oracle "lv6 ring_oracle.lus -n oracle -exec" -oracle "lv6 ring_oracle.lus -n oracle -exec"
test100: test100:
for i in $$(seq 100); do make lurette && make clean; done for i in $$(seq 100); do make lurette && make clean; done
rdbg: grid4.ml
echo "" > include.ml
ledit rdbg --sasa -sut "sasa grid4.dot --locally-central-daemon"
rdbgui: grid4.ml
echo "" > include.ml
rdbgui4sasa -sut "sasa grid4.dot --locally-central-daemon"
rdbgui-demo: grid10.ml
echo "" > include.ml
rdbgui4sasa -sut "sasa grid10.dot --central-daemon"
rdbg-luciole: grid4.ml
echo "" > include.ml
rdbg --sasa --luciole -sut "sasa -rif grid4.dot --custom-daemon"
rdbgui-custd: grid4.ml
echo "" > include.ml
rdbgui4sasa -sut "sasa -rif grid4.dot --custom-daemon"
rdbg3: ring.ml
echo "" > include.ml
ledit rdbg --sasa -sut "sasa ring.dot -wd"
rdbg1: ring.ml ring_oracle.lus
echo "" > include.ml
ledit rdbg --sasa -o rdbg-ring.rif \
-sut "sasa --replay ring.dot -rif -lcd " \
-oracle "lv6 ring_oracle.lus -n oracle -exec"
rdbg2: ring.cmxs ring.lut
echo "" > include.ml
ledit rdbg --sasa -o ring.rif \
-env "$(sasa) --replay ring.dot -custd -rif" \
-sut-nd "lutin ring.lut -n distributed"
rdbg4: ring.ml
ledit rdbg --sasa -o ring.rif -env "sasa ring.dot -custd "
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment