Merge branch 'master' of gricad-gitlab.univ-grenoble-alpes.fr:verimag/synchrone/sasa

.gitignore

@@ -15,14 +15,20 @@ rdbg-session*.ml
 *.jpg
 *.bak
 *.save
-*.lus
+*.res
 *.lut
+clique*.lus
+ER*.lus
 flymd.html
 log
 *.sh
+*.c
+*.h
 test/**/*.ml
 !test/**/p.ml
+!test/**/root.ml
 !test/**/state.ml
+!test/**/config.ml
 results
 Makefile.local
 .ocamldebug

.gitlab-ci.yml

@@ -11,7 +11,7 @@ build:
     - opam repo add verimag-sync-repo "http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/opam-repository"
     - eval `opam config env`
     - sudo apt-get update
-    - opam depext sasa rdbgui4sasa lutin lustre-v6 || echo "not needed for recent opam version"
+    - opam depext sasa rdbgui4sasa kind2 lutin lustre-v6 || echo "not needed for recent opam version"
     - opam install --deps-only ./sasa.opam ./rdbgui4sasa.opam
     - make
     - make install

salut/Makefile

+
+
+# build: lib/sasacore/sasaVersion.ml
+build:
+	dune build  @install
+
+clean:
+	dune clean
+	cd test; make clean
+
+install:
+	dune install
+
+reinstall:install
+
+uninstall:
+	dune uninstall
+
+.PHONY:test
+test:
+	make
+	cd test; make test

salut/README.md

