From c7add39a5011e247d99024390029697af11fa366 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr>
Date: Wed, 27 Jul 2022 13:53:37 +0200
Subject: [PATCH] test: add a script to compare -2cmc and -2c
---
lib/socNameC.ml | 4 +-
utils/compare_exec_and_2cmc | 80 +++++++++++++++++++++++++++++++++++++
2 files changed, 82 insertions(+), 2 deletions(-)
create mode 100755 utils/compare_exec_and_2cmc
diff --git a/lib/socNameC.ml b/lib/socNameC.ml
index be1059d1..0d397c53 100644
--- a/lib/socNameC.ml
+++ b/lib/socNameC.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 21/07/2022 (at 10:23) by Erwan Jahier> *)
+(** Time-stamp: <modified the 22/07/2022 (at 14:31) by Erwan Jahier> *)
type variable_type = {
id: int;
@@ -63,7 +63,7 @@ let get_variables_assoc : Soc.t -> (string * variable_type) list = fun soc ->
let lvars =
match step_impl with
| Gaol (vl,_) -> vl
- | Predef -> assert false
+ | Predef
| Iterator _
| Boolred _
| Condact _
diff --git a/utils/compare_exec_and_2cmc b/utils/compare_exec_and_2cmc
new file mode 100755
index 00000000..bf1e1392
--- /dev/null
+++ b/utils/compare_exec_and_2cmc
@@ -0,0 +1,80 @@
+#!/bin/sh
+
+# compares with lurette the results of:
+# lus2lic -2c
+# lus2lic -exec
+
+lustre_file=$1
+OPT=$3
+PORT=$2
+
+node=`basename $lustre_file .lus`
+_oracle=_"$node"_oracle.lus
+oracle="$node"_oracle
+lv4="$node"_lv4.lus
+ec="$node".ec
+lv4_node="$node__$node"
+env=_"$node"_env.lut
+env_node="$node"_env
+
+
+. /home/jahier/.opam/opam-init/variables.sh
+set -x verbose #echo on
+
+
+if
+ [ -f $env_node ];
+then
+ echo "$env_node generated"
+
+else if
+ ./lus2lic $OPT $lustre_file -n $node --gen-autotest -np;
+ cat $lustre_file >> $_oracle;
+then
+ echo "./lus2lic $OPT $lustre_file -n $node --gen-autotest -np: ok"
+else
+ echo "Error"
+ exit 2
+fi
+fi
+
+# XXXXX
+if
+ ./lus2lic -dir /tmp/lustre-test-$lustre_file-$node $OPT $lustre_file -n $node -2cmc -cc -o $node.exec;
+then
+ echo "lus2lic -2c done"
+else
+ echo "Error"
+ exit 2
+fi
+# XXXXX
+
+if
+ ./lus2lic -dir /tmp/lustre-test-$lustre_file-$node $OPT $_oracle -n $oracle -2c -cc -o $node-oracle.exec;
+then
+ echo "lus2lic -2c done"
+else
+ echo "Error"
+ exit 2
+fi
+
+
+# call-via-socket -server -addr 127.0.0.1 -port $PORT ./$node.exec &
+
+export PATH=/usr/local/tools/lustre/v4/bin/:$PATH
+PRECISION=4
+if
+ lurette -l 10 -o xxx.rif \
+ -sut "./$node.exec" \
+ -env "lutin $env -n $env_node -p $PRECISION -seed 42" \
+ -oracle "./$node-oracle.exec";
+# lurettetop_exe -p $PRECISION -rp "sut:socket:127.0.0.1:$PORT" -rp "env:lutin:$env:-p:$PRECISION" -rp "oracle:v6:$_oracle:$oracle:$OPT" \
+# -go -l 10 -ns2c --stop-on-oracle-error;
+then
+ echo "Comparison of lus2lic -2c and lus2lic -exec with lurette on $lustre_file: ok"
+ echo "lurette ok"
+else
+ echo "error"
+ exit 2
+fi
+exit 0
--
GitLab