ci: fix test and continue the refactoring

salut/test/Makefile.inc

@@ -37,7 +37,7 @@ OCAMLOPT=ocamlfind ocamlopt -bin-annot
 
 GITROOT=$(shell git rev-parse --show-toplevel)
 LIB_LUS=$(GITROOT)/test/lustre/round.lus $(GITROOT)/salut/lib/sas.lus
-
+RUN_KIND2=$(GITROOT)/salut/test/run-kind2.sh
 
 ##########################################################################################"
 # Simulations
@@ -71,8 +71,10 @@ LIB_LUS=$(GITROOT)/test/lustre/round.lus $(GITROOT)/salut/lib/sas.lus
 %.ml: %.dot
 	sasa -reg $<
 
+
 ##########################################################################################"
 # model-checking with kind2
+# nb: it's probably better to use $(GITROOT)/salut/run-kind2.sh instead
 
 ifndef $(prop)
 prop = verify

salut/test/bfs-spanning-tree/Makefile

@@ -10,10 +10,17 @@ include ./Makefile.dot
 ##############################################################################
 # Non-regression tests
 
-test: tree3.kind2-test tree3.lurette #tree3.lesar
+test: tree3.lurette 
+	$(RUN_KIND2) tree 3 closure
+	$(RUN_KIND2) tree 2 theorem 
+
 
 clean: genclean
 	rm -f $(TOPOLOGY)*.* tree3*.*
+
+realclean: clean
+	rm -rf .tmp-`uname -n`
+
 ##############################################################################
 # Other examples of use
 

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

-include "../../lib/sas.lus"
 
 ----------------------------------------------------------------------------
 -- function verify
 ----------------------------------------------------------------------------
-node verify(activations : bool^actions_number^card; inits : state^card) returns (ok : bool);
+node verify(activations : bool^actions_number^card; inits : state^card) 
+returns (ok : bool);
 var
-	config : state^card;
-	enables : bool^actions_number^card;
-	legitimate, closure, CD_disable, lustre_round : bool;
-        lustre_round_nb:int;
+  config : state^card;
+  enables : bool^actions_number^card;
+  legitimate, closure, CD_disable, theorem, lustre_round : bool;
+  lustre_round_nb:int;
 let
