diff --git a/_oasis b/_oasis
index 01cf90633bdf966cf3c0587c47367c86f71fbdb9..b66062daeba341a33ede2f0488c28344aec417db 100644
--- a/_oasis
+++ b/_oasis
@@ -1,6 +1,6 @@
OASISFormat: 0.4
Name: lustre-v6
-Version: 1.667
+Version: 1.668
Synopsis: The Lustre V6 Verimag compiler
Description: This package contains:
(1) lus2lic: the (current) name of the compiler (and interpreter via -exec).
diff --git a/arduino/led_puzlle/Makefile b/arduino/led_puzlle/Makefile
index 80ceb18f2bac1f6e5c78ae942fafd5dfe831423b..1f55edb1fa265924e8d79289585f4f8b814379cb 100644
--- a/arduino/led_puzlle/Makefile
+++ b/arduino/led_puzlle/Makefile
@@ -17,7 +17,7 @@ v6: led.lus
%.no_sol:
lus2lic -ec -o no_sol.ec led.lus -n $*_has_no_solution
- ecverif no_sol.ec -diag || cat msg
+ ecverif no_sol.ec -diag | sed 's/not\ red//' | sed 's/not\ blue//' | sed 's/\ and\ //' || cat msg
clean:
rm -f *.c *.h *.ec *.sh *.rif rdbg-session.ml *.gp *.log *.dro
diff --git a/arduino/led_puzlle/doc/puzzle.org b/arduino/led_puzlle/doc/puzzle.org
index 3589ff426f5f4f55b1b9d5635ea33f551bf20f12..ae307d8ea55c4f838d66d902fe493cd549736511 100644
--- a/arduino/led_puzlle/doc/puzzle.org
+++ b/arduino/led_puzlle/doc/puzzle.org
@@ -23,7 +23,8 @@ Plusieurs approches :
- *Langages* de programmation (empêcher les programmeurs de faire des erreurs)
- *Analyse de programme*
- Tests automatisés
-* Nous allons embarquer des puzzles écrits en =Lustre= sur un =Arduino=
+
+Nous allons embarquer des puzzles écrits en =Lustre= sur un =Arduino=
file:arduino.jpg
@@ -73,13 +74,40 @@ true and true = true
true and false = false and true = false and false = false
#+END_SRC
-- Bouton blue => la led courante devient le « xor » des 2 leds autour
+- Bouton bleu => la led courante devient le « xor » des 2 leds autour
- Bouton red => la led courante devient le « and » des 2 leds autour
-- la led courante est le première au début, puis la deuxième, etc.
+- la led courante est la première au début, puis la deuxième, etc.
# Existe-t'il une configuration initiale qui rende le problème impossible ?
-* Puzzle 6 : saute mouton :noexport:
+* Puzzle 6
+
+- Bouton rouge => inverse l'état de la led 1
+- Bouton bleu => allume la led suivant la première led éteinte (en
+ partant de la led1)
+
+#+BEGIN_SRC lustre
+node puzzle6(red,blue:bool)
+returns (led1,led2,led3,led4,led5:bool);
+var
+ -- Xi = je suis la led qui suit la plus petite led eteinte
+ X2, X3, X4, X5 : bool;
+let
+ X2, X3, X4, X5 = (true, F, F, F) ->
+ if not(pre(led1)) then (true, F, F, F) else
+ if not(pre(led2)) then (F, true, F, F) else
+ if not(pre(led3)) then (F, F, true, F) else
+ if not(pre(led4)) then (F, F, F, true) else (F, F, F, F);
+
+ led1 = F -> if red then not(pre(led1)) else pre(led1);
+ led2 = F -> if blue and X2 then not(pre(led2)) else pre(led2);
+ led3 = F -> if blue and X3 then not(pre(led3)) else pre(led3);
+ led4 = F -> if blue and X4 then not(pre(led4)) else pre(led4);
+ led5 = F -> if blue and X5 then not(pre(led5)) else pre(led5);
+tel
+#+END_SRC
+
+* Puzzle : saute mouton :noexport:
- les leds jouent chacun leur tour
- pion présent = led allumé
diff --git a/arduino/led_puzlle/doc/puzzle.pdf b/arduino/led_puzlle/doc/puzzle.pdf
index 10281803ee5e1fa6f827c9e1a4f6ed1888fdcb71..24d8a915fd70ce922530a1fed0b948259f7c5650 100644
Binary files a/arduino/led_puzlle/doc/puzzle.pdf and b/arduino/led_puzlle/doc/puzzle.pdf differ
diff --git a/arduino/led_puzlle/led.lus b/arduino/led_puzlle/led.lus
index 5fdb5bf26e6c26185c115c8b3aa73a3494c83c7f..710f1cb185578e4eb5e34b5a5d66561cb5e8f6d2 100644
--- a/arduino/led_puzlle/led.lus
+++ b/arduino/led_puzlle/led.lus
@@ -8,7 +8,7 @@ const T=true;
const Eteint=false;
const Allume=true;
-const led1_0 = Eteint; -- demo : a mettre Vrai au debut, puis a faux apres la 1ere expe
+const led1_0 = Allume; -- demo : a mettre Vrai au debut, puis a faux apres la 1ere expe
const led2_0 = Allume;
const led3_0 = Eteint;
const led4_0 = Eteint;
@@ -153,35 +153,26 @@ tel
----------------------------------------------------------------------------
-- red => inversion de la led 1
--- blue => allume la led a droite de la premiere led non allumée
-
-const led1_p6 = F;
-const led2_p6 = F;
-const led3_p6 = F;
-const led4_p6 = F;
-const led5_p6 = F;
+-- blue => allume la led suivant la première led eteinte
+-- pour l'odre lexicographique (i.e.,led1<led2<led3<led4<led5)
node puzzle6(red,blue:bool)
returns (led1,led2,led3,led4,led5:bool);
var
+ -- Xi = je suis la led qui suit la plus petite led eteinte
X2, X3, X4, X5 : bool;
let
X2, X3, X4, X5 = (true, F, F, F) ->
- if blue or red then
- (
if not(pre(led1)) then (true, F, F, F) else
if not(pre(led2)) then (F, true, F, F) else
if not(pre(led3)) then (F, F, true, F) else
- if not(pre(led4)) then (F, F, F, true) else
- (F, F, F, F)
- )
- else (pre X2, pre X3, pre X4, pre X5);
+ if not(pre(led4)) then (F, F, F, true) else (F, F, F, F);
- led1 = led1_p6 -> if red then not(pre(led1)) else pre(led1);
- led2 = led2_p6 -> if blue and X2 then not(pre(led2)) else pre(led2);
- led3 = led3_p6 -> if blue and X3 then not(pre(led3)) else pre(led3);
- led4 = led4_p6 -> if blue and X4 then not(pre(led4)) else pre(led4);
- led5 = led5_p6 -> if blue and X5 then not(pre(led5)) else pre(led5);
+ led1 = F -> if red then not(pre(led1)) else pre(led1);
+ led2 = F -> if blue and X2 then not(pre(led2)) else pre(led2);
+ led3 = F -> if blue and X3 then not(pre(led3)) else pre(led3);
+ led4 = F -> if blue and X4 then not(pre(led4)) else pre(led4);
+ led5 = F -> if blue and X5 then not(pre(led5)) else pre(led5);
tel
----------------------------------------------------------------------------
----------------------------------------------------------------------------
diff --git a/arduino/led_puzlle/p6 b/arduino/led_puzlle/p6
index 11360fc88ad7d0e80aeae644e1abbee820fd7ce6..e9e89331891d21243ba7ba3fbe5ac706631eb27c 100755
--- a/arduino/led_puzlle/p6
+++ b/arduino/led_puzlle/p6
@@ -1 +1 @@
-make puzzle6.no_sol
\ No newline at end of file
+make puzzle6.no_sol
\ No newline at end of file
diff --git a/src/l2lSplit.ml b/src/l2lSplit.ml
index fed08a5bd73904ebdd2ac6b53c2984671b9ea22b..9c98679b1eae37e251f503ef019ee0a9daf1c56e 100644
--- a/src/l2lSplit.ml
+++ b/src/l2lSplit.ml
@@ -160,18 +160,18 @@ type split_acc = (Lic.eq_info srcflagged) list * Lic.var_info list
let rec (eq : Lic.eq_info Lxm.srcflagged -> split_acc) =
fun { src = lxm_eq ; it = (lhs, rhs) } ->
- let n_rhs, (neqs, nlocs) = split_val_exp false true rhs in
- { src = lxm_eq ; it = (lhs, n_rhs) }::neqs, nlocs
+ let n_rhs, (neqs, nlocs) = split_val_exp false true rhs in
+ { src = lxm_eq ; it = (lhs, n_rhs) }::neqs, nlocs
and (split_eq_acc : split_acc -> Lic.eq_info srcflagged -> split_acc) =
fun (eqs, locs) equation ->
- let (neqs, nlocs) = eq equation in
- let neqs = split_tuples neqs in
- List.rev_append neqs eqs, List.rev_append nlocs locs
+ let (neqs, nlocs) = eq equation in
+ let neqs = split_tuples neqs in
+ List.rev_append neqs eqs, List.rev_append nlocs locs
and (split_val_exp : bool -> bool -> Lic.val_exp -> Lic.val_exp * split_acc) =
fun when_flag top_level ve ->
- (* [when_flag] is true is the call is made from a "when" statement.
+ (* [when_flag] is true is the call is made from a "when" statement.
We need this flag in order to know if it is necessary to add
a when on constants. Indeed, in Lustre V6, it is not necessary
to write " 1 when clk + x " if x in on clk (it's more sweet).
@@ -181,197 +181,201 @@ and (split_val_exp : bool -> bool -> Lic.val_exp -> Lic.val_exp * split_acc) =
But is is not forbidden either! so we need to make sure that there
is no "when"...
- *)
- match ve.ve_core with
- | Merge(ce,cl) -> (
- let ce,(eql1, vl1) = split_val_exp false false ce in
- let const_l, vel = List.split cl in
- let vel,(eql2, vl2) = split_val_exp_list false false vel in
- let eql, vl = eql1@eql2, vl1@vl2 in
- let cl = List.combine const_l vel in
- let rhs = { ve with ve_core = Merge(ce,cl)} in
- if top_level then rhs, (eql, vl) else
- (* create the var for the current call *)
- let clk_l = ve.ve_clk in
- let typ_l = ve.ve_typ in
- assert (List.length typ_l = List.length clk_l);
- let nv_l = List.map2 new_var typ_l clk_l
- in
- let lxm = lxm_of_val_exp ve in
- let vi2val_exp nv =
- let _,clk = nv.var_clock_eff in
- {
- ve_core = CallByPosLic(Lxm.flagit (Lic.VAR_REF (nv.var_name_eff)) lxm,[]);
- ve_typ = [nv.var_type_eff];
- ve_clk = [clk];
- }
- in
- let nve = match nv_l with
- | [] -> assert false (* SNO *)
- | [nv] -> vi2val_exp nv
- | _ -> { ve with ve_core =
- CallByPosLic(Lxm.flagit Lic.TUPLE lxm, List.map vi2val_exp nv_l)
- }
- in
- let lpl = List.map (fun nv -> LeftVarLic(nv, lxm)) nv_l in
- let eq = Lxm.flagit (lpl, rhs) lxm in
- nve, (eql@[eq], vl@nv_l)
- )
- | CallByPosLic({it=Lic.VAR_REF _}, _) -> ve, ([],[])
- | CallByPosLic({it=Lic.CONST_REF _}, _) -> ve, ([],[])
- | CallByPosLic({src=lxm;it=Lic.CONST _}, _)
- -> if not when_flag then
- let clk = ve.ve_clk in
- match (clk) with
- | On(clock,clk)::_ ->
- { ve with ve_core =
- CallByPosLic({src=lxm;it=Lic.WHEN(On(clock,clk))},[ve])},
- ([],[])
- | (ClockVar _)::_ (* should not occur *)
- | BaseLic::_ -> ve, ([],[])
- | [] -> assert false (* should not occur *)
- else
- ve, ([],[])
- | CallByNameLic (by_name_op_eff, fl) -> (
- let lxm = by_name_op_eff.src in
- let fl, eql, vl =
- List.fold_left
- (fun (fl_acc, eql_acc, vl_acc) (fn, fv) ->
- let fv, (eql, vl) = split_val_exp false false fv in
- ((fn,fv)::fl_acc, eql@eql_acc, vl@vl_acc)
- )
- ([],[],[])
- fl
- in
- let rhs = { ve with ve_core = CallByNameLic (by_name_op_eff, List.rev fl) } in
- if top_level then
- rhs, (eql, vl)
- else
- (* create the var for the current call *)
- let clk_l = ve.ve_clk in
- let typ_l = ve.ve_typ in
- assert (List.length typ_l = List.length clk_l);
- let nv_l = List.map2 new_var typ_l clk_l in
- let nve = match nv_l with
- | [nv] -> { ve with ve_core =
- CallByPosLic(
- Lxm.flagit (Lic.VAR_REF (nv.var_name_eff)) lxm,
- []
- )}
- | _ -> assert false
- in
- let lpl = List.map (fun nv -> LeftVarLic(nv, lxm)) nv_l in
- let eq = Lxm.flagit (lpl, rhs) lxm in
- nve, (eql@[eq], vl@nv_l)
- )
- | CallByPosLic(by_pos_op_eff, vel) -> (
- (* recursively split the arguments *)
- let lxm = by_pos_op_eff.src in
- let (rhs, (eql,vl)) =
- match by_pos_op_eff.it with
- | Lic.HAT(i) ->
- let vel, (eql, vl) = split_val_exp_list false false vel in
- let by_pos_op_eff = Lxm.flagit (Lic.HAT(i)) lxm in
- let rhs = CallByPosLic(by_pos_op_eff, vel) in
- rhs, (eql, vl)
- | Lic.WHEN ve -> (* should we create a var for the clock? *)
- let vel,(eql, vl) = split_val_exp_list true false vel in
- let by_pos_op_eff = Lxm.flagit (Lic.WHEN(ve)) lxm in
- let rhs = CallByPosLic(by_pos_op_eff, vel) in
- rhs, (eql, vl)
- | _ ->
- let vel, (eql, vl) = split_val_exp_list false false vel in
- let rhs = CallByPosLic(by_pos_op_eff, vel) in
- rhs, (eql, vl)
- in
- let rhs = { ve with ve_core = rhs } in
- if top_level || by_pos_op_eff.it = TUPLE then
- rhs, (eql, vl)
- else
- (* create the var for the current call *)
- let clk_l = ve.ve_clk in
- let typ_l = ve.ve_typ in
- assert (List.length typ_l = List.length clk_l);
- let nv_l = List.map2 new_var typ_l clk_l in
- let nve =
- match nv_l with
- | [nv] -> {
- ve_typ = [nv.var_type_eff];
- ve_clk = clk_l;
- ve_core = CallByPosLic(
- Lxm.flagit (Lic.VAR_REF (nv.var_name_eff)) lxm,
- [])
- }
- | _ -> {
- ve_typ = List.map (fun v -> v.var_type_eff) nv_l;
- ve_clk = clk_l;
- ve_core = CallByPosLic(
- Lxm.flagit Lic.TUPLE lxm,
- (List.map
- (fun nv ->
- let nnv = {
- ve_core = CallByPosLic
- (Lxm.flagit (Lic.VAR_REF (nv.var_name_eff)) lxm, []);
- ve_typ = [nv.var_type_eff];
- ve_clk = [snd nv.var_clock_eff]
- }
- in
- nnv
- )
- nv_l
- )
- )
- }
- in
- let lpl = List.map (fun nv -> LeftVarLic(nv, lxm)) nv_l in
- let eq = Lxm.flagit (lpl, rhs) lxm in
- nve, (eql@[eq], vl@nv_l)
- )
+ *)
+ match ve.ve_core with
+ | Merge(ce,cl) -> (
+ let ce,(eql1, vl1) = split_val_exp false false ce in
+ let const_l, vel = List.split cl in
+ let vel,(eql2, vl2) = split_val_exp_list false false vel in
+ let eql, vl = eql1@eql2, vl1@vl2 in
+ let cl = List.combine const_l vel in
+ let rhs = { ve with ve_core = Merge(ce,cl)} in
+ if top_level then rhs, (eql, vl) else
+ (* create the var for the current call *)
+ let clk_l = ve.ve_clk in
+ let typ_l = ve.ve_typ in
+ assert (List.length typ_l = List.length clk_l);
+ let nv_l = List.map2 new_var typ_l clk_l
+ in
+ let lxm = lxm_of_val_exp ve in
+ let vi2val_exp nv =
+ let _,clk = nv.var_clock_eff in
+ {
+ ve_core = CallByPosLic(Lxm.flagit (Lic.VAR_REF (nv.var_name_eff)) lxm,[]);
+ ve_typ = [nv.var_type_eff];
+ ve_clk = [clk];
+ }
+ in
+ let nve = match nv_l with
+ | [] -> assert false (* SNO *)
+ | [nv] -> vi2val_exp nv
+ | _ -> { ve with ve_core =
+ CallByPosLic(Lxm.flagit Lic.TUPLE lxm, List.map vi2val_exp nv_l)
+ }
+ in
+ let lpl = List.map (fun nv -> LeftVarLic(nv, lxm)) nv_l in
+ let eq = Lxm.flagit (lpl, rhs) lxm in
+ nve, (eql@[eq], vl@nv_l)
+ )
+ | CallByPosLic({it=Lic.VAR_REF _}, _) -> ve, ([],[])
+ | CallByPosLic({it=Lic.CONST_REF _}, _) -> ve, ([],[])
+ | CallByPosLic({src=lxm;it=Lic.CONST _}, _)
+ -> if not when_flag then
+ let clk = ve.ve_clk in
+ match (clk) with
+ | On(clock,clk)::_ ->
+ { ve with ve_core =
+ CallByPosLic({src=lxm;it=Lic.WHEN(On(clock,clk))},[ve])},
+ ([],[])
+ | (ClockVar _)::_ (* should not occur *)
+ | BaseLic::_ -> ve, ([],[])
+ | [] -> assert false (* should not occur *)
+ else
+ ve, ([],[])
+ | CallByNameLic (by_name_op_eff, fl) -> (
+ let lxm = by_name_op_eff.src in
+ let fl, eql, vl =
+ List.fold_left
+ (fun (fl_acc, eql_acc, vl_acc) (fn, fv) ->
+ let fv, (eql, vl) = split_val_exp false false fv in
+ ((fn,fv)::fl_acc, eql@eql_acc, vl@vl_acc)
+ )
+ ([],[],[])
+ fl
+ in
+ let rhs = { ve with ve_core = CallByNameLic (by_name_op_eff, List.rev fl) } in
+ if top_level then
+ rhs, (eql, vl)
+ else
+ (* create the var for the current call *)
+ let clk_l = ve.ve_clk in
+ let typ_l = ve.ve_typ in
+ assert (List.length typ_l = List.length clk_l);
+ let nv_l = List.map2 new_var typ_l clk_l in
+ let nve = match nv_l with
+ | [nv] -> { ve with ve_core =
+ CallByPosLic(
+ Lxm.flagit (Lic.VAR_REF (nv.var_name_eff)) lxm,
+ []
+ )}
+ | _ -> assert false
+ in
+ let lpl = List.map (fun nv -> LeftVarLic(nv, lxm)) nv_l in
+ let eq = Lxm.flagit (lpl, rhs) lxm in
+ nve, (eql@[eq], vl@nv_l)
+ )
+ | CallByPosLic(by_pos_op_eff, vel) -> (
+ (* recursively split the arguments *)
+ let lxm = by_pos_op_eff.src in
+ let (rhs, (eql,vl)) =
+ match by_pos_op_eff.it with
+ | Lic.HAT(i) ->
+ let vel, (eql, vl) = split_val_exp_list false false vel in
+ let by_pos_op_eff = Lxm.flagit (Lic.HAT(i)) lxm in
+ let rhs = CallByPosLic(by_pos_op_eff, vel) in
+ rhs, (eql, vl)
+ | Lic.WHEN ve -> (* should we create a var for the clock? *)
+ let vel,(eql, vl) = split_val_exp_list true false vel in
+ let by_pos_op_eff = Lxm.flagit (Lic.WHEN(ve)) lxm in
+ let rhs = CallByPosLic(by_pos_op_eff, vel) in
+ rhs, (eql, vl)
+ | _ ->
+ let vel, (eql, vl) = split_val_exp_list false false vel in
+ let rhs = CallByPosLic(by_pos_op_eff, vel) in
+ rhs, (eql, vl)
+ in
+ let rhs = { ve with ve_core = rhs } in
+ if top_level || by_pos_op_eff.it = TUPLE then
+ rhs, (eql, vl)
+ else
+ (* create the var for the current call *)
+ let clk_l = ve.ve_clk in
+ let typ_l = ve.ve_typ in
+ assert (List.length typ_l = List.length clk_l);
+ let nv_l = List.map2 new_var typ_l clk_l in
+ let nve =
+ match nv_l with
+ | [nv] -> {
+ ve_typ = [nv.var_type_eff];
+ ve_clk = clk_l;
+ ve_core = CallByPosLic(
+ Lxm.flagit (Lic.VAR_REF (nv.var_name_eff)) lxm,
+ [])
+ }
+ | _ -> {
+ ve_typ = List.map (fun v -> v.var_type_eff) nv_l;
+ ve_clk = clk_l;
+ ve_core = CallByPosLic(
+ Lxm.flagit Lic.TUPLE lxm,
+ (List.map
+ (fun nv ->
+ let nnv = {
+ ve_core = CallByPosLic
+ (Lxm.flagit (Lic.VAR_REF (nv.var_name_eff)) lxm, []);
+ ve_typ = [nv.var_type_eff];
+ ve_clk = [snd nv.var_clock_eff]
+ }
+ in
+ nnv
+ )
+ nv_l
+ )
+ )
+ }
+ in
+ let lpl = List.map (fun nv -> LeftVarLic(nv, lxm)) nv_l in
+ let eq = Lxm.flagit (lpl, rhs) lxm in
+ nve, (eql@[eq], vl@nv_l)
+ )
-and (split_val_exp_list : bool -> bool -> Lic.val_exp list -> Lic.val_exp list * split_acc) =
+and (split_val_exp_list : bool -> bool -> Lic.val_exp list ->
+ Lic.val_exp list * split_acc) =
fun when_flag top_level vel ->
- let vel, accl =
- List.split (List.map (split_val_exp when_flag top_level) vel)
- in
- let eqll,vll = List.split accl in
- let eql, vl = List.flatten eqll, List.flatten vll in
- (vel,(eql,vl))
+ let vel, accl =
+ List.split (List.map (split_val_exp when_flag top_level) vel)
+ in
+ let eqll,vll = List.split accl in
+ let eql, vl = List.flatten eqll, List.flatten vll in
+ (vel,(eql,vl))
and split_node (opt:Lv6MainArgs.t) (n: Lic.node_exp) : Lic.node_exp =
- Lv6Verbose.exe ~flag:dbg (fun () ->
- Printf.eprintf "*** Splitting node %s\n"
- (LicDump.string_of_node_key_iter n.node_key_eff);
- flush stderr);
+ Lv6Verbose.exe
+ ~flag:dbg (fun () ->
+ Printf.eprintf "*** Splitting node %s\n"
+ (LicDump.string_of_node_key_iter n.node_key_eff);
+ flush stderr);
let res = match n.def_eff with
| ExternLic
| MetaOpLic
| AbstractLic None -> n
| AbstractLic (Some pn) ->
- { n with def_eff = AbstractLic (Some (split_node opt pn)) }
+ { n with def_eff = AbstractLic (Some (split_node opt pn)) }
| BodyLic b ->
- let loc = match n.loclist_eff with None -> [] | Some l -> l in
- let (neqs, nv) = List.fold_left (split_eq_acc) ([], loc) b.eqs_eff in
- profile_info (Printf.sprintf "Split %i equations into %i ones\n"
- (List.length b.eqs_eff)(List.length neqs));
-
- let (nasserts,neqs, nv) =
- if opt.Lv6MainArgs.gen_autotest then
- (* do not split assertions when generating lutin because we
+ let loc = match n.loclist_eff with None -> [] | Some l -> l in
+ let (neqs, nv) = List.fold_left (split_eq_acc) ([], loc) b.eqs_eff in
+ profile_info (Printf.sprintf "Split %i equations into %i ones\n"
+ (List.length b.eqs_eff) (List.length neqs));
+ let (nasserts,neqs, nv) =
+ if Lv6MainArgs.global_opt.Lv6MainArgs.gen_autotest then
+ (* do not split assertions when generating Lutin because we
would handle less assertions *)
- (b.asserts_eff,neqs, nv)
- else
- let asserts = List.map (fun x -> x.it) b.asserts_eff in
- let lxm_asserts = List.map (fun x -> x.src) b.asserts_eff in
- let nasserts,(neqs_asserts,nv_asserts) =
- split_val_exp_list false true asserts
- in
- assert (List.length nasserts = List.length lxm_asserts);
- let nasserts = List.map2 Lxm.flagit nasserts lxm_asserts in
- (nasserts,neqs@neqs_asserts, nv@nv_asserts)
- in
- let neqs = List.map remove_tuple_from_eq neqs in
- let nb = { eqs_eff = neqs ; asserts_eff = nasserts } in
- { n with loclist_eff = Some nv; def_eff = BodyLic nb }
+ (b.asserts_eff,neqs, nv)
+ else
+ let asserts = List.map (fun x -> x.it) b.asserts_eff in
+ let lxm_asserts = List.map (fun x -> x.src) b.asserts_eff in
+ let nasserts,(neqs_asserts,nv_asserts) =
+ split_val_exp_list false false
+ (* force the creation of a new var for
+ assert so that it is easier to
+ check in SocExec *) asserts
+ in
+ assert (List.length nasserts = List.length lxm_asserts);
+ let nasserts = List.map2 Lxm.flagit nasserts lxm_asserts in
+ (nasserts,neqs@neqs_asserts, nv@nv_asserts)
+ in
+ let neqs = List.map remove_tuple_from_eq neqs in
+ let nb = { eqs_eff = neqs ; asserts_eff = nasserts } in
+ { n with loclist_eff = Some nv; def_eff = BodyLic nb }
in
res
diff --git a/src/lic2soc.ml b/src/lic2soc.ml
index cff1bf7491deb0cb20ffb8131a8fbca471f6c7bd..1cd16da7722af79b4a87673b4a2d2a4073a569f6 100644
--- a/src/lic2soc.ml
+++ b/src/lic2soc.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 03/02/2016 (at 15:10) by Erwan Jahier> *)
+(** Time-stamp: <modified the 19/10/2016 (at 16:15) by Erwan Jahier> *)
(* XXX ce module est mal écrit. A reprendre. (R1) *)
@@ -161,9 +161,10 @@ let rec get_leaf: (LicPrg.t -> Lic.val_exp -> Soc.var_expr list option) =
let type_ = lic_to_data_type (List.hd type_) in
let filter_expr = match get_leaf licprg expr with
| Some [f] -> f
- | None -> assert false (* should not happen, since the expression should be a leaf *)
- | _ -> assert false (* We should get only ONE filter, otherwise it doesn't make any
- sense *)
+ | None -> assert false
+ (* should not happen, since the expression should be a leaf *)
+ | _ -> assert false
+ (* We should get only ONE filter, otherwise it doesn't make any sense *)
in
Some [Soc.Index(filter_expr, i, type_)]
)
@@ -261,6 +262,15 @@ let build_extern_step: Lxm.t -> string -> Lic.node_exp -> Soc.step_method =
(* Soc.impl = Soc.Gaol ([], []) *)
}
+let (lic_val_exp_to_soc_var : LicPrg.t -> Lic.val_exp Lxm.srcflagged ->
+ Lxm.t * Soc.var) =
+ fun prg ve ->
+ match get_leaf prg ve.it with
+ | Some [Var v] -> ve.src, v
+ | Some _ -> assert false
+ | None ->
+ failwith ("Should be a var: "^(LicDump.string_of_val_exp_eff ve.it))
+
let (lic_to_soc_var : Lic.var_info -> Soc.var) =
fun vi ->
vi.Lic.var_name_eff, lic_to_data_type vi.Lic.var_type_eff
@@ -789,14 +799,17 @@ let rec f: (LicPrg.t -> Lic.node_key -> Soc.key * Soc.tbl) =
];
Soc.memory = Soc.Mem Data.Bool; (* to hold the first step flag *)
Soc.precedences = [];
+ Soc.assertions = [ (* something to do? *)];
}
in
soc_tbl, soc
(** Produit des soc de noeuds. *)
- and (soc_of_node: LicPrg.t -> Lic.node_exp -> Soc.tbl -> (ctx * Soc.t * Soc.tbl) option) =
+ and (soc_of_node: LicPrg.t -> Lic.node_exp -> Soc.tbl ->
+ (ctx * Soc.t * Soc.tbl) option) =
fun licprg node soc_tbl ->
- profile_info ("Lic2soc.soc_of_node..."^(Lic.string_of_node_key node.node_key_eff)^"\n");
+ profile_info ("Lic2soc.soc_of_node..."^
+ (Lic.string_of_node_key node.node_key_eff)^"\n");
let io_list = node.Lic.inlist_eff @ node.Lic.outlist_eff in
let io_type = List.map (fun vi -> lic_to_data_type vi.var_type_eff) io_list in
let soc_key = make_soc_key_of_node_key node.Lic.node_key_eff None io_type in
@@ -839,6 +852,12 @@ let rec f: (LicPrg.t -> Lic.node_key -> Soc.key * Soc.tbl) =
Soc.step = [step];
Soc.memory = Soc.No_mem;
Soc.precedences = [];
+ Soc.assertions =
+ if Lv6MainArgs.global_opt.Lv6MainArgs.gen_autotest then
+ [] (* In this mode no code is generated and the var creation
+ is inhibited in L2Lsplit *)
+ else
+ List.map (lic_val_exp_to_soc_var licprg) b.asserts_eff;
}
in
Some(ctx, soc, soc_tbl)
@@ -880,6 +899,7 @@ let rec f: (LicPrg.t -> Lic.node_key -> Soc.key * Soc.tbl) =
];
Soc.memory = Soc.No_mem;
Soc.precedences = [];
+ Soc.assertions = [];
}
in
@@ -919,6 +939,7 @@ let rec f: (LicPrg.t -> Lic.node_key -> Soc.key * Soc.tbl) =
];
Soc.memory = Soc.No_mem;
Soc.precedences = [];
+ Soc.assertions = [];
}
in
Some(ctx, soc, soc_tbl)
@@ -940,6 +961,7 @@ let rec f: (LicPrg.t -> Lic.node_key -> Soc.key * Soc.tbl) =
Soc.step = [step];
Soc.memory = if node.Lic.has_mem_eff then Soc.Mem_hidden else Soc.No_mem;
Soc.precedences = [];
+ Soc.assertions = [];
}
in
Some(ctx, soc, soc_tbl)
diff --git a/src/lv6MainArgs.ml b/src/lv6MainArgs.ml
index 72e25be03a733c38968133cd84089d99d81229b5..10b6585fe5695cdcc6b5957d4dc03a709cf335e2 100644
--- a/src/lv6MainArgs.ml
+++ b/src/lv6MainArgs.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 07/10/2016 (at 15:44) by Erwan Jahier> *)
+(* Time-stamp: <modified the 19/10/2016 (at 15:30) by Erwan Jahier> *)
(*
Le manager d'argument adapté de celui de lutin, plus joli
N.B. solution un peu batarde : les options sont stockées, comme avant, dans Global,
@@ -34,7 +34,6 @@ type t = {
mutable expand_arrays : bool;
mutable expand_io_type : bool;
mutable optim_ite : bool;
- mutable gen_autotest : bool;
mutable oc : Pervasives.out_channel;
mutable tlex : bool;
mutable exec : bool;
@@ -52,6 +51,7 @@ type global_opt = {
mutable lv4 : bool;
mutable kcg : bool;
mutable ec : bool;
+ mutable gen_autotest : bool;
mutable expand_enums : enum_mode;
mutable one_op_per_equation : bool;
mutable when_on_ident : bool;
@@ -72,6 +72,7 @@ type global_opt = {
let (global_opt:global_opt) =
{
gen_c_inline_predef = true;
+ gen_autotest = false;
lv4 = false;
kcg = false;
ec = false;
@@ -113,7 +114,6 @@ let (make_opt : unit -> t) =
expand_arrays = false;
expand_io_type = false;
optim_ite = false;
- gen_autotest = false;
(** the output channel *)
oc = Pervasives.stdout;
tlex = false;
@@ -532,7 +532,7 @@ let mkoptab (opt:t) : unit = (
;
mkopt opt ~doc_level:Dev
["--gen-autotest"]
- (Arg.Unit (fun () -> opt.gen_autotest <- true))
+ (Arg.Unit (fun () -> global_opt.gen_autotest <- true))
["Generate a Lutin Stimulator and a Lustre oracle to compare the ";
"result of 2 Lustre compilers"]
;
diff --git a/src/lv6MainArgs.mli b/src/lv6MainArgs.mli
index 2d5951cd20f589e34b20f94e4c0db0b10a1c3fea..78311d48bb3b1bcf0bfea5a32d5e6aa4ccdfdc6b 100644
--- a/src/lv6MainArgs.mli
+++ b/src/lv6MainArgs.mli
@@ -37,7 +37,6 @@ type t = {
mutable expand_arrays : bool;
mutable expand_io_type : bool;
mutable optim_ite : bool;
- mutable gen_autotest : bool;
mutable oc : Pervasives.out_channel;
mutable tlex : bool;
mutable exec : bool;
@@ -54,6 +53,7 @@ type global_opt = {
mutable lv4 : bool;
mutable kcg : bool;
mutable ec : bool;
+ mutable gen_autotest : bool;
mutable expand_enums : enum_mode;
mutable one_op_per_equation : bool;
mutable when_on_ident : bool;
diff --git a/src/lv6version.ml b/src/lv6version.ml
index e2fdf4acd29ed64480eeb48c17d00acdcb5e1154..1846eea21c8bd2b1af3d0f4a61d9244236907dfd 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 = "667"
-let sha_1 = "0a4f0ac51cb58e08145ea1e34ce815003f98d304"
+let commit = "668"
+let sha_1 = "35901e970a0c377cc36d6437dcbc61beb8001b54"
let str = (branch ^ "." ^ commit ^ " (" ^ sha_1 ^ ")")
let maintainer = "jahier@imag.fr"
diff --git a/src/main.ml b/src/main.ml
index 48838b5f07c1aaf2b22c1f11a9248c768dea9fd9..eb61eb00e597d7f2ff08be59805de5c0c30753f6 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 06/09/2016 (at 10:29) by Erwan Jahier> *)
+(* Time-stamp: <modified the 19/10/2016 (at 16:28) by Erwan Jahier> *)
open Lv6Verbose
open AstV6
@@ -268,7 +268,7 @@ let main () = (
profile_info "bye!";
my_exit opt 0
);
- if opt.Lv6MainArgs.gen_autotest then
+ if global_opt.Lv6MainArgs.gen_autotest then
gen_autotest_files lic_prg main_node opt
else if opt.gen_ocaml then
GenOcamlGlue.f Sys.argv opt
@@ -329,6 +329,9 @@ let main () = (
flush opt.oc;
print_compile_error lxm msg;
my_exit opt 1
+ | SocExec.AssertViolation lxm ->
+ print_compile_error lxm "An assertion is violated in the Lustre program";
+ my_exit opt 1
| Assert_failure (file, line, col) ->
prerr_string (
"\n*** oops: lus2lic internal error\n\tFile \""^ file ^
diff --git a/src/soc.ml b/src/soc.ml
index 6d224e98e2d01a82e8f7903760be7ed9c8f78557..04ff65dd3dcdc6d4d7685609dffa2483db293ebc 100644
--- a/src/soc.ml
+++ b/src/soc.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 09/04/2015 (at 11:36) by Erwan Jahier> *)
+(* Time-stamp: <modified the 19/10/2016 (at 16:13) by Erwan Jahier> *)
(** Synchronous Object Component *)
@@ -93,7 +93,8 @@ type t = {
precedences : precedence list; (* partial order over step methods *)
instances : instance list;
memory : memory;
- (* Do this soc have a memory (pre, fby) + its type *)
+ (* Do this soc have a memory (pre, fby) + its type *)
+ assertions: (Lxm.t * var) list;
}
(* SocKeyMap ? *)
diff --git a/src/socExec.ml b/src/socExec.ml
index 93df2a19e5ab3e8fb93bb810704d366e89ad31e4..04f27735f8dfa663f988e5f36cfd48e2c7544af0 100644
--- a/src/socExec.ml
+++ b/src/socExec.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 20/09/2016 (at 15:17) by Erwan Jahier> *)
+(* Time-stamp: <modified the 19/10/2016 (at 16:28) by Erwan Jahier> *)
open Soc
open Data
@@ -206,7 +206,8 @@ let (add_data_subst : var list -> Data.subst list -> SocExecValue.substs -> SocE
let s = SocVar.unexpand_profile s vntl_i in
List.fold_left (fun acc (id,v) -> sadd acc [id] v) ctx_s s
-let (read_soc_input : Lv6MainArgs.t -> var list -> Data.vntl -> out_channel -> substs -> substs) =
+let (read_soc_input : Lv6MainArgs.t -> var list -> Data.vntl -> out_channel ->
+ substs -> substs) =
fun opt vntl_i exp_vntl_i_str oc ctx_s ->
let s:Data.subst list =
RifIO.read ~debug:(Lv6Verbose.level()>0) stdin
@@ -214,6 +215,18 @@ let (read_soc_input : Lv6MainArgs.t -> var list -> Data.vntl -> out_channel -> s
in
add_data_subst vntl_i s ctx_s
+
+exception AssertViolation of Lxm.t
+let (check_assertions : SocExecValue.ctx -> Lxm.t * Soc.var -> unit) =
+ fun ctx (lxm,(v,t)) ->
+ assert(t=Data.Bool);
+ match SocExecValue.get_val v ctx with
+ | Data.B true -> ()
+ | Data.B false -> raise (AssertViolation lxm)
+ | _ -> assert false (* sno *)
+
+
+
let rec (loop_step : Lv6MainArgs.t -> Soc.tbl -> Soc.var list -> Data.vntl -> Data.vntl
-> Soc.t -> SocExecValue.ctx -> int -> out_channel -> unit) =
fun opt soc_tbl vntl_i exp_vntl_i_str exp_vntl_o_str soc ctx step_nb oc ->
@@ -229,6 +242,7 @@ let rec (loop_step : Lv6MainArgs.t -> Soc.tbl -> Soc.var list -> Data.vntl -> Da
RifIO.write oc "\n";
RifIO.flush oc;
Lv6Verbose.exe ~flag:dbg (fun () -> dump_substs ctx.s; flush stdout);
+ List.iter (check_assertions ctx) soc.assertions;
loop_step opt soc_tbl vntl_i exp_vntl_i_str exp_vntl_o_str soc ctx (step_nb+1) oc
let (f : Lv6MainArgs.t -> Soc.tbl -> Soc.key -> unit) =
diff --git a/src/socExec.mli b/src/socExec.mli
index 38e747738f5b87c0ed898f27c000e50d8d98159c..c59c1b156f20326c9086ddfad8bb8aa47a72f3fb 100644
--- a/src/socExec.mli
+++ b/src/socExec.mli
@@ -1,4 +1,6 @@
-(* Time-stamp: <modified the 25/01/2016 (at 11:16) by Erwan Jahier> *)
+(* Time-stamp: <modified the 19/10/2016 (at 16:29) by Erwan Jahier> *)
+
+exception AssertViolation of Lxm.t
(* The entry point for lus2lic -exec *)
val f : Lv6MainArgs.t -> Soc.tbl -> Soc.key -> unit
diff --git a/src/socPredef.ml b/src/socPredef.ml
index b3b51548e8099366d1e196a2ff6bd6dad3d50773..d864a1675c3b35eaaeb61293ec0bf306e29cbd08 100644
--- a/src/socPredef.ml
+++ b/src/socPredef.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 08/09/2016 (at 17:08) by Erwan Jahier> *)
+(* Time-stamp: <modified the 14/10/2016 (at 17:02) by Erwan Jahier> *)
(** Synchronous Object Code for Predefined operators. *)
@@ -63,6 +63,7 @@ let make_soc key profile steps = {
precedences = [];
step = steps;
memory = No_mem;
+ assertions = [];
}
let (get_mem_name : Soc.key -> Data.t -> string) =
@@ -114,6 +115,7 @@ let of_fby_soc_key : Soc.var_expr -> Soc.key -> Soc.t =
};
];
precedences = ["set", ["get"]];
+ assertions = [];
}
(* exported *)
@@ -199,6 +201,7 @@ let of_soc_key : Soc.key -> Soc.t =
};
];
precedences = [];
+ assertions = [];
}
)
@@ -234,6 +237,7 @@ let of_soc_key : Soc.key -> Soc.t =
};
];
precedences = ["set", ["get"]];
+ assertions = [];
}
| "Lustre::arrow" ->
let prof = sp tl in
@@ -251,6 +255,7 @@ let of_soc_key : Soc.key -> Soc.t =
}
];
precedences = [];
+ assertions = [];
memory = Mem Bool;
}
| "Lustre::if" -> {
@@ -259,6 +264,7 @@ let of_soc_key : Soc.key -> Soc.t =
instances = [];
(* init = None; *)
precedences = [];
+ assertions = [];
memory = No_mem;
step = [
{
@@ -289,6 +295,7 @@ let of_soc_key : Soc.key -> Soc.t =
];
Soc.memory = No_mem;
Soc.precedences = [];
+ Soc.assertions = [];
}
| "Lustre::diese" ->
let size = match sk with
@@ -310,6 +317,7 @@ let of_soc_key : Soc.key -> Soc.t =
];
Soc.memory = No_mem;
Soc.precedences = [];
+ Soc.assertions = [];
}
| _ ->
failwith ("*** The soc of "^id ^ " is not defined! \n")
@@ -389,6 +397,7 @@ let make_array_slice_soc : Lic.slice_info -> int -> Data.t -> Soc.t =
};
];
precedences = [];
+ assertions = [];
memory = No_mem;
}
@@ -417,6 +426,7 @@ let make_array_soc: int -> Data.t -> Soc.t =
};
];
precedences = [];
+ assertions = [];
memory = No_mem;
}
@@ -439,6 +449,7 @@ let make_array_concat_soc: int -> int -> Data.t -> Soc.t =
};
];
precedences = [];
+ assertions = [];
memory = No_mem;
}
@@ -463,6 +474,7 @@ let make_hat_soc: int -> Data.t -> Soc.t =
};
];
precedences = [];
+ assertions = [];
memory = No_mem;
}