diff --git a/_oasis b/_oasis
index 95a9e332d57461927f75c78ba7a65ea8aae0ee93..d3279d7b7b9738b4556c5c2bc2cb5908f26e068c 100644
--- a/_oasis
+++ b/_oasis
@@ -1,6 +1,6 @@
OASISFormat: 0.4
Name: lustre-v6
-Version: 1.732
+Version: 1.733
Synopsis: The Lustre V6 Verimag compiler
Description: This package contains:
- lus2lic: the (current) name of the compiler (and interpreter via -exec)
diff --git a/lustre-v6.install b/lustre-v6.install
index 9f2ec7f82a51080a791e7a7c60b821ce9b7e816a..444093900456084ab3462abb04fcd18bd7255b07 100644
--- a/lustre-v6.install
+++ b/lustre-v6.install
@@ -6,4 +6,9 @@ etc: [
doc: [
"lv6-ref-man/lv6-ref-man.pdf"
-]
\ No newline at end of file
+]
+
+bin: [
+ "utils/lv6"
+ "utils/lustrequiv"
+]
diff --git a/lv6-ref-man/lv6-ref-man.pdf b/lv6-ref-man/lv6-ref-man.pdf
index 40bbb39dc9e046391c145ca85948874871165a56..257468bad6c412ace3d0b5f91ba69184c6718b3d 100644
Binary files a/lv6-ref-man/lv6-ref-man.pdf and b/lv6-ref-man/lv6-ref-man.pdf differ
diff --git a/src/lv6version.ml b/src/lv6version.ml
index 93bef373b336cc08721d77b10de02424101ebb4b..5fb6102904ba5ccd698aab7226a46261a82fc614 100644
--- a/src/lv6version.ml
+++ b/src/lv6version.ml
@@ -1,7 +1,7 @@
(** Automatically generated from Makefile *)
let tool = "lus2lic"
let branch = "master"
-let commit = "732"
-let sha_1 = "33d4cd49003dd0b3d3b21eca09e86d8ef25ec0c2"
+let commit = "733"
+let sha_1 = "8fd1d262784f8a40fdde9b9fdb1345b4fad850c0"
let str = (branch ^ "." ^ commit ^ " (" ^ sha_1 ^ ")")
let maintainer = "erwan.jahier@univ-grenoble-alpes.fr"
diff --git a/src/main.ml b/src/main.ml
index e40244ae69e75f5814169903ccb0d131e358d2ec..6a3923fa446ae13152054b33b09fc9112ef93f55 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 22/02/2018 (at 15:50) by Erwan Jahier> *)
+(* Time-stamp: <modified the 21/03/2018 (at 14:18) by Erwan Jahier> *)
open Lv6Verbose
open AstV6
@@ -73,11 +73,6 @@ let (gen_rif_interface : LicPrg.t -> Lv6Id.idref option -> Lv6MainArgs.t -> unit
output_string opt.oc ("#outputs "^ (String.concat " " outvars_str) ^"\n");
flush opt.oc
-(* make sur f is fresh *)
-let fresh f =
- if not (Sys.file_exists f) then f else
- Filename.temp_file ~temp_dir:Filename.current_dir_name "_" f
-
(* Generates a lutin env and a lustre oracle for the node *)
let (gen_autotest_files : LicPrg.t -> Lv6Id.idref option -> Lv6MainArgs.t -> unit) =
@@ -135,7 +130,7 @@ let (gen_autotest_files : LicPrg.t -> Lv6Id.idref option -> Lv6MainArgs.t -> uni
let invars_str = List.map (fun (n,t) -> n^":"^(my_type_to_string true t)) invars in
let outvars_str = List.map (fun (n,t) -> n^":"^(my_type_to_string false t)) outvars in
let name = main_node.Lv6Id.id_id in
- let lutin_file_name = fresh ("_"^name^"_env.lut") in
+ let lutin_file_name = ("_"^name^"_env.lut") in
let oc = open_out lutin_file_name in
LicDump.dump_entete oc;
output_string oc ("node " ^ (name) ^ "_env("^ (String.concat ";" outvars_str) ^
@@ -144,7 +139,7 @@ let (gen_autotest_files : LicPrg.t -> Lv6Id.idref option -> Lv6MainArgs.t -> uni
flush oc;
close_out oc;
output_string stdout (lutin_file_name ^" generated.\n");
- let oracle_file_name = fresh ("_"^name^"_oracle.lus") in
+ let oracle_file_name = ("_"^name^"_oracle.lus") in
let oc = open_out oracle_file_name in
let invars,outvars=soc.Soc.profile in
let locals = List.map (fun (n,t) -> n^"_bis",t) outvars in
diff --git a/utils/lustrequiv b/utils/lustrequiv
index 78eba3e524a463b48277b97c0ebf059b23670209..048ce8fa854ceab0cc77ff1cee2188aa4178576f 100755
--- a/utils/lustrequiv
+++ b/utils/lustrequiv
@@ -1,5 +1,7 @@
#!/bin/sh
-# compares with lesar and lurette the behavior of 2 lustre programs
+#
+# compares with lesar the semantics of 2 lustre programs
+# using lesar and lurette.
EXPECTED_ARGS=4
@@ -8,7 +10,8 @@ if [ $# -ne $EXPECTED_ARGS ]
then
echo "usage: $0 lustrefile1 node1 lustrefile2 node2
- Uses lurette and lesar to state if node1 and node2 are equivalent or not.
+ Launch Lurette to check if node1 and node2 are not equivalent.
+ Launch Lesar to check if node1 and node2 are equivalent.
"
else
file1=$1
@@ -17,11 +20,13 @@ else
node2=$4
oracle_node=${node1}_oracle
oracle_file=_${oracle_node}.lus
+ riffile=${node1}"_equal_"${node2}.rif
env=_${node1}_env.lut
+ oracle_ec=${node1}_oracle_prog.ec
- echo " Are nodes $node1@$file1 and $node2@$file2 equivalent?"
+ echo " Are nodes $node1@$file1 and $node2@$file2 different?"
echo " let's check it with lurette... "
- set -x #echo on
+ # set -x #echo on
if
lus2lic $file1 -n $node1 --gen-autotest -np;
@@ -39,12 +44,10 @@ else
echo "node P1 = ${node1}" >> $oracle_file;
echo "node P2 = ${node2}" >> $oracle_file;
- lurette -p 6 -l 100 \
+ lurette -l 100 -o $ {riffile} \
-sut "lus2lic $file2 -n $node2" \
-env "lutin -seed 42 $env" \
-oracle "lus2lic $oracle_file -n $oracle_node"
-# ./lurettetop_exe -p 6 -seed 42 -rp "sut:v6:$file2:$node2" -rp "env:lutin:$env" \
-# -rp "oracle:v6:$oracle_file:$oracle_node" -go -l 100 -ns2c --stop-on-oracle-error;
set - #echo off
if [ $? -eq 0 ] # Test du code de sortie de la commande "lurette".
@@ -53,7 +56,7 @@ else
echo " let's check it with lesar... "
else if [ $? -eq 1 ]
then
- echo " ===> nodes $node1@$file1 and $node2@$file2 _ARE NOT_ equivalent (cf lurette.rif)"
+ echo " ===> nodes $node1@$file1 and $node2@$file2 _ARE NOT_ equivalent (cf ${riffile}"
exit
else
echo " A pb occured in lurettop (exit $?)"
@@ -61,8 +64,8 @@ else
fi
fi
set -x #echo on
- lus2lic -ec ${oracle_file} -n ${node1}_oracle_prog -o ${node1}_oracle_prog.ec
- ecverif ${node1}_oracle_prog.ec
+ lus2lic -ec ${oracle_file} -n ${node1}_oracle_prog -o ${oracle_ec}
+ ecverif ${oracle_ec}
set - #echo off
if [ $? -eq 0 ] # Test du code de sortie de la commande "lurette".
@@ -73,6 +76,9 @@ else
echo " ===> nodes $node1@$file1 and $node2@$file2 _seems_ to differ"
fi
-
+ echo "rm ${env} ${oracle_file} ${riffile} ${oracle_ec}" > lustrequiv-clean-me
+ echo "rm *.cm* *.o luretteSession* *.log " >> lustrequiv-clean-me
+ echo "rm lurette.cov my-rdbg-tuning.ml lustrequiv-clean-me" >> lustrequiv-clean-me
+ echo "To clean up this mess, consider doing a \n\t sh lustrequiv-clean-me"
exit 0
fi
\ No newline at end of file
diff --git a/utils/lv6 b/utils/lv6
new file mode 100755
index 0000000000000000000000000000000000000000..ee4bb58aa3ebd848af3ca78d2b1fd1c992c17985
--- /dev/null
+++ b/utils/lv6
@@ -0,0 +1 @@
+lus2lic $@