test: add sh scripts to perform various experiments

salut/test/gen-salut-batch.sh

+#!/bin/bash 
+#set -x
+
+GITROOT=$(git rev-parse --show-toplevel)
+LIB_LUS="${GITROOT}/test/lustre/round.lus ${GITROOT}/salut/lib/sas.lus"
+daemon_lustre_file=${GITROOT}/salut/lib/daemon.lus
+
+help=" Generate a (standalone) lustre program that runs salut with a lustre daemon
+
+It is useful to perform batch simulations.
+
+usage:
+  $0 daemon topology n [an]
+
+where:
+  - daemon is the name of one the node in ${daemon_lustre_file}
+  - topology is one of graph supported by gg (ring, diring, grid, etc.)
+  - n is the size of the topology [*]
+  - an is the action number of the algorithm (1 by default)
+
+nb: only work for algorithms which node state is made of an integer
+
+[*] except for grids, where the size of the topology would be n*n
+
+"
+
+# 3 or 4 arguments only
+  if [[ $# < 3 ]]
+  then
+      printf "$help"
+      exit 2
+  elif [[ $# = 3 ]]
+  then
+      an=1
+  else
+      an=$4
+fi
+daemon=$1
+topology=$2
+n=$3
+
+  if [[ $topology == "grid" ]]
+  then
+      size=$(($n * $n))
+  else
+      size=$n
+  fi
+
+
+
+# work in a tmp dir to ease the cleaning
+TMP=.tmp
+[ -d ${TMP} ] || mkdir ${TMP}
+cp Makefile ${TMP}
+cp ${GITROOT}/salut/test/Makefile.inc  ${TMP}
+cp ${GITROOT}/salut/test/Makefile.dot  ${TMP}
+cp *.ml *.lus ${TMP}
+
+# to measure the perf, we don't want the algo to stop too soon.
+echo "let legitimate = None" >> ${TMP}/config.ml
+cd  ${TMP}
+
+main_node=${daemon}_${topology}${n}
+outfile=${main_node}.lus
+dotfile=${topology}${n}.dot
+lusfile=${topology}${n}.lus
+lusconstfile=${topology}${n}_const.lus
+
+make ${dotfile} || (echo "Beware: Makefile.dot should be in the scope of make!"; exit 2)
+
+salut ${dotfile}
+
+# XXX state should me made of an integer
+config_init=`printf "["; for ((a=1; a < $size ; a++)) do printf "%d," $RANDOM; done;  printf "%d]" $RANDOM`
+
+timestamp=`date +"%d/%m/%Y- %H:%M:%S"` 
+printf "(* Automatically generated ($timestamp) by '$0 $*' *)
+
+include \"${daemon_lustre_file}\"
+include \"${lusfile}\"
+include \"${lusconstfile}\"
+
+node ${main_node}(any:int)\n\
+    returns (p_c : state^${size}; Enab_p : bool^${an}^${size});\n\
+var\n\
+  round:bool; round_nb:int;\n\
+  initials : state^${size};\n\
+let\n\
+    initials = ${config_init};\n\
+    p_c, Enab_p, round, round_nb = ${topology}${n}([false] ^ ${size} -> ${daemon}<<$an,$size>>(any, pre Enab_p), initials);\n\
+tel"   > $outfile
+
+echo "
+The file '$outfile' has been generated.
+To run simulations, you can generate an executable:
+
+   lv6 -2c -cc $outfile -n ${main_node} ${LIB_LUS} -dir ${main_node}
+   
+and run it:
+
+  ./${main_node}.exec 
+
+or, to avoid the need to provide the dummy input:
+
+   (for i in {1..10}; do echo $((((1<<15)| RANDOM))); done ; echo q) | ./${main_node}.exec
+   (for i in {1..10}; do echo $((((1<<15)| RANDOM))); done ; echo q) | time ./${main_node}.exec  > /dev/null
+"
+

salut/test/run-kind2.sh

+#!/bin/bash 
+set -x
+
+GITROOT=$(git rev-parse --show-toplevel)
+LIB_LUS="${GITROOT}/test/lustre/round.lus ${GITROOT}/salut/lib/sas.lus"
+
+help=" 
+usage:
+  $0 topology n [property]
+
+where:
+  - topology is one of graph supported by gg (ring, diring, grid, etc.)
+  - n is the size of the topology [*]
+  - property is one of the verify node (in verify.lus) variable (ok by default)
+  
+[*] except for grids, where the size of the topology would be n*n
+
+"
+
+# 2 arguments only
+  if [[ $# < 2 ]]
+  then
+      printf "$help"
+      exit 2
+  elif [[ $# == 2 ]]
+  then
+      prop=ok
+  else
+      prop=$3
+fi
+topology=$1
+n=$2
+main=$1$2
+
+if [[ $topology == "grid" ]]
+    then
+    size=$(($n * $n))
+else
+    size=$n
+fi
+
+
+kind2_opt="--enable BMC --enable IND --enable INVGEN --timeout 36000"
+
+
+# work in a tmp dir to ease the cleaning
+TMP=.tmp-`uname -n`
+[ -d ${TMP} ] || mkdir ${TMP}
+cp Makefile ${TMP}
+cp ${GITROOT}/salut/test/Makefile.inc  ${TMP}
+cp ${GITROOT}/salut/test/Makefile.dot  ${TMP}
+cp *.lus ${TMP}
+cp ${LIB_LUS} ${TMP} 
+cd  ${TMP}
+
+
+make $main.dot || (echo "Beware: Makefile.dot should be in the scope of make!"; exit 2)
+
+make ${main}_const.lus
+
+
+#make $main.verify.int8.lv4 
+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:]]+)/ (int8 \1)/g" | \
+    sed -r "s/\(((-)?[[:digit:]]+)\)/(int8 \1)/g" | \
+    sed -r "s/:int/:int8/g" \
+    > $main.verify.int8.lv4
+
+start=`date +%s.%N`
+time kind2 --color true ${kind2_opt} $main.verify.int8.lv4
+end=`time date +%s.%N`
+wallclock=$( echo "$end - $start" | bc -l )
+
+timestamp=`date +"%d/%m/%Y-%H:%M:%S"` 
+algodir=$(dirname $PWD)
+algo=$(basename $algodir)
+
+LC_NUMERIC="en_US.UTF-8"
+
+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

salut/test/salut-vs-sasa.sh

+#!/bin/bash
+ set -x
+
+MY_DIR=$(dirname $(readlink -f $0))
+
+source $MY_DIR/gen-salut-batch.sh
+
+LENGTH=$5
+
+################################################################
+lv6 -2c -cc $outfile -n ${main_node} ${LIB_LUS} -dir ${main_node} > lv6_${main_node}.log
+
+start=`date +%s.%N`
+
+[ -f ./${main_node}.exec ] && (for (( c=1; c<=$LENGTH; c++ )) ; do echo $((((1<<15)| RANDOM))); done ; echo q) | time ./${main_node}.exec   | tail
+
+end=`date +%s.%N`
+
+runtime_salut=$( echo "$end - $start" | bc -l )
+
+################################################################
+case $daemon in
+    synchronous)
+	sasad="-sd"
+	;;
+    central)
+	sasad="-cd"
+	;;
+    *)
+	sasas=""
+	;;
+esac
+
+make ${topology}${n}.dot
+make ${topology}${n}.cmxs
+
+# set -x
+start=`date +%s.%N`
+time sasa ${sasad} ${topology}${n}.dot -l ${LENGTH}  > sasa_${main_node}.log
+end=`time date +%s.%N`
+
+runtime_sasa=$( echo "$end - $start" | bc -l )
+
+################################################################
+
+ratio1=$( echo "${runtime_salut}  / ${runtime_sasa} * 100 " | bc -l )
+ratio2=$( echo "$runtime_sasa  / $runtime_salut * 100 " | bc -l )
+
+LC_NUMERIC="en_US.UTF-8"
+
+printf "   ===> speedup = %.2f (%.2f)\n" $ratio1 $ratio2
+
+echo "* $0 $* " `date +"%d/%m/%Y- %H:%M:%S"` >> ../result.org
+echo "   ===> salut a mis $runtime_salut secondes"  >> ../result.org
+echo "   ===> sasa a mis $runtime_sasa secondes"  >> ../result.org
+printf "   ===> speedup = %.2f (%.2f)\n" $ratio1 $ratio2 >>  ../result.org
+
+DATE=`date +"%d/%m/%Y-%H:%M:%S"`
+algodir=$(dirname $PWD)
+algo=$(basename $algodir)
+printf "| %s | %s | %s | %s | %s | %.2f | %.2f | %.2f | %s | %s |\n"  \
+    ${topology} ${size} $algo  $daemon \
+    ${LENGTH} $runtime_salut $runtime_sasa $ratio1  $DATE  `uname -n` >>  ../../result-tab.org
\ No newline at end of file