verimag
synchrone
sasa

Repository



The 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.


test/skeleton/: a fake algorithm meant to be used as a skeleton

test/dijkstra-ring/: Dijkstra token ring

test/unison/: Synchronous unison

test/async-unison/: Asynchronous unison

test/coloring/: a graph coloring algorithm

test/alea-coloring/: a randomized variant of the previous one

test/bfs-spanning-tree/: a Breadth First Search Spanning tree construction

It also contains implementations of algorithms found in the literature:


test/st-CYH91: another Spanning tree construction ("A self-stabilizing algorithm for constructing spanning trees" by Chen, Yu, and Huang in 1991)

test/bfs-st-HC92: another BFS Spanning tree construction ("A self-stabilizing algorithm for constructing breadth-first trees" by Huang and Chen in 1992)

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)

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)

test/dfs-list/: the same Depth First Search, but using lists instead or arrays

Each directories contains working examples, which are checked using the Continuous Integration facilities of Gitlab (cf the .gitlab-ci.yml script and the CI 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 one).
The test directory also contains sub-directories which gathers programs shared by all examples:


test/lustre/: contains Lustre programs used as (test/*/*.lus) oracles

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.

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).