Restructure project

.gitignore

@@ -8,3 +8,5 @@
 *.cov
 
 *.lv4
+
+bin/

README.md

-# Self-stabilizing Algorithms in LUsTre
+# SALut - Self-stabilizing Algorithms in LUsTre
 
-```shell
-$ cd $example_folder
-$ make build
-$ make test   # requires lurette and sasa algorithm
-$ make verify # requires kind2
+[SALut](.) is a companion project to [Verimag's Synchrone Reactive Toolbox](https://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/reactive-toolbox/).
+
+It is dedicated to the [Simulation and Formal Verification of Self-stabilizing Algorithms](https://ensiwiki.ensimag.fr/index.php?title=IRL_-_Simulation_and_Formal_Verification_of_Self-stabilizing_Algorithms) in the [the Lustre Programming Language](https://www-verimag.imag.fr/The-Lustre-Programming-Language-and), relying on [Lurette][lurette] and [SASA](https://verimag.gricad-pages.univ-grenoble-alpes.fr/synchrone/sasa/) for testing/simulation and on [Kind2][kind2] for SMT-powered verification.
+
+
+## [dot2lus](dot2lus.ml)
+
+### Summary
+
+dot2lus compiles a graph described in the [DOT format](https://en.wikipedia.org/wiki/DOT_(graph_description_language)) into a Lustre program that executes some [Distributed Self-Stabilizing Algorithm](https://www-verimag.imag.fr/New-Book-Introduction-to-Distributed.html) over an equivalent network topology.
+
+```
+dot2lus <dotfile> [-o lusfile] [--clock] [--help]
+  -o Set output file (default is inferred from input file)
+  --clock Generate clocked code (default is unclocked)
+  --help  Display this list of options
 ```
+
+### Algorithm API
+
+Following the conventions used in [SASA's API](https://verimag.gricad-pages.univ-grenoble-alpes.fr/synchrone/sasa/_html/algo/Algo/index.html), every algorithm currently needs to provide the following definitions, which are shared by all nodes:
+
+```ocaml
+(* Represents a node's state. *)
+type state;
+
+(* Enumerates the possible atomic actions a node might execute. *)
+type action;
+const actions_number : int;
+
+(* Given an integer in [0,actions_number), maps to an equivalent action. *)
+function action_of_int(i : int) returns (a : action);
+```
+
+And each algorithmic node needs `enable` and `step` functions prefixed by its name:
+
+```ocaml
+(* p.lus *)
+
+(* Computes the set of actions enabled in this configuration of current and visible neighboring nodes' state. *)
+function p_enable<<const degree:int>>(this : state; neighbors : state^degree)
+returns (enabled : bool^actions_number);
+
+(* Executes the given action, returning the updated node state. *)
+function p_step<<const degree:int>>(this : state; neighbors : state^degree; action : action)
+returns (new : state);
+```
+
+**Check out the generated Lustre topology for the graph constants it defines.**
+
+### Examples
+
+Some [example algorithms](test/) are provided in this repository.
+Each folder contains a distributed algorithm defined in both OCaml+SASA and LustreV6+SALUT and with a common network topology.
+
+The [shared Makefile](test/Makefile.inc) has instructions on how to `build` the Lustre-defined network and use [Lurette][lurette] to `test` it agains the SASA model.
+
+You can also `verify` it with [Kind2][kind2].
+Note that this currently requires converting LustreV6 to LustreV4 and adding Kind2's required annotations (to the generated LV4), which is also handled by the makefile.
+
+### Build instructions
+
+```sh
+$ cd src/
+$ make # => bin/dot2lus
+```
+
+[lurette]: https://www-verimag.imag.fr/Lurette-107.html
+[kind2]: https://kind2-mc.github.io/kind2/

sas.lus → lib/sas.lus

@@ -5,19 +5,19 @@ include "bitset.lus"
 function silent<<const an:int; const pn:int>>(enab: bool^an^pn)
 returns (y : bool);
 let
-	y = none<<pn>>(map<<any<<an>>, pn>>(enab));
+	y = boolnone<<pn>>(map<<boolany<<an>>, pn>>(enab));
 tel;
 
 node node_is_proper<<const an:int>>(acti, enab : bool^an) returns (y : bool);
 let
-	y = true -> all<<an>>(map<<=>,an>>(acti, pre(enab)));
+	y = true -> boolall<<an>>(map<<=>,an>>(acti, pre(enab)));
 tel;
 
 -- Any activation Ai implies Ei was previously enabled.
 node daemon_is_proper<<const an:int; const pn:int>>(acti, enab : bool^an^pn)
 returns (y : bool);
 let
-	y = all<<pn>>(map<<node_is_proper,pn>>(acti, enab));
+	y = boolall<<pn>>(map<<node_is_proper,pn>>(acti, enab));
 tel;
 
 -- |A| >= 1 for non-silent states.
@@ -25,7 +25,7 @@ function daemon_is_distributed<<const an:int; const pn:int>>(acti, enab : bool^a
 returns (y : bool);
 let
 	y = silent<<an,pn>>(enab) or
-	    boolred<<1,pn,pn>>(map<<any<<an>>, pn>>(acti));
+	    boolred<<1,pn,pn>>(map<<boolany<<an>>, pn>>(acti));
 tel;
 
 -- No two neighboring nodes are active at once.
@@ -39,11 +39,11 @@ var
 	no_active_adjacencies : bool ^ pn;
 	locally_central : bool ^ pn;
 let
-	active = map<<any<<an>>, pn>>(acti);
+	active = map<<boolany<<an>>, pn>>(acti);
 	active_adjacencies = map<<inter,pn>>(active^pn, adjacency);
-	no_active_adjacencies = map<<none<<pn>>, pn>>(active_adjacencies);
+	no_active_adjacencies = map<<boolnone<<pn>>, pn>>(active_adjacencies);
 	locally_central = map<<=>,pn>>(active, no_active_adjacencies);
-	y = all<<pn>>(locally_central);
+	y = boolall<<pn>>(locally_central);
 tel;
 
 -- |A| = 1 for non-silent states.
@@ -51,7 +51,7 @@ function daemon_is_central<<const an:int; const pn:int>>(acti : bool^an^pn)
 returns (y : bool);
 let
 	y = silent<<an,pn>>(enab) or
-	    boolred<<1,1,pn>>(map<<any<<an>>, pn>>(acti));
+	    boolred<<1,1,pn>>(map<<boolany<<an>>, pn>>(acti));
 tel;
 
 -- |A| = n for non-silent states.
@@ -59,12 +59,12 @@ function daemon_is_synchronous<<const an:int; const pn:int>>(acti, enab : bool^a
 returns (y:bool);
 let
 	y = silent<<an,pn>>(enab) or
-	    boolred<<pn,pn,pn>>(map<<any<<an>>, pn>>(acti));
+	    boolred<<pn,pn,pn>>(map<<boolany<<an>>, pn>>(acti));
 tel;
 
 -- Measures time complexity in moves.
 node move_count<<const an:int; const pn:int>>(acti : bool^an^pn)
 returns (count:int);
 let
-  count = (0 -> pre(count)) + pop_count<<pn>>(map<<any<<an>>, pn>>(acti));
+  count = (0 -> pre(count)) + pop_count<<pn>>(map<<boolany<<an>>, pn>>(acti));
 tel;

utils.lus → lib/utils.lus

@@ -4,7 +4,7 @@ let
 	r = with (N = 1) then [ 0 ] else range<<N-1>>() | [ N-1 ];
 tel;
 
--- "First-class" if statement, since we don't have lambdas.
+-- First-class if statement, since we don't have lambdas.
 function choice_of_bool<<type T; const t:T; const f:T>>(b : bool) returns (y : T);
 let
 	y = if b then t else f;
@@ -13,17 +13,17 @@ tel;
 -- |> true -> 1 | false -> 0
 function int_of_bool = choice_of_bool<<int, 1, 0>>;
 
-function none<<const N:int>>(s : bool^N) returns (y : bool);
+function boolnone<<const N:int>>(s : bool^N) returns (y : bool);
 let
 	y = boolred<<0,0,N>>(s);
 tel;
 
-function any<<const N:int>>(s : bool^N) returns (y : bool);
+function boolany<<const N:int>>(s : bool^N) returns (y : bool);
 let
 	y = boolred<<1,N,N>>(s);
 tel;
 
-function all<<const N:int>>(s : bool^N) returns (y : bool);
+function boolall<<const N:int>>(s : bool^N) returns (y : bool);
 let
 	y = boolred<<N,N,N>>(s);
 tel;

src/Makefile

+.PHONY = build clean
+
+# default rule
+build: ../bin/dot2lus
+
+clean:
+	rm -f *.cmx *.cmi *.o
+	rm -f ../bin/dot2lus
+	-rmdir ../bin
+
+../bin/dot2lus: dot2lus.ml
+	mkdir -p ../bin
+	ocamlfind ocamlopt -o ../bin/$@ -linkpkg -package sasacore $^

dot2lus.ml → src/dot2lus.ml

-#use "topfind";;
-#require "sasacore";; (* simplified DOT parsing *)
+(* #use "topfind";; *)
+(* #require "sasacore";; *)
 
 open Sasacore
 

Makefile.inc → test/Makefile.inc

 #
-# To use this file, `include` it and define the following variables:
-# DOT2LUS     # dot2lus command, can include flags (eg. --clock)
-# TOPOLOGY    # graph file name, without the .dot extension
-# SASA_ALGOS  # .ml files used in sasa/lurette tests
-# SASAFLAGS   # flags passed in to sasa (eg. to define the daemon)
+# To use this file, define the following variables and `include` it:
+# TOPOLOGY     # graph file name, without the .dot extension
+# DOT2LUSFLAGS # optional: dot2lus flags (eg. --clock)
+# SASA_ALGOS   # .ml files used in sasa/lurette tests
+# SASAFLAGS    # optional: flags passed in to sasa (eg. to define the daemon)
 #
 
-.PHONY = build clean test verify
+.PHONY = build all clean test verify
+
+# extra ../ because this is called from within each test folder
+D2L := ../../bin/dot2lus
 
 # default rule
 build: $(TOPOLOGY).lus
 
+all: $(TOPOLOGY).lus $(TOPOLOGY).cmxs $(TOPOLOGY)_verify.lv4
+
 clean:
 	rm -f *.cmxs *.cmx *.cmi *.o
 	rm -f $(TOPOLOGY).ml config.ml
@@ -19,14 +24,13 @@ clean:
 	rm -f $(TOPOLOGY)_verify.lv4
 
 test: $(TOPOLOGY).cmxs $(TOPOLOGY).lus
-	lurette -sut "sasa $(TOPOLOGY).dot $(SASAFLAGS)" \
-	        -oracle "lv6 $(TOPOLOGY)_oracle.lus -n oracle"
+	lurette -sut "sasa $(TOPOLOGY).dot $(SASAFLAGS)" -oracle "lv6 $(TOPOLOGY)_oracle.lus -n oracle"
 
 verify: $(TOPOLOGY)_verify.lv4
 	kind2 $<
 
 $(TOPOLOGY).lus: $(TOPOLOGY).dot
-	$(DOT2LUS) $<
+	$(D2L) $(DOT2LUSFLAGS) $<
 
 $(TOPOLOGY).cmxs: state.ml $(SASA_ALGOS) config.ml $(TOPOLOGY).ml
 	ocamlfind ocamlopt -package algo -shared $^ -o $@
@@ -34,6 +38,7 @@ $(TOPOLOGY).cmxs: state.ml $(SASA_ALGOS) config.ml $(TOPOLOGY).ml
 $(TOPOLOGY).ml config.ml: $(TOPOLOGY).dot
 	sasa -reg $<
 
+# XXX: this method of adding kind2 annotations is brittle
 $(TOPOLOGY)_verify.lv4: $(TOPOLOGY)_oracle.lus $(TOPOLOGY).lus verify.lus
 	lv6 $< -n verify --lustre-v4 -o $@
 	sed -i -e "s/tel/--%MAIN ;\n--%PROPERTY ok;\ntel/" $@

coloring/Makefile → test/coloring/Makefile

-DOT2LUS := ocaml ../dot2lus.ml
-TOPOLOGY := dice5
+TOPOLOGY ?= dice5
+DOT2LUSFLAGS ?=
 SASA_ALGOS := p.ml
-SASAFLAGS := --locally-central-daemon
+SASAFLAGS += --locally-central-daemon
 
 include ../Makefile.inc

coloring/p.lus → test/coloring/p.lus

-include "../bitset.lus"
+include "../../lib/bitset.lus"
 
 type state = int;
 

coloring/verify.lus → test/coloring/verify.lus

-include "../sas.lus"
+include "../../lib/sas.lus"
 
 node verify(activations : bool^actions_number^card; inits : state^card) returns (ok : bool);
 var

token/Makefile → test/token/Makefile

-DOT2LUS := ocaml ../dot2lus.ml
-TOPOLOGY := ring8
+TOPOLOGY ?= ring8
+DOT2LUSFLAGS ?=
 SASA_ALGOS := p.ml root.ml
-SASAFLAGS := --distributed-daemon
 
 include ../Makefile.inc