+# SALut - Self-stabilizing Algorithms in LUsTre
+
+[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 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](src/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;
+
+(* Maps an integer in [0,actions_number) 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. *)
+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/

salut/lib/Random/lustre_consts.c

+/* This file was generated by lv6 version v6.106.1. */
+/*  lv6 utils.lus -n random -2c -exec -dir Random */
+/* on PC-Travail the 18/07/2022 at 15:00:26 */
+#include "lustre_consts.h"
\ No newline at end of file

salut/lib/Random/lustre_consts.h

+/* This file was generated by lv6 version v6.106.1. */
+/*  lv6 utils.lus -n random -2c -exec -dir Random */
+/* on PC-Travail the 18/07/2022 at 15:00:26 */
+#include "lustre_types.h"
\ No newline at end of file

salut/lib/Random/lustre_types.h

+/* This file was generated by lv6 version v6.106.1. */
+/*  lv6 utils.lus -n random -2c -exec -dir Random */
+/* on PC-Travail the 18/07/2022 at 15:00:26 */
+
+#ifndef _SOC2C_PREDEF_TYPES
+#define _SOC2C_PREDEF_TYPES
+typedef int _boolean;
+typedef int _integer;
+typedef char* _string;
+typedef double _real;
+typedef double _double;
+typedef float _float;
+#define _false 0
+#define _true 1
+#endif
+// end of _SOC2C_PREDEF_TYPES
\ No newline at end of file

salut/lib/Random/random.sh

+if [ -z ${C_COMPILER} ]; then C_COMPILER=gcc; fi
+$C_COMPILER -o random.exec \
+	Random/utils_random_ext.c Random/lustre_consts.c Random/utils_random.c  Random/utils_random_loop.c
+

salut/lib/Random/utils_random.c

+/* This file was generated by lv6 version v6.106.1. */
+/*  lv6 utils.lus -n random -2c -exec -dir Random */
+/* on PC-Travail the 18/07/2022 at 15:00:26 */
+#include "utils_random.h"
+//// Defining step functions
+// Step function(s) for utils_c_rand_ctx
+// Step function(s) for utils_random_ctx
+void utils_random_step(_integer x,_integer *res){
+
+  utils_c_rand_step(x,res); 
+
+} // End of utils_random_step
+

salut/lib/Random/utils_random.h

+/* This file was generated by lv6 version v6.106.1. */
+/*  lv6 utils.lus -n random -2c -exec -dir Random */
+/* on PC-Travail the 18/07/2022 at 15:00:26 */
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include "lustre_consts.h"
+
+// User typedef 
+#ifndef _utils_random_TYPES
+#define _utils_random_TYPES
+// Memoryless soc ctx typedef 
+// Memoryfull soc ctx typedef 
+#endif // end of  _utils_random_TYPES
+
+#ifndef _utils_random_H_FILE
+#include "utils_random_ext.h"
+#define _utils_random_H_FILE
+#endif // _utils_random_H_FILE
+
+void utils_random_step(_integer ,_integer *);
+
+/////////////////////////////////////////////////

salut/lib/Random/utils_random_ext.c

+#include "utils_random.h"
+#include <assert.h>
+void utils_c_rand_step(_integer x,_integer *res){
+  assert (0 < x );
+  *res = (rand() % x);
+}

salut/lib/Random/utils_random_ext.h

+void utils_c_rand_step(_integer ,_integer *);

salut/lib/Random/utils_random_loop.c

+/* This file was generated by lv6 version v6.106.1. */
+/*  lv6 utils.lus -n random -2c -exec -dir Random */
+/* on PC-Travail the 18/07/2022 at 15:00:26 */
+
+#include <stdlib.h>
+#include <stdio.h>
+#include <unistd.h>
+#include "utils_random.h" 
+/* Print a promt ? ************************/
+static int ISATTY;
+/* MACROS DEFINITIONS ****************/
+#ifndef TT
+#define TT "1"
+#endif
+#ifndef FF
+#define FF "0"
+#endif
+#ifndef BB
+#define BB "bottom"
+#endif
+#ifdef CKCHECK
+/* set this macro for testing output clocks */
+#endif
+
+void _read_pragma(char b[]) {
+
+   if (!strcmp(b,"#quit")) exit(0);
+   if (!strcmp(b,"#q")) exit(0);
+}
+char* _get_string(char* n){
+   static char b[10] = "dummy";
+   return b;
+}
+/* Standard Input procedures **************/
+_boolean _get_bool(char* n){
+   char b[512];
+   char c;
+   _boolean r = 0;
+   int s = 1;
+   do {
+      if(ISATTY) {
+         if((s != 1)||(r == -1)) printf("\a");
+         // printf("%s (1,t,T/0,f,F) ? ", n);
+      }
+      if(scanf("%s", b)==EOF) exit(0);
+      r = -1;
+      c=b[0];
+      if(c == 'q') exit(0);
+      if(c == '#') _read_pragma(b);
+      if((c == '0') || (c == 'f') || (c == 'F')) r = 0;
+      if((c == '1') || (c == 't') || (c == 'T')) r = 1;
+   } while((s != 1) || (r == -1));
+   return r;
+}
+_integer _get_int(char* n){
+   char b[512];
+   _integer r;
+   int s = 1;
+   do {
+      if(ISATTY) {
+         if(s != 1) printf("\a");
+         //printf("%s (integer) ? ", n);
+      }
+      if(scanf("%s", b)==EOF) exit(0);
+      if(*b == 'q') exit(0);
+      if(*b == '#') {
+         _read_pragma(b);
+      } else {
+        s = sscanf(b, "%d", &r);
+      }
+   } while(s != 1);
+   return r;
+}
+#define REALFORMAT ((sizeof(_real)==8)?"%lf":"%f")
+_real _get_real(char* n){
+   char b[512];
+   _real r;
+   int s = 1;
+   do {
+      if(ISATTY) {
+         if(s != 1) printf("\a");
+         //printf("%s (real) ? ", n);
+      }
+      if(scanf("%s", b)==EOF) exit(0);
+      if(*b == 'q') exit(0);
+      if(*b == '#') {
+         _read_pragma(b);
+      } else {
+         s = sscanf(b, REALFORMAT, &r);
+      }
+   } while(s != 1);
+   return r;
+}
+/* Standard Output procedures **************/
+void _put_bottom(char* n){
+   if(ISATTY) printf("%s = ", n);
+   printf("%s ", BB);
+   if(ISATTY) printf("\n");
+}
+void _put_bool(char* n, _boolean _V){
+   if(ISATTY) printf("%s = ", n);
+   printf("%s ", (_V)? TT : FF);
+   if(ISATTY) printf("\n");
+}
+void _put_int(char* n, _integer _V){
+   if(ISATTY) printf("%s = ", n);
+   printf("%d ", _V);
+   if(ISATTY) printf("\n");
+}
+void _put_real(char* n, _real _V){
+   if(ISATTY) printf("%s = ", n);
+   printf("%f ", _V);
+   if(ISATTY) printf("\n");
+}
+void _put_string(char* n, char* _V){
+   if(ISATTY) printf("%s = ", n);
+   printf("%s ", _V);
+   if(ISATTY) printf("\n");
+}
+
+/* Output procedures **********************/
+#ifdef CKCHECK
+void %s_BOT_n(void* cdata){
+   _put_bottom("n");
+}
+#endif
+
+/* Main procedure *************************/
+int main(){
+  int _s = 0;
+  _integer x;
+  _integer res;
+  
+  printf("#inputs \"x\":int\n");
+  printf("#outputs \"res\":int\n");
+
+  /* Main loop */
+  ISATTY = isatty(0);
+  while(1){
+    if (ISATTY) printf("#step %d \n", _s+1);
+    else if(_s) printf("\n");
+    fflush(stdout);
+    ++_s;
+    x = _get_int("x");
+    utils_random_step(x,&res);
+    // printf("%d #outs %d\n",x,res);
+    printf("%d\n",res);
+  }
+  return 1;
+   
+}

salut/lib/UsrIntBinary.lus

+
+-- Signed binary 
+
+-- const BIN_SZ=8;
+type UsrInt = bool^BIN_SZ;
+
+--const UsrInt_0 = false^BIN_SZ;
+
+
+node UsrIntIf(
+	c : bool; x : UsrInt; y : UsrInt
+) returns (
+	s : UsrInt
+);
+let
+	s = if c^BIN_SZ then x else y;
+tel
+
+node UsrIntPlus( x : UsrInt; y : UsrInt) returns ( s : UsrInt);
+var c : bool^(BIN_SZ+1);
+let
+	c[0] = false;
+
+	c[1..BIN_SZ] = if c[0..BIN_SZ-1] then (x or y) else (x and y); 
+	s = x xor y xor c[0..BIN_SZ-1];
+tel
+
+node UsrInt
+Chs( x : UsrInt) returns ( s : UsrInt);
+var c : bool^(BIN_SZ+1);
+let
+	c[0] = false;
+	c[1..BIN_SZ] = c[0..BIN_SZ-1] or x;	
+	s = c[0..BIN_SZ-1] xor x;
+tel
+
+node UsrIntIncr(x : UsrInt) returns (s : UsrInt);
+var c : bool^(BIN_SZ+1);
+let
+	c[0] = true;
+	c[1..BIN_SZ] = c[0..BIN_SZ-1] and x;	
+	s = c[0..BIN_SZ-1] xor x;
+tel
+
+node UsrIntDecr(x : UsrInt) returns (s : UsrInt);
+var c : bool^(BIN_SZ+1);
+let
+	c[0] = true;
+	c[1..BIN_SZ] = c[0..BIN_SZ-1] and not x;	
+	s = c[0..BIN_SZ-1] xor x;
+tel
+
+node UsrIntMinus( x : UsrInt; y : UsrInt) returns ( s : UsrInt);
+let
+	s = UsrIntPlus(x, UsrIntChs(y));
+tel
+
+
+node UsrIntGt( x : UsrInt; y : UsrInt) returns ( o : bool);
+var
+	z : UsrInt;
+let
+	-- x > y <=> y - x < 0
+	z = UsrIntPlus(y, UsrIntChs(x));
+	o = z[BIN_SZ-1];
+tel
+
+node UsrIntLt( x : UsrInt; y : UsrInt) returns ( o : bool);
+let
+	-- x < y <=> y > x
+	o = UsrIntGt(y,x);
+tel
+
+node UsrIntGte( x : UsrInt; y : UsrInt) returns ( o : bool);
+let
+	-- x >= y <=> not y > x
+	o = not UsrIntGt(y,x);
+tel
+
+node UsrIntLte( x : UsrInt; y : UsrInt) returns ( o : bool);
+let
+	-- x <= y <=> not x > y
+	o = not UsrIntGt(x,y);
+tel
+
+node UsrIntEq( x : UsrInt; y : UsrInt) returns ( o : bool);
+var
+	a : bool^BIN_SZ+1;
+let
+	a[0] = true;
+	a[1..BIN_SZ] = a[0..BIN_SZ-1] and (x = y);	
+	o = a[BIN_SZ];
+tel
+
+node UsrIntNeq( x : UsrInt; y : UsrInt) returns ( o : bool);
+let
+	o = not UsrIntEq(x,y);
+tel
+
+

salut/lib/UsrIntBinary5.lus

+
+-- to be included BEFORE binary.lus
+-- Signed binary on 5 bits
+-- (range [-15, 15] + nan (0001) 
+
+const BIN_SZ=5;
+
+const UsrInt_0  = [0, 0, 0, 0, 0];
+const UsrInt_1  = [1, 0, 0, 0, 0];
+const UsrInt_2  = [0, 1, 0, 0, 0];
+const UsrInt_3  = [1, 1, 0, 0, 0];
+const UsrInt_4  = [0, 0, 1, 0, 0];
+const UsrInt_5  = [1, 0, 1, 0, 0];
+const UsrInt_6  = [0, 1, 1, 0, 0];
+const UsrInt_7  = [1, 1, 1, 0, 0];
+const UsrInt_8  = [0, 0, 0, 1, 0];
+const UsrInt_9  = [1, 0, 0, 1, 0];
+const UsrInt_10 = [0, 1, 0, 1, 0];
+const UsrInt_11 = [1, 1, 0, 1, 0];
+const UsrInt_12 = [0, 0, 1, 1, 0];
+const UsrInt_13 = [1, 0, 1, 1, 0];
+const UsrInt_14 = [0, 1, 1, 1, 0];
+const UsrInt_15 = [1, 1, 1, 1, 0];

salut/lib/UsrIntCounters.lus

+
+-- UNSIGNED binary 
+/*
+	- modulo max arithmetic (no overflow)
+	- diff with signed :
+		* no csh (indeed)
+		* comparisons
+*/
+
+--const BIN_SZ=5;
+type UsrInt = bool^BIN_SZ;
+
+--const UsrInt_0 = false^BIN_SZ;
+
+
+node UsrIntIf(
+	c : bool; x : UsrInt; y : UsrInt
+) returns (
+	s : UsrInt
+);
+let
+	s = if c^BIN_SZ then x else y;
+tel
+
+node UsrIntPlus( x : UsrInt; y : UsrInt) returns ( s : UsrInt);
+var c : bool^(BIN_SZ+1);
+let
+	c[0] = false;
+	c[1..BIN_SZ] = if c[0..BIN_SZ-1] then (x or y) else (x and y); 
+	s = x xor y xor c[0..BIN_SZ-1];
+tel
+
+node UsrIntMinus( x : UsrInt; y : UsrInt) returns ( s : UsrInt);
+var c : bool^(BIN_SZ+1);
+    ny: UsrInt;
+let
+	c[0] = true;
+	ny = not y;
+	c[1..BIN_SZ] = if c[0..BIN_SZ-1] then (x or ny) else (x and ny); 
+	s = x xor ny xor c[0..BIN_SZ-1];
+tel
+
+
+node UsrIntIncr(x : UsrInt) returns (s : UsrInt);
+var c : bool^(BIN_SZ+1);
+let
+	c[0] = true;
+	c[1..BIN_SZ] = c[0..BIN_SZ-1] and x;	
+	s = c[0..BIN_SZ-1] xor x;
+tel
+
+node UsrIntDecr(x : UsrInt) returns (s : UsrInt);
+var c : bool^(BIN_SZ+1);
+let
+	c[0] = true;
+	c[1..BIN_SZ] = c[0..BIN_SZ-1] and not x;	
+	s = c[0..BIN_SZ-1] xor x;
+tel
+
+node _internal_GT (const sz : int; x, y: bool^sz) returns (o: bool);
+let
+	o = with (sz = 1) then (x[0] and not y[0])
+	    else if (x[sz-1] and not y[sz-1]) then true
+	    else if (not x[sz-1] and y[sz-1]) then false
+	    else _internal_GT(sz-1, x[0..sz-2], y[0..sz-2]);
+tel
+
+node UsrIntGt( x : UsrInt; y : UsrInt) returns ( o : bool);
+let
+	o = _internal_GT(BIN_SZ, x, y);
+tel
+
+node UsrIntLt( x : UsrInt; y : UsrInt) returns ( o : bool);
+let
+	o = UsrIntGt(y,x);
+tel
+
+node UsrIntGte( x : UsrInt; y : UsrInt) returns ( o : bool);
+let
+	o = not UsrIntGt(y,x);
+tel
+
+node UsrIntLte( x : UsrInt; y : UsrInt) returns ( o : bool);
+let
+	o = not UsrIntGt(x,y);
+tel
+
+node UsrIntEq( x : UsrInt; y : UsrInt) returns ( o : bool);
+var
+	a : bool^BIN_SZ+1;
+let
+	a[0] = true;
+	a[1..BIN_SZ] = a[0..BIN_SZ-1] and (x = y);	
+	o = a[BIN_SZ];
+tel
+
+node UsrIntNeq( x : UsrInt; y : UsrInt) returns ( o : bool);
+let
+	o = not UsrIntEq(x,y);
+tel
+
+

salut/lib/UsrIntCounters5.lus

+
+-- to be included BEFORE binary.lus
+-- unigned binary on 5 bits
+-- (range [0, 31])
+
+const BIN_SZ=5;
+
+const UsrInt_0  = [0, 0, 0, 0, 0];
+const UsrInt_1  = [1, 0, 0, 0, 0];
+const UsrInt_2  = [0, 1, 0, 0, 0];
+const UsrInt_3  = [1, 1, 0, 0, 0];
+const UsrInt_4  = [0, 0, 1, 0, 0];
+const UsrInt_5  = [1, 0, 1, 0, 0];
+const UsrInt_6  = [0, 1, 1, 0, 0];
+const UsrInt_7  = [1, 1, 1, 0, 0];
+const UsrInt_8  = [0, 0, 0, 1, 0];
+const UsrInt_9  = [1, 0, 0, 1, 0];
+const UsrInt_10 = [0, 1, 0, 1, 0];
+const UsrInt_11 = [1, 1, 0, 1, 0];
+const UsrInt_12 = [0, 0, 1, 1, 0];
+const UsrInt_13 = [1, 0, 1, 1, 0];
+const UsrInt_14 = [0, 1, 1, 1, 0];
+const UsrInt_15 = [1, 1, 1, 1, 0];
+const UsrInt_16 = [0, 0, 0, 0, 1];
+const UsrInt_17 = [1, 0, 0, 0, 1];
+const UsrInt_18 = [0, 1, 0, 0, 1];
+const UsrInt_19 = [1, 1, 0, 0, 1];
+const UsrInt_20 = [0, 0, 1, 0, 1];
+const UsrInt_21 = [1, 0, 1, 0, 1];
+const UsrInt_22 = [0, 1, 1, 0, 1];
+const UsrInt_23 = [1, 1, 1, 0, 1];
+const UsrInt_24 = [0, 0, 0, 1, 1];
+const UsrInt_25 = [1, 0, 0, 1, 1];
+const UsrInt_26 = [0, 1, 0, 1, 1];
+const UsrInt_27 = [1, 1, 0, 1, 1];
+const UsrInt_28 = [0, 0, 1, 1, 1];
+const UsrInt_29 = [1, 0, 1, 1, 1];
+const UsrInt_30 = [0, 1, 1, 1, 1];
+const UsrInt_31 = [1, 1, 1, 1, 1];

salut/lib/bit-blast/Makefile

+
+
+gen_binary: gen_binary.ml
+	ocamlopt gen_binary.ml -o $@

salut/lib/bit-blast/README.md

+
+Some lustre files that implements int using bool arrays.
+
+Very useful to perform proof with lesar on integers.
\ No newline at end of file

salut/lib/bit-blast/UsrIntChs.ec

+node UsrIntChs
+  (x_0: bool;
+  x_1: bool;
+  x_2: bool;
+  x_3: bool;
+  x_4: bool)
+returns
+  (s_0: bool;
+  s_1: bool;
+  s_2: bool;
+  s_3: bool;
+  s_4: bool);
+
+var
+  V145_c_1: bool;
+  V146_c_2: bool;
+  V147_c_3: bool;
+  V148_c_4: bool;
+  V149_c_5: bool;
+
+let
+  s_0 = (false xor x_0);
+  s_1 = (V145_c_1 xor x_1);
+  s_2 = (V146_c_2 xor x_2);
+  s_3 = (V147_c_3 xor x_3);
+  s_4 = (V148_c_4 xor x_4);
+  V145_c_1 = (false or x_0);
+  V146_c_2 = (V145_c_1 or x_1);
+  V147_c_3 = (V146_c_2 or x_2);
+  V148_c_4 = (V147_c_3 or x_3);
+  V149_c_5 = (V148_c_4 or x_4);
+tel
+