clean-up utils/lustrequiv, and install in the opam bin dir.

add and install an alias to lus2lic name lv6.

lus2lic --gen-autotest now overrides existing _oracle*.lus and _env*.lut files

_oasis

 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)

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"
+]

src/lv6version.ml

 (** 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"

src/main.ml

-(* 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

utils/lustrequiv

 #!/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

utils/lv6

+lus2lic $@