Amélioration des scripts

test/Cycle_unison/Sh/do_org_lines.sh

@@ -23,36 +23,45 @@ log=Log/$topology${k}_$n.log
 valid=""
 invalid=""
 timeout=""
+stack_overflow=""
 
 grep "ok: valid" $log && valid="true"
 grep "ok: invalid" $log && invalid="true"
 grep "Wallclock timeout" $log && timeout="true"
-
+grep "Stack overflow" $log && stack_overflow="true"
 
 time=`grep "total runtime" $log | cut -d ' ' -f5`
 
 if [ $valid = "true" ]
     then resultat="legitimate"
     step=`grep "ok: " $log | cut -d ' ' -f4 | tr -d ')'`
+fi
 
-else if  [ $invalid = "true" ]
+if [ "$invalid" = "true" ]
     then resultat="cycle found"
     step=`grep "ok: " $log | cut -d ' ' -f4`
-else if  [ $timeout = "true" ]
-    then resultat="Timeout (${TIMEOUT})"
+fi
+
+if [ "$timeout" = "true" ]
+    then time="TIMEOUT"
     step=`grep "ok: " $log | cut -d ' ' -f5`
-    time="-"
-else
-    resultat="..."
 fi
+
+if [ "$valid$invalid$timeout" = "" ]
+    then resultat="..."
 fi
+
+# nb: a SO does not mean that kind2 is over
+if  [ "$valid$invalid" = "" -a "$stack_overflow" = "true" ]
+    then resultat="$resultat (SO)"
 fi
 
+
 # d=$(expr $n / 2)
 d=$(expr $n / 2)
 dx2m1=$(expr $d \* 2 - 1)
 dx3m1=$(expr $d \* 3 - 1)
 
 
-echo "| $topology | $n | $k | $dx2m1 | $dx3m1 | $step | $resultat | $time |"  > $log.org
+echo "| $topology | $k ($dx2m1) | $n | $resultat | $step | $dx3m1 | $time |"  > $log.org
 

test/Cycle_unison/Sh/search_config.sh

@@ -38,7 +38,8 @@ lv6 -eei ${topology}$n.lus check_cycles.lus $topology${n}_const.lus -n check_cyc
 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
 mv $topology${n}_check_cycles.noexpand.lv4.tmp $topology${n}_check_cycles.noexpand.lv4
 [ -d Log ] || mkdir Log
-time kind2 --timeout ${TIMEOUT} --color false --modular true --compositional true $topology${n}_check_cycles.noexpand.lv4 > $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
 
 ##############################################################
 clean $topology$n

test/Cycle_unison/check_cycles.lus

@@ -3,37 +3,33 @@ include "../../lib/sas.lus"
 
 
 node check_cycles(activations : bool^actions_number^card; inits : state^card) returns (ok : bool);
-var nb_step: int;
 var config,mirror_inits : state^card;
 var enables : bool^actions_number^card;
-var legitimate, noinit : bool;
+var legitimate, no_loop : 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)));
+
+  -- 
   assert(true -> daemon_is_synchronous<<actions_number,card>>(activations, pre enables));
   assert(rangei<<0,card,k>>(inits));   
   assert(true -> inits = pre 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);
-  nb_step = (-1) -> pre(nb_step) + 1;
   mirror_inits = mirror<<card>>(inits);
 
-  noinit = true -> not (config=inits or
-                        config=mirror_inits 
-or
-                        eq_forall_permutations<<card,card-1>>(inits,mirror_inits,config)
-);
-  -- verify that the execution terminates after at most |N|−1 moves:
-  ok = -- closure
-    ( noinit or legitimate )
---  and (nb_step>=(3*diameter-2) => legitimate)
-;
+  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 ;
 tel;
+
 --type state = int;
 --node test = permutation<<2,3>>;
 

test/unison/Makefile

@@ -37,10 +37,11 @@ kind2: $(TOPOLOGY).kind2
 lesar: $(TOPOLOGY).lesar
 
 org:
-	echo "| Topology | n | k | 2xD-1 | 3xD-1 | step | Resultat | time  |" > resultat.org
+	echo "|-|"  > resultat.org
+	echo "| Topology | k (2xD-1) | n | Resultat | step | 3xD-1 | time  |" >> resultat.org
 	echo "|-|"  >> resultat.org
 	for n in `seq 3 35`; \
-	   do for k in `seq 3 2 35`; do \
+	   do for k in `seq 1 2 35`; do \
 	     [ -f Log/ring$${k}_$${n}.log ] && sh Sh/do_org_lines.sh $${k} $${n}  ring && \
 	     cat Log/ring$${k}_$${n}.log.org >>  resultat.org; \
 	   done; \
@@ -51,3 +52,7 @@ org:
 
 RUN:
 	for i in `seq 3 35`; do sleep 2; sh Sh/search_config.sh 11 $i ring &; done
+
+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