-        daemon_is_distributed<<actions_number,card>>(activations, pre enables));
-        assert(rangei<<0,diameter,card>>(inits));   
-	assert(true ->
+  assert(daemon_is_distributed<<actions_number,card>>(activations, pre enables));
+  assert(rangei<<0,diameter,card>>(inits)); 
+  config, enables, lustre_round, lustre_round_nb = topology(activations, inits);
 
-	config, enables, lustre_round, lustre_round_nb = topology(activations, inits);
+  legitimate = legitimate<<actions_number,card>>(enables,config);
+  closure = true -> (pre(legitimate) => legitimate);
+  CD_disable =  all_CD_are_false(enables);
 
-	legitimate = legitimate<<actions_number,card>>(enables,config);
-	closure = true -> (pre(legitimate) => legitimate);
-        CD_disable =  all_CD_are_false(enables);
-
-	-- verify that the execution terminates after at most |N|−1 moves:
-	ok = closure
-         and ( (lustre_round_nb>=diameter+1) => CD_disable )
-         and ( (lustre_round_nb>=diameter+2) => legitimate )
-;
+  -- verify that the execution terminates after at most |N|−1 moves:
+  theorem = ( (lustre_round_nb>=diameter+1) => CD_disable )
+        and ( (lustre_round_nb>=diameter+2) => legitimate );
+  ok = closure and theorem;
 tel;
 
 ----------------------------------------------------------------------------
 -- all states are initially in correctly
 ----------------------------------------------------------------------------
-node rangei<<const low:int; const D:int; const card:int>>(config:state^card) returns (res:bool);
+function rangei<<const low:int; const D:int; const card:int>>(config:state^card) returns (res:bool);
 var
   e:state;
 let

salut/test/kclustering/verify.lus

-include "../../lib/sas.lus"
-include "../../lib/utils.lus"
 
 --include "cost.lus"
 --const worst_case=3*card*(card-1)/2 - card - 1;

salut/test/rsp_tree/verify.lus

-include "../../lib/sas.lus"
 
 ----------------------------------------------------------------------------
 -- function verify

salut/test/run-kind2.sh

@@ -41,7 +41,8 @@ fi
 
 
 kind2_opt="--timeout 36000 -json -v "
-kind2_opt=" --enable BMC --enable IND --timeout 36000 -json -v"
+kind2_opt="--enable BMC --enable IND --timeout 36000 -json -v"
+kind2_opt="--enable BMC --enable IND --timeout 36000"
 
 
 # work in a tmp dir to ease the cleaning
@@ -69,13 +70,16 @@ INT=int8
 lv6 -eei ${LIB_LUS} $main.lus verify.lus ${main}_const.lus -n verify --lustre-v4 -en -o $main.verify.lv4
 sed -i -e "s/tel/--%MAIN ;\n--%PROPERTY $prop;\ntel/" $main.verify.lv4
 cat $main.verify.lv4 | \
-    sed -r "s/[ =]((-)?[[:digit:]]+)/ (${INT} \1)/g" | \
+    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 > $main.json
+time kind2 --color true ${kind2_opt} $main.verify.${INT}.lv4
 end=`time date +%s.%N`
 wallclock=$( echo "$end - $start" | bc -l )
 
@@ -85,5 +89,9 @@ 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)
+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` >> ../../kind2-result-`uname -n`.org
+     $prop $wallclock $timestamp `kind2 --version | cut -d ' ' -f2` >> ${ALL_RESULT}
+
+echo "cf ${ALL_RESULT}"
\ No newline at end of file

salut/test/unison/Makefile

@@ -5,17 +5,34 @@ DECO_PATTERN="0-:unison.ml"
 
 include ./Makefile.inc
 include ./Makefile.dot
+-include Makefile.untrack
 
-RUN:
-	for i in `seq 1 16`; do sleep 2; sh Sh/search_config_en_int8.sh 1 $${i} diring & done
-	for i in `seq 6 16`; do sleep 2; sh Sh/search_config_en_int8.sh 3 $${i} diring & done
-	for i in `seq 8 16`; do sleep 2; sh Sh/search_config_en_int8.sh 5 $${i} diring & done
-	for i in `seq 10 16`; do sleep 2; sh Sh/search_config_en_int8.sh 7 $${i} diring & done
-	for i in `seq 12 16`; do sleep 2; sh Sh/search_config_en_int8.sh 9 $${i} diring & done
-	for i in `seq 14 16`; do sleep 2; sh Sh/search_config_en_int8.sh 11 $${i} diring & done
-	for i in `seq 16 16`; do sleep 2; sh Sh/search_config_en_int8.sh 13 $${i} diring & done
-xxx:
-
-uptime:
-	ps -eo pid,comm,lstart,etime,time,args| grep search_conf | grep -v grep
-	ps -eo pid,comm,lstart,etime,time,args| grep search_conf | grep -v grep | wc
+##############################################################################
+# Non-regression tests
+
+test: clique3.kind2-test clique3.lurette #lesar not work because of the modulo.
+
+clean: genclean
+	rm -f $(TOPOLOGY)*.* clique3*.*	grid* ring* diring* er* 
+
+##############################################################################
+# Other examples of use
+
+## Some examples of use of ../Makefile.inc
+
+# run a simulation with luciole
+simu: $(TOPOLOGY).simu
+
+# Compare the ocaml version with the lustre one (with seed)
+compare_seed: $(TOPOLOGY).lurette
+	cat unison.rif
+
+# Compare the ocaml version with the lustre one (no seed)
+compare: $(TOPOLOGY).lurette_no_seed
+	cat unison.rif
+
+# make diring4.simu
+kind2: $(TOPOLOGY).kind2
+
+## do not work because there is a modulo in p.lus, which is not (yet) implemented in ../../bit-blast/*.lus
+lesar: $(TOPOLOGY).lesar