diff --git a/guides/users/README.org b/guides/users/README.org
index 5f08215404c4f8b69788ee8e5a557ab964969ec8..de1916cd04a3816a3d977607f306b4b4a50d6033 100644
--- a/guides/users/README.org
+++ b/guides/users/README.org
@@ -501,7 +501,7 @@ More =sasa= options:
#+end_example
* Interactive simulations
-
+<<interactive-simulations>>
In order to run interactive simulations, one can run =sasa= under the control of
=rdbgui4sasa=. More specifically, instead of running
diff --git a/lib/algo/algo.mli b/lib/algo/algo.mli
index 6b823fc12c5fe9a378f2dfb3c6eb3979a2ec7afc..380c6fca07718dd62586d8b5d1ffa4261f8d39b5 100644
--- a/lib/algo/algo.mli
+++ b/lib/algo/algo.mli
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 26/05/2022 (at 12:16) by Erwan Jahier> *)
+(* Time-stamp: <modified the 21/03/2023 (at 14:20) by Erwan Jahier> *)
(** {1 The Algorithm programming Interface}
A SASA process is an instance of an algorithm defined via this
@@ -179,7 +179,7 @@ val get_graph_attribute_opt : string -> string option
Note that it is not necessary to expose the whole state to the
optimization process. To do that, one just needs to filter some of
the state value in the ['s -> value list] function. This is the
- reason the state reconstruction function ([num list -> 's -> 's])
+ reason the state reconstruction function ([value list -> 's -> 's])
takes a state as argument (to be able to fill the previously
filtered values, that will therefore never change during the
search).
diff --git a/salut/lib/README.org b/salut/lib/README.org
new file mode 100644
index 0000000000000000000000000000000000000000..b4ed70303474962700f8df634374e4a9fe6dfd6f
--- /dev/null
+++ b/salut/lib/README.org
@@ -0,0 +1 @@
+Lustre files useful to define ASM algorithms
diff --git a/salut/lib/UsrIntBinary.lus b/salut/lib/UsrIntBinary.lus
deleted file mode 100644
index 35b4ec5fa6346a5ef338ab716e406a7f0ca8fdce..0000000000000000000000000000000000000000
--- a/salut/lib/UsrIntBinary.lus
+++ /dev/null
@@ -1,100 +0,0 @@
-
--- 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
-
-
diff --git a/salut/lib/UsrIntBinary5.lus b/salut/lib/UsrIntBinary5.lus
deleted file mode 100644
index b1d55c222de03b4ad14e30b64a33411c60e1ddba..0000000000000000000000000000000000000000
--- a/salut/lib/UsrIntBinary5.lus
+++ /dev/null
@@ -1,23 +0,0 @@
-
--- 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];
diff --git a/salut/lib/UsrIntCounters.lus b/salut/lib/UsrIntCounters.lus
deleted file mode 100644
index 248690af6619a870bbfd5e16654e59fb30de6380..0000000000000000000000000000000000000000
--- a/salut/lib/UsrIntCounters.lus
+++ /dev/null
@@ -1,102 +0,0 @@
-
--- 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
-
-
diff --git a/salut/lib/UsrIntCounters5.lus b/salut/lib/UsrIntCounters5.lus
deleted file mode 100644
index a0c686037d78cd1c93e3a0921c72121f57f50630..0000000000000000000000000000000000000000
--- a/salut/lib/UsrIntCounters5.lus
+++ /dev/null
@@ -1,39 +0,0 @@
-
--- 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];
diff --git a/salut/lib/bit-blast/README.md b/salut/lib/bit-blast/README.md
index d299e3cbe9440a670a6a47f5e086119494d56ae4..25af654b4fd784f4a4a925f512e9b96e028adb6c 100644
--- a/salut/lib/bit-blast/README.md
+++ b/salut/lib/bit-blast/README.md
@@ -1,4 +1,4 @@
Some lustre files that implements int using bool arrays.
-Very useful to perform proof with lesar on integers.
\ No newline at end of file
+Useful to perform proof with lesar on integers.
diff --git a/salut/lib/bit-blast/UsrIntChs.ec b/salut/lib/bit-blast/UsrIntChs.ec
deleted file mode 100644
index 3136d796062423e61af340dfad6de2b2d7ccb223..0000000000000000000000000000000000000000
--- a/salut/lib/bit-blast/UsrIntChs.ec
+++ /dev/null
@@ -1,33 +0,0 @@
-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
-
diff --git a/salut/lib/bit-blast/UsrIntLt.ec b/salut/lib/bit-blast/UsrIntLt.ec
deleted file mode 100644
index 6540c43ffe32b576aa6b2c4ae54e9cb0fe8e330b..0000000000000000000000000000000000000000
--- a/salut/lib/bit-blast/UsrIntLt.ec
+++ /dev/null
@@ -1,78 +0,0 @@
-node UsrIntLt
- (x_0: bool;
- x_1: bool;
- x_2: bool;
- x_3: bool;
- x_4: bool;
- x_5: bool;
- x_6: bool;
- y_0: bool;
- y_1: bool;
- y_2: bool;
- y_3: bool;
- y_4: bool;
- y_5: bool;
- y_6: bool)
-returns
- (o: bool);
-
-var
- V421_z_0: bool;
- V422_z_1: bool;
- V423_z_2: bool;
- V424_z_3: bool;
- V425_z_4: bool;
- V426_z_5: bool;
- V427_c_1: bool;
- V428_c_2: bool;
- V429_c_3: bool;
- V430_c_4: bool;
- V431_c_5: bool;
- V432_c_6: bool;
- V433_c_7: bool;
- V434_c_1: bool;
- V435_c_2: bool;
- V436_c_3: bool;
- V437_c_4: bool;
- V438_c_5: bool;
- V439_c_6: bool;
- V440_c_7: bool;
- V441_y_0: bool;
- V442_y_1: bool;
- V443_y_2: bool;
- V444_y_3: bool;
- V445_y_4: bool;
- V446_y_5: bool;
- V447_y_6: bool;
-
-let
- o = ((x_6 xor V447_y_6) xor V439_c_6);
- V421_z_0 = ((x_0 xor V441_y_0) xor false);
- V422_z_1 = ((x_1 xor V442_y_1) xor V434_c_1);
- V423_z_2 = ((x_2 xor V443_y_2) xor V435_c_2);
- V424_z_3 = ((x_3 xor V444_y_3) xor V436_c_3);
- V425_z_4 = ((x_4 xor V445_y_4) xor V437_c_4);
- V426_z_5 = ((x_5 xor V446_y_5) xor V438_c_5);
- V427_c_1 = (false or y_0);
- V428_c_2 = (V427_c_1 or y_1);
- V429_c_3 = (V428_c_2 or y_2);
- V430_c_4 = (V429_c_3 or y_3);
- V431_c_5 = (V430_c_4 or y_4);
- V432_c_6 = (V431_c_5 or y_5);
- V433_c_7 = (V432_c_6 or y_6);
- V434_c_1 = (if false then (x_0 or V441_y_0) else (x_0 and V441_y_0));
- V435_c_2 = (if V434_c_1 then (x_1 or V442_y_1) else (x_1 and V442_y_1));
- V436_c_3 = (if V435_c_2 then (x_2 or V443_y_2) else (x_2 and V443_y_2));
- V437_c_4 = (if V436_c_3 then (x_3 or V444_y_3) else (x_3 and V444_y_3));
- V438_c_5 = (if V437_c_4 then (x_4 or V445_y_4) else (x_4 and V445_y_4));
- V439_c_6 = (if V438_c_5 then (x_5 or V446_y_5) else (x_5 and V446_y_5));
- V440_c_7 = (if V439_c_6 then (x_6 or V447_y_6) else (x_6 and V447_y_6));
- V441_y_0 = (false xor y_0);
- V442_y_1 = (V427_c_1 xor y_1);
- V443_y_2 = (V428_c_2 xor y_2);
- V444_y_3 = (V429_c_3 xor y_3);
- V445_y_4 = (V430_c_4 xor y_4);
- V446_y_5 = (V431_c_5 xor y_5);
- V447_y_6 = (V432_c_6 xor y_6);
-tel
-
diff --git a/salut/lib/bit-blast/UsrIntLt.oc b/salut/lib/bit-blast/UsrIntLt.oc
deleted file mode 100644
index b39cf73bc5334a24435bb69c73b2bfda56b03582..0000000000000000000000000000000000000000
--- a/salut/lib/bit-blast/UsrIntLt.oc
+++ /dev/null
@@ -1,356 +0,0 @@
-oc5:
-module: UsrIntLt
-
-signals: 15
- 0: input:x_0 - single:1 bool:0
- 1: input:x_1 - single:2 bool:0
- 2: input:x_2 - single:3 bool:0
- 3: input:x_3 - single:4 bool:0
- 4: input:x_4 - single:5 bool:0
- 5: input:x_5 - single:6 bool:0
- 6: input:x_6 - single:7 bool:0
- 7: input:y_0 - single:8 bool:0
- 8: input:y_1 - single:9 bool:0
- 9: input:y_2 - single:10 bool:0
- 10: input:y_3 - single:11 bool:0
- 11: input:y_4 - single:12 bool:0
- 12: input:y_5 - single:13 bool:0
- 13: input:y_6 - single:14 bool:0
- 14: output:o - single:15
-end:
-
-variables: 16
- 0: $0
- 1: $0
- 2: $0
- 3: $0
- 4: $0
- 5: $0
- 6: $0
- 7: $0
- 8: $0
- 9: $0
- 10: $0
- 11: $0
- 12: $0
- 13: $0
- 14: $0
- 15: $0
-end:
-
-actions: 31
- 0: present: 0
- 1: present: 1
- 2: present: 2
- 3: present: 3
- 4: present: 4
- 5: present: 5
- 6: present: 6
- 7: present: 7
- 8: present: 8
- 9: present: 9
- 10: present: 10
- 11: present: 11
- 12: present: 12
- 13: present: 13
- 14: output: 14
- 15: if: 7
- 16: if: 14
- 17: if: 13
- 18: if: 12
- 19: if: 11
- 20: if: 10
- 21: if: 8
- 22: if: 9
- 23: if: 6
- 24: if: 5
- 25: if: 4
- 26: if: 3
- 27: if: 2
- 28: if: 1
- 29: call:$0 (15) (@$0)
- 30: call:$0 (15) (@$1)
-end:
-
-states: 1
-startpoint: 0
-calls: 4620
-0: 15 ( 16 ( 17 ( 18 ( 19 ( 20 ( 21 ( 22 ( 23 ( 24 ( 25 ( 26 ( 27 ( 28 ( 29 14
-)( 30 14))( 30 14))( 30 14))( 30 14))( 30 14))( 30 14))( 23 ( 24 ( 25 ( 26 ( 27
- ( 29 14)( 28 ( 29 14)( 30 14)))( 30 14))( 30 14))( 30 14))( 30 14)))( 22 ( 23
- ( 24 ( 25 ( 26 ( 27 ( 29 14)( 30 14))( 30 14))( 30 14))( 30 14))( 30 14))( 23
- ( 24 ( 25 ( 26 ( 29 14)( 30 14))( 30 14))( 30 14))( 30 14))))( 21 ( 22 ( 23 (
-24 ( 25 ( 26 ( 29 14)( 27 ( 28 ( 29 14)( 30 14))( 30 14)))( 30 14))( 30 14))(
-30 14))( 23 ( 24 ( 25 ( 26 ( 29 14)( 27 ( 29 14)( 28 ( 29 14)( 30 14))))( 30 14
-))( 30 14))( 30 14)))( 22 ( 23 ( 24 ( 25 ( 26 ( 29 14)( 27 ( 29 14)( 30 14)))(
-30 14))( 30 14))( 30 14))( 23 ( 24 ( 25 ( 29 14)( 30 14))( 30 14))( 30 14)))))(
- 20 ( 21 ( 22 ( 23 ( 24 ( 25 ( 29 14)( 26 ( 27 ( 28 ( 29 14)( 30 14))( 30 14))(
- 30 14)))( 30 14))( 30 14))( 23 ( 24 ( 25 ( 29 14)( 26 ( 27 ( 29 14)( 28 ( 29
-14)( 30 14)))( 30 14)))( 30 14))( 30 14)))( 22 ( 23 ( 24 ( 25 ( 29 14)( 26 ( 27
- ( 29 14)( 30 14))( 30 14)))( 30 14))( 30 14))( 23 ( 24 ( 25 ( 29 14)( 26 ( 29
-14)( 30 14)))( 30 14))( 30 14))))( 21 ( 22 ( 23 ( 24 ( 25 ( 29 14)( 26 ( 29 14
-)( 27 ( 28 ( 29 14)( 30 14))( 30 14))))( 30 14))( 30 14))( 23 ( 24 ( 25 ( 29 14
-)( 26 ( 29 14)( 27 ( 29 14)( 28 ( 29 14)( 30 14)))))( 30 14))( 30 14)))( 22 (
-23 ( 24 ( 25 ( 29 14)( 26 ( 29 14)( 27 ( 29 14)( 30 14))))( 30 14))( 30 14))(
-23 ( 24 ( 29 14)( 30 14))( 30 14))))))( 19 ( 20 ( 21 ( 22 ( 23 ( 24 ( 29 14)(
-25 ( 26 ( 27 ( 28 ( 29 14)( 30 14))( 30 14))( 30 14))( 30 14)))( 30 14))( 23 (
-24 ( 29 14)( 25 ( 26 ( 27 ( 29 14)( 28 ( 29 14)( 30 14)))( 30 14))( 30 14)))(
-30 14)))( 22 ( 23 ( 24 ( 29 14)( 25 ( 26 ( 27 ( 29 14)( 30 14))( 30 14))( 30 14
-)))( 30 14))( 23 ( 24 ( 29 14)( 25 ( 26 ( 29 14)( 30 14))( 30 14)))( 30 14))))(
- 21 ( 22 ( 23 ( 24 ( 29 14)( 25 ( 26 ( 29 14)( 27 ( 28 ( 29 14)( 30 14))( 30 14
-)))( 30 14)))( 30 14))( 23 ( 24 ( 29 14)( 25 ( 26 ( 29 14)( 27 ( 29 14)( 28 (
-29 14)( 30 14))))( 30 14)))( 30 14)))( 22 ( 23 ( 24 ( 29 14)( 25 ( 26 ( 29 14)(
- 27 ( 29 14)( 30 14)))( 30 14)))( 30 14))( 23 ( 24 ( 29 14)( 25 ( 29 14)( 30 14
-)))( 30 14)))))( 20 ( 21 ( 22 ( 23 ( 24 ( 29 14)( 25 ( 29 14)( 26 ( 27 ( 28 (
-29 14)( 30 14))( 30 14))( 30 14))))( 30 14))( 23 ( 24 ( 29 14)( 25 ( 29 14)( 26
- ( 27 ( 29 14)( 28 ( 29 14)( 30 14)))( 30 14))))( 30 14)))( 22 ( 23 ( 24 ( 29
-14)( 25 ( 29 14)( 26 ( 27 ( 29 14)( 30 14))( 30 14))))( 30 14))( 23 ( 24 ( 29
-14)( 25 ( 29 14)( 26 ( 29 14)( 30 14))))( 30 14))))( 21 ( 22 ( 23 ( 24 ( 29 14
-)( 25 ( 29 14)( 26 ( 29 14)( 27 ( 28 ( 29 14)( 30 14))( 30 14)))))( 30 14))( 23
- ( 24 ( 29 14)( 25 ( 29 14)( 26 ( 29 14)( 27 ( 29 14)( 28 ( 29 14)( 30 14)))))
-)( 30 14)))( 22 ( 23 ( 24 ( 29 14)( 25 ( 29 14)( 26 ( 29 14)( 27 ( 29 14)( 30
-14)))))( 30 14))( 23 ( 29 14)( 30 14)))))))( 18 ( 19 ( 20 ( 21 ( 22 ( 23 ( 29
-14)( 24 ( 25 ( 26 ( 27 ( 28 ( 29 14)( 30 14))( 30 14))( 30 14))( 30 14))( 30 14
-)))( 23 ( 29 14)( 24 ( 25 ( 26 ( 27 ( 29 14)( 28 ( 29 14)( 30 14)))( 30 14))(
-30 14))( 30 14))))( 22 ( 23 ( 29 14)( 24 ( 25 ( 26 ( 27 ( 29 14)( 30 14))( 30
-14))( 30 14))( 30 14)))( 23 ( 29 14)( 24 ( 25 ( 26 ( 29 14)( 30 14))( 30 14))(
-30 14)))))( 21 ( 22 ( 23 ( 29 14)( 24 ( 25 ( 26 ( 29 14)( 27 ( 28 ( 29 14)( 30
-14))( 30 14)))( 30 14))( 30 14)))( 23 ( 29 14)( 24 ( 25 ( 26 ( 29 14)( 27 ( 29
-14)( 28 ( 29 14)( 30 14))))( 30 14))( 30 14))))( 22 ( 23 ( 29 14)( 24 ( 25 ( 26
- ( 29 14)( 27 ( 29 14)( 30 14)))( 30 14))( 30 14)))( 23 ( 29 14)( 24 ( 25 ( 29
-14)( 30 14))( 30 14))))))( 20 ( 21 ( 22 ( 23 ( 29 14)( 24 ( 25 ( 29 14)( 26 (
-27 ( 28 ( 29 14)( 30 14))( 30 14))( 30 14)))( 30 14)))( 23 ( 29 14)( 24 ( 25 (
-29 14)( 26 ( 27 ( 29 14)( 28 ( 29 14)( 30 14)))( 30 14)))( 30 14))))( 22 ( 23 (
- 29 14)( 24 ( 25 ( 29 14)( 26 ( 27 ( 29 14)( 30 14))( 30 14)))( 30 14)))( 23 (
-29 14)( 24 ( 25 ( 29 14)( 26 ( 29 14)( 30 14)))( 30 14)))))( 21 ( 22 ( 23 ( 29
-14)( 24 ( 25 ( 29 14)( 26 ( 29 14)( 27 ( 28 ( 29 14)( 30 14))( 30 14))))( 30 14
-)))( 23 ( 29 14)( 24 ( 25 ( 29 14)( 26 ( 29 14)( 27 ( 29 14)( 28 ( 29 14)( 30
-14)))))( 30 14))))( 22 ( 23 ( 29 14)( 24 ( 25 ( 29 14)( 26 ( 29 14)( 27 ( 29 14
-)( 30 14))))( 30 14)))( 23 ( 29 14)( 24 ( 29 14)( 30 14)))))))( 19 ( 20 ( 21 (
-22 ( 23 ( 29 14)( 24 ( 29 14)( 25 ( 26 ( 27 ( 28 ( 29 14)( 30 14))( 30 14))( 30
- 14))( 30 14))))( 23 ( 29 14)( 24 ( 29 14)( 25 ( 26 ( 27 ( 29 14)( 28 ( 29 14)(
- 30 14)))( 30 14))( 30 14)))))( 22 ( 23 ( 29 14)( 24 ( 29 14)( 25 ( 26 ( 27 (
-29 14)( 30 14))( 30 14))( 30 14))))( 23 ( 29 14)( 24 ( 29 14)( 25 ( 26 ( 29 14
-)( 30 14))( 30 14))))))( 21 ( 22 ( 23 ( 29 14)( 24 ( 29 14)( 25 ( 26 ( 29 14)(
-27 ( 28 ( 29 14)( 30 14))( 30 14)))( 30 14))))( 23 ( 29 14)( 24 ( 29 14)( 25 (
-26 ( 29 14)( 27 ( 29 14)( 28 ( 29 14)( 30 14))))( 30 14)))))( 22 ( 23 ( 29 14)(
- 24 ( 29 14)( 25 ( 26 ( 29 14)( 27 ( 29 14)( 30 14)))( 30 14))))( 23 ( 29 14)(
-24 ( 29 14)( 25 ( 29 14)( 30 14)))))))( 20 ( 21 ( 22 ( 23 ( 29 14)( 24 ( 29 14
-)( 25 ( 29 14)( 26 ( 27 ( 28 ( 29 14)( 30 14))( 30 14))( 30 14)))))( 23 ( 29 14
-)( 24 ( 29 14)( 25 ( 29 14)( 26 ( 27 ( 29 14)( 28 ( 29 14)( 30 14)))( 30 14))))
-))( 22 ( 23 ( 29 14)( 24 ( 29 14)( 25 ( 29 14)( 26 ( 27 ( 29 14)( 30 14))( 30
-14)))))( 23 ( 29 14)( 24 ( 29 14)( 25 ( 29 14)( 26 ( 29 14)( 30 14)))))))( 21 (
- 22 ( 23 ( 29 14)( 24 ( 29 14)( 25 ( 29 14)( 26 ( 29 14)( 27 ( 28 ( 29 14)( 30
-14))( 30 14))))))( 23 ( 29 14)( 24 ( 29 14)( 25 ( 29 14)( 26 ( 29 14)( 27 ( 29
-14)( 28 ( 29 14)( 30 14))))))))( 22 ( 23 ( 29 14)( 24 ( 29 14)( 25 ( 29 14)( 26
- ( 29 14)( 27 ( 29 14)( 30 14))))))( 29 14)))))))( 17 ( 18 ( 19 ( 20 ( 21 ( 22
- ( 23 ( 24 ( 25 ( 26 ( 27 ( 28 ( 30 14)( 29 14))( 29 14))( 29 14))( 29 14))( 29
- 14))( 29 14))( 23 ( 24 ( 25 ( 26 ( 27 ( 30 14)( 28 ( 30 14)( 29 14)))( 29 14)
-)( 29 14))( 29 14))( 29 14)))( 22 ( 23 ( 24 ( 25 ( 26 ( 27 ( 30 14)( 29 14))(
-29 14))( 29 14))( 29 14))( 29 14))( 23 ( 24 ( 25 ( 26 ( 30 14)( 29 14))( 29 14)
-)( 29 14))( 29 14))))( 21 ( 22 ( 23 ( 24 ( 25 ( 26 ( 30 14)( 27 ( 28 ( 30 14)(
-29 14))( 29 14)))( 29 14))( 29 14))( 29 14))( 23 ( 24 ( 25 ( 26 ( 30 14)( 27 (
-30 14)( 28 ( 30 14)( 29 14))))( 29 14))( 29 14))( 29 14)))( 22 ( 23 ( 24 ( 25 (
- 26 ( 30 14)( 27 ( 30 14)( 29 14)))( 29 14))( 29 14))( 29 14))( 23 ( 24 ( 25 (
-30 14)( 29 14))( 29 14))( 29 14)))))( 20 ( 21 ( 22 ( 23 ( 24 ( 25 ( 30 14)( 26
- ( 27 ( 28 ( 30 14)( 29 14))( 29 14))( 29 14)))( 29 14))( 29 14))( 23 ( 24 ( 25
- ( 30 14)( 26 ( 27 ( 30 14)( 28 ( 30 14)( 29 14)))( 29 14)))( 29 14))( 29 14))
-)( 22 ( 23 ( 24 ( 25 ( 30 14)( 26 ( 27 ( 30 14)( 29 14))( 29 14)))( 29 14))( 29
- 14))( 23 ( 24 ( 25 ( 30 14)( 26 ( 30 14)( 29 14)))( 29 14))( 29 14))))( 21 (
-22 ( 23 ( 24 ( 25 ( 30 14)( 26 ( 30 14)( 27 ( 28 ( 30 14)( 29 14))( 29 14))))(
-29 14))( 29 14))( 23 ( 24 ( 25 ( 30 14)( 26 ( 30 14)( 27 ( 30 14)( 28 ( 30 14)(
- 29 14)))))( 29 14))( 29 14)))( 22 ( 23 ( 24 ( 25 ( 30 14)( 26 ( 30 14)( 27 (
-30 14)( 29 14))))( 29 14))( 29 14))( 23 ( 24 ( 30 14)( 29 14))( 29 14))))))( 19
- ( 20 ( 21 ( 22 ( 23 ( 24 ( 30 14)( 25 ( 26 ( 27 ( 28 ( 30 14)( 29 14))( 29 14)
-)( 29 14))( 29 14)))( 29 14))( 23 ( 24 ( 30 14)( 25 ( 26 ( 27 ( 30 14)( 28 ( 30
- 14)( 29 14)))( 29 14))( 29 14)))( 29 14)))( 22 ( 23 ( 24 ( 30 14)( 25 ( 26 (
-27 ( 30 14)( 29 14))( 29 14))( 29 14)))( 29 14))( 23 ( 24 ( 30 14)( 25 ( 26 (
-30 14)( 29 14))( 29 14)))( 29 14))))( 21 ( 22 ( 23 ( 24 ( 30 14)( 25 ( 26 ( 30
-14)( 27 ( 28 ( 30 14)( 29 14))( 29 14)))( 29 14)))( 29 14))( 23 ( 24 ( 30 14)(
-25 ( 26 ( 30 14)( 27 ( 30 14)( 28 ( 30 14)( 29 14))))( 29 14)))( 29 14)))( 22 (
- 23 ( 24 ( 30 14)( 25 ( 26 ( 30 14)( 27 ( 30 14)( 29 14)))( 29 14)))( 29 14))(
-23 ( 24 ( 30 14)( 25 ( 30 14)( 29 14)))( 29 14)))))( 20 ( 21 ( 22 ( 23 ( 24 (
-30 14)( 25 ( 30 14)( 26 ( 27 ( 28 ( 30 14)( 29 14))( 29 14))( 29 14))))( 29 14)
-)( 23 ( 24 ( 30 14)( 25 ( 30 14)( 26 ( 27 ( 30 14)( 28 ( 30 14)( 29 14)))( 29
-14))))( 29 14)))( 22 ( 23 ( 24 ( 30 14)( 25 ( 30 14)( 26 ( 27 ( 30 14)( 29 14)
-)( 29 14))))( 29 14))( 23 ( 24 ( 30 14)( 25 ( 30 14)( 26 ( 30 14)( 29 14))))(
-29 14))))( 21 ( 22 ( 23 ( 24 ( 30 14)( 25 ( 30 14)( 26 ( 30 14)( 27 ( 28 ( 30
-14)( 29 14))( 29 14)))))( 29 14))( 23 ( 24 ( 30 14)( 25 ( 30 14)( 26 ( 30 14)(
-27 ( 30 14)( 28 ( 30 14)( 29 14))))))( 29 14)))( 22 ( 23 ( 24 ( 30 14)( 25 ( 30
- 14)( 26 ( 30 14)( 27 ( 30 14)( 29 14)))))( 29 14))( 23 ( 30 14)( 29 14)))))))(
- 18 ( 19 ( 20 ( 21 ( 22 ( 23 ( 30 14)( 24 ( 25 ( 26 ( 27 ( 28 ( 30 14)( 29 14)
-)( 29 14))( 29 14))( 29 14))( 29 14)))( 23 ( 30 14)( 24 ( 25 ( 26 ( 27 ( 30 14
-)( 28 ( 30 14)( 29 14)))( 29 14))( 29 14))( 29 14))))( 22 ( 23 ( 30 14)( 24 (
-25 ( 26 ( 27 ( 30 14)( 29 14))( 29 14))( 29 14))( 29 14)))( 23 ( 30 14)( 24 (
-25 ( 26 ( 30 14)( 29 14))( 29 14))( 29 14)))))( 21 ( 22 ( 23 ( 30 14)( 24 ( 25
- ( 26 ( 30 14)( 27 ( 28 ( 30 14)( 29 14))( 29 14)))( 29 14))( 29 14)))( 23 ( 30
- 14)( 24 ( 25 ( 26 ( 30 14)( 27 ( 30 14)( 28 ( 30 14)( 29 14))))( 29 14))( 29
-14))))( 22 ( 23 ( 30 14)( 24 ( 25 ( 26 ( 30 14)( 27 ( 30 14)( 29 14)))( 29 14)
-)( 29 14)))( 23 ( 30 14)( 24 ( 25 ( 30 14)( 29 14))( 29 14))))))( 20 ( 21 ( 22
- ( 23 ( 30 14)( 24 ( 25 ( 30 14)( 26 ( 27 ( 28 ( 30 14)( 29 14))( 29 14))( 29
-14)))( 29 14)))( 23 ( 30 14)( 24 ( 25 ( 30 14)( 26 ( 27 ( 30 14)( 28 ( 30 14)(
-29 14)))( 29 14)))( 29 14))))( 22 ( 23 ( 30 14)( 24 ( 25 ( 30 14)( 26 ( 27 ( 30
- 14)( 29 14))( 29 14)))( 29 14)))( 23 ( 30 14)( 24 ( 25 ( 30 14)( 26 ( 30 14)(
-29 14)))( 29 14)))))( 21 ( 22 ( 23 ( 30 14)( 24 ( 25 ( 30 14)( 26 ( 30 14)( 27
- ( 28 ( 30 14)( 29 14))( 29 14))))( 29 14)))( 23 ( 30 14)( 24 ( 25 ( 30 14)( 26
- ( 30 14)( 27 ( 30 14)( 28 ( 30 14)( 29 14)))))( 29 14))))( 22 ( 23 ( 30 14)(
-24 ( 25 ( 30 14)( 26 ( 30 14)( 27 ( 30 14)( 29 14))))( 29 14)))( 23 ( 30 14)(
-24 ( 30 14)( 29 14)))))))( 19 ( 20 ( 21 ( 22 ( 23 ( 30 14)( 24 ( 30 14)( 25 (
-26 ( 27 ( 28 ( 30 14)( 29 14))( 29 14))( 29 14))( 29 14))))( 23 ( 30 14)( 24 (
-30 14)( 25 ( 26 ( 27 ( 30 14)( 28 ( 30 14)( 29 14)))( 29 14))( 29 14)))))( 22 (
- 23 ( 30 14)( 24 ( 30 14)( 25 ( 26 ( 27 ( 30 14)( 29 14))( 29 14))( 29 14))))(
-23 ( 30 14)( 24 ( 30 14)( 25 ( 26 ( 30 14)( 29 14))( 29 14))))))( 21 ( 22 ( 23
- ( 30 14)( 24 ( 30 14)( 25 ( 26 ( 30 14)( 27 ( 28 ( 30 14)( 29 14))( 29 14)))(
-29 14))))( 23 ( 30 14)( 24 ( 30 14)( 25 ( 26 ( 30 14)( 27 ( 30 14)( 28 ( 30 14
-)( 29 14))))( 29 14)))))( 22 ( 23 ( 30 14)( 24 ( 30 14)( 25 ( 26 ( 30 14)( 27 (
- 30 14)( 29 14)))( 29 14))))( 23 ( 30 14)( 24 ( 30 14)( 25 ( 30 14)( 29 14)))))
-))( 20 ( 21 ( 22 ( 23 ( 30 14)( 24 ( 30 14)( 25 ( 30 14)( 26 ( 27 ( 28 ( 30 14
-)( 29 14))( 29 14))( 29 14)))))( 23 ( 30 14)( 24 ( 30 14)( 25 ( 30 14)( 26 ( 27
- ( 30 14)( 28 ( 30 14)( 29 14)))( 29 14))))))( 22 ( 23 ( 30 14)( 24 ( 30 14)(
-25 ( 30 14)( 26 ( 27 ( 30 14)( 29 14))( 29 14)))))( 23 ( 30 14)( 24 ( 30 14)(
-25 ( 30 14)( 26 ( 30 14)( 29 14)))))))( 21 ( 22 ( 23 ( 30 14)( 24 ( 30 14)( 25
- ( 30 14)( 26 ( 30 14)( 27 ( 28 ( 30 14)( 29 14))( 29 14))))))( 23 ( 30 14)( 24
- ( 30 14)( 25 ( 30 14)( 26 ( 30 14)( 27 ( 30 14)( 28 ( 30 14)( 29 14))))))))(
-22 ( 23 ( 30 14)( 24 ( 30 14)( 25 ( 30 14)( 26 ( 30 14)( 27 ( 30 14)( 29 14))))
-))( 30 14))))))))( 16 ( 17 ( 18 ( 19 ( 20 ( 21 ( 22 ( 23 ( 24 ( 25 ( 26 ( 27 (
-28 ( 30 14)( 29 14))( 29 14))( 29 14))( 29 14))( 29 14))( 29 14))( 23 ( 24 ( 25
- ( 26 ( 27 ( 30 14)( 28 ( 30 14)( 29 14)))( 29 14))( 29 14))( 29 14))( 29 14))
-)( 22 ( 23 ( 24 ( 25 ( 26 ( 27 ( 30 14)( 29 14))( 29 14))( 29 14))( 29 14))( 29
- 14))( 23 ( 24 ( 25 ( 26 ( 30 14)( 29 14))( 29 14))( 29 14))( 29 14))))( 21 (
-22 ( 23 ( 24 ( 25 ( 26 ( 30 14)( 27 ( 28 ( 30 14)( 29 14))( 29 14)))( 29 14))(
-29 14))( 29 14))( 23 ( 24 ( 25 ( 26 ( 30 14)( 27 ( 30 14)( 28 ( 30 14)( 29 14))
-))( 29 14))( 29 14))( 29 14)))( 22 ( 23 ( 24 ( 25 ( 26 ( 30 14)( 27 ( 30 14)(
-29 14)))( 29 14))( 29 14))( 29 14))( 23 ( 24 ( 25 ( 30 14)( 29 14))( 29 14))(
-29 14)))))( 20 ( 21 ( 22 ( 23 ( 24 ( 25 ( 30 14)( 26 ( 27 ( 28 ( 30 14)( 29 14)
-)( 29 14))( 29 14)))( 29 14))( 29 14))( 23 ( 24 ( 25 ( 30 14)( 26 ( 27 ( 30 14
-)( 28 ( 30 14)( 29 14)))( 29 14)))( 29 14))( 29 14)))( 22 ( 23 ( 24 ( 25 ( 30
-14)( 26 ( 27 ( 30 14)( 29 14))( 29 14)))( 29 14))( 29 14))( 23 ( 24 ( 25 ( 30
-14)( 26 ( 30 14)( 29 14)))( 29 14))( 29 14))))( 21 ( 22 ( 23 ( 24 ( 25 ( 30 14
-)( 26 ( 30 14)( 27 ( 28 ( 30 14)( 29 14))( 29 14))))( 29 14))( 29 14))( 23 ( 24
- ( 25 ( 30 14)( 26 ( 30 14)( 27 ( 30 14)( 28 ( 30 14)( 29 14)))))( 29 14))( 29
-14)))( 22 ( 23 ( 24 ( 25 ( 30 14)( 26 ( 30 14)( 27 ( 30 14)( 29 14))))( 29 14)
-)( 29 14))( 23 ( 24 ( 30 14)( 29 14))( 29 14))))))( 19 ( 20 ( 21 ( 22 ( 23 ( 24
- ( 30 14)( 25 ( 26 ( 27 ( 28 ( 30 14)( 29 14))( 29 14))( 29 14))( 29 14)))( 29
-14))( 23 ( 24 ( 30 14)( 25 ( 26 ( 27 ( 30 14)( 28 ( 30 14)( 29 14)))( 29 14))(
-29 14)))( 29 14)))( 22 ( 23 ( 24 ( 30 14)( 25 ( 26 ( 27 ( 30 14)( 29 14))( 29
-14))( 29 14)))( 29 14))( 23 ( 24 ( 30 14)( 25 ( 26 ( 30 14)( 29 14))( 29 14)))(
- 29 14))))( 21 ( 22 ( 23 ( 24 ( 30 14)( 25 ( 26 ( 30 14)( 27 ( 28 ( 30 14)( 29
-14))( 29 14)))( 29 14)))( 29 14))( 23 ( 24 ( 30 14)( 25 ( 26 ( 30 14)( 27 ( 30
-14)( 28 ( 30 14)( 29 14))))( 29 14)))( 29 14)))( 22 ( 23 ( 24 ( 30 14)( 25 ( 26
- ( 30 14)( 27 ( 30 14)( 29 14)))( 29 14)))( 29 14))( 23 ( 24 ( 30 14)( 25 ( 30
-14)( 29 14)))( 29 14)))))( 20 ( 21 ( 22 ( 23 ( 24 ( 30 14)( 25 ( 30 14)( 26 (
-27 ( 28 ( 30 14)( 29 14))( 29 14))( 29 14))))( 29 14))( 23 ( 24 ( 30 14)( 25 (
-30 14)( 26 ( 27 ( 30 14)( 28 ( 30 14)( 29 14)))( 29 14))))( 29 14)))( 22 ( 23 (
- 24 ( 30 14)( 25 ( 30 14)( 26 ( 27 ( 30 14)( 29 14))( 29 14))))( 29 14))( 23 (
-24 ( 30 14)( 25 ( 30 14)( 26 ( 30 14)( 29 14))))( 29 14))))( 21 ( 22 ( 23 ( 24
- ( 30 14)( 25 ( 30 14)( 26 ( 30 14)( 27 ( 28 ( 30 14)( 29 14))( 29 14)))))( 29
-14))( 23 ( 24 ( 30 14)( 25 ( 30 14)( 26 ( 30 14)( 27 ( 30 14)( 28 ( 30 14)( 29
-14))))))( 29 14)))( 22 ( 23 ( 24 ( 30 14)( 25 ( 30 14)( 26 ( 30 14)( 27 ( 30 14
-)( 29 14)))))( 29 14))( 23 ( 30 14)( 29 14)))))))( 18 ( 19 ( 20 ( 21 ( 22 ( 23
- ( 30 14)( 24 ( 25 ( 26 ( 27 ( 28 ( 30 14)( 29 14))( 29 14))( 29 14))( 29 14))(
- 29 14)))( 23 ( 30 14)( 24 ( 25 ( 26 ( 27 ( 30 14)( 28 ( 30 14)( 29 14)))( 29
-14))( 29 14))( 29 14))))( 22 ( 23 ( 30 14)( 24 ( 25 ( 26 ( 27 ( 30 14)( 29 14)
-)( 29 14))( 29 14))( 29 14)))( 23 ( 30 14)( 24 ( 25 ( 26 ( 30 14)( 29 14))( 29
-14))( 29 14)))))( 21 ( 22 ( 23 ( 30 14)( 24 ( 25 ( 26 ( 30 14)( 27 ( 28 ( 30 14
-)( 29 14))( 29 14)))( 29 14))( 29 14)))( 23 ( 30 14)( 24 ( 25 ( 26 ( 30 14)( 27
- ( 30 14)( 28 ( 30 14)( 29 14))))( 29 14))( 29 14))))( 22 ( 23 ( 30 14)( 24 (
-25 ( 26 ( 30 14)( 27 ( 30 14)( 29 14)))( 29 14))( 29 14)))( 23 ( 30 14)( 24 (
-25 ( 30 14)( 29 14))( 29 14))))))( 20 ( 21 ( 22 ( 23 ( 30 14)( 24 ( 25 ( 30 14
-)( 26 ( 27 ( 28 ( 30 14)( 29 14))( 29 14))( 29 14)))( 29 14)))( 23 ( 30 14)( 24
- ( 25 ( 30 14)( 26 ( 27 ( 30 14)( 28 ( 30 14)( 29 14)))( 29 14)))( 29 14))))(
-22 ( 23 ( 30 14)( 24 ( 25 ( 30 14)( 26 ( 27 ( 30 14)( 29 14))( 29 14)))( 29 14)
-))( 23 ( 30 14)( 24 ( 25 ( 30 14)( 26 ( 30 14)( 29 14)))( 29 14)))))( 21 ( 22 (
- 23 ( 30 14)( 24 ( 25 ( 30 14)( 26 ( 30 14)( 27 ( 28 ( 30 14)( 29 14))( 29 14))
-))( 29 14)))( 23 ( 30 14)( 24 ( 25 ( 30 14)( 26 ( 30 14)( 27 ( 30 14)( 28 ( 30
-14)( 29 14)))))( 29 14))))( 22 ( 23 ( 30 14)( 24 ( 25 ( 30 14)( 26 ( 30 14)( 27
- ( 30 14)( 29 14))))( 29 14)))( 23 ( 30 14)( 24 ( 30 14)( 29 14)))))))( 19 ( 20
- ( 21 ( 22 ( 23 ( 30 14)( 24 ( 30 14)( 25 ( 26 ( 27 ( 28 ( 30 14)( 29 14))( 29
-14))( 29 14))( 29 14))))( 23 ( 30 14)( 24 ( 30 14)( 25 ( 26 ( 27 ( 30 14)( 28 (
- 30 14)( 29 14)))( 29 14))( 29 14)))))( 22 ( 23 ( 30 14)( 24 ( 30 14)( 25 ( 26
- ( 27 ( 30 14)( 29 14))( 29 14))( 29 14))))( 23 ( 30 14)( 24 ( 30 14)( 25 ( 26
- ( 30 14)( 29 14))( 29 14))))))( 21 ( 22 ( 23 ( 30 14)( 24 ( 30 14)( 25 ( 26 (
-30 14)( 27 ( 28 ( 30 14)( 29 14))( 29 14)))( 29 14))))( 23 ( 30 14)( 24 ( 30 14
-)( 25 ( 26 ( 30 14)( 27 ( 30 14)( 28 ( 30 14)( 29 14))))( 29 14)))))( 22 ( 23 (
- 30 14)( 24 ( 30 14)( 25 ( 26 ( 30 14)( 27 ( 30 14)( 29 14)))( 29 14))))( 23 (
-30 14)( 24 ( 30 14)( 25 ( 30 14)( 29 14)))))))( 20 ( 21 ( 22 ( 23 ( 30 14)( 24
- ( 30 14)( 25 ( 30 14)( 26 ( 27 ( 28 ( 30 14)( 29 14))( 29 14))( 29 14)))))( 23
- ( 30 14)( 24 ( 30 14)( 25 ( 30 14)( 26 ( 27 ( 30 14)( 28 ( 30 14)( 29 14)))(
-29 14))))))( 22 ( 23 ( 30 14)( 24 ( 30 14)( 25 ( 30 14)( 26 ( 27 ( 30 14)( 29
-14))( 29 14)))))( 23 ( 30 14)( 24 ( 30 14)( 25 ( 30 14)( 26 ( 30 14)( 29 14))))
-)))( 21 ( 22 ( 23 ( 30 14)( 24 ( 30 14)( 25 ( 30 14)( 26 ( 30 14)( 27 ( 28 ( 30
- 14)( 29 14))( 29 14))))))( 23 ( 30 14)( 24 ( 30 14)( 25 ( 30 14)( 26 ( 30 14)(
- 27 ( 30 14)( 28 ( 30 14)( 29 14))))))))( 22 ( 23 ( 30 14)( 24 ( 30 14)( 25 (
-30 14)( 26 ( 30 14)( 27 ( 30 14)( 29 14))))))( 30 14)))))))( 17 ( 18 ( 19 ( 20
- ( 21 ( 22 ( 23 ( 24 ( 25 ( 26 ( 27 ( 28 ( 29 14)( 30 14))( 30 14))( 30 14))(
-30 14))( 30 14))( 30 14))( 23 ( 24 ( 25 ( 26 ( 27 ( 29 14)( 28 ( 29 14)( 30 14)
-))( 30 14))( 30 14))( 30 14))( 30 14)))( 22 ( 23 ( 24 ( 25 ( 26 ( 27 ( 29 14)(
-30 14))( 30 14))( 30 14))( 30 14))( 30 14))( 23 ( 24 ( 25 ( 26 ( 29 14)( 30 14)
-)( 30 14))( 30 14))( 30 14))))( 21 ( 22 ( 23 ( 24 ( 25 ( 26 ( 29 14)( 27 ( 28 (
- 29 14)( 30 14))( 30 14)))( 30 14))( 30 14))( 30 14))( 23 ( 24 ( 25 ( 26 ( 29
-14)( 27 ( 29 14)( 28 ( 29 14)( 30 14))))( 30 14))( 30 14))( 30 14)))( 22 ( 23 (
- 24 ( 25 ( 26 ( 29 14)( 27 ( 29 14)( 30 14)))( 30 14))( 30 14))( 30 14))( 23 (
-24 ( 25 ( 29 14)( 30 14))( 30 14))( 30 14)))))( 20 ( 21 ( 22 ( 23 ( 24 ( 25 (
-29 14)( 26 ( 27 ( 28 ( 29 14)( 30 14))( 30 14))( 30 14)))( 30 14))( 30 14))( 23
- ( 24 ( 25 ( 29 14)( 26 ( 27 ( 29 14)( 28 ( 29 14)( 30 14)))( 30 14)))( 30 14)
-)( 30 14)))( 22 ( 23 ( 24 ( 25 ( 29 14)( 26 ( 27 ( 29 14)( 30 14))( 30 14)))(
-30 14))( 30 14))( 23 ( 24 ( 25 ( 29 14)( 26 ( 29 14)( 30 14)))( 30 14))( 30 14)
-)))( 21 ( 22 ( 23 ( 24 ( 25 ( 29 14)( 26 ( 29 14)( 27 ( 28 ( 29 14)( 30 14))(
-30 14))))( 30 14))( 30 14))( 23 ( 24 ( 25 ( 29 14)( 26 ( 29 14)( 27 ( 29 14)(
-28 ( 29 14)( 30 14)))))( 30 14))( 30 14)))( 22 ( 23 ( 24 ( 25 ( 29 14)( 26 ( 29
- 14)( 27 ( 29 14)( 30 14))))( 30 14))( 30 14))( 23 ( 24 ( 29 14)( 30 14))( 30
-14))))))( 19 ( 20 ( 21 ( 22 ( 23 ( 24 ( 29 14)( 25 ( 26 ( 27 ( 28 ( 29 14)( 30
-14))( 30 14))( 30 14))( 30 14)))( 30 14))( 23 ( 24 ( 29 14)( 25 ( 26 ( 27 ( 29
-14)( 28 ( 29 14)( 30 14)))( 30 14))( 30 14)))( 30 14)))( 22 ( 23 ( 24 ( 29 14)(
- 25 ( 26 ( 27 ( 29 14)( 30 14))( 30 14))( 30 14)))( 30 14))( 23 ( 24 ( 29 14)(
-25 ( 26 ( 29 14)( 30 14))( 30 14)))( 30 14))))( 21 ( 22 ( 23 ( 24 ( 29 14)( 25
- ( 26 ( 29 14)( 27 ( 28 ( 29 14)( 30 14))( 30 14)))( 30 14)))( 30 14))( 23 ( 24
- ( 29 14)( 25 ( 26 ( 29 14)( 27 ( 29 14)( 28 ( 29 14)( 30 14))))( 30 14)))( 30
-14)))( 22 ( 23 ( 24 ( 29 14)( 25 ( 26 ( 29 14)( 27 ( 29 14)( 30 14)))( 30 14))
-)( 30 14))( 23 ( 24 ( 29 14)( 25 ( 29 14)( 30 14)))( 30 14)))))( 20 ( 21 ( 22 (
- 23 ( 24 ( 29 14)( 25 ( 29 14)( 26 ( 27 ( 28 ( 29 14)( 30 14))( 30 14))( 30 14)
-)))( 30 14))( 23 ( 24 ( 29 14)( 25 ( 29 14)( 26 ( 27 ( 29 14)( 28 ( 29 14)( 30
-14)))( 30 14))))( 30 14)))( 22 ( 23 ( 24 ( 29 14)( 25 ( 29 14)( 26 ( 27 ( 29 14
-)( 30 14))( 30 14))))( 30 14))( 23 ( 24 ( 29 14)( 25 ( 29 14)( 26 ( 29 14)( 30
-14))))( 30 14))))( 21 ( 22 ( 23 ( 24 ( 29 14)( 25 ( 29 14)( 26 ( 29 14)( 27 (
-28 ( 29 14)( 30 14))( 30 14)))))( 30 14))( 23 ( 24 ( 29 14)( 25 ( 29 14)( 26 (
-29 14)( 27 ( 29 14)( 28 ( 29 14)( 30 14))))))( 30 14)))( 22 ( 23 ( 24 ( 29 14)(
- 25 ( 29 14)( 26 ( 29 14)( 27 ( 29 14)( 30 14)))))( 30 14))( 23 ( 29 14)( 30 14
-)))))))( 18 ( 19 ( 20 ( 21 ( 22 ( 23 ( 29 14)( 24 ( 25 ( 26 ( 27 ( 28 ( 29 14)(
- 30 14))( 30 14))( 30 14))( 30 14))( 30 14)))( 23 ( 29 14)( 24 ( 25 ( 26 ( 27 (
- 29 14)( 28 ( 29 14)( 30 14)))( 30 14))( 30 14))( 30 14))))( 22 ( 23 ( 29 14)(
-24 ( 25 ( 26 ( 27 ( 29 14)( 30 14))( 30 14))( 30 14))( 30 14)))( 23 ( 29 14)(
-24 ( 25 ( 26 ( 29 14)( 30 14))( 30 14))( 30 14)))))( 21 ( 22 ( 23 ( 29 14)( 24
- ( 25 ( 26 ( 29 14)( 27 ( 28 ( 29 14)( 30 14))( 30 14)))( 30 14))( 30 14)))( 23
- ( 29 14)( 24 ( 25 ( 26 ( 29 14)( 27 ( 29 14)( 28 ( 29 14)( 30 14))))( 30 14))(
- 30 14))))( 22 ( 23 ( 29 14)( 24 ( 25 ( 26 ( 29 14)( 27 ( 29 14)( 30 14)))( 30
-14))( 30 14)))( 23 ( 29 14)( 24 ( 25 ( 29 14)( 30 14))( 30 14))))))( 20 ( 21 (
-22 ( 23 ( 29 14)( 24 ( 25 ( 29 14)( 26 ( 27 ( 28 ( 29 14)( 30 14))( 30 14))( 30
- 14)))( 30 14)))( 23 ( 29 14)( 24 ( 25 ( 29 14)( 26 ( 27 ( 29 14)( 28 ( 29 14)(
- 30 14)))( 30 14)))( 30 14))))( 22 ( 23 ( 29 14)( 24 ( 25 ( 29 14)( 26 ( 27 (
-29 14)( 30 14))( 30 14)))( 30 14)))( 23 ( 29 14)( 24 ( 25 ( 29 14)( 26 ( 29 14
-)( 30 14)))( 30 14)))))( 21 ( 22 ( 23 ( 29 14)( 24 ( 25 ( 29 14)( 26 ( 29 14)(
-27 ( 28 ( 29 14)( 30 14))( 30 14))))( 30 14)))( 23 ( 29 14)( 24 ( 25 ( 29 14)(
-26 ( 29 14)( 27 ( 29 14)( 28 ( 29 14)( 30 14)))))( 30 14))))( 22 ( 23 ( 29 14)(
- 24 ( 25 ( 29 14)( 26 ( 29 14)( 27 ( 29 14)( 30 14))))( 30 14)))( 23 ( 29 14)(
-24 ( 29 14)( 30 14)))))))( 19 ( 20 ( 21 ( 22 ( 23 ( 29 14)( 24 ( 29 14)( 25 (
-26 ( 27 ( 28 ( 29 14)( 30 14))( 30 14))( 30 14))( 30 14))))( 23 ( 29 14)( 24 (
-29 14)( 25 ( 26 ( 27 ( 29 14)( 28 ( 29 14)( 30 14)))( 30 14))( 30 14)))))( 22 (
- 23 ( 29 14)( 24 ( 29 14)( 25 ( 26 ( 27 ( 29 14)( 30 14))( 30 14))( 30 14))))(
-23 ( 29 14)( 24 ( 29 14)( 25 ( 26 ( 29 14)( 30 14))( 30 14))))))( 21 ( 22 ( 23
- ( 29 14)( 24 ( 29 14)( 25 ( 26 ( 29 14)( 27 ( 28 ( 29 14)( 30 14))( 30 14)))(
-30 14))))( 23 ( 29 14)( 24 ( 29 14)( 25 ( 26 ( 29 14)( 27 ( 29 14)( 28 ( 29 14
-)( 30 14))))( 30 14)))))( 22 ( 23 ( 29 14)( 24 ( 29 14)( 25 ( 26 ( 29 14)( 27 (
- 29 14)( 30 14)))( 30 14))))( 23 ( 29 14)( 24 ( 29 14)( 25 ( 29 14)( 30 14)))))
-))( 20 ( 21 ( 22 ( 23 ( 29 14)( 24 ( 29 14)( 25 ( 29 14)( 26 ( 27 ( 28 ( 29 14
-)( 30 14))( 30 14))( 30 14)))))( 23 ( 29 14)( 24 ( 29 14)( 25 ( 29 14)( 26 ( 27
- ( 29 14)( 28 ( 29 14)( 30 14)))( 30 14))))))( 22 ( 23 ( 29 14)( 24 ( 29 14)(
-25 ( 29 14)( 26 ( 27 ( 29 14)( 30 14))( 30 14)))))( 23 ( 29 14)( 24 ( 29 14)(
-25 ( 29 14)( 26 ( 29 14)( 30 14)))))))( 21 ( 22 ( 23 ( 29 14)( 24 ( 29 14)( 25
- ( 29 14)( 26 ( 29 14)( 27 ( 28 ( 29 14)( 30 14))( 30 14))))))( 23 ( 29 14)( 24
- ( 29 14)( 25 ( 29 14)( 26 ( 29 14)( 27 ( 29 14)( 28 ( 29 14)( 30 14))))))))(
-22 ( 23 ( 29 14)( 24 ( 29 14)( 25 ( 29 14)( 26 ( 29 14)( 27 ( 29 14)( 30 14))))
-))( 29 14)))))))) <0>
-
-end:
-
-endmodule:
\ No newline at end of file
diff --git a/salut/lib/bit-blast/a.out b/salut/lib/bit-blast/a.out
deleted file mode 100755
index a8e822261ff3a0527c09a607b669802dbe85775f..0000000000000000000000000000000000000000
Binary files a/salut/lib/bit-blast/a.out and /dev/null differ
diff --git a/salut/lib/bit-blast/gen_binary b/salut/lib/bit-blast/gen_binary
deleted file mode 100755
index b8a161139fe96403e008b0bad16a073f93429789..0000000000000000000000000000000000000000
Binary files a/salut/lib/bit-blast/gen_binary and /dev/null differ
diff --git a/salut/lib/daemon.lus b/salut/lib/daemon.lus
new file mode 100644
index 0000000000000000000000000000000000000000..f7404b1b73842724717566aadf6d7414700d2582
--- /dev/null
+++ b/salut/lib/daemon.lus
@@ -0,0 +1,132 @@
+-- Defines various daemons (recognizers and generators)
+
+include "utils.lus"
+include "bitset.lus"
+
+--------------------------------------------------------------------------------------------
+-- recognizers
+-- |A| >= 1 for non-silent states.
+function daemon_is_distributed<<const an:int; const pn:int>>(acti, enab : bool^an^pn)
+returns (ok : bool);
+let
+ ok = daemon_is_valid<<an, pn>>(acti, enab)
+ and (silent<<an,pn>>(enab) or boolred<<1,pn,pn>>(map<<boolany<<an>>, pn>>(acti)));
+tel;
+
+-- Exactly one node is activated.
+function daemon_is_central<<const an:int; const pn:int>>(acti, enab : bool^an^pn)
+returns (ok : bool);
+let
+ ok = daemon_is_valid<<an, pn>>(acti, enab)
+ and (silent<<an,pn>>(enab) or boolred<<1,1,pn>>(map<<boolany<<an>>, pn>>(acti)));
+
+tel;
+
+-- No two neighboring nodes are active at once.
+function daemon_is_locally_central<<const an:int; const pn:int>>(
+ acti, enab : bool^an^pn;
+ adjacency : bool^pn^pn
+) returns (ok : bool);
+var
+ active : bool ^ pn;
+ active_adjacencies : bool ^ pn ^ pn;
+ no_active_adjacencies : bool ^ pn;
+ locally_central : bool ^ pn;
+let
+ active = map<<boolany<<an>>, pn>>(acti);
+ active_adjacencies = map<<inter<<pn>>, pn>>(active^pn, adjacency);
+ no_active_adjacencies = map<<boolnone<<pn>>, pn>>(active_adjacencies);
+ locally_central = map<<=>,pn>>(active, no_active_adjacencies);
+ ok = daemon_is_distributed<<an,pn>>(acti, enab)
+ and boolall<<pn>>(locally_central);
+tel;
+
+
+-- All enabled nodes are activated.
+function daemon_is_synchronous<<const an:int; const pn:int>>(acti, enab : bool^an^pn)
+returns (ok:bool);
+let
+ ok = (acti = enab);
+tel;
+
+--------------------------------------------------------------------------------------------
+-- generators
+
+-- the i in input is used to get random numbers from daemons; it
+-- should not be necessary for the synchronous daemon, but it makes
+-- it more homogeneous to have the same interface for all daemons.
+function synchronous<<const an:int; const pn:int>>(i:int; enab : bool^an^pn)
+returns (acti: bool^an^pn);
+let
+ acti = enab;
+tel;
+
+function central<<const an:int; const pn:int>>(i:int;enab : bool^an^pn)
+returns (acti : bool^an^pn);
+var
+ rng, temp, nb_enab:int;
+let
+ nb_enab = red<<if_true_add_1<<an>>,pn>>(0,enab);
+ rng = i mod (if nb_enab = 0 then pn else nb_enab);
+ temp,acti = fillred<<make_activ_tab<<an>>,pn>>(rng,enab);
+tel;
+function test_central = central<<1,7>>
+
+function make_activ_tab<<const an:int>>(ain:int; elem:bool^an)
+returns(aout:int; res:bool^an);
+var
+ elem_is_true:bool;
+let
+ elem_is_true = boolany<<an>>(elem);
+ res= if elem_is_true and (ain=0) then elem else false^an; -- hyp: at most 1 action/process is enab
+ aout = if elem_is_true then ain-1 else ain;
+tel;
+
+function if_true_add_1<<const an:int>>(ain: int; elem: bool^an)
+returns(aout : int);
+let
+ aout= if boolany<<an>>(elem) then ain+1 else ain;
+tel;
+
+-- function distributed<<const an:int; const pn:int>>(enab : bool^an^pn)
+-- returns (acti : bool^an^pn);
+-- var
+-- nb_enab,rng:int;
+-- XXX todo
+
+
+--------------------------------------------------------------------------------------------
+-- utils
+
+-- No nodes enabled, the network is silent.
+function silent<<const an:int; const pn:int>>(enab: bool^an^pn)
+returns (ok : bool);
+let
+ ok = boolnone<<pn>>(map<<boolany<<an>>, pn>>(enab));
+tel;
+
+-- All nodes enabled.
+function all_active<<const an:int; const pn:int>>(enab: bool^an^pn)
+returns (ok : bool);
+let
+ ok = boolall<<pn>>(map<<boolany<<an>>, pn>>(enab));
+tel;
+
+-- Any activation Ai implies Ei was previously enabled.
+function activation_is_valid<<const an:int>>(acti, enab : bool^an) returns (ok : bool);
+let
+ ok = boolall<<an>>(map<<=>,an>>(acti, enab));
+tel;
+
+function daemon_is_valid<<const an:int; const pn:int>>(acti, enab : bool^an^pn)
+returns (ok : bool);
+let
+ ok = boolall<<pn>>(map<<activation_is_valid<<an>>, pn>>(acti, enab));
+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<<boolany<<an>>, pn>>(acti)));
+tel;
diff --git a/salut/lib/sas.lus b/salut/lib/sas.lus
deleted file mode 100644
index 78654684cf3660f67f9d8d2776c7089693273d22..0000000000000000000000000000000000000000
--- a/salut/lib/sas.lus
+++ /dev/null
@@ -1,86 +0,0 @@
-include "utils.lus"
-include "bitset.lus"
--- include "../../test/lustre/round.lus"
-
--- No nodes enabled, the network is silent.
-function silent<<const an:int; const pn:int>>(enab: bool^an^pn)
-returns (y : bool);
-let
- y = boolnone<<pn>>(map<<boolany<<an>>, pn>>(enab));
-tel;
-
--- All nodes enabled.
-function all_active<<const an:int; const pn:int>>(enab: bool^an^pn)
-returns (y : bool);
-let
- y = boolall<<pn>>(map<<boolany<<an>>, pn>>(enab));
-tel;
-
--- Any activation Ai implies Ei was previously enabled.
-function activation_is_valid<<const an:int>>(acti, enab : bool^an) returns (y : bool);
-let
- y = boolall<<an>>(map<<=>,an>>(acti, enab));
-tel;
-
-function daemon_is_valid<<const an:int; const pn:int>>(acti, enab : bool^an^pn)
-returns (y : bool);
-let
- y = boolall<<pn>>(map<<activation_is_valid<<an>>, pn>>(acti, enab));
-tel;
-
-
--- |A| >= 1 for non-silent states.
-function daemon_is_distributed<<const an:int; const pn:int>>(acti, enab : bool^an^pn)
-returns (y : bool);
-let
- y = daemon_is_valid<<an, pn>>(acti, enab)
- and (silent<<an,pn>>(enab) or boolred<<1,pn,pn>>(map<<boolany<<an>>, pn>>(acti)));
-tel;
-
-(*function distributed<<const an:int; const pn:int>>(enab : bool^an^pn)
-returns (acti : bool^an^pn);
-var
- nb_enab,rng:int;*)
--- Exactly one node is activated.
-function daemon_is_central<<const an:int; const pn:int>>(acti, enab : bool^an^pn)
-returns (y : bool);
-let
- y = daemon_is_valid<<an, pn>>(acti, enab)
- and (silent<<an,pn>>(enab) or boolred<<1,1,pn>>(map<<boolany<<an>>, pn>>(acti)));
-
-tel;
-
--- No two neighboring nodes are active at once.
-function daemon_is_locally_central<<const an:int; const pn:int>>(
- acti, enab : bool^an^pn;
- adjacency : bool^pn^pn
-) returns (y : bool);
-var
- active : bool ^ pn;
- active_adjacencies : bool ^ pn ^ pn;
- no_active_adjacencies : bool ^ pn;
- locally_central : bool ^ pn;
-let
- active = map<<boolany<<an>>, pn>>(acti);
- active_adjacencies = map<<inter<<pn>>, pn>>(active^pn, adjacency);
- no_active_adjacencies = map<<boolnone<<pn>>, pn>>(active_adjacencies);
- locally_central = map<<=>,pn>>(active, no_active_adjacencies);
- y = daemon_is_distributed<<an,pn>>(acti, enab)
- and boolall<<pn>>(locally_central);
-tel;
-
-
--- All enabled nodes are activated.
-function daemon_is_synchronous<<const an:int; const pn:int>>(acti, enab : bool^an^pn)
-returns (y:bool);
-let
- y = (acti = enab);
-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<<boolany<<an>>, pn>>(acti)));
-tel;
-
diff --git a/salut/test/Cycle_unison/Sh/search_config.sh b/salut/test/Cycle_unison/Sh/search_config.sh
index c534d7922d0d1acdd7ebc72044bf5cc4346e64a4..abb8b9a4176e22870e3a9e8bbab8b7efbdafca16 100644
--- a/salut/test/Cycle_unison/Sh/search_config.sh
+++ b/salut/test/Cycle_unison/Sh/search_config.sh
@@ -24,22 +24,27 @@ clean(){
rm -f *_check_cycles.lv4
rm -f *.c *.h *_const.lus *.cmt *.exec *.sh rdbg-session* *.log *.pdf
rm -f $k*
- rm k.lus
+ rm -f k.lus
}
+if [ -z ${LV6OPT} ]; then LV6OPT="" ; fi # n: 194400s = 54 hours
if [ -z ${TIMEOUT} ]; then TIMEOUT=194400.; fi # n: 194400s = 54 hours
+if [ -z ${kind2_opt} ]; then kind2_opt ="--modular true --compositional true"; fi # n: 194400s = 54 hours
+
clean $3$n
echo "const k = $k ;" > k.lus
make $topology$n.dot
salut $topology$n.dot
-lv6 -eei ${topology}$n.lus check_cycles.lus $topology${n}_const.lus -n check_cycles -rnc --lustre-v4 -o $topology${n}_check_cycles.noexpand.lv4
-cat $topology${n}_check_cycles.noexpand.lv4 | tr '\n' '@' |sed "s/tel@/tel/g" | sed "s/@/\\n/g" | sed "s/tel-- end of node check_cycles/--%MAIN ;\n--%PROPERTY ok;\ntel\n/" > $topology${n}_check_cycles.noexpand.lv4.tmp
+lv6 ${LV6OPT} -eei ${topology}$n.lus check_cycles.lus $topology${n}_const.lus ../../lib/daemon.lus ../../../test/lustre/round.lus -n check_cycles -rnc --lustre-v4 -o $topology${n}_check_cycles.noexpand.lv4pascal
+cat $topology${n}_check_cycles.noexpand.lv4pascal | tr '\n' '@' |sed "s/tel@/tel/g" | sed "s/@/\\n/g" | sed "s/tel-- end of node check_cycles/--%MAIN ;\n--%PROPERTY ok;\ntel\n/" | sed "s/telnode/tel\\nnode/" > $topology${n}_check_cycles.noexpand.lv4.tmp
+
+
mv $topology${n}_check_cycles.noexpand.lv4.tmp $topology${n}_check_cycles.noexpand.lv4
[ -d Log ] || mkdir Log
-echo "time kind2 --timeout ${TIMEOUT} --color false --modular true --compositional true $topology${n}_check_cycles.noexpand.lv4" > $log
-time kind2 --timeout ${TIMEOUT} --color false --modular true --compositional true $topology${n}_check_cycles.noexpand.lv4 >> $log
+echo "time kind2 --color false ${kind2_opt} $topology${n}_check_cycles.noexpand.lv4" > $log
+time kind2 --color false ${kind2_opt} $topology${n}_check_cycles.noexpand.lv4 >> $log
##############################################################
clean $topology$n
diff --git a/salut/test/Cycle_unison/check_cycles.lus b/salut/test/Cycle_unison/check_cycles.lus
index 9a2e1037ab98c7b7d4ce2a130e9fe27a7ece058e..52f257ecd3f099a0807f7ba1c6270354b94c4df6 100644
--- a/salut/test/Cycle_unison/check_cycles.lus
+++ b/salut/test/Cycle_unison/check_cycles.lus
@@ -1,60 +1,147 @@
-include "../../lib/sas.lus"
-
-
+-- include "../../lib/daemon.lus"
node check_cycles(activations : bool^actions_number^card; inits : state^card) returns (ok : bool);
-var config,mirror_inits : state^card;
+var config : state^card;
var enables : bool^actions_number^card;
-var legitimate, no_loop : bool;
+
+ -- i2 : state^card;
+var legitimate, noloop : bool;
lustre_round : bool;
lustre_round_nb : int;
--- all_permuts: state^card^(card-1);
let
- -- forbid legitimate configurations
- assert(not (legitimate<<actions_number, card>>(enables, inits)));
+ -- forbid legitimate configurations for the initial one
+-- assert(not (legitimate<<actions_number, card>>(enables, inits)));
+
+-- Bad idea in the end
+-- assert(not(exists_a_smaller_rot_mir(inits)));
+
+ -- not necessary, saves a few percents
+-- assert( --rangei_basic<<card-1>>(inits) and
+-- inits[0]=0);
+
+-- assert(rangei<<card-1>>(inits));
+
+ assert(rangei_alt(inits));
+
- --
assert(true -> daemon_is_synchronous<<actions_number,card>>(activations, pre enables));
- assert(rangei<<0,card,k>>(inits));
assert(true -> inits = pre inits);
-
+-- inits = inits0 -> pre(inits);
+
config, enables, lustre_round, lustre_round_nb = topology(activations, inits);
legitimate = legitimate<<actions_number, card>>(enables, config);
- mirror_inits = mirror<<card>>(inits);
-
- no_loop = true -> not (config=inits or
- config=mirror_inits or
- eq_forall_permutations<<card,card-1>>(inits,mirror_inits,config)
- );
- ok = no_loop or legitimate ;
+-- noloop = not (inits = config);
+-- When a no cycle exists, it is better to use rot_mir. Otherwise, no.
+ noloop = not (rot_mir(inits, config));
+ ok = true -> noloop or legitimate;
tel;
---type state = int;
---node test = permutation<<2,3>>;
-function mirror<<const card:int>>(config: state^card) returns (res: state^card);
+-- c1 and c2 are equals up to rotation and mirroring
+function rot_mir(c1, c2:state^card) returns (res:bool);
+let
+ res = rot(c1,c2) or rot(mirror(c1), c2);
+tel
+function rot(c1, c2:state^card) returns (res:bool);
+let
+ res = c1=c2 or rot_rec<<card-1>>(c1,c2);
+tel
+function rot_rec<< const N:int>>(c1, c2:state^card) returns (res:bool);
+var c2_rot:state^card;
+let
+ c2_rot = c2[1..card-1] | [c2[0]];
+ res =
+ with (N=1) then (c1=c2_rot)
+ else (c1=c2_rot) or rot_rec<<N-1>>(c1,c2_rot);
+tel
+
+function mirror<<const card:int >>(config: state^card) returns (res: state^card);
let
res = with (card=1) then [config[0]]
else mirror<<card-1>>(config[1..card-1]) | [config[0]];
tel
-function eq_forall_permutations<< const card:int; const N:int>>
-(inits,mir_inits, c:state^card) returns (res:bool);
-var cp:state^card;
+
+-----------------------------------------------------------------------------------
+node rangei4<<const i:int; const k:int>>(c:state^card) returns (res:bool);
+let
+ res = with i = 0 then c[0] = 0 else
+-- with i <= k then
+ 0 <= c[i] and c[i] <= i and rangei4<<i-1,k>>(c);
+-- else 0 <= c[i] and c[i] <= k and rangei<<i-1,k>>(c);
+tel
+
+function rangei<<const i:int>>(c:state^i+1) returns (res:bool);
+let
+ res = 0 <= c[i] and
+ with i = 0 then c[0]=0
+ else with i < k then rangei<<i-1>>(c[0..i-1]) and c[i] <= i
+ else rangei<<i-1>>(c[0..i-1]) and c[i] <= k ;
+tel
+
+
+type acc = { i:int; res:bool };
+function range_0_k(acc: acc; ci:state) returns (res:acc);
+let
+ res = acc { i = acc.i+1; res = acc.res and 0 <= ci and ci < k};
+tel
+function rangei_alt(c:state^card) returns (res:bool);
+let
+ res = fillred<<range_0_k, card>>(acc {i=0;res=true}, c).res;
+tel
+
+
+
+function rangei_basic<<const i:int>>(c:state^card) returns (res:bool);
let
- cp = c[1..card-1] | [c[0]];
- res =
- with (N=1) then (cp=inits or cp=mir_inits)
- else (cp=inits or cp=mir_inits) or eq_forall_permutations<<card, N-1>>(inits,mir_inits,cp);
+ res = with i < 0 then true
+ else 0 <= c[i] and c[i] <= k and rangei_basic<<i-1>>(c);
tel
+
-- all states are initially in [0; card|[
-node rangei<<const low:int; const card:int; const k:int>>(c:state^card) returns (res:bool);
-var
+function rangeii<<const low:int; const k:int>>(c:state^card) returns (res:bool);
+var
ranges_min, ranges_max : bool^card;
let
ranges_min = map<< <= , card>>(low^card, c);
- ranges_max = map<< < , card>>(c, k^card);
+ ranges_max = map<< <= , card>>(c, k^card);
res = boolall<<card>>(ranges_min) and boolall<<card>>(ranges_max);
tel
+
+
+-----------------------------------------------------------------------------------
+-- unused
+
+
+function smaller<< const N : int >>(c1,c2:state^N) returns (res:bool);
+let
+ res = with (N=1) then (c1[0] < c2[0])
+ else (c1[0] < c2[0]) or (c1[0]=c2[0] and smaller<<N-1>>(c1[1..N-1], c2[1..N-1]));
+
+tel
+
+function exists_a_smaller_rot_mir(c1:state^card) returns (res:bool);
+var
+ c2 : state^card;
+let
+ c2 = mirror(c1);
+ res = smaller<<card>>(c2, c1) or exists_a_smaller_rot(c1, c1)
+ or exists_a_smaller_rot(c1, c2);
+tel
+
+-- there exists a rotation of c2 that is smaller than c1
+function exists_a_smaller_rot(c1, c2:state^card) returns (res:bool);
+let
+ res = exists_a_smaller_rot_rec<<card-1>>(c1, c2);
+tel
+-- there exists a rotation (among N) of c2 that is smaller than c1
+function exists_a_smaller_rot_rec<< const N:int>>(c1, c2:state^card) returns (res:bool);
+var c2_rot:state^card;
+let
+ c2_rot = c2[1..card-1] | [c2[0]];
+ res =
+ with (N=1) then smaller<<card>>(c2_rot, c1)
+ else smaller<<card>>(c2_rot, c1) or exists_a_smaller_rot_rec<<N-1>>(c1,c2_rot);
+tel
diff --git a/salut/test/Makefile.inc b/salut/test/Makefile.inc
index b18391744efcfe6208deb2035976f93da630c88f..2b298c840669349eeeccea14124de5f9aec8f9a3 100644
--- a/salut/test/Makefile.inc
+++ b/salut/test/Makefile.inc
@@ -37,57 +37,13 @@ OCAMLOPT=ocamlfind ocamlopt -bin-annot
ROOTDIR=$(shell git rev-parse --show-toplevel || echo $(CI_PROJECT_DIR))
-LIB_LUS=$(ROOTDIR)/test/lustre/round.lus $(ROOTDIR)/salut/lib/sas.lus
+LIB_LUS=$(ROOTDIR)/test/lustre/round.lus $(ROOTDIR)/salut/lib/daemon.lus
RUN_KIND2=$(ROOTDIR)/salut/test/run-kind2.sh
-##########################################################################################"
-# Simulations
-
-%.simu:
- make $*.dot $*_const.lus
- luciole-rif lv6 $(LIB_LUS) $*.lus $*_const.lus -n $* -exec
-
-%.rdbg: %.cma
- make $*_const.lus
- rdbg -l 10000 -sut-nd "lv6 $(LIB_LUS) $*_const.lus $*.lus -n $* -exec"
-
-%.rdbgui: %.cma
- make $*_const.lus
- rdbgui4sasa -l 10000 -sut-nd "lv6 $(LIB_LUS) $*_const.lus $*.lus -n $* -exec"
-
-##########################################################################################"
-# Use lurette to compare the lustre and the ocaml version of the algorithm
-# nb : the <dirname>/<dirname>_oracle.lus should exist and contain a valid oracle
-
-%.lurette:
- make $*.dot $*_const.lus $*.cmxs $*_oracle.lus
- lurette -sut "sasa -seed 172317971 $*.dot $(SASAFLAGS)" -oracle "lv6 $(LIB_LUS) $*.lus $*_oracle.lus -n oracle -2c-exec"
-
-%.lurette_no_seed:
- make $*.dot $*_const.lus $*.cmxs $*_oracle.lus
- lurette -sut "sasa $*.dot $(SASAFLAGS)" -oracle "lv6 $(LIB_LUS) $*.lus $*_oracle.lus -n oracle -2c-exec"
-
-### now built by dune
-#%.cmxs: %.ml
-# $(OCAMLOPT) $(LIB) -shared state.ml $(shell sasa -algo $*.dot) config.ml $< -o $@
-
-%.cmxs: %.dot
- topology=$* dune build
-%.cma: %.dot
- topology=$* dune build
-
-
-%_oracle.lus: %.cmxs
- sasa -glos $*.dot || echo ""
-
-### now built by dune
-# %.ml: %.dot
-# sasa -reg $<
-
##########################################################################################"
# model-checking with kind2
-# nb: it's probably better to use $(ROOTDIR)/salut/run-kind2.sh instead
+# nb: it's probably better to use $(ROOTDIR)/salut/test/run-kind2.sh instead
ifndef $(prop)
prop = verify
@@ -107,24 +63,14 @@ else
TIME=
endif
-%.expand.kind2: %_verify.lv4
- $(TIME) kind2 --color $(color) $(kind2_opt) $<
-
-
-%.kind2:
- make $*.dot
- make $*_const.lus
- make $*.verify.int8.lv4
- $(TIME) kind2 --color $(color) $(kind2_opt) $*.verify.int8.lv4
-
-%.kind2-test:
- make color=false $*.kind2 | (grep "^ok: valid" > $*-kind2.res || echo "") ; [ -s $*-kind2.res ]
-# XXX: this method of adding kind2 annotations is brittle
+# From lustre v6 to to lustre v4 (to be able to use kind2 and lesar)
+# nb: This method of adding kind2 annotations is brittle
%.verify.lv4: %_const.lus %.lus verify.lus
lv6 -eei $(LIB_LUS) $*.lus $^ $*_const.lus -n $(prop) --lustre-v4 -en -o $@
sed -i -e "s/tel/--%MAIN ;\n--%PROPERTY ok;\ntel/" $@
+# replace int by int8 (for kind2)
%.verify.int8.lv4: %.verify.lv4
cat $^ | \
sed -r "s/[ =](\[)?((-)?[[:digit:]]+)/ \1(int8 \2)/g" | \
@@ -132,6 +78,53 @@ endif
sed -r "s/:int/:int8/g" \
> $@
+# run kind2
+%.kind2:
+ make $*.dot
+ make $*_const.lus
+ make $*.verify.int8.lv4
+ $(TIME) kind2 --color $(color) $(kind2_opt) $*.verify.int8.lv4
+
+%.kind2-test:
+ make color=false $*.kind2
+
+##########################################################################################"
+# Simulates the Lustre algo with rdbgui4sasa
+
+%.simu:
+ make $*.rdbgui4sasa
+%.rdbgui4sasa: %.cma
+ make $*_const.lus
+ rdbgui4sasa -l 10000 -sut-nd "lv6 $(LIB_LUS) $*_const.lus $*.lus -n $* -exec"
+
+##########################################################################################"
+# Use lurette to compare the lustre and the ocaml version of the algorithm
+# nb : the <dirname>/<dirname>_oracle.lus should exist and contain a valid oracle
+
+%.lurette:
+ make $*.dot $*_const.lus $*.cmxs $*_oracle.lus
+ lurette -sut "sasa -seed 172317971 $*.dot $(SASAFLAGS)" -oracle "lv6 $(LIB_LUS) $*.lus $*_oracle.lus -n oracle -2c-exec"
+
+# ditto, without a seed
+%.lurette_no_seed:
+ make $*.dot $*_const.lus $*.cmxs $*_oracle.lus
+ lurette -sut "sasa $*.dot $(SASAFLAGS)" -oracle "lv6 $(LIB_LUS) $*.lus $*_oracle.lus -n oracle -2c-exec"
+
+
+%.cmxs: %.dot
+ topology=$* dune build
+%.cma: %.dot
+ topology=$* dune build
+
+
+%_oracle.lus: %.cmxs
+ sasa -glos $*.dot || echo ""
+
+
+##########################################################################################"
+# model-checking with lesar
+
+
# Do not expand nodes
%_verify.noexpand.lv4: verify.lus
make $*_const.lus
@@ -157,7 +150,7 @@ endif
%.lesar:%_verify.ec
- $(TIME)lesar $< $(prop) -forward -states 10000000
+ $(TIME) lesar $< $(prop) -forward -states 10000000
##########################################################################################"
# Compare sasa and salut simulation perf
diff --git a/salut/test/dijkstra-ring/Makefile b/salut/test/dijkstra-ring/Makefile
index ce9f33c2172f5842def1d74045885b2e419b10c7..43a6883ce91c41fcc9e0e257ba4bc8c061f612b1 100644
--- a/salut/test/dijkstra-ring/Makefile
+++ b/salut/test/dijkstra-ring/Makefile
@@ -13,7 +13,7 @@ include ./Makefile.dot
test: diring3.kind2-test diring4.lurette
clean: genclean
- rm -f diring*.* ring*.*
+ rm -f diring*.* ring*.*
##############################################################################
# Other examples of use
@@ -23,7 +23,7 @@ clean: genclean
# run a simulation with luciole
simu: diring4.simu
-# Compare the ocaml version with the lustre one
+# Compare the ocaml version with the lustre one
compare: diring4.lurette
cat dijkstra-ring.rif
diff --git a/salut/test/dijkstra-ring/cost.lus b/salut/test/dijkstra-ring/cost.lus
index 13d94acc8cc3c8c49689af2d40902f5c91c7ef4c..bec06fca0b0ec96b9a3191514b10dbae9fee31ff 100644
--- a/salut/test/dijkstra-ring/cost.lus
+++ b/salut/test/dijkstra-ring/cost.lus
@@ -1,5 +1,5 @@
--- By convention, the root is node 0.
+-- By convention, the root is node 0.
function is_root(pid: int) returns (res:bool);
let
res = (pid = 0);
@@ -7,7 +7,7 @@ tel
-- Computes the value Z of the book, that is 0 if the values are convex,
-- and the minimum number of incrementations the root has to do so that its value
--- is different to every other value of the ring.
+-- is different to every other value of the ring.
-- A configuration is convex if there is no value that is the same than the root seperated from the
-- root with another value.
-- 2 2 2 3 0 1 3 -> convex, z=0
@@ -21,7 +21,7 @@ var
free: bool^card;
smallest_incre, _i:int;
index:int^card;
-let
+let
acc0 = acc_t {is_root=true;convex=true; root_val=config[0]; pval_dif=false };
acc_end = red<<iter_z, card>>(acc0, config);
@@ -44,7 +44,7 @@ type idx_conf = {
function get_smallest_incre(acc:int; idx:int; root_val: int; free:bool) returns (nacc:int);
let
- nacc = if free
+ nacc = if free
then mini(acc, if root_val<idx then idx-root_val else idx-root_val+card)
else acc;
tel
@@ -57,17 +57,17 @@ tel
type acc_t = {
is_root : bool;
- convex : bool;
- root_val: int; -- constant
+ convex : bool;
+ root_val: int; -- constant
pval_dif: bool; -- exists j <= curr_idx s.t. config[j] <> config[0]
};
function iter_z(acc:acc_t; curval : int) returns (res:acc_t);
let
- res =
- acc_t{
+ res =
+ acc_t{
is_root = false;
- convex = acc.convex and not (acc.pval_dif and acc.root_val = curval);
- root_val = acc.root_val;
+ convex = acc.convex and not (acc.pval_dif and acc.root_val = curval);
+ root_val = acc.root_val;
pval_dif = acc.pval_dif or acc.root_val <> curval
};
tel
@@ -80,7 +80,7 @@ var
enabled_process: bool^card;
dist_root: int^card;
_d:int;
-let
+let
enabled_process = map<<n_or<<actions_number>>,card>> (enabled_actions);
_d, dist_root = fill<<decr,card>>(card); -- [0; card-1; card-2; ...; 2; 1]
res= red<<root_distance, card>>(0, dist_root, enabled_process);
diff --git a/salut/test/dijkstra-ring/root.lus b/salut/test/dijkstra-ring/root.lus
index dc6fef20ea606985ec108090065e0531c782cbf5..99b7c193363117a28be90fac4a27ce8a2b8a6f0c 100644
--- a/salut/test/dijkstra-ring/root.lus
+++ b/salut/test/dijkstra-ring/root.lus
@@ -10,9 +10,10 @@ function root_step<<const degree:int>>(
action : action)
returns (new : state);
let
--- new = (this + 1) mod card;
+ new = (this + 1) mod (card+1);
-- to be able to use lesar (via ec2ec -usrint)
- new = if this = card then 0 else (this + 1);
-tel;
+-- new = if this = card then 0 else (this + 1);
+-- new = this + 1;
+tel;
diff --git a/salut/test/dijkstra-ring/verify.lus b/salut/test/dijkstra-ring/verify.lus
index ac7b6d4781f7d10d6924e1bc6fc84ac06dc1cd48..b628fedb35995f0a03c6e4f99c253f64ccec7b93 100644
--- a/salut/test/dijkstra-ring/verify.lus
+++ b/salut/test/dijkstra-ring/verify.lus
@@ -1,23 +1,30 @@
include "cost.lus"
-const worst_case=3*card*(card-1) div 2 - card - 1;
+
+const n = card;
+
+-- Theorem 6.30 p76 in [zebook]
+const worst_case = n*(n-1) + (n-4)*(n+1) div 2 + 1;
+
+-- const worst_case=3*n*(n-1) div 2 - card - 1;
node verify(
- active : bool^actions_number^card;
+ active : bool^actions_number^card;
init_config : state^card
-)
+)
returns (ok : bool);
var
config : state^card;
enabled : bool^actions_number^card;
- legitimate, at_least_1, closure, converge, theorem : bool;
+ legitimate, at_least_1, closure, converge, theorem, worst_case_is_tigth : bool;
steps, cost : int;
round:bool; round_nb:int;
let
--- assert(true -> daemon_is_central<<actions_number,card>>(active, pre enabled));
- assert(true -> daemon_is_distributed<<actions_number,card>>(active, pre enabled));
+-- the worst-case in necessarily central
+ assert(true -> daemon_is_central<<actions_number,card>>(active, pre enabled));
+-- assert(true -> daemon_is_distributed<<actions_number,card>>(active, pre enabled));
-- assert(true -> daemon_is_synchronous<<actions_number,card>>(active, pre enabled));
- assert(rangei<<0,card>>(init_config));
+ assert(rangei<<0,card>>(init_config));
config, enabled, round, round_nb = topology(active, init_config);
assert(config = init_config -> true);
@@ -28,27 +35,28 @@ let
closure = true -> (pre(legitimate) => legitimate);
- cost = cost(enabled, config);
+ cost = cost(enabled, config);
converge = (true -> legitimate or pre(cost)>cost);
steps = 0 -> (pre(steps) + 1);
- theorem = (steps > worst_case) => legitimate;
- ok = true
+ theorem = (steps >= worst_case) => legitimate;
+
+ worst_case_is_tigth = (steps >= worst_case - 1) => legitimate;
+
+ ok = true
and at_least_1
and closure
and converge
- and theorem -- the worst-case stabilization
- -- and (steps > worst_case - 1) => legitimate -- is tigth!
+ and theorem
;
tel;
function rangei<<const low:int; const card:int>>(c:state^card) returns (res:bool);
-var
+var
ranges_min, ranges_max : bool^card;
let
ranges_min = map<< <= , card>>(low^card, c);
ranges_max = map<< < , card>>(c, card^card);
res = boolall<<card>>(ranges_min) and boolall<<card>>(ranges_max);
tel
-
diff --git a/salut/test/gen-salut-batch.sh b/salut/test/gen-salut-batch.sh
index 5b94c197663b1df1cdafec2f93f0722bb6d3fbc8..11a85d921e13c979c338568aeb96bb041203fd69 100755
--- a/salut/test/gen-salut-batch.sh
+++ b/salut/test/gen-salut-batch.sh
@@ -1,8 +1,8 @@
-#!/bin/bash
+#!/bin/bash
#set -x
GITROOT=$(git rev-parse --show-toplevel)
-LIB_LUS="${GITROOT}/test/lustre/round.lus ${GITROOT}/salut/lib/sas.lus"
+LIB_LUS="${GITROOT}/test/lustre/round.lus ${GITROOT}/salut/lib/daemon.lus"
daemon_lustre_file=${GITROOT}/salut/lib/daemon.lus
help=" Generate a (standalone) lustre program that runs salut with a lustre daemon
@@ -73,7 +73,7 @@ salut ${dotfile}
# XXX state should me made of an integer
config_init=`printf "["; for ((a=1; a < $size ; a++)) do printf "%d," $RANDOM; done; printf "%d]" $RANDOM`
-timestamp=`date +"%d/%m/%Y- %H:%M:%S"`
+timestamp=`date +"%d/%m/%Y- %H:%M:%S"`
printf "(* Automatically generated ($timestamp) by '$0 $*' *)
include \"${daemon_lustre_file}\"
@@ -95,14 +95,13 @@ The file '$outfile' has been generated.
To run simulations, you can generate an executable:
lv6 -2c -cc $outfile -n ${main_node} ${LIB_LUS} -dir ${main_node}
-
+
and run it:
- ./${main_node}.exec
+ ./${main_node}.exec
or, to avoid the need to provide the dummy input:
(for i in {1..10}; do echo $((((1<<15)| RANDOM))); done ; echo q) | ./${main_node}.exec
(for i in {1..10}; do echo $((((1<<15)| RANDOM))); done ; echo q) | time ./${main_node}.exec > /dev/null
"
-
diff --git a/salut/test/run-kind2.sh b/salut/test/run-kind2.sh
index 2692b014f21a276b54143f55c998d72d41109380..8e34bd26889616e1fd0a03b77377bd5ebfa12acc 100755
--- a/salut/test/run-kind2.sh
+++ b/salut/test/run-kind2.sh
@@ -1,36 +1,93 @@
-#!/bin/bash
-set -x
+#!/bin/bash
+#set -x
GITROOT=$(git rev-parse --show-toplevel)
-LIB_LUS="${GITROOT}/test/lustre/round.lus ${GITROOT}/salut/lib/sas.lus"
+LIB_LUS="${GITROOT}/test/lustre/round.lus ${GITROOT}/salut/lib/daemon.lus"
+
+help="This script calls kind2 to model-check the algoritm of the current dir
+(meant to be run from one of the salut/test/*/ directories).
-help="
usage:
- $0 topology n [property]
+ $0 topology n [[[property] [int]] [solver]]
where:
- topology is one of graph supported by gg (ring, diring, grid, etc.)
- - n is the size of the topology [*]
- - property is one of the verify node (in verify.lus) variable (ok by default)
-
-[*] except for grids, where the size of the topology would be n*n
-
+ - n is the size of the topology [1]
+ - property is one of the verify node variable (in verify.lus) (ok by default)
+ - int is in {int, int8, uint8, int16, uint16, ..., uinit64} [2] (int by default)
+ - solver is in {Z3, Bitwuzla, cvc5, MathSAT, Yices, Yices2} [3] (Bitwuzla by default)
+
+example of use:
+ $0 diring 5
+ $0 diring 5 theorem
+ $0 diring 5 theorem int8
+ $0 diring 5 theorem int8 Z3
+
+[1] except for grids, where the size of the topology is n*n
+[2] int means natural numbers (infinite)
+ uint8 : 0 to 255
+ uint16 : 0 to 65535
+ uint32 : 0 to 4294967295
+ uint64 : 0 to 18446744073709551615
+ int8 : -128 to 127
+ int16 : -32768 to 32767
+ int32 : -2147483648 to 2147483647
+ int64 : -9223372036854775808 to 9223372036854775807
+[3] cf kind2 documentation
"
-# 2 arguments only
+#### Dealing with CL arguments
+# at least 2 arguments are required
if [[ $# < 2 ]]
then
printf "$help"
exit 2
elif [[ $# == 2 ]]
then
- prop=ok
+ topology=$1
+ n=$2
+ main=$1$2
+ prop=ok
+ int=int
+ solver=Bitwuzla
+ shift
+ shift
+ elif [[ $# == 3 ]]
+ then
+ topology=$1
+ n=$2
+ main=$1$2
+ prop=$3
+ int=int
+ solver=Bitwuzla
+ shift
+ shift
+ shift
+ elif [[ $# == 4 ]]
+ then
+ topology=$1
+ n=$2
+ main=$1$2
+ prop=$3
+ int=$4
+ solver=Bitwuzla
+ shift
+ shift
+ shift
+ shift
else
+ topology=$1
+ n=$2
+ main=$1$2
prop=$3
+ int=$4
+ solver=$5
+ shift
+ shift
+ shift
+ shift
+ shift
fi
-topology=$1
-n=$2
-main=$1$2
if [[ $topology == "grid" ]]
then
@@ -39,11 +96,13 @@ else
size=$n
fi
-
+#### playing with kind2 options
kind2_opt="--timeout 36000 -json -v "
kind2_opt="--enable BMC --enable IND --timeout 36000 -json -v"
-kind2_opt="--enable BMC --enable IND --timeout 36000"
+kind2_opt="--enable BMC --enable IND --enable IC3 --timeout 36000"
+kind2_opt="--smt_solver $solver --enable BMC --enable IND --timeout 36000 $@"
+# --qe_method {precise|impl|cooper}
# work in a tmp dir to ease the cleaning
TMP=.tmp-`uname -n`
@@ -52,46 +111,41 @@ cp Makefile ${TMP}
cp ${GITROOT}/salut/test/Makefile.inc ${TMP}
cp ${GITROOT}/salut/test/Makefile.dot ${TMP}
cp *.lus ${TMP}
-cp ${LIB_LUS} ${TMP}
+cp ${LIB_LUS} ${TMP}
cd ${TMP}
-
-make $main.dot || (echo "Beware: Makefile.dot should be in the scope of make!"; exit 2)
-
+make $main.dot || (echo "E: is Makefile.dot included from Makefile?"; exit 2)
make ${main}_const.lus
+# Get rif of the lutre v6 constructs that kind2 does not handle
+lv6 -eei ${LIB_LUS} $main.lus verify.lus ${main}_const.lus -n verify --lustre-v4 -en -knc -o $main.verify.lv4
-INT=uint8
-INT=uint16
-INT=int8
-
-# Building the $main.verify.${INT}.lv4 (cf make $main.verify.${INT}.lv4
-# using lv6 and sed (to set the property and to perform $INT conversion
-lv6 -eei ${LIB_LUS} $main.lus verify.lus ${main}_const.lus -n verify --lustre-v4 -en -o $main.verify.lv4
+# set the property to check
sed -i -e "s/tel/--%MAIN ;\n--%PROPERTY $prop;\ntel/" $main.verify.lv4
-cat $main.verify.lv4 | \
- sed -r "s/[ =](\[)?((-)?[[:digit:]]+)/ \1(${INT} \2)/g" | \
- sed -r "s/\(((-)?[[:digit:]]+)\)/(${INT} \1)/g" | \
- sed -r "s/:int/:${INT}/g" \
- > $main.verify.${INT}.lv4
-
+# using machine integers instead of int
+cat $main.verify.lv4 | \
+ sed -r "s/[ =](\[)?((-)?[[:digit:]]+)/ \1(${int} \2)/g" | \
+ sed -r "s/\(((-)?[[:digit:]]+)\)/(${int} \1)/g" | \
+ sed -r "s/:int/:${int}/g" \
+ > $main.verify.${int}.lv4
start=`date +%s.%N`
-time kind2 --color true ${kind2_opt} $main.verify.${INT}.lv4
+time kind2 --color true ${kind2_opt} $main.verify.${int}.lv4
end=`time date +%s.%N`
wallclock=$( echo "$end - $start" | bc -l )
-timestamp=`date +"%d/%m/%Y-%H:%M:%S"`
+timestamp=`date +"%d/%m/%Y-%H:%M:%S"`
algodir=$(dirname $PWD)
algo=$(basename $algodir)
LC_NUMERIC="en_US.UTF-8"
-# let's keep a track of all runs (it's expensive, it should not be lost)
+# let's keep a track of all runs (it can expensive, it should not be lost)
+# in a .org file
ALL_RESULT="${GITROOT}/salut/test/kind2-result-`uname -n`.org"
-printf "| %s | %s | %s | %s | %.2f | %s | %s |\n" $algo ${topology} ${size} \
- $prop $wallclock $timestamp `kind2 --version | cut -d ' ' -f2` >> ${ALL_RESULT}
+printf "| %s | %s | %s | %s | %.2f | %s | %s | %s | %s |\n" $algo ${topology} ${size} \
+ $prop $wallclock $int $solver $timestamp `kind2 --version | cut -d ' ' -f2` >> ${ALL_RESULT}
echo "cf ${ALL_RESULT}"
\ No newline at end of file
diff --git a/test/README.org b/test/README.org
index bec896c6bf483f7800ee07b7badeb34acb8980af..91b0753799bc2b6e9bd385757f92b996bf446ae6 100644
--- a/test/README.org
+++ b/test/README.org
@@ -18,26 +18,29 @@ Self-Stabilizing Algorithms'' By Altisen, Devismes, Dubois, and Petit.
It also contains implementations of algorithms found in the
literature:
-1. =test/async-unison/=: Asynchronous unison ("Asynchronous
+1) =test/async-unison/=: Asynchronous unison ("Asynchronous
unison" by Couvreur, J., Francez, N., and Gouda, M. G. in 1992)
-2. =test/st-CYH91=: another Spanning tree construction ("A
+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/bfs-st-HC92=: another BFS Spanning tree construction ("A
+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/st-KK06_algo1= and =test/st-KK06_algo2=: another Spanning tree
+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/=: a Depth First Search using arrays (the ``atomic state
+5) =test/dfs/=: a Depth First Search using arrays (the ``atomic state
model'' version of a [[http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.57.1100&rep=rep1&type=pdf][Depth First Search algorithm proposed by Collin and Dolev in 1994]])
-6. =test/dfs-list/=: the same Depth First Search, but using lists
+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
+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.
-
+8) =test/toy-example-a5sf=: The Algorithm described page 5 of
+ "Acyclic Strategy for Silent Self-Stabilization in Spanning
+ Forests" by Karine Altisen, SteÌphane Devismes, and Anaı̈s Durand,
+ SSS 2018
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]]
diff --git a/test/async-unison/p.ml b/test/async-unison/p.ml
index dfc79496755aef404c653a0dd0c3da0b8b93a38b..15ea759aff00bcaf5c74705328a06b83b19693b3 100644
--- a/test/async-unison/p.ml
+++ b/test/async-unison/p.ml
@@ -1,9 +1,13 @@
-(* Time-stamp: <modified the 07/02/2023 (at 12:06) by Erwan Jahier> *)
+(* Time-stamp: <modified the 01/03/2023 (at 11:28) by Erwan Jahier> *)
-(* Couvreur, J., Francez, N., and Gouda, M. G. (1992) Asynchronous
- unison (extended abstract). Proceedings of the 12th International
- Conference on Distributed Computing Systems, Yokohama, Japan, June
- 9-12, pp. 486–493. IEEE Computer Society. *)
+(* Bouded unison, cf Section 5 in:
+
+ Couvreur, J., Francez, N., and Gouda, M. G. (1992) Asynchronous
+ unison (extended abstract). Proceedings of the 12th International
+ Conference on Distributed Computing Systems, Yokohama, Japan, June
+ 9-12, pp. 486–493. IEEE Computer Society.
+
+*)
open Algo
let n = Algo.card()
@@ -11,16 +15,15 @@ let k = n * n + 1
let (init_state: int state_init_fun) = fun _n _ -> (Random.int k)
-let modulo x n = if x < 0 then n+x mod n else x mod n
+let modulo x n = x mod n |> fun x -> if x < 0 then n+x mod n else x
let behind pc qc = (modulo (qc-pc) k) <= n
+let far pc qc = (not (behind pc qc)) && (not (behind qc pc))
let (enable_f: int enable_fun) =
fun c nl ->
if List.for_all (fun q -> behind c (state q)) nl then ["I(p)"] else
- if List.exists (fun q -> not (behind c (state q)) &&
- not (behind (state q) c)) nl
- && c <> 0 then ["R(p)"] else []
+ if List.exists (fun q -> far c (state q)) nl && c <> 0 then ["R(p)"] else []
let (step_f: int step_fun) =
fun c _nl a ->
diff --git a/test/async-unison/ring.dot b/test/async-unison/ring.dot
index dbb0da3d8000571d23b4a4bbc661b0b8bff33185..0646597301dc20c63837f6c5736d51682fe61fa1 100644
--- a/test/async-unison/ring.dot
+++ b/test/async-unison/ring.dot
@@ -1,5 +1,4 @@
graph ring7 {
-
p1 [algo="p.ml"]
p2 [algo="p.ml" ]
p3 [algo="p.ml"]
@@ -7,7 +6,6 @@ graph ring7 {
p5 [algo="p.ml"]
p6 [algo="p.ml"]
p7 [algo="p.ml"]
-
p1 -- p2 -- p3 -- p4 -- p5 -- p6 -- p7 -- p1
}
diff --git a/test/k-clustering/Makefile b/test/k-clustering/Makefile
index 53467270fd883006e0c37de04e2ae015d45b4b66..98a93925fde74518a8c738862e166c4dc8af8945 100644
--- a/test/k-clustering/Makefile
+++ b/test/k-clustering/Makefile
@@ -1,4 +1,4 @@
-# Time-stamp: <modified the 18/01/2023 (at 11:49) by Erwan Jahier>
+# Time-stamp: <modified the 06/03/2023 (at 15:47) by Erwan Jahier>
DECO_PATTERN="0-:p.ml"
SEED=--seed 42
@@ -30,9 +30,6 @@ sim2chrogtk: fig52_kcl.rif
gnuplot: fig52_kcl.rif
gnuplot-rif $<
-rdbg: fig52_kcl.ml
- rdbg --sasa -o fig52_kcl.rif -env "sasa fig52_kcl.dot -gcd"
-
rdbg: fig52_kcl.ml
rdbg --sasa -o fig52_kcl.rif -env "sasa fig52_kcl.dot -cd"
diff --git a/test/lustre/README.org b/test/lustre/README.org
new file mode 100644
index 0000000000000000000000000000000000000000..db968bdd9bd92383a7af9763544256bf01e4e9ed
--- /dev/null
+++ b/test/lustre/README.org
@@ -0,0 +1 @@
+Lustre files useful to define test oracles of ASM algorithms defined in ocaml/sasa
diff --git a/test/unison/config.ml b/test/unison/config.ml
index 92348ed0af24185c59ed7320fa87643f41e1fb21..e76247170e1347fe916a1d9f02b7b30abda40e23 100644
--- a/test/unison/config.ml
+++ b/test/unison/config.ml
@@ -1,5 +1,4 @@
-let potential = None (* None => only -sd, -cd, -lcd, -dd, or -custd are possible *)
let fault = None (* None => the simulation stop once a legitimate configuration is reached *)
@@ -13,3 +12,4 @@ let legitimate pidl from_pid =
let legitimate = Some legitimate
let init_search_utils = None
+let potential = None