Merge pull request #46 from audrey-jardin/main

New set of unit tests for built-in and ETL operators

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

@@ -9,7 +9,7 @@ model BecomesTrue_no_ext is {
 	Boolean b2 is true;
 	Boolean b3 is false;
 
-	Clock c1 is b1 'becomes true'; //Two events should be generated at instants 2.5s and 7.5s
+	Clock c1 is b1 'becomes true'; // Two events should be generated at instants 2.5s and 7.5s
 	Clock c2 is b2 'becomes true'; // No event should be generated
 	Clock c3 is b3 'becomes true'; // No event should be generated
 

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

@@ -17,8 +17,8 @@ model CheckOver_no_ext is {
 
 	// 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 true else false;
-	Period P1 is [b1, not b1];
+	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;
+	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.crml

@@ -1,15 +1,15 @@
 model CountInside is {
 	// Filter clock ticks inside a time period
 	Operator [ Clock ] Clock C 'inside' Period P 
-		= C filter (tick >= P start) and (tick <= P end);
+		= C filter (tick C >= P start) and (tick C <= P end);
 
 	// Operators on clocks
 	// Count the occurrences of events inside a time period
 	Operator [ Integer ] 'count' Clock C 'inside' Period P = card (C 'inside' P);
 
 	// Example of function call
 	Boolean b1 is external;
-	Period P1 is [ b1, not b1 ];
+	Period P1 is [ new Event b1, new Event not b1 ];
 	Clock C1 is external;
 
 	Integer i_count_ticks_of_c1_inside_p1 is 'count' C1 'inside' P1;

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

@@ -1,7 +1,7 @@
 model CountInside_no_ext is {
 	// Filter clock ticks inside a time period
 	Operator [ Clock ] Clock C 'inside' Period P 
-		= C filter (tick >= P start) and (tick <= P end);
+		= C filter (tick C >= P start) and (tick C <= P end);
 
 	// Operators on clocks
 	// Count the occurrences of events inside a time period
@@ -11,7 +11,7 @@ model CountInside_no_ext is {
 	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;
-	Clock C1 is Clock b2;
+	Clock C1 is new Clock b2;
 
-	Integer i_count_ticks_of_c1_inside_p1 is 'count' C1 'inside' P1; // Value should be 1
+	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_no_ext.crml

@@ -8,8 +8,8 @@ model DecideOver_no_ext is {
 
 	// 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 true else false;
-	Period P1 is [b1, not b1];
+	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;
+	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

@@ -12,8 +12,8 @@ model EvaluateOver_no_ext is {
 
 	// 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 true else false;
-	Period P1 is [b1, not b1];
+	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;
+	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.crml

@@ -1,7 +1,7 @@
 model Inside is {
 	// Filter clock ticks inside a time period
 	Operator [ Clock ] Clock C 'inside' Period P 
-		= C filter (tick C >= P start) and (tick C <= P end);
+		= C filter ((tick C >= P start) and (tick C <= P end));
 
 	// Example of function call
 	Boolean b1 is external;

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

@@ -1,11 +1,11 @@
 model Inside_no_ext is {
 	// Filter clock ticks inside a time period
 	Operator [ Clock ] Clock C 'inside' Period P 
-		= C filter (tick C >= P start) and (tick C <= P end);
+		= 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;
-	Period P1 is [ b1, not b1 ];
+	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;
 	Clock C1 is new Clock b2;
 

src/test/resources/testModels/spec-doc-examples/BooleanAtEvent_no_ext.crml

@@ -1,6 +1,6 @@
 model BooleanAtEvent_no_ext is {
 	Boolean b1 is if 2.5 < time and time < 5 then true else false;
-	Boolean b is if 2.0 < time and time < 3.5 then true else false;
+	Boolean b is if (2.0 <= time and time < 3.5) or (4.0 <= time and time < 5.5) then true else false;
 	Clock c is new Clock b;
-	Boolean b_at_event is b1 at c;
+	Boolean b_at_event is b1 at c; // Should start at false and becomes true at t=4s
 };

src/test/resources/testModels/spec-doc-examples/BooleanIntegration_no_ext.crml

@@ -1,6 +1,15 @@
 model BooleanIntegration is {
 	Boolean a is if 2.0 < time and time < 3.5 then true else false;
-	Boolean b is if 2.5 < time and time < 5 then true else false;
-	Period P is [ new Event b, new Event not b ];
-	Boolean b_integration is integrate a on P;
+	Period P is [ new Event a new Event not a ];
+
+	Boolean b_true is if 2.5 < time and time < 5 then undefined else true;
+	Boolean b_false is if 2.5 < time and time < 5 then undefined else false;
+	Boolean b_undecided is if 2.5 < time and time < 5 then undecided else true;
+	Boolean b_undefined is undefined;
+
+	Boolean b_integration_true is integrate b_true on P; //Value is undefined and becomes true at 2.5s
+	Boolean b_integration_false is integrate b_false on P; //Value is undefined and becomes false at 2.5s
+	Boolean b_integration_undecided is integrate b_undecided on P; //Value is undefined and becomes undecided at 2.5s
+	Boolean b_integration_undefined is integrate b_undefined on P; //Value is and remains undefined	
+
 };

src/test/resources/testModels/spec-doc-examples/ClockConstructors_no_ext.crml

@@ -1,5 +1,5 @@
 model ClockConstructors_no_ext is {
 	// Constructors
-	Boolean b is if 2.0 < time and time < 3.5 then true else false;;
-	Clock c is new Clock b; // one event should be generated at instant t=2.0
+	Boolean b is if 2.0 <= time and time < 3.5 then true else false;;
+	Clock c is new Clock b; // One event should be generated at instant t=2.0
 };

src/test/resources/testModels/spec-doc-examples/ClockCurrentTick_no_ext.crml

@@ -1,5 +1,8 @@
 model ClockCurrentTick_no_ext is {
-	Boolean b is if 2.0 < time and time < 3.5 then true else false;
+	Boolean b is if (2.0 <= time and time < 3.5) and (4.0 <= time and time < 5.5) then true else false;
 	Clock c is new Clock b;
-	Event e_current_tick is tick c;
+	Event e_current_tick is tick c; 
+	// Should start with an empty set,
+	//	then at t=2.0s becomes a set with one event at t=2.0s 
+	//  and turns at t=4.0s to a set with two events at t=2.0s and t=4.0s
 };

src/test/resources/testModels/spec-doc-examples/ClockFilter.crml

@@ -1,5 +1,5 @@
 model ClockFilter is {
-	Clock c1 is external;
-	Clock c2 is external;
-	Clock c_filter is c1 filter tick c2;
+	Event e is external;
+	Clock c is external;
+	Clock c_filter is c filter (tick c >= e); // Should only keep c ticks which happen after or at the same time than event e.
 };

src/test/resources/testModels/spec-doc-examples/ClockFilter_no_ext.crml

@@ -0,0 +1,8 @@
+model ClockFilter_no_ext is {
+	Boolean b1 is if 2.5 < time and time < 5 then true else false;
+	Boolean b is if (2.0 <= time and time < 3.5) or (4.0 <= time and time < 5.5) then true else false;
+
+	Event e is new Event b1; // One event at t=2.5s
+	Clock c is new Clock b;  // Two ticks at t=2.0s and t=4.0s
+	Clock c_filter is c filter (tick c >= e); // Should only keep tick at t=4.0s.
+};

src/test/resources/testModels/spec-doc-examples/ClockNumberOfTicks_no_ext.crml

@@ -0,0 +1,6 @@
+model ClockNumberOfTicks_no_ext is {
+	Boolean b is if (2.0 <= time and time < 3.5) or (4.0 <= time and time < 5.5) then true else false;
+
+	Clock c is new Clock b;  // Two ticks at t=2.0s and t=4.0s
+	Integer n_number_of_ticks is card c; // Should be 0 at start, then 1 at t=2.0s and becomes 2 at t=4.0s
+};

src/test/resources/testModels/spec-doc-examples/IntegerBinaryAddition.crml

@@ -1,5 +1,5 @@
 model IntegerBinaryAddition is {
-	Integer n1 is 25;
-	Integer n2 is -3;
+	Integer n1 is external;
+	Integer n2 is external;
 	Integer n_binary_addition is n1 + n2;
 };

src/test/resources/testModels/spec-doc-examples/IntegerBinaryAddition_no_ext.crml

@@ -0,0 +1,5 @@
+model IntegerBinaryAddition_no_ext is {
+	Integer n1 is 25;
+	Integer n2 is -3;
+	Integer n_binary_addition is n1 + n2; //Value is 22
+};

src/test/resources/testModels/spec-doc-examples/IntegerUnaryAddition.crml

@@ -1,6 +1,6 @@
 model IntegerUnaryAddition is {
-	Integer n1 is 25;
-	Integer n2 is -3;
+	Integer n1 is external;
+	Integer n2 is external;
 	Integer n_unary_addition_1 is +n1;
 	Integer n_unary_addition_2 is +n2;
 };

src/test/resources/testModels/spec-doc-examples/IntegerUnaryAddition_no_ext.crml

@@ -0,0 +1,6 @@
+model IntegerUnaryAddition is {
+	Integer n1 is 25;
+	Integer n2 is -3;
+	Integer n_unary_addition_1 is +n1; //Value is 26
+	Integer n_unary_addition_2 is +n2; //Value is -2
+};

src/test/resources/testModels/spec-doc-examples/PeriodClosingEvent_no_ext.crml

@@ -0,0 +1,9 @@
+model PeriodClosingEvent_no_ext is {
+	Boolean b1 is if (2.0 <= time and time < 3.5) then true else false;
+	Boolean b2 is if (3.0 <= time and time < 5.5) then true else false;
+	Clock c1 is new Clock b1;
+	Clock c2 is new Clock b2;
+	Period P is [c1, c2];
+	Event e is P end; // Should return an event at t=3.0s
+
+};

src/test/resources/testModels/spec-doc-examples/PeriodOpeningEvent_no_ext.crml

@@ -0,0 +1,6 @@
+model PeriodOpeningEvent_no_ext is {
+	Boolean b is if (2.0 <= time and time < 3.5) then true else false;
+	Clock c is new Clock b;
+	Period P is [c, new Clock false];
+	Event e is P start; // Should return an event at t=2.0s
+};

src/test/resources/testModels/spec-doc-examples/RealBinaryAddition.crml

@@ -1,5 +1,5 @@
 model RealBinaryAddition is {
-	Real x1 is -28.775E+3;
-	Real x2 is 0.28e-7;
+	Real x1 is external;
+	Real x2 is external;
 	Real x_binary_addition is x1 + x2;
 };

src/test/resources/testModels/spec-doc-examples/RealBinaryAddition_no_ext.crml

@@ -0,0 +1,5 @@
+model RealBinaryAddition_no_ext is {
+	Real x1 is 2.5;
+	Real x2 is 3.0;
+	Real x_binary_addition is x1 + x2; //Value is 5.5
+};

src/test/resources/testModels/spec-doc-examples/RealMultiplication.crml

@@ -1,5 +1,5 @@
 model RealMultiplication is {
-	Real x1 is -28.775E+3;
-	Real x2 is 0.28e-7;
+	Real x1 is external;
+	Real x2 is external;
 	Real x_multiplication is x1 * x2;
 };

src/test/resources/testModels/spec-doc-examples/RealMultiplication_no_ext.crml

@@ -0,0 +1,5 @@
+model RealMultiplication is {
+	Real x1 is 2.5;
+	Real x2 is 3.0;
+	Real x_multiplication is x1 * x2; //Value is 7.5
+};

src/test/resources/testModels/spec-doc-examples/RealUnaryAddition.crml

@@ -1,6 +1,6 @@
 model RealUnaryAddition is {
-	Real x1 is -28.775E+3;
-	Real x2 is 0.28e-7;
+	Real x1 is external;
+	Real x2 is external;
 	Real x_unary_addition_1 is +x1;
 	Real x_unary_addition_2 is +x2;
 };

src/test/resources/testModels/spec-doc-examples/RealUnaryAddition_no_ext.crml

@@ -0,0 +1,6 @@
+model RealUnaryAddition_no_ext is {
+	Real x1 is 2.5;
+	Real x2 is 3.0;
+	Real x_unary_addition_1 is +x1; //Value is 3.5
+	Real x_unary_addition_2 is +x2; //Value is 4.0
+};

src/test/resources/testModels/spec-doc-examples/SetCard_no_ext.crml

@@ -0,0 +1,5 @@
+model SetCard_no_ext is {
+	// Example with set of Real variables
+	Real {} S is {3.0, 1.5, 237};
+	Integer n is card S; // Should be equal to 3.
+};

src/test/resources/testModels/spec-doc-examples/StringConcatenation.crml

@@ -1,5 +1,5 @@
 model StringConcatenation is {
-	String s1 is "conca";
-	String s2 is "tenation";
+	String s1 is external;
+	String s2 is external;
 	String s_s1_is_concatenated_with_s2 is s1 + s2; //value should be "s1s2"
 };

src/test/resources/testModels/spec-doc-examples/StringOperatorsExample1.crml → src/test/resources/testModels/spec-doc-examples/StringConcatenationExample1.crml

@@ -1,6 +1,6 @@
-model StringOperatorsExample1 is {
-	Integer n is 3;
-	Real x is 2.5;
-	String s is "The " + new String n + " ships follow each other from a distance of " + new String x + " kilometers.";
-	// The value of s is "The 3 ships follow each other from a distance of 2.5 kilometers."
+model StringOperatorsExample1 is {
+	Integer n is 3;
+	Real x is 2.5;
+	String s is "The " + new String n + " ships follow each other from a distance of " + new String x + " kilometers.";
+	// The value of s is "The 3 ships follow each other from a distance of 2.5 kilometers."
 };

src/test/resources/testModels/spec-doc-examples/StringOperatorsExample2.crml → src/test/resources/testModels/spec-doc-examples/StringConcatenationExample2.crml

@@ -1,4 +1,4 @@
-model StringOperatorsExample2 is {
-	String s is "The set of 4-valued Booleans is { " + new String undecided + ", "  + new String undefined + ", " + new String false + ", " + new String true + " }. ";
-	// The value of s is "The set of 4-valued Booleans is { undecided, undefined, false, true }."
+model StringOperatorsExample2 is {
+	String s is "The set of 4-valued Booleans is { " + new String undecided + ", "  + new String undefined + ", " + new String false + ", " + new String true + " }. ";
+	// The value of s is "The set of 4-valued Booleans is { undecided, undefined, false, true }."
 };

src/test/resources/testModels/spec-doc-examples/StringConcatenation_no_ext.crml

@@ -0,0 +1,5 @@
+model StringConcatenation_no_ext is {
+	String s1 is "conca";
+	String s2 is "tenation";
+	String s_s1_is_concatenated_with_s2 is s1 + s2; //value should be "concatenation"
+};