test: check for cycle-convergence in salut/test

salut/test/bfs-spanning-tree/verify.lus

@@ -9,7 +9,7 @@ returns (ok : bool; enables : bool^actions_number^card);
 var
   config : state^card;
   legitimate,CD_disable, lustre_round : bool;
-  closure, converge_worst_case, worst_case_is_tigth1, worst_case_is_tigth2 : bool;
+  closure, converge, converge_worst_case, worst_case_is_tigth1, worst_case_is_tigth2 : bool;
   lustre_round_nb:int;
 let
   assert(daemon<<actions_number,card>>(activations, pre enables));
@@ -25,7 +25,10 @@ let
                     and ( (lustre_round_nb>=diameter+2) => legitimate );
   worst_case_is_tigth1 = (lustre_round_nb>=diameter) => legitimate;
   worst_case_is_tigth2 = (lustre_round_nb>=diameter) => CD_disable;
-  ok = closure and converge_worst_case;
+
+  assert(true -> inits = pre inits);
+  converge = true -> (not(inits = config) or legitimate);
+  ok = closure and converge_worst_case and converge;
 tel;
 
 ----------------------------------------------------------------------------

salut/test/coloring/verify.lus

@@ -6,7 +6,7 @@ returns (ok : bool; enables : bool^actions_number^card);
 var
   config : state^card;
 
-  r, legitimate,closure, converge_cost, converge_worst_case : bool;
+  r, legitimate,closure, converge, converge_cost, converge_worst_case : bool;
   rn,pot, moves : int;
 let
    assert(true -> daemon<<actions_number,card>>(activations, pre enables));
@@ -26,7 +26,10 @@ let
 
   -- much easier to prove than the converge_worst_case
   converge_cost = (true -> legitimate or pre(pot) > pot);
-  ok = closure and converge_cost and converge_worst_case;
+
+  assert(true -> inits = pre inits);
+  converge = true -> (not(inits = config) or legitimate);
+  ok = closure and converge_cost and converge_worst_case and converge;
 tel;
 
 

salut/test/dijkstra-ring/verify.lus

@@ -10,7 +10,7 @@ var
 --  enabled : bool^1^n; -- 1 because that algo has only 1 rule
   enabled1: bool^n;   -- enabled projection
   legitimate, round : bool;
-  closure, converge_cost, converge_wc, wc_is_tigth : bool;
+  closure, converge_cost, converge_wc, converge, wc_is_tigth : bool;
   steps, cost, round_nb : int;
 let
   assert(true -> daemon<<1,n>>(active, pre enabled));
@@ -25,7 +25,9 @@ let
   steps = 0 -> (pre(steps) + 1); -- 0, 1, 2, ...
   converge_wc = (steps >= worst_case) => legitimate;
   wc_is_tigth = (steps >= worst_case - 1) => legitimate;
-  ok = closure and converge_cost and converge_wc;
+  assert(true -> init_config = pre init_config);
+  converge = true -> ((init_config = config) => legitimate);
+  ok = closure and converge_cost and converge_wc and converge;
 tel;
 
 function rangei<<const low:int; const n:int>>(c:state^n)

salut/test/ghosh/verify.lus

@@ -9,7 +9,7 @@ node verify(active : bool^actions_number^card; init_config : state^card)
 returns (enabled : bool^actions_number^card;ok : bool);
 var
   config : state^card;
-  legitimate, closure, converge_worst_case,worst_case_is_tigth : bool;
+  legitimate, closure, converge, converge_worst_case,worst_case_is_tigth : bool;
   steps : int;
   round:bool; round_nb:int;
 let
@@ -23,5 +23,8 @@ let
   closure = true -> (pre(legitimate) => legitimate);
   converge_worst_case = (steps >= worst_case) => legitimate;
   worst_case_is_tigth = (steps >= worst_case-3) => legitimate;
-  ok =  closure and converge_worst_case;
+
+  assert(true -> init_config = pre init_config);
+  converge = true -> (not(init_config = config) or legitimate);
+  ok = closure and converge_worst_case and converge;
 tel;
\ No newline at end of file

salut/test/k-clustering/verify.lus

@@ -12,7 +12,7 @@ var
 
   legitimate, closure, lustre_round : bool;
   lustre_round_nb:int;
-  converge_cost, converge_worst_case, worst_case_is_tigth : bool;
+  converge_cost, converge, converge_worst_case, worst_case_is_tigth : bool;
   steps, cost : int;
 let
   assert(config_is_correct<<card>>(init_config));
@@ -29,7 +29,12 @@ let
   converge_worst_case = (steps > worst_case) => legitimate;
   worst_case_is_tigth = (steps > worst_case - 1) => legitimate;
   steps = 0 -> (pre(steps) + 1);
+
+  assert(true -> init_config = pre init_config);
+  converge = true -> (not(init_config = config) or legitimate);
+
   ok =  closure
+      and converge
       and converge_cost
       and converge_worst_case;
 -- and worst_case_is_tigth;

salut/test/ring-orientation/verify.lus

@@ -11,7 +11,7 @@ returns (ok : bool;
   config : state^card;)
 var
 --  enabled : bool^actions_number^card;
-  silent,legitimate, closure, converge_worst_case,worst_case_is_tigth : bool;
+  silent,legitimate, closure, converge, converge_worst_case,worst_case_is_tigth : bool;
   steps : int;
   round:bool; round_nb:int;
 let
@@ -33,7 +33,10 @@ let
 
   silent = silent<<actions_number,card>>(enabled);
 
+  assert(true -> init_config = pre init_config);
+  converge = true -> (not(init_config = config) or legitimate);
+
   ok =
     -- nb: closure is wrong because legitimate needs to be more specific (cf state.lus)
-    closure and converge_worst_case ; -- closure and;
+    closure and converge_worst_case  and converge;
 tel;
\ No newline at end of file

salut/test/unison/verify.lus

@@ -6,7 +6,7 @@ returns (ok : bool; enables : bool^actions_number^card;);
 var
   nb_step: int;
   config : state^card;
-  legitimate, closure, converge_worst_case, worst_case_is_tigth : bool;
+  legitimate, closure, converge, converge_worst_case, worst_case_is_tigth : bool;
   lustre_round : bool;
   lustre_round_nb : int;
 let
@@ -23,7 +23,10 @@ let
   converge_worst_case = (nb_step>=(3*diameter-2) => legitimate);
   worst_case_is_tigth = (nb_step>=(3*diameter-3) => legitimate); -- lead to a proof failure
   -- verify that the execution terminates after at most |N|−1 moves:
-  ok = closure and converge_worst_case;
+
+  assert(true -> inits = pre inits);
+  converge = true -> (not(inits = config) or legitimate);
+  ok = closure and converge_worst_case and converge;
 tel;