fix links

test/Makefile.inc

@@ -78,8 +78,7 @@ endif
 	sed -i -e "s/tel/--%MAIN ;\n--%PROPERTY ok;\ntel/" $@
 
 # Do not expand nodes 
-%_verify.noexpand.lv4:  verify.lus
-	make $*_const.lus
+%_verify.noexpand.lv4:  verify.lus %_const.lus
 	lv6 $*.lus $^ $*_const.lus -n $(prop) -rnc --lustre-v4 -o $@
 	tac $@ | sed  -z "s/tel/tel\n--%MAIN ;\n--%PROPERTY ok;/" | tac > $@.tmp
 	mv $@.tmp $@

test/kclustering/Makefile

@@ -4,8 +4,8 @@ SASA_ALGOS := p.ml
 DECO_PATTERN="0-:p.ml"
 
 
-include ~/sasa/salut/test/Makefile.inc
--include ~/sasa/salut/test/Makefile.dot
+include ../Makefile.inc
+-include ../Makefile.dot
 
 clean: genclean
 	rm -f tree*.*

test/kclustering/verify.lus

-include "../../sasa/salut/lib/sas.lus"
-include "../../sasa/salut/lib/utils.lus"
+include "../../lib/sas.lus"
+include "../../lib/utils.lus"
 
 include "cost.lus"
 const worst_case=3*card*(card-1)/2 - card - 1;
@@ -12,7 +12,7 @@ returns (ok : bool);
 var
   config : state^card;
   enabled : bool^actions_number^card;
-  legitimate, closure : bool;
+  legitimate, closure,converge : bool;
   steps, cost : int;
 let
 	assert(true -> daemon_is_distributed<<actions_number,card>>(active, pre enabled));
@@ -22,15 +22,15 @@ let
 	config, enabled = topology(active, init_config);
         assert(config = init_config -> true);
 
-	-- stability in this algo means mutual exclusion: exactly 1 node is enabled at a time
-        legitimate = n_xor<<card>>(map<<n_or<<actions_number>>,card>> (enabled));
+	legitimate = silent<<actions_number,card>>(enabled);
 	closure = true -> (pre(legitimate) => legitimate);
 
         cost = cost(enabled, config);
-       -- converge = (true -> legitimate or pre(cost)>cost);
+       converge = (true -> legitimate or pre(cost)>cost);
 
 	steps = 0 -> (pre(steps) + 1);
 	ok =  closure
+             and converge
      --        and (steps > worst_case) => legitimate      -- the worst-case stabilization
      
      --      and (steps > worst_case - 1) => legitimate  -- is tigth!