From 9bad9c8b99dac4809ab8d9bee40db85d4d9afba9 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr>
Date: Tue, 30 Aug 2022 15:24:51 +0200
Subject: [PATCH] =?UTF-8?q?Am=C3=A9lioration=20des=20scripts?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
test/Cycle_unison/Sh/do_org_lines.sh | 25 +++++++++++++++++--------
test/Cycle_unison/Sh/search_config.sh | 3 ++-
test/Cycle_unison/check_cycles.lus | 26 +++++++++++---------------
test/unison/Makefile | 9 +++++++--
4 files changed, 37 insertions(+), 26 deletions(-)
diff --git a/test/Cycle_unison/Sh/do_org_lines.sh b/test/Cycle_unison/Sh/do_org_lines.sh
index cdfb1a0c..36176807 100644
--- a/test/Cycle_unison/Sh/do_org_lines.sh
+++ b/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
diff --git a/test/Cycle_unison/Sh/search_config.sh b/test/Cycle_unison/Sh/search_config.sh
index 67048aaa..c534d792 100644
--- a/test/Cycle_unison/Sh/search_config.sh
+++ b/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
diff --git a/test/Cycle_unison/check_cycles.lus b/test/Cycle_unison/check_cycles.lus
index db500c38..9a2e1037 100644
--- a/test/Cycle_unison/check_cycles.lus
+++ b/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>>;
diff --git a/test/unison/Makefile b/test/unison/Makefile
index 13c77c70..89c56b9a 100644
--- a/test/unison/Makefile
+++ b/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
--
GitLab