diff --git a/src/ident.ml b/src/ident.ml
index b40a3c8f03e474a07875375e26b001f67dac0989..c399a627aff2eb82e9cd5a590f1db6ef972fa68b 100644
--- a/src/ident.ml
+++ b/src/ident.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 01/02/2013 (at 17:32) by Erwan Jahier> *)
+(* Time-stamp: <modified the 04/02/2013 (at 18:46) by Erwan JAHIER> *)
(* J'ai appele ca symbol (mais ca remplace le ident) :
c'est juste une couche qui garantit l'unicite en memoire
diff --git a/src/licDump.ml b/src/licDump.ml
index 5cec0adfdf9ee03c85b47e33ad36bbe5430f764c..f81a6584b1a5d911ee922b11d9fe3ea1d97386de 100644
--- a/src/licDump.ml
+++ b/src/licDump.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 01/02/2013 (at 16:18) by Erwan Jahier> *)
+(* Time-stamp: <modified the 04/02/2013 (at 19:02) by Erwan JAHIER> *)
open Errors
open Printf
@@ -226,15 +226,7 @@ and string_of_decl var_info_eff =
(string_of_type_eff var_info_eff.var_type_eff)
in
let clk_str = (string_of_clock (snd var_info_eff.var_clock_eff)) in
- let vt_str =
- if !Global.ec &&
- (match (snd var_info_eff.var_clock_eff) with
- BaseLic | ClockVar _ -> false
- | _ -> true)
- then "(" ^ vt_str ^ ")"
- else vt_str
- in
- vt_str ^ clk_str
+ if !Global.ec then vt_str else vt_str ^ clk_str
and (string_of_type_decl_list : Lic.var_info list -> string -> string) =
fun tel sep ->
@@ -436,10 +428,15 @@ and string_of_val_exp_eff_core ve_core =
(* ICI : on pourrait afficher en commentaire l'éventuel type_matches ? *)
(string_of_by_pos_op_eff by_pos_op_eff vel)
- | Merge (ve, [({it=Bool_const_eff true}, ct); ({it=Bool_const_eff false}, cf)])
- | Merge (ve, [({it=Bool_const_eff false}, cf); ({it=Bool_const_eff true}, ct)]) -> (
- "merge(" ^ (Ident.to_string ve.it) ^ ", " ^
- (string_of_val_exp_eff ct) ^ ", "^ (string_of_val_exp_eff cf) ^")"
+ | Merge (ve, [({it=Bool_const_eff true }, ct); ({it=Bool_const_eff false}, cf)])
+ | Merge (ve, [({it=Bool_const_eff false}, cf); ({it=Bool_const_eff true}, ct)]) ->
+ if !Global.lv4 then (
+ "if " ^ (Ident.to_string ve.it) ^ " then current (" ^
+ (string_of_val_exp_eff ct) ^ ") else current (" ^
+ (string_of_val_exp_eff cf) ^")"
+ ) else (
+ "merge " ^ (Ident.to_string ve.it) ^ " (true -> " ^
+ (string_of_val_exp_eff ct) ^ ") (false -> "^ (string_of_val_exp_eff cf) ^")"
)
| Merge (ve, cl) -> (
"merge " ^ (Ident.to_string ve.it) ^ " " ^
diff --git a/test/lus2lic.log.ref b/test/lus2lic.log.ref
index 31bfbd55638a38365abab8770d6ca580b9dfc2ea..63e3b305527b5a56182231a6f6dde5d25f1900dc 100644
--- a/test/lus2lic.log.ref
+++ b/test/lus2lic.log.ref
@@ -1,4 +1,4 @@
-Test Run By jahier on Fri Feb 1 17:47:52 2013
+Test Run By jahier on Mon Feb 4 19:16:58 2013
Native configuration is i686-pc-linux-gnu
=== lus2lic tests ===
@@ -1428,9 +1428,7 @@ PASS: ./lus2lic {-o /tmp/merge.lic should_work/merge.lus}
spawn ./lus2lic -ec -o /tmp/merge.ec should_work/merge.lus
PASS: ./lus2lic {-ec -o /tmp/merge.ec should_work/merge.lus}
spawn ./ec2c -o /tmp/merge.c /tmp/merge.ec
-syntax error - at line 14
-syntax errors...
-FAIL: Try ec2c on the result: ./ec2c {-o /tmp/merge.c /tmp/merge.ec}
+PASS: ./ec2c {-o /tmp/merge.c /tmp/merge.ec}
spawn ./lus2lic -o /tmp/decl.lic should_work/decl.lus
PASS: ./lus2lic {-o /tmp/decl.lic should_work/decl.lus}
spawn ./lus2lic -ec -o /tmp/decl.ec should_work/decl.lus
@@ -1715,42 +1713,10 @@ spawn ./lus2lic -o /tmp/m.lic should_fail/semantics/m.lus
XFAIL: Test bad programs (semantics): lus2lic {-o /tmp/m.lic should_fail/semantics/m.lus}
testcase ./lus2lic.tests/non-reg.exp completed in 54 seconds
Running ./lus2lic.tests/progression.exp ...
-spawn ./lus2lic -o /tmp/when_enum.out should_work/broken/when_enum.lus
-*** Error in file "/home/jahier/lus2lic/test/should_work/broken/when_enum.lus", line 10, col 11 to 14, token 'toto':
-***
-*** clock error: The two following clocks are not unifiable:
-*** on when_enum::A(a) on base
-*** on clk on base
-
-
-FAIL: without any option: ./lus2lic { -o /tmp/when_enum.out should_work/broken/when_enum.lus}
-spawn ./lus2lic -ec -o /tmp/when_enum.ec should_work/broken/when_enum.lus
-*** Error in file "/home/jahier/lus2lic/test/should_work/broken/when_enum.lus", line 10, col 11 to 14, token 'toto':
-***
-*** clock error: The two following clocks are not unifiable:
-*** on A(a) on base
-*** on clk on base
-
-
-FAIL: Generate ec code : ./lus2lic {-ec -o /tmp/when_enum.ec should_work/broken/when_enum.lus}
spawn ./lus2lic -o /tmp/when_not.out should_work/broken/when_not.lus
-*** Error in file "/home/jahier/lus2lic/test/should_work/broken/when_not.lus", line 7, col 11 to 16, token 'clock4':
-***
-*** clock error: The two following clocks are not unifiable:
-*** on not a on base
-*** on clock4_u on base
-
-
-FAIL: without any option: ./lus2lic { -o /tmp/when_not.out should_work/broken/when_not.lus}
+PASS: ./lus2lic { -o /tmp/when_not.out should_work/broken/when_not.lus}
spawn ./lus2lic -ec -o /tmp/when_not.ec should_work/broken/when_not.lus
-*** Error in file "/home/jahier/lus2lic/test/should_work/broken/when_not.lus", line 7, col 11 to 16, token 'clock4':
-***
-*** clock error: The two following clocks are not unifiable:
-*** on not a on base
-*** on clock4_u on base
-
-
-FAIL: Generate ec code : ./lus2lic {-ec -o /tmp/when_not.ec should_work/broken/when_not.lus}
+PASS: ./lus2lic {-ec -o /tmp/when_not.ec should_work/broken/when_not.lus}
spawn ./lus2lic -o /tmp/packages.out should_work/broken/packages.lus
PASS: ./lus2lic { -o /tmp/packages.out should_work/broken/packages.lus}
spawn ./lus2lic -ec -o /tmp/packages.ec should_work/broken/packages.lus
@@ -1759,34 +1725,10 @@ spawn ./lus2lic -o /tmp/when_node.out should_work/broken/when_node.lus
PASS: ./lus2lic { -o /tmp/when_node.out should_work/broken/when_node.lus}
spawn ./lus2lic -ec -o /tmp/when_node.ec should_work/broken/when_node.lus
PASS: ./lus2lic {-ec -o /tmp/when_node.ec should_work/broken/when_node.lus}
-spawn ./lus2lic -o /tmp/testSystem.out should_work/broken/testSystem.lus
-*** Error in file "/home/jahier/lus2lic/test/should_work/broken/testSystem.lus", line 3, col 5 to 8, token 'capt':
-*** unknown package
-
-FAIL: without any option: ./lus2lic { -o /tmp/testSystem.out should_work/broken/testSystem.lus}
-spawn ./lus2lic -ec -o /tmp/testSystem.ec should_work/broken/testSystem.lus
-*** Error in file "/home/jahier/lus2lic/test/should_work/broken/testSystem.lus", line 3, col 5 to 8, token 'capt':
-*** unknown package
-
-FAIL: Generate ec code : ./lus2lic {-ec -o /tmp/testSystem.ec should_work/broken/testSystem.lus}
spawn ./lus2lic -o /tmp/car-orig.out should_work/broken/car-orig.lus
-*** Error in file "/home/jahier/lus2lic/test/should_work/broken/car-orig.lus", line 95, col 40 to 40, token '=':
-*** type error:
-*** type 'bool * int' was provided whereas
-*** type 'any * any' was expected
-***
-*** bool and int are not unifiable
-
-FAIL: without any option: ./lus2lic { -o /tmp/car-orig.out should_work/broken/car-orig.lus}
+PASS: ./lus2lic { -o /tmp/car-orig.out should_work/broken/car-orig.lus}
spawn ./lus2lic -ec -o /tmp/car-orig.ec should_work/broken/car-orig.lus
-*** Error in file "/home/jahier/lus2lic/test/should_work/broken/car-orig.lus", line 95, col 40 to 40, token '=':
-*** type error:
-*** type 'bool * int' was provided whereas
-*** type 'any * any' was expected
-***
-*** bool and int are not unifiable
-
-FAIL: Generate ec code : ./lus2lic {-ec -o /tmp/car-orig.ec should_work/broken/car-orig.lus}
+PASS: ./lus2lic {-ec -o /tmp/car-orig.ec should_work/broken/car-orig.lus}
spawn ./lus2lic -o /tmp/bad_call03.lic should_fail/type/broken/bad_call03.lus
XPASS: Test bad programs (type): lus2lic {-o /tmp/bad_call03.lic should_fail/type/broken/bad_call03.lus}
spawn ./lus2lic -o /tmp/ts03.lic should_fail/type/broken/ts03.lus
@@ -1806,13 +1748,12 @@ spawn ./lus2lic -o /tmp/activation1.lic should_fail/semantics/broken/activation1
XPASS: Test bad programs (semantics): lus2lic {-o /tmp/activation1.lic should_fail/semantics/broken/activation1.lus}
spawn ./lus2lic -o /tmp/bug.lic should_fail/semantics/broken/bug.lus
XPASS: Test bad programs (semantics): lus2lic {-o /tmp/bug.lic should_fail/semantics/broken/bug.lus}
-testcase ./lus2lic.tests/progression.exp completed in 0 seconds
+testcase ./lus2lic.tests/progression.exp completed in 1 seconds
=== lus2lic Summary ===
-# of expected passes 734
-# of unexpected failures 9
+# of expected passes 739
# of unexpected successes 11
# of expected failures 37
# of unresolved testcases 2
-runtest completed at Fri Feb 1 17:48:46 2013
+runtest completed at Mon Feb 4 19:17:53 2013
diff --git a/test/lus2lic.sum b/test/lus2lic.sum
index fa0d3fd6562ac95352ab37dbbd29695094fa2ca6..3797267e749845c4618673d2deab7c421ff9f5e6 100644
--- a/test/lus2lic.sum
+++ b/test/lus2lic.sum
@@ -1,4 +1,4 @@
-Test Run By jahier on Fri Feb 1 17:52:18 2013
+Test Run By jahier on Mon Feb 4 19:26:05 2013
Native configuration is i686-pc-linux-gnu
=== lus2lic tests ===
@@ -716,7 +716,7 @@ PASS: ./lus2lic {-ec -o /tmp/clock1_2ms.ec should_work/clock1_2ms.lus}
PASS: ./ec2c {-o /tmp/clock1_2ms.c /tmp/clock1_2ms.ec}
PASS: ./lus2lic {-o /tmp/merge.lic should_work/merge.lus}
PASS: ./lus2lic {-ec -o /tmp/merge.ec should_work/merge.lus}
-FAIL: Try ec2c on the result: ./ec2c {-o /tmp/merge.c /tmp/merge.ec}
+PASS: ./ec2c {-o /tmp/merge.c /tmp/merge.ec}
PASS: ./lus2lic {-o /tmp/decl.lic should_work/decl.lus}
PASS: ./lus2lic {-ec -o /tmp/decl.ec should_work/decl.lus}
PASS: ./ec2c {-o /tmp/decl.c /tmp/decl.ec}
@@ -782,18 +782,14 @@ XFAIL: Test bad programs (semantics): lus2lic {-o /tmp/patrick.lic should_fail/s
XFAIL: Test bad programs (semantics): lus2lic {-o /tmp/const.lic should_fail/semantics/const.lus}
XFAIL: Test bad programs (semantics): lus2lic {-o /tmp/m.lic should_fail/semantics/m.lus}
Running ./lus2lic.tests/progression.exp ...
-FAIL: without any option: ./lus2lic { -o /tmp/when_enum.out should_work/broken/when_enum.lus}
-FAIL: Generate ec code : ./lus2lic {-ec -o /tmp/when_enum.ec should_work/broken/when_enum.lus}
-FAIL: without any option: ./lus2lic { -o /tmp/when_not.out should_work/broken/when_not.lus}
-FAIL: Generate ec code : ./lus2lic {-ec -o /tmp/when_not.ec should_work/broken/when_not.lus}
+PASS: ./lus2lic { -o /tmp/when_not.out should_work/broken/when_not.lus}
+PASS: ./lus2lic {-ec -o /tmp/when_not.ec should_work/broken/when_not.lus}
PASS: ./lus2lic { -o /tmp/packages.out should_work/broken/packages.lus}
PASS: ./lus2lic {-ec -o /tmp/packages.ec should_work/broken/packages.lus}
PASS: ./lus2lic { -o /tmp/when_node.out should_work/broken/when_node.lus}
PASS: ./lus2lic {-ec -o /tmp/when_node.ec should_work/broken/when_node.lus}
-FAIL: without any option: ./lus2lic { -o /tmp/testSystem.out should_work/broken/testSystem.lus}
-FAIL: Generate ec code : ./lus2lic {-ec -o /tmp/testSystem.ec should_work/broken/testSystem.lus}
-FAIL: without any option: ./lus2lic { -o /tmp/car-orig.out should_work/broken/car-orig.lus}
-FAIL: Generate ec code : ./lus2lic {-ec -o /tmp/car-orig.ec should_work/broken/car-orig.lus}
+PASS: ./lus2lic { -o /tmp/car-orig.out should_work/broken/car-orig.lus}
+PASS: ./lus2lic {-ec -o /tmp/car-orig.ec should_work/broken/car-orig.lus}
XPASS: Test bad programs (type): lus2lic {-o /tmp/bad_call03.lic should_fail/type/broken/bad_call03.lus}
XFAIL: Test bad programs (type): lus2lic {-o /tmp/ts03.lic should_fail/type/broken/ts03.lus}
XPASS: Test bad programs (semantics): lus2lic {-o /tmp/piege.lic should_fail/semantics/broken/piege.lus}
@@ -805,8 +801,7 @@ XPASS: Test bad programs (semantics): lus2lic {-o /tmp/bug.lic should_fail/seman
=== lus2lic Summary ===
-# of expected passes 734
-# of unexpected failures 9
+# of expected passes 739
# of unexpected successes 11
# of expected failures 37
# of unresolved testcases 2
diff --git a/test/should_fail/semantics/broken/piege.lus b/test/should_fail/semantics/broken/piege.lus
index 3c0033cf4d7b849da1a34fba6acdb20eedae2ab3..85ba4a124a1e603b0c35d0e5e669bd673addfa5a 100644
--- a/test/should_fail/semantics/broken/piege.lus
+++ b/test/should_fail/semantics/broken/piege.lus
@@ -1,5 +1,6 @@
+-- Could work with a smart modular compilation à la raymond-pouzet or à la v4
--- out depend on out: should be rejected!
+-- out depend on out: should be rejected! (unless we inline)
node piege(in : bool) returns (out : bool);
let
out = in and aux1(aux2(out,out));
diff --git a/test/should_work/broken/car-orig.lus b/test/should_work/broken/car-orig.lus
index 0edd7b4dc48d05f1f6b7c3fdfd9424c1053db570..9d9b920397a5951a06bcb5e3595f66a56f8ed66b 100644
--- a/test/should_work/broken/car-orig.lus
+++ b/test/should_work/broken/car-orig.lus
@@ -54,7 +54,7 @@ tel
node CD(f_ir:int) returns(presence:bool)
let
- presence = if(f_ir>100) then 1 else 0;
+ presence = (f_ir>100);
-- 1 imply there is no obstacle in front
--0 imply there is a obstacle in front
@@ -71,20 +71,20 @@ tel
node STARTPOS(l_gap:bool;shaft_l:int) returns(start:int);
let
-start = 0 -> if(shaft_l = 0 and l_gap =1 ) then 0
- else if ((pre(l_gap)=0) and (shaft_l<>0)) then shaft_l
+start = 0 -> if(shaft_l = 0 and l_gap ) then 0
+ else if ((pre(l_gap)=false) and (shaft_l<>0)) then shaft_l
else pre(start);
tel
--------------------------------------------------------
-node PARKING_LENGHT(shaft_l,start_pos:int) returns(park_lenght:int);
+node PARKING_LENGHT_SUFFICIENT(shaft_l,start_pos:int) returns(park_lenght:bool);
let
- park_lenght = if((shaft_l - start_pos) > REQ_GAP) then 1 else 0; -- 1 indicate sufficient parking space else not sufficient
+ park_lenght = ((shaft_l - start_pos) > REQ_GAP); -- 1 indicate sufficient parking space else not sufficient
tel
-------------------------------------------
node required_back1(shaft_l,start_back:int) returns(done_back1:bool);
let
- done_back1 = if(shaft_l -start_back = 20) then 1 else 0;
+ done_back1 = (shaft_l -start_back = 20);
tel
@@ -92,7 +92,7 @@ node required_back1(shaft_l,start_back:int) returns(done_back1:bool);
node STARTBACK1_POS(gap_found:bool;shaft_l:int) returns(back1:int);
let
back1 = 0 -> if(shaft_l = 0 and gap_found ) then 0
- else if(pre(gap_found) =0 and shaft_l<>0 ) then shaft_l
+ else if(pre(gap_found) =false and shaft_l<>0 ) then shaft_l
else pre(back1);
tel
@@ -111,31 +111,31 @@ var dir1,vel1,empty_start_pos,mode,start_back_pos,start_rightturn_pos:int; block
-- mode =6 : parking(bcking2)
-- mode =7 :stop(buzzer off)
let
- left_gap = 0 -> gap1(LEFT_IR_VALUE);
+ left_gap = false -> gap1(LEFT_IR_VALUE);
(dir1,vel1) = whiteline(RIGHT_WHITELINE_VALUE,MIDDLE_WHITELINE_VALUE,LEFT_WHITELINE_VALUE);
- blocked = 0 ->CD(FRONT_IR_VALUE);
+ blocked = false ->CD(FRONT_IR_VALUE);
empty_start_pos = 0 -> STARTPOS(left_gap,SHAFT_COUNT_LEFT);
- enough_gap = 0 -> PARKING_LENGHT(SHAFT_COUNT_LEFT, empty_start_pos);
+ enough_gap = false -> PARKING_LENGHT_SUFFICIENT(SHAFT_COUNT_LEFT, empty_start_pos);
- start_back_pos = 0 -> if (enough_gap=1) then STARTBACK1_POS(enough_gap,SHAFT_COUNT_LEFT) else 0;
- enough_back1 = 0 -> if (enough_gap=1) then required_back1(SHAFT_COUNT_LEFT, start_back_pos) else 0;
+ start_back_pos = 0 -> if (enough_gap) then STARTBACK1_POS(enough_gap,SHAFT_COUNT_LEFT) else 0;
+ enough_back1 = false -> if (enough_gap) then required_back1(SHAFT_COUNT_LEFT, start_back_pos) else false;
-- turn_r_Complete = 0 -> if(enough_back = 1) then TURN_RIGHT(REQ_RIGHT_DEGREE) else 0;
- start_rightturn_pos = 0 -> if ((pre(mode)=4) and (enough_back1 =1)) then SHAFT_COUNT_LEFT else pre(start_rightturn_pos);
- turn_r_Complete = 0 -> if ((pre(mode)=5) and (SHAFT_COUNT_LEFT - start_rightturn_pos >= 25)) then 1 else 0;
-
- mode = 1 -> if(pre(mode) = 1 and blocked = 0 and enough_gap =0 ) then 2 -- waiting mode
- else if(pre(mode) = 1 and blocked = 1 and enough_gap=0) then 1 -- farward mode
- else if(pre(mode) = 2 and blocked = 0 and enough_gap=0 ) then 2 -- waiting mode
- else if(pre(mode) = 2 and blocked = 1 and enough_gap=0 ) then 1 -- farward mode
- else if(pre(mode) =2 and enough_gap=1) then 3 -- parking mode(buzzer on)
- else if(pre(mode) = 1 and enough_gap=1) then 3-- parking mode(buzzer on)
+ start_rightturn_pos = 0 -> if ((pre(mode)=4) and (enough_back1)) then SHAFT_COUNT_LEFT else pre(start_rightturn_pos);
+ turn_r_Complete = false -> ((pre(mode)=5) and (SHAFT_COUNT_LEFT - start_rightturn_pos >= 25));
+
+ mode = 1 -> if(pre(mode) = 1 and blocked = false and enough_gap = false ) then 2 -- waiting mode
+ else if(pre(mode) = 1 and blocked and enough_gap= false) then 1 -- farward mode
+ else if(pre(mode) = 2 and blocked = false and enough_gap=false ) then 2 -- waiting mode
+ else if(pre(mode) = 2 and blocked and enough_gap=false ) then 1 -- farward mode
+ else if(pre(mode) =2 and enough_gap) then 3 -- parking mode(buzzer on)
+ else if(pre(mode) = 1 and enough_gap) then 3-- parking mode(buzzer on)
else if(pre(mode) = 3) then 4 -- first back by small amount (parking back)
- else if(pre(mode)=4 and enough_back1=0 ) then 4-- not enough backing
- else if(pre(mode)=4 and enough_back1=1 ) then 5 -- complete backing process, goes to turn right mode
- else if(pre(mode) = 5 and turn_r_Complete = 0 ) then 5-- not completed turning
- else if(pre(mode) = 5 and turn_r_Complete = 1) then 6 -- after turn right , go to stop mode
+ else if(pre(mode)=4 and enough_back1=false ) then 4-- not enough backing
+ else if(pre(mode)=4 and enough_back1 ) then 5 -- complete backing process, goes to turn right mode
+ else if(pre(mode) = 5 and turn_r_Complete = false ) then 5-- not completed turning
+ else if(pre(mode) = 5 and turn_r_Complete ) then 6 -- after turn right , go to stop mode
else 6;
@@ -145,7 +145,7 @@ let
(DIRECTION,VELOCITY) = if (mode =1 or mode =3) then (dir1,vel1) else if(mode =4) then (2,vel1) else if(mode = 5) then (3,vel1) else (0,0);
- BUZZER = if(mode = 3 or mode =4 or mode =5) then 1 else 0 ; -- buzzer on imply that car is parking mode else off
+ BUZZER = (mode = 3 or mode =4 or mode =5) ; -- buzzer on imply that car is parking mode else off
diff --git a/test/should_work/broken/testSystem.lus b/test/should_work/broken/testSystem.lus
deleted file mode 100644
index 90b0f313df4eed5398f55064af2842cf0796520f..0000000000000000000000000000000000000000
--- a/test/should_work/broken/testSystem.lus
+++ /dev/null
@@ -1,218 +0,0 @@
-package system
-
-uses capt, boite, pilote;
-
-provides
-
-
-
-node system(in : bool;
- Hcapt, Hpilote : bool;
- semMemAutP : bool) --Happli : bool;)
-returns
- (HupdatePiloteData : bool;
- -- dataBoiteCP_IN :int when Hcapt;
- piloteData : int when HupdatePiloteData; -- when HrinstCount ; when dataBoiteCP_PUT !!!!!!!!!!!!!
--- localDataFromRead : int;
--- HrinstCount : bool;
--- indCount : int;
--- retard : int; nbrCopy : int^10
- );
-
-body
-
-
-
-node system (in : bool;
- Hcapt, Hpilote : bool;
- semMemAutP : bool) -- Happli : bool;)
-returns (--v : bool;
- HupdatePiloteData : bool;
- piloteData : int when HupdatePiloteData;
- ) -- when dataBoiteCP_PUT;
--- localDataFromRead : int;
--- Hcapt, Hpilote, Happli : bool;
--- HrinstCount : bool;
- --indCount : int;
--- retard : int; nbrCopy : int^10);
- --var --Hcapt, Hpilote, Happli : bool; -- les horloges
- --dataBoiteCP_IN,
- -- dataBoiteCP_OUT : int; -- donn?es en entr?es/sorties de la boite aux lettres
- -- dataBoiteCP_PUT, dataBoiteCP_GET : bool; -- commandes de la boite aux lettres
- -- semMemTakeP, semMemTakeR, semMemGive : bool; -- commandes du s?maphore
- -- semMemAutP,semMemAutR : bool; -- autorisations en sortie du s?maphore
- --piloteData, readData : int;
- -- getMem,
- -- putMem : bool;
-var
--- free, demandeR : bool;
- dataBoiteCP_OUT : int when dataBoiteCP_GET;
- dataBoiteCP_IN : int when dataBoiteCP_PUT;
--- piloteData : int when HupdatePiloteData;
--- readData : int;
--- getMem : bool;
- dataBoiteCP_PUT : bool;
- dataBoiteCP_GET : bool;
--- semMemTakeP : bool;
--- semMemTakeR : bool;
--- semMemGive : bool;
--- semMemAutP : bool;
--- semMemAutR : bool;
- putMem : bool;
-
-
--- localErasedDataFromBoiteCP : int;
--- localCopiedDataFromBoiteCP : int;
--- localErasedDataFromPilote : int when Hpilote;
--- localCopiedDataFromPilote : int when Hpilote;
--- localErasedDataFromMem : int when putMem;
--- localCopiedDataFromMem : int when putMem;
--- productionEvent,
--- consumptionEvent,
--- eraseMemEvent,
--- eraseBoiteCPEvent,
--- erasePiloteEvent,
--- copyBoiteCPEvent,
--- copyPiloteEvent,
--- copyMemEvent : bool;
-
--- sortieCapt : int when Hcapt;
-
- sortieCapt : int when Hcapt;
-
- toto : bool;
-
-let
-
--- (Hcapt, Hpilote, Happli) = ctrl(in);
-
-
--- dataBoiteCP_IN = sortieCapt;
-
-
-
- -- capt : done !!!!!!!!!!!!!!!!!!!!!!!!!!!!
- (dataBoiteCP_PUT,
- sortieCapt)
--- productionEvent)
- = capt(Hcapt);
--- HrinstCount,
--- indCount);
- -- dataBoiteCP_IN : when HrinstCount !!
-
-
- toto = Hcapt and dataBoiteCP_PUT;
-
- dataBoiteCP_IN = current(sortieCapt) when dataBoiteCP_PUT;
-
-
- -- boiteCP : done !!!!!!!!!!!!!!!!!!!!!!!!!!!!
- (dataBoiteCP_OUT) =
--- localErasedDataFromBoiteCP,
--- localCopiedDataFromBoiteCP,
--- copyBoiteCPEvent,
--- eraseBoiteCPEvent) =
- boite(
- dataBoiteCP_GET,
- dataBoiteCP_PUT,
- --current(dataBoiteCP_IN) when dataBoiteCP_PUT);
- dataBoiteCP_IN);
- -- dataBoiteCP_IN : when dataBoiteCP_PUT
- -- dataBoiteCP_OUT : when dataBoiteCP_GET
-
-
-
-
-
-
-
-
- -- pilote : done !!!!!!!!!!!!!!!!!!!!!!!!!!!!
- (--semMemTakeP,
- putMem,
- dataBoiteCP_GET,
- HupdatePiloteData,
- piloteData)
- -- when HupdatePiloteData
--- localErasedDataFromPilote,
--- erasePiloteEvent,
--- copyPiloteEvent,
--- localCopiedDataFromPilote)
- = pilote(Hpilote,
- semMemAutP,
--- HupdatePiloteData,
- current(dataBoiteCP_OUT));
-
-
- -- piloteData : when semMemAutP
- -- localErasedDataFromPilote : when Hpilote
- -- localCopiedDataFromPilote : when Hpilote
- -- assert HupdatePiloteData = Hpilote and semAutP;
-
-
--- HupdatePiloteData = Hpilote and semMemAutP;
-
-
- -- semMem, mem : done !!!!!!!!!!!!!!!!!!!!!!!!!!!!
--- (semMemGive,
--- readData,
--- localErasedDataFromMem,
--- localCopiedDataFromMem,
--- eraseMemEvent,
--- copyMemEvent)
--- = mem(getMem,
--- putMem,
--- piloteData);
--- (semMemAutP,
--- semMemAutR,
--- free,
--- demandeR)
--- = semMem(semMemTakeP,
--- semMemTakeR,
--- semMemGive);
- -- piloteData : when putMem
- -- localDataErasedFromMem, localDataCopiedDataFromMem : when putMem
-
-
-
-
- -- read : done !!!!!!!!!!!!!!!!!!!!!!!!!!!!!
--- (getMem,
--- semMemTakeR,
--- localDataFromRead,
--- consumptionEvent)
--- = read(Happli,
--- semMemAutR,
--- readData);
-
- -- observer : done !!!!!!!!!!!!!??????????????????
--- (retard,
--- indCount,
--- HrinstCount,
--- nbrCopy)
--- = observer(current(dataBoiteCP_IN),
--- localDataFromRead,
--- localErasedDataFromBoiteCP,
--- localCopiedDataFromBoiteCP,
--- current(localErasedDataFromPilote),
--- current(localCopiedDataFromPilote),
--- current(localErasedDataFromMem),
--- current(localCopiedDataFromMem),
--- productionEvent,
--- consumptionEvent,
--- eraseMemEvent,
--- eraseBoiteCPEvent,
--- erasePiloteEvent,
--- copyBoiteCPEvent,
--- copyPiloteEvent,
--- copyMemEvent);
--- une valeur bidon;
--- v = not(dataBoiteCP_IN=-1) and not(localDataFromRead=-1);
--- res = false -> v or pre(res);
-
-assert Hcapt = dataBoiteCP_PUT;
-
-tel
-
-
-end
\ No newline at end of file
diff --git a/test/should_work/broken/when_enum.lus b/test/should_work/broken/when_enum.lus
deleted file mode 100644
index df436c416ad494f14df8378e48bf826009bc8e57..0000000000000000000000000000000000000000
--- a/test/should_work/broken/when_enum.lus
+++ /dev/null
@@ -1,17 +0,0 @@
-
-
-type t = enum {A, B, C};
-
-node clock(a : t ; b, c: bool) returns (x: bool when a; y: bool when a);
-var
- clk : bool;
-let
- clk = tutu(a);
- (x, y) = toto(b when clk, c when A(a)); -- clock error !
-
-tel
-
-
-extern node toto(u: bool; v: bool) returns (x: bool; y: bool);
-extern node tutu(u: t) returns (x: bool);
-
diff --git a/test/should_work/broken/when_not.lus b/test/should_work/broken/when_not.lus
index 650f545f395c7f33b02e811171d37fd8fc8caa84..ea3fb0ad48447d71fe926f03658cce7197932b1f 100644
--- a/test/should_work/broken/when_not.lus
+++ b/test/should_work/broken/when_not.lus
@@ -3,13 +3,12 @@
node clock(a: bool; b: bool) returns (c: bool; d: bool when c);
let
- -- XXX should we accept that ?
(c, d) = clock4(a, b when not(a));
tel
-- Entree sur entree et sortie sur sortie: ok
-extern node clock4(clock4_u: bool; clock4_v: bool when clock4_u)
+extern node clock4(clock4_u: bool; clock4_v: bool when not clock4_u)
returns (clock4_x: bool; clock4_y: bool when clock4_x);