diff --git a/src/lus2licRun.ml b/src/lus2licRun.ml
index c74dac92afb70842227a67ea73754e0965233e5c..0b2982e82f6675446365e1a78e17e09a96d47d98 100644
--- a/src/lus2licRun.ml
+++ b/src/lus2licRun.ml
@@ -1,15 +1,14 @@
-(* Time-stamp: <modified the 29/11/2013 (at 15:23) by Erwan Jahier> *)
+(* Time-stamp: <modified the 20/02/2014 (at 11:26) by Erwan Jahier> *)
(*-----------------------------------------------------------------------
** Copyright (C) - Verimag.
*)
-type vars = (string * string) list
+type vars = (string * Data.t) list
open Lv6MainArgs
open Soc
open SocExecValue
-(* xxx avoidable code duplic with main.ml *)
let make argv =
let opt = Lv6MainArgs.parse argv in
let node = opt.main_node in
@@ -44,11 +43,10 @@ let make argv =
)
in
let soc = try Soc.SocMap.find sk soc_tbl with Not_found -> assert false in
- let vntl_of_profile = List.map (fun (x,t) -> x,SocUtils.string_of_type_ref t) in
let soc_inputs = (SocExec.expand_profile false (fst soc.profile)) in
let soc_outputs = (SocExec.expand_profile true (snd soc.profile)) in
- let (vntl_i:Data.vntl) = vntl_of_profile soc_inputs in
- let (vntl_o:Data.vntl) = vntl_of_profile soc_outputs in
+ let (vntl_i:Data.vntl) = (fst soc.profile) in
+ let (vntl_o:Data.vntl) = (snd soc.profile) in
let oc = stdout in
(* Lv6util.dump_entete oc; *)
(* RifIO.write_interface oc vntl_i vntl_o None None; *)
diff --git a/src/lus2licRun.mli b/src/lus2licRun.mli
index f6cc3eb0a74f01e8c3d40008b13151abeed95e6a..2d6dcdc8ccd86aad2a067841db52d166d10c0297 100644
--- a/src/lus2licRun.mli
+++ b/src/lus2licRun.mli
@@ -1,8 +1,11 @@
-type vars = (string * string) list
+type vars = (string * Data.t) list
val make: string array ->
vars * vars * (string -> unit)
* (Data.subst list -> Data.subst list)
* (Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t)
* Data.subst list * Data.subst list
+
+(* type lustre_event = None *)
+(* type lustre_event = Eq of string *)
diff --git a/src/lv6version.ml b/src/lv6version.ml
index 14bcbb683a6bbab7f741a0590a7ac7a12dd36c68..94187169ba436f8c95bb7a6ba5b61ca19eed0a6d 100644
--- a/src/lv6version.ml
+++ b/src/lv6version.ml
@@ -1,7 +1,7 @@
(** Automatically generated from Makefile *)
let tool = "lus2lic"
-let branch = "(no"
-let commit = "433"
-let sha_1 = "360a5c237ffd24aaae3d180f62ecf25cb539fb4d"
+let branch = "master"
+let commit = "409"
+let sha_1 = "06ddb863bcbd023f74876adc12e50778a2afe9d7"
let str = (branch ^ "." ^ commit ^ " (" ^ sha_1 ^ ")")
let maintainer = "jahier@imag.fr"
diff --git a/src/socExec.ml b/src/socExec.ml
index 9e6fd931b88636d3e17a9970dcd2859fb9f9f817..18c5d5c9c2872abe0faa09392da2787ad9f89d96 100644
--- a/src/socExec.ml
+++ b/src/socExec.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 09/12/2013 (at 10:24) by Erwan Jahier> *)
+(* Time-stamp: <modified the 20/02/2014 (at 11:21) by Erwan Jahier> *)
open Soc
open Data
@@ -323,11 +323,8 @@ let (f : Lv6MainArgs.t -> Soc.tbl -> Soc.key -> unit) =
fun opt soc_tbl sk ->
let soc = try SocMap.find sk soc_tbl with Not_found -> assert false in
let ctx = SocExecValue.create_ctx soc_tbl soc in
- let vntl_of_profile = List.map (fun (x,t) -> x,SocUtils.string_of_type_ref t) in
let exp_vntl_i = expand_profile true (fst soc.profile) in
let exp_vntl_o = expand_profile true (snd soc.profile) in
- let exp_vntl_i_str = vntl_of_profile exp_vntl_i in
- let exp_vntl_o_str = vntl_of_profile exp_vntl_o in
let oc =
if opt.Lv6MainArgs.outfile = "" then stdout else
let rif_file =
@@ -337,9 +334,9 @@ let (f : Lv6MainArgs.t -> Soc.tbl -> Soc.key -> unit) =
open_out rif_file
in
Lv6util.dump_entete oc;
- RifIO.write_interface oc exp_vntl_i_str exp_vntl_o_str None None;
+ RifIO.write_interface oc exp_vntl_i exp_vntl_o None None;
RifIO.flush oc;
- try loop_step opt soc_tbl (fst soc.profile) exp_vntl_i_str exp_vntl_o_str soc ctx 1 oc
+ try loop_step opt soc_tbl (fst soc.profile) exp_vntl_i exp_vntl_o soc ctx 1 oc
with RifIO.Bye ->
close_out oc
@@ -365,8 +362,8 @@ let rec (do_step_dbg : Soc.tbl -> Soc.t -> Event.ctx -> SocExecValue.ctx ->
Event.ctx_name = soc_name;
Event.ctx_depth = ectx.Event.ctx_depth+1;
Event.ctx_data = datal;
- Event.ctx_inputs = List.map fst (fst soc.profile);
- Event.ctx_outputs = List.map fst (snd soc.profile);
+ Event.ctx_inputs = fst soc.profile;
+ Event.ctx_outputs = snd soc.profile;
}
in
let cont2 ctx =
@@ -387,16 +384,13 @@ let rec (do_step_dbg : Soc.tbl -> Soc.t -> Event.ctx -> SocExecValue.ctx ->
Event.step = ectx.Event.ctx_step;
Event.nb = enb;
Event.depth = ectx.Event.ctx_depth;
- Event.kind =
- Event.Node {
- Event.lang = "lustre";
- Event.name = soc_name;
- Event.port = Event.Exit ("",Expr.True,lazy_si);
- Event.inputs = ectx.Event.ctx_inputs;
- Event.outputs = ectx.Event.ctx_outputs;
- };
+ Event.kind = Event.Exit;
+ Event.lang = "lustre";
+ Event.name = soc_name;
+ Event.inputs = ectx.Event.ctx_inputs;
+ Event.outputs = ectx.Event.ctx_outputs;
+ Event.sinfo = None;
Event.data = ectx.Event.ctx_data;
- Event.other = "";
Event.next = (fun () -> Event.event_nb := enb; cont ctx);
Event.terminate = ectx.Event.ctx_terminate;
}
@@ -405,16 +399,13 @@ let rec (do_step_dbg : Soc.tbl -> Soc.t -> Event.ctx -> SocExecValue.ctx ->
Event.step = ectx.Event.ctx_step;
Event.nb = (Event.incr_nb (); Event.get_nb ());
Event.depth = ectx.Event.ctx_depth;
- Event.kind =
- Event.Node {
- Event.lang = "lustre";
- Event.name = soc_name;
- Event.port = Event.Call;
- Event.inputs = ectx.Event.ctx_inputs;
- Event.outputs = ectx.Event.ctx_outputs;
- };
+ Event.kind = Event.Call;
+ Event.lang = "lustre";
+ Event.name = soc_name;
+ Event.inputs = ectx.Event.ctx_inputs;
+ Event.outputs = ectx.Event.ctx_outputs;
+ Event.sinfo = None;
Event.data = ectx.Event.ctx_data;
- Event.other = "";
Event.next = (fun () ->
let step = match soc.step with [step] -> step | _ -> assert false in
let ctx = soc_step step soc_tbl soc ctx in
diff --git a/test/lus2lic.sum b/test/lus2lic.sum
index 47a9bcbe10967956cb1bac577dff55f04e22d21f..2e8d506a7bb07bb9d850a605c72792229ce05bdc 100644
--- a/test/lus2lic.sum
+++ b/test/lus2lic.sum
@@ -1,4 +1,4 @@
-Test Run By jahier on Wed Jan 22 17:58:47 2014
+Test Run By jahier on Thu Feb 20 11:26:43 2014
Native configuration is i686-pc-linux-gnu
=== lus2lic tests ===
@@ -1028,5 +1028,7 @@ XPASS: Test bad programs (semantics): lus2lic {-o /tmp/bug.lic should_fail/seman
# of unexpected failures 76
# of unexpected successes 21
# of expected failures 37
-testcase ./lus2lic.tests/non-reg.exp completed in 110 seconds
+testcase ./lus2lic.tests/non-reg.exp completed in 103 seconds
+testcase ./lus2lic.tests/progression.exp completed in 1 seconds
+testcase ./lus2lic.tests/non-reg.exp completed in 103 seconds
testcase ./lus2lic.tests/progression.exp completed in 1 seconds
diff --git a/test/lus2lic.time b/test/lus2lic.time
index b1fee80fdd16289034d6be1d24a2195d4702924b..424e721127614bbeee095b184882208e3d2b5378 100644
--- a/test/lus2lic.time
+++ b/test/lus2lic.time
@@ -1,2 +1,2 @@
-testcase ./lus2lic.tests/non-reg.exp completed in 110 seconds
+testcase ./lus2lic.tests/non-reg.exp completed in 103 seconds
testcase ./lus2lic.tests/progression.exp completed in 1 seconds
diff --git a/utils/test_lus2lic_no_node b/utils/test_lus2lic_no_node
index 3e12738eed6d69331b689296f265781f24a39957..9ea95c56d2c8c23b46d326b2ffff63bce01dcf69 100755
--- a/utils/test_lus2lic_no_node
+++ b/utils/test_lus2lic_no_node
@@ -13,6 +13,7 @@ ec="$node".ec
lv4_node="$node__$node"
env=_"$node"_env.lut
+
set -x verbose #echo on
if
@@ -40,6 +41,7 @@ else
fi
+
export PATH=/usr/local/tools/lustre/bin/:$PATH
# if
# ./lus2lic $_oracle -n $oracle -ec -o $oracle.ec
diff --git a/utils/test_lus2lic_no_node_rdbg b/utils/test_lus2lic_no_node_rdbg
index e811dfd5718af35818c4a0953f0e78b2b1616c9c..99c5e2f233869278ba7ff8703d550f82f434796f 100755
--- a/utils/test_lus2lic_no_node_rdbg
+++ b/utils/test_lus2lic_no_node_rdbg
@@ -1,6 +1,7 @@
#!/bin/sh
+ocamlopt=/usr/local/soft/ocaml/4.01.0/bin/ocamlopt.opt
lustre_file=$1
node=`basename $lustre_file .lus`
_oracle=_"$node"_oracle.lus
@@ -10,7 +11,6 @@ ec="$node".ec
lv4_node="$node__$node"
env=_"$node"_env.lut
export RDBG_PATH="$HOME/rdbg"
-
set -x verbose #echo on
if
@@ -53,15 +53,9 @@ export PATH=/usr/local/tools/lustre/bin/:$PATH
-# ./lus2lic -4ocaml -o oracle.ml $_oracle -n $oracle
-# ./lus2lic -4ocaml -o sut.ml $ec -n $lv4_node
-# ./lutin -4ocaml -o env.ml $env
-# ocamlopt -shared -o -I +lustre sut.cmxs lus4ocaml.cmxa sut.ml
-# ocamlopt -shared -o -I +lustre oracle.cmxs lus4ocaml.cmxa oracle.ml
-# ocamlopt -shared -o -I +lutin env.cmxs $CLIB $CMXA env.ml
+export CMXA="polka.cmxa bdd.cmxa lut4ocaml.cmxa"
+export CLIB="-cclib -lgmp -cclib -lpolkag_caml -cclib -lpolkal_caml -cclib -lpolkai_caml -cclib -lcamlidl -cclib -lpolkag -cclib -lpolkal -cclib -lpolkai -cclib -lbdd_stubs -cclib -lEzdl_c_stubs"
-# ./rdbgbatch -lurette --seed 42 -l 10 --sut sut.cmxs --env env.cmxs --oracle oracle.cmxs -p 6
-#--stop-on-oracle-error ;
# ./lurettetop -p 6 -seed 42 \
# -rp "sut:ec:$ec:$lv4_node" \
@@ -71,10 +65,42 @@ export PATH=/usr/local/tools/lustre/bin/:$PATH
#--stop-on-oracle-error;
if
-$RDBG_PATH/rdbgbatch.native -lurette --seed 42 -p 6 -l 10 --stop-on-oracle-error \
- --sut-stdio "./patch_ecexe $ec $lv4_node" \
- --env-stdio "./lutin -boot -rif $env" \
- --oracle-stdio "./lus2lic -exec -rif $_oracle -n $oracle" ;
+ echo "Generating oracle.cmxs";
+ ./lus2lic -ocaml -o oracle.ml $_oracle -n $oracle &&
+ $ocamlopt -shared -o oracle.cmxs -I +lustre-v6 -I +rdbg-plugin lus4ocaml.cmxa oracle.ml &&
+
+ echo "Generating sut.cmxs" &&
+ ./lus2lic -ocaml -o sut.ml $ec -n $lv4_node &&
+ $ocamlopt -shared -o sut.cmxs -I +lustre-v6 -I +rdbg-plugin lus4ocaml.cmxa sut.ml &&
+
+ echo "Generating env.cmxs" &&
+ ./lutin -seed 42 -ocaml -o env.ml $env &&
+ $ocamlopt -shared -o env.cmxs -I +lutin -I +rdbg-plugin $CLIB $CMXA env.ml &&
+
+ ./lurettetop -p 6 -seed 42 \
+ -rp "sut:ec:$ec:$lv4_node" \
+ -rp "env:lutin:$env" \
+ -rp "oracle:v6:$_oracle:$oracle" \
+ -go -l 10 -ns2c --stop-on-oracle-error;
+
+ echo " $RDBG_PATH/rdbgbatch.native -lurette --seed 42 -l 100 -p 6 --stop-on-oracle-error \
+ --sut sut.cmxs \
+ --env env.cmxs \
+ --oracle oracle.cmxs ";
+
+ echo " $RDBG_PATH/rdbgbatch.native -lurette --seed 42 -l 100 -p 6 --stop-on-oracle-error \
+ --sut-stdio \"./patch_ecexe $ec $lv4_node\" \
+ --env-stdio \"./lutin -boot -rif $env\" \
+ --oracle-stdio \"./lus2lic -exec -rif $_oracle -n $oracle\" ";
+# --sut sut.cmxs \
+# --env-stdio "./lutin -boot -rif $env" \
+# --oracle-stdio "./lus2lic -exec -rif $_oracle -n $oracle" ;
+
+
+#$RDBG_PATH/rdbgbatch.native -lurette --seed 42 -p 6 -l 10 --stop-on-oracle-error \
+# --sut-stdio "./patch_ecexe $ec $lv4_node" \
+# --env-stdio "./lutin -boot -rif $env" \
+# --oracle-stdio "./lus2lic -exec -rif $_oracle -n $oracle" ;
then
echo "rdbg -lurette: ok"
else