Merge pull request #50 from lenaRB/ETL-translation-fix

Editing the ETL examples so they pass the translation phase

src/test/resources/testModels/libraries/ETL_test/CheckOver.crml

@@ -2,18 +2,18 @@ model CheckOver is {
 	// Operators on Boolean
 	// Logical disjunction
 	Template b1 'or' b2 = not (not b1 and not b2);
-
-	// Operators for the evaluation of requirements
-	// Check
-	Operator [ Boolean ] 'check' Boolean phi 'over' Periods P 
-		= and ('evaluate' phi 'over' P);
+
+	// Decide
+	Operator [ Boolean ] 'decide' Boolean phi 'over' Period P = phi 'or' (P end);
 
 	// Evaluate
 	Operator [ Boolean ] 'evaluate' Boolean phi 'over' Period P 
 		= integrate (('decide' phi 'over' P) * phi) on P;
 
-	// Decide
-	Operator [ Boolean ] 'decide' Boolean phi 'over' Period P = phi 'or' (P end));
+	// Operators for the evaluation of requirements
+	// Check
+	Operator [ Boolean ] 'check' Boolean phi 'over' Periods P 
+		= and ('evaluate' phi 'over' P);
 
 	// Example of function call
 	Boolean phi1 is external;

src/test/resources/testModels/libraries/ETL_test/CheckOver_no_ext.crml

@@ -3,21 +3,21 @@ model CheckOver_no_ext is {
 	// Logical disjunction
 	Template b1 'or' b2 = not (not b1 and not b2);
 
-	// Operators for the evaluation of requirements
-	// Check
-	Operator [ Boolean ] 'check' Boolean phi 'over' Periods P 
-		= and ('evaluate' phi 'over' P);
+	// Decide
+	Operator [ Boolean ] 'decide' Boolean phi 'over' Period P = phi 'or' (P end);
 
 	// Evaluate
 	Operator [ Boolean ] 'evaluate' Boolean phi 'over' Period P 
 		= integrate (('decide' phi 'over' P) * phi) on P;
-
-	// Decide
-	Operator [ Boolean ] 'decide' Boolean phi 'over' Period P = phi 'or' (P end));
+
+	// Operators for the evaluation of requirements
+	// Check
+	Operator [ Boolean ] 'check' Boolean phi 'over' Periods P 
+		= and ('evaluate' phi 'over' P);
 
 	// Example of function call
-	Boolean phi1 is if 2.0 < time and time < 3.5 then true else false;
-	Boolean b1 is if 2.5 < time and time < 5 then undecided else false;
+	Boolean phi1 is if (2.0 < time) and (time < 3.5) then true else false;
+	Boolean b1 is if (2.5 < time) and (time < 5) then undecided else false;
 	Period P1 is [new Event b1, new Event not b1];
 
 	Boolean b_check_over is 'evaluate' phi1 'over' P1; //Value is undefined, becomes undecided at 2.5s and then false at t=3.5s

src/test/resources/testModels/libraries/ETL_test/CountInside_no_ext.crml

@@ -8,9 +8,9 @@ model CountInside_no_ext is {
 	Operator [ Integer ] 'count' Clock C 'inside' Period P = card (C 'inside' P);
 
 	// Example of function call
-	Boolean b1 is if 2.5 < time and time < 5 then true else false;
+	Boolean b1 is if (2.5 < time) and (time < 5) then true else false;
 	Period P1 is [ b1, not b1 ];
-	Boolean b2 is if (2 < time and time < 3) or (3.5 < time and time < 4.5) then true else false;
+	Boolean b2 is if ((2 < time) and (time < 3)) or ((3.5 < time) and (time < 4.5)) then true else false;
 	Clock C1 is new Clock b2;
 
 	Integer i_count_ticks_of_c1_inside_p1 is 'count' C1 'inside' P1; // Value should be 1 (there is only one tick of C1 inside Period P1)

src/test/resources/testModels/libraries/ETL_test/DecideOver.crml

@@ -3,6 +3,8 @@ model DecideOver is {
 	// Logical disjunction
 	Template b1 'or' b2 = not (not b1 and not b2);
 
+
+
 	// Decide
 	//Operator 'decide' is 
 	Operator [ Boolean ] 'decide' Boolean phi 'over' Period P = phi 'or' (P end);

src/test/resources/testModels/libraries/ETL_test/DecideOver_no_ext.crml

@@ -7,8 +7,8 @@ model DecideOver_no_ext is {
 	Operator [ Boolean ] 'decide' Boolean phi 'over' Period P = phi 'or' (P end));
 
 	// Example of function call
-	Boolean phi1 is if 2.0 < time and time < 3.5 then true else false;
-	Boolean b1 is if 2.5 < time and time < 5 then undecided else false;
+	Boolean phi1 is if (2.0 < time) and (time < 3.5) then true else false;
+	Boolean b1 is if (2.5 < time) and (time < 5) then undecided else false;
 	Period P1 is [ new Event b1, new Event not b1];
 
 	Boolean b_decide_over is 'decide' phi1 'over' P1; //Value is undecided and becomes false at t=3.5s

src/test/resources/testModels/libraries/ETL_test/EvaluateOver_no_ext.crml

@@ -11,8 +11,8 @@ model EvaluateOver_no_ext is {
 		= integrate (('decide' phi 'over' P) * phi) on P;
 
 	// Example of function call
-	Boolean phi1 is if 2.0 < time and time < 3.5 then true else false;
-	Boolean b1 is if 2.5 < time and time < 5 then undecided else false;
+	Boolean phi1 is if (2.0 < time) and (time < 3.5) then true else false;
+	Boolean b1 is if (2.5 < time) and (time < 5) then undecided else false;
 	Period P1 is [ new Event b1, new Event not b1];
 
 	Boolean b_evaluate_over is 'evaluate' phi1 'over' P1; //Value is undefined, becomes undecided at 2.5s and then false at t=3.5s

src/test/resources/testModels/libraries/ETL_test/Inside_no_ext.crml

@@ -4,9 +4,9 @@ model Inside_no_ext is {
 		= C filter ((tick C >= P start) and (tick C <= P end));
 
 	// Example of function call
-	Boolean b1 is if 2.5 < time and time < 5 then true else false;
+	Boolean b1 is if (2.5 < time) and (time < 5) then true else false;
 	Period P1 is [ new Event b1, new Event not b1 ];
-	Boolean b2 is if (2 < time and time < 3) or (3.5 < time and time < 4.5) then true else false;
+	Boolean b2 is if ((2 < time) and (time < 3)) or ((3.5 < time) and (time < 4.5)) then true else false;
 	Clock C1 is new Clock b2;
 
 	Clock c_filtered_ticks_of_c1_inside_p1 is C1 'inside' P1; // Only one event should be kept at instant 3.5 s

src/test/resources/testModels/libraries/ETL_test/old_EnsureAtEnd.crml

@@ -1,13 +1,17 @@
 model EnsureAtEnd is ETL union {
+
+
 	// Operator for checking that a requirement is satisfied at the end of a time period
 	Operator [ Boolean ] 'check' Boolean b 'at end of' Periods P = 'check' varying1 'id' b 'over' P;
 
+	// Requirement
+	Boolean y is 'check' u 'at end of' {timePeriod};	
+
 	// Inputs
 	Event e1 is external;
 	Event e2 is external;
 	Boolean u is external;
 	Period timePeriod is ] e1, e2 [;
 
-	// Requirement
-	Boolean y is 'check' u 'at end of' {timePeriod};
+
 };