diff --git a/_oasis b/_oasis
index 2e5d5805e3f9bbd152a1e6a3eb4ea65d0ae2dd53..51598dbdd75deb9ec1444cfda270fd990fecf3ee 100644
--- a/_oasis
+++ b/_oasis
@@ -1,6 +1,6 @@
OASISFormat: 0.4
Name: lustre-v6
-Version: 1.692
+Version: 1.693
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/doc/puzzle.org b/arduino/led_puzlle/doc/puzzle.org
index 92f4391034f09719dc20f47866d26fbf9f33a9cd..c2a334dfc3f897fc2efdef734f3376244bbcff49 100644
--- a/arduino/led_puzlle/doc/puzzle.org
+++ b/arduino/led_puzlle/doc/puzzle.org
@@ -21,7 +21,7 @@ _corrects_.
- La correction des programmes est cruciale, en particulier pour les
*systèmes embarqués*, car des vies sont souvent en jeu.
- Mais elle est difficile à cause de *l'explosion combinatoire*. Une
- bonne illustration de ce phénoméne est donnée par l'échiquer de
+ bonne illustration de ce phénomène est donnée par l'échiquier de
Sissa, comportant 1 grain de riz sur case 1, 2 grains sur la case
2, 4 sur la case 3, 8 sur la case 4, etc. Un tel échiquier comporte
$2^{64}-1$ grains de riz, c'est à dire plus de 18\nbsp{}milliards de
@@ -51,19 +51,20 @@ permettant de montrer
3. comment prouver automatiquement des propriétés sur ces programmes ;
4. comment tester automatiquement ces programmes.
-Il s'agit donc de valider est donc un petit système, composé d'un
+Il s'agit donc de valider un petit système, composé d'un
programme Lustre et d'une carte =Arduino=, comportant 2 entrées,
contrôllées par un bouton rouge et un bouton bleu, et 5 sorties,
représentées par 5 leds.
-La propriété de sureté que l'on veut vérifier est « il est impossible
-d'allumer les 5 leds ». Pour chaque programme qu'on embarquera sur
-la carte, la question sera donc
-de savoir s'il est possible d'allumer les
-5 leds (signifiant qu'il y a un problème) en jouant sur les entrées.
-Nous montreront ensuite comment des outils peuvent automatiser la
-preuve de correction ou de non correction.
+Nous proposons plusieurs programmes. Pour chacun d'entre eux, l'effet
+sur les leds d'une pression sur le bouton bleu ou le bouton rouge est
+différent. Mais à chaque fois, la propriété de sûreté que l'on veut
+vérifier est « il est impossible d'allumer les 5 leds ».
+Le public pourra essayer de résoudre ces petits puzzles, en essayant
+de déterminer s'il existe une séquence qui amène le système dans
+l'état dangereux. Nous montrerons ensuite comment des outils peuvent
+automatiser la réponse à ces petits puzzles.
* Puzzle 1
diff --git a/src/l2lExpandNodes.ml b/src/l2lExpandNodes.ml
index 64dd273ef91c2e3037088a30b1770d237cd30a51..84b17028ce014027ea272494bee0deb76fe00dcf 100644
--- a/src/l2lExpandNodes.ml
+++ b/src/l2lExpandNodes.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 24/11/2016 (at 16:26) by Erwan Jahier> *)
+(* Time-stamp: <modified the 20/06/2017 (at 11:38) by Erwan Jahier> *)
open Lxm
@@ -106,7 +106,7 @@ and (subst_in_val_exp : subst * new_base -> val_exp -> val_exp) =
let by_pos_op = by_pos_op.it in
let vel = List.map (subst_in_val_exp s) vel in
let by_pos_op = match by_pos_op with
- | CONST_REF idl -> CONST_REF idl
+ | CONST_REF idl -> CONST_REF idl
| VAR_REF id -> VAR_REF (subst_in_id_id (fst s) id)
| WHEN(clk) -> WHEN(subst_in_clock s clk)
| HAT(i) -> HAT(i)
diff --git a/src/l2lSplit.ml b/src/l2lSplit.ml
index 4a395a6c957cc8e12175626fe105ab3d8e1bda9b..30cd02d364c77991f08f625301adf1913432b1a4 100644
--- a/src/l2lSplit.ml
+++ b/src/l2lSplit.ml
@@ -162,19 +162,19 @@ let (split_tuples:Lic.eq_info Lxm.srcflagged list -> Lic.eq_info Lxm.srcflagged
*)
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
+let rec (eq : LicPrg.t -> Lic.eq_info Lxm.srcflagged -> split_acc) =
+ fun lic_prg { src = lxm_eq ; it = (lhs, rhs) } ->
+ let n_rhs, (neqs, nlocs) = split_val_exp lic_prg 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
+and (split_eq_acc : LicPrg.t -> split_acc -> Lic.eq_info srcflagged -> split_acc) =
+ fun lic_prg (eqs, locs) equation ->
+ let (neqs, nlocs) = eq lic_prg 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 ->
+and (split_val_exp : LicPrg.t -> bool -> bool -> Lic.val_exp -> Lic.val_exp * split_acc) =
+ fun lic_prg when_flag top_level ve ->
(* [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
@@ -188,9 +188,9 @@ and (split_val_exp : bool -> bool -> Lic.val_exp -> Lic.val_exp * split_acc) =
*)
match ve.ve_core with
| Merge(ce,cl) -> (
- let ce,(eql1, vl1) = split_val_exp false false ce in
+ let ce,(eql1, vl1) = split_val_exp lic_prg 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 vel,(eql2, vl2) = split_val_exp_list lic_prg 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
@@ -222,7 +222,31 @@ and (split_val_exp : bool -> bool -> Lic.val_exp -> Lic.val_exp * split_acc) =
nve, (eql@[eq], vl@nv_l)
)
| CallByPosLic({it=Lic.VAR_REF _}, _) -> ve, ([],[])
- | CallByPosLic({it=Lic.CONST_REF _}, _) -> ve, ([],[])
+ | CallByPosLic({src=lxm;it=Lic.CONST_REF idl}, vel) ->
+ (* expand const ref in -eei mode *)
+ (try
+ if Lv6MainArgs.global_opt.Lv6MainArgs.ec then raise Not_found else
+ let const =
+ let c = match LicPrg.find_const lic_prg idl with
+ Some c -> c | None -> raise Not_found (* meant to catched *)
+ in
+ match c with
+ | (Enum_const_eff (s,Enum_type_eff(_,ll))) ->
+ (match Lv6MainArgs.global_opt.Lv6MainArgs.expand_enums with
+ | Lv6MainArgs.AsInt ->
+ let i = Lv6util.pos_in_list 0 s ll in
+ (Int_const_eff (string_of_int i))
+ | Lv6MainArgs.AsBool
+ | Lv6MainArgs.AsConst
+ | Lv6MainArgs.AsEnum -> raise Not_found (* meant to catched *)
+ )
+ | _ -> raise Not_found
+ in
+ { ve with
+ ve_core=CallByPosLic({src=lxm;it=Lic.CONST const}, vel)
+ }, ([],[])
+ with Not_found -> ve, ([],[])
+ )
| CallByPosLic({src=lxm;it=Lic.CONST _}, _)
-> if not when_flag then
let clk = ve.ve_clk in
@@ -241,7 +265,7 @@ and (split_val_exp : bool -> bool -> Lic.val_exp -> Lic.val_exp * split_acc) =
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
+ let fv, (eql, vl) = split_val_exp lic_prg false false fv in
((fn,fv)::fl_acc, eql@eql_acc, vl@vl_acc)
)
([],[],[])
@@ -274,17 +298,17 @@ and (split_val_exp : bool -> bool -> Lic.val_exp -> Lic.val_exp * split_acc) =
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 vel, (eql, vl) = split_val_exp_list lic_prg 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 vel,(eql, vl) = split_val_exp_list lic_prg 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 vel, (eql, vl) = split_val_exp_list lic_prg false false vel in
let rhs = CallByPosLic(by_pos_op_eff, vel) in
rhs, (eql, vl)
in
@@ -300,50 +324,50 @@ and (split_val_exp : bool -> bool -> Lic.val_exp -> Lic.val_exp * split_acc) =
let nve =
match nv_l with
| [nv] -> { ve with
- 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 = [nv.var_type_eff];
+ ve_clk = clk_l;
+ ve_core = CallByPosLic(
+ Lxm.flagit (Lic.VAR_REF (nv.var_name_eff)) lxm,
+ [])
+ }
| _ -> { ve with
- 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];
- ve_src = lxm
- }
- in
- nnv
- )
- nv_l
- )
- )
- }
+ 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];
+ ve_src = lxm
+ }
+ 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 ->
+and (split_val_exp_list : LicPrg.t -> bool -> bool -> Lic.val_exp list ->
Lic.val_exp list * split_acc) =
- fun when_flag top_level vel ->
+ fun lic_prg when_flag top_level vel ->
let vel, accl =
- List.split (List.map (split_val_exp when_flag top_level) vel)
+ List.split (List.map (split_val_exp lic_prg 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 =
+and split_node (lic_prg:LicPrg.t) (opt:Lv6MainArgs.t) (n: Lic.node_exp) : Lic.node_exp =
Lv6Verbose.exe
~flag:dbg (fun () ->
Printf.eprintf "*** Splitting node %s\n"
@@ -354,10 +378,10 @@ and split_node (opt:Lv6MainArgs.t) (n: Lic.node_exp) : Lic.node_exp =
| 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 lic_prg 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
+ let (neqs, nv) = List.fold_left (split_eq_acc lic_prg) ([], 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) =
@@ -369,7 +393,7 @@ and split_node (opt:Lv6MainArgs.t) (n: Lic.node_exp) : Lic.node_exp =
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
+ split_val_exp_list lic_prg false false
(* force the creation of a new var for
assert so that it is easier to
check in SocExec *) asserts
@@ -405,7 +429,7 @@ let rec doit (opt:Lv6MainArgs.t) (inprg : LicPrg.t) : LicPrg.t =
let rec do_node k (ne:Lic.node_exp) =
(* On passe en parametre un constructeur de nouvelle variable locale *)
profile_info (Printf.sprintf "#DBG: split equations of '%s'\n" (Lic.string_of_node_key k));
- let ne' = split_node opt ne in
+ let ne' = split_node inprg opt ne in
res := LicPrg.add_node k ne' !res
in
(*LET's GO *)
diff --git a/src/licDump.ml b/src/licDump.ml
index 5821c5c5fc68f5dd4cf42b724c8f78760b44f4b5..784b24c9d2b46c2e7d1b624cebf5a214dbc4f8c5 100644
--- a/src/licDump.ml
+++ b/src/licDump.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 16/01/2017 (at 11:29) by Erwan Jahier> *)
+(* Time-stamp: <modified the 20/06/2017 (at 15:25) by Erwan Jahier> *)
open Lv6errors
open Printf
@@ -214,7 +214,8 @@ and string_of_const = function
| Real_const_eff r -> r
| Extern_const_eff (s,_) -> (string_of_ident s)
| Abstract_const_eff (s,t,v,_) -> (string_of_ident s)
- | Enum_const_eff (s,Enum_type_eff(_,ll)) -> (string_of_int (Lv6util.pos_in_list 0 s ll))
+ | Enum_const_eff (s,Enum_type_eff(_,ll)) ->
+ (string_of_int (Lv6util.pos_in_list 0 s ll))
| Enum_const_eff _ -> assert false
| Struct_const_eff (fl, t) ->
let string_of_field (id, veff) =
diff --git a/src/licPrg.ml b/src/licPrg.ml
index be2c2bcb26e084d244214c24ba2c9ba9c5150268..ed686a034085867c82e57581a328f581eaa22231 100644
--- a/src/licPrg.ml
+++ b/src/licPrg.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 05/09/2016 (at 10:26) by Erwan Jahier> *)
+(* Time-stamp: <modified the 20/06/2017 (at 15:25) by Erwan Jahier> *)
open Lv6MainArgs
module ItemKeyMap = struct
@@ -178,7 +178,7 @@ let to_file (opt: Lv6MainArgs.t) (this:t) (main_node: Lv6Id.idref option) =
)
this.types
[]
- in
+ in
(match Lv6MainArgs.global_opt.Lv6MainArgs.expand_enums with
| Lv6MainArgs.AsConst ->
if global_opt.kcg then () else (
@@ -202,7 +202,7 @@ let to_file (opt: Lv6MainArgs.t) (this:t) (main_node: Lv6Id.idref option) =
const_list;
)
| Lv6MainArgs.AsInt ->
- if global_opt.kcg then () else (
+ if global_opt.kcg || global_opt.ec then () else (
let const_list = to_const_list this.types in
List.iter
(List.iteri
@@ -213,6 +213,7 @@ let to_file (opt: Lv6MainArgs.t) (this:t) (main_node: Lv6Id.idref option) =
const_list;
)
| Lv6MainArgs.AsBool -> (
+ if global_opt.kcg || global_opt.ec then () else (
let const_list = to_const_list this.types in
List.iter
(fun l ->
@@ -233,6 +234,7 @@ let to_file (opt: Lv6MainArgs.t) (this:t) (main_node: Lv6Id.idref option) =
)
l)
const_list;
+ )
)
| Lv6MainArgs.AsEnum -> ()
);
diff --git a/src/lv6MainArgs.ml b/src/lv6MainArgs.ml
index 313b47c28c8703a34e956a51d16364fb12b06720..5a6985626042a3445698fe9aa9e75a2dd539353f 100644
--- a/src/lv6MainArgs.ml
+++ b/src/lv6MainArgs.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 21/04/2017 (at 17:15) by Erwan Jahier> *)
+(* Time-stamp: <modified the 19/06/2017 (at 15:01) 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,
@@ -358,10 +358,12 @@ let mkoptab (opt:t) : unit = (
(Arg.Unit (fun _ -> opt.expand_nodes <- true; opt.inline_iterator <- true (* an iterator is a kind of node *)))
["Expand all node calls in the main node"]
;
- mkopt opt ~doc_level:Advanced
+ mkopt opt
["-et"; "--expand-io-type"]
(Arg.Unit (fun _ -> opt.expand_io_type <- true))
- ["Expand structured types of the main node (impact the simulation only)"]
+ ["Expand structured types of the main node (impact the rif output only).";
+ "Necessary to use lurette and rdbg in presence of lutin (that only ";
+ "knows about basic the types int/bool/real)" ]
;
mkopt opt ~doc_level:Advanced
["-enc"; "---expand-node-call"]
diff --git a/src/lv6version.ml b/src/lv6version.ml
index 3ce1895e510cb8d34144c02e4f622122ef32b086..dbfbd0728198899cfff53b9f4602b8b4cc02d89e 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 = "692"
-let sha_1 = "1adfcf741e7130599563f6c5667e829f5efad671"
+let commit = "693"
+let sha_1 = "c533df3e8195236dd128f41e2dd862bba83a2322"
let str = (branch ^ "." ^ commit ^ " (" ^ sha_1 ^ ")")
let maintainer = "jahier@imag.fr"
diff --git a/test/lus2lic.sum b/test/lus2lic.sum
index ed8918d8593bc795e2ee93691df87e61636b9ce2..1e22de3681ef11e15df3793d11e1b4ccd193790c 100644
--- a/test/lus2lic.sum
+++ b/test/lus2lic.sum
@@ -1,5 +1,5 @@
==> lus2lic0.sum <==
-Test Run By jahier on Thu Jun 1 16:16:10
+Test Run By jahier on Tue Jun 20 15:40:10
Native configuration is x86_64-unknown-linux-gnu
=== lus2lic0 tests ===
@@ -64,7 +64,7 @@ XFAIL: Test bad programs (assert): test_lus2lic_no_node should_fail/assert/lecte
XFAIL: Test bad programs (assert): test_lus2lic_no_node should_fail/assert/s.lus
==> lus2lic1.sum <==
-Test Run By jahier on Thu Jun 1 16:16:11
+Test Run By jahier on Tue Jun 20 15:40:11
Native configuration is x86_64-unknown-linux-gnu
=== lus2lic1 tests ===
@@ -398,7 +398,7 @@ PASS: sh multipar.sh
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c multipar.lus {}
==> lus2lic2.sum <==
-Test Run By jahier on Thu Jun 1 16:17:05
+Test Run By jahier on Tue Jun 20 15:41:04
Native configuration is x86_64-unknown-linux-gnu
=== lus2lic2 tests ===
@@ -738,7 +738,7 @@ PASS: sh zzz2.sh
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c zzz2.lus {}
==> lus2lic3.sum <==
-Test Run By jahier on Thu Jun 1 16:18:03
+Test Run By jahier on Tue Jun 20 15:42:01
Native configuration is x86_64-unknown-linux-gnu
=== lus2lic3 tests ===
@@ -1243,7 +1243,7 @@ PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node multipar.lus {}
==> lus2lic4.sum <==
-Test Run By jahier on Thu Jun 1 16:19:48
+Test Run By jahier on Tue Jun 20 15:43:45
Native configuration is x86_64-unknown-linux-gnu
=== lus2lic4 tests ===
@@ -1761,13 +1761,13 @@ PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node zzz2.lus {}
===============================
# Total number of failures: 23
lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in 0 seconds
-lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 53 seconds
-lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 58 seconds
-lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 105 seconds
-lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 57 seconds
+lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 52 seconds
+lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 57 seconds
+lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 104 seconds
+lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 50 seconds
* Ref time:
-0.04user 0.02system 4:35.78elapsed 0%CPU (0avgtext+0avgdata 5672maxresident)k
-64inputs+0outputs (0major+6088minor)pagefaults 0swaps
+0.07user 0.00system 4:26.07elapsed 0%CPU (0avgtext+0avgdata 5600maxresident)k
+96inputs+0outputs (0major+6098minor)pagefaults 0swaps
* Quick time (-j 4):
-0.04user 0.04system 2:28.15elapsed 0%CPU (0avgtext+0avgdata 5660maxresident)k
-160inputs+0outputs (0major+6123minor)pagefaults 0swaps
+0.05user 0.02system 1:54.24elapsed 0%CPU (0avgtext+0avgdata 5644maxresident)k
+128inputs+0outputs (0major+6132minor)pagefaults 0swaps
diff --git a/test/should_work/test_Int.lus b/test/should_work/test_Int.lus
index 1095a9b5e988bfa837451a36c1a2ded95fe2e17e..88bf866972543a0d7cd8c3a20829ba8f67b17c31 100644
--- a/test/should_work/test_Int.lus
+++ b/test/should_work/test_Int.lus
@@ -43,7 +43,7 @@ provides
node test_Int(evt, reset: bool) returns (nat: Int8::t);
body
node test_Int(evt, reset: bool) returns (nat: Int8::t);
- let
+ let
nat = if true -> reset then Int8::zero else
if evt then Int8::incr(pre(nat))
else pre(nat);