new test models for ETL operators

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

@@ -0,0 +1,9 @@
+model BecomesFalse is {
+	// Operators on events
+	// Events generated when a Boolean becomes false
+	Operator [ Clock ] Boolean b 'becomes false' = new Clock (not b);
+
+	// Example of function call
+	Boolean b1 is external;
+	Clock c_b1_becomes_false is b1 'becomes false';
+};

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

@@ -0,0 +1,16 @@
+model BecomesFalse_no_ext is {
+	// Operators on events
+	// Events generated when a Boolean becomes false
+	Operator [ Clock ] Boolean b 'becomes false' = new Clock (not b);
+
+	// Example of function call
+
+	Boolean b1 is if ((2.5 < time) and (time < 5)) or ((7.5 < time) and (time < 9)) then true else false;
+	Boolean b2 is true;
+	Boolean b3 is false;
+
+	Clock c1 is b1 'becomes false'; // Two events should be generated at instants 5s and 9s
+	Clock c2 is b2 'becomes false'; // No event should be generated
+	Clock c3 is b3 'becomes false'; // No event should be generated
+
+};

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

@@ -0,0 +1,19 @@
+model BecomesTrueInside is {
+	// Operators on clocks
+		// 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));
+
+	// Operators on events
+		// Events generated when a Boolean becomes true
+		Operator [ Clock ] Boolean b 'becomes true' = new Clock b;
+
+		// Events generated when a Boolean becomes true inside a time period
+		Operator [ Clock ] Boolean b 'becomes true inside' Period P = ( b 'becomes true') 'inside' P;
+
+	// Example of function call
+	Boolean b1 is external;
+	Boolean b2 is external;
+	Period P1 is [ b1, not b1];
+	Clock c_b2_becomes_true_inside_p1 is b2 'becomes true inside' P1;
+};

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

@@ -0,0 +1,26 @@
+model BecomesTrue_no_ext is {
+	// Operators on clocks
+		// 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));
+
+	// Operators on events
+		// Events generated when a Boolean becomes true
+		Operator [ Clock ] Boolean b 'becomes true' = new Clock b;
+
+		// Events generated when a Boolean becomes true inside a time Period
+		Operator [ Clock ] Boolean b 'becomes true inside' Period P = ( b 'becomes true') 'inside' P;
+
+	// Example of function call
+	Boolean b1 is if ((2.5 < time) and (time < 5)) or ((7.5 < time) and (time < 9)) then true else false;
+	Boolean b2 is if ((3.5 < time) and (time < 4.5)) then true else false;
+	Boolean b3 is true;
+	Boolean b4 is false;
+
+	Period P1 is [ b1, not b1];
+
+	Clock c_b2_becomes_true_inside_p1 is b2 'becomes true inside' P1; // One event should be generated at instant 3.5s.
+	Clock c_b3_becomes_true_inside_p1 is b3 'becomes true inside' P1; // No event should be generated
+	Clock c_b4_becomes_true_inside_p1 is b4 'becomes true inside' P1; // No event should be generated
+
+};

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

@@ -0,0 +1,12 @@
+model Implies is {
+	// Definition of disjunction of two Booleans.
+	Template b1 'or' b2 = not(not b1 and not b2);	
+
+	// Definition of logical inference
+	Template b1 'implies' b2 = (not b1) 'or' b2;
+
+	// Example of function call
+	Boolean b1 is external;
+	Boolean b2 is external;
+	Boolean b1_implies_b2 is b1 'implies' b2;
+};

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

@@ -0,0 +1,38 @@
+model Implies_no_ext is {
+	// Definition of disjunction of two Booleans.
+	Template b1 'or' b2 = not ( (not b1) and (not b2) );
+
+	// Definition of logical inference
+	Template b1 'implies' b2 = (not b1) 'or' b2;
+
+	// Example of function call
+	Boolean b_true is true;
+	Boolean b_false is false;
+	Boolean b_undecided is undecided;
+	Boolean b_undefined is undefined;
+
+	//Test truth table for the logical inference
+	//Values should be the same as for the built-in or operator
+
+	//First row
+	Boolean b_true_implies_true is b_true 'implies' b_true; //value should be true
+	Boolean b_true_implies_false is b_true 'implies' b_false; //value should be false
+	Boolean b_true_implies_undecided is b_true 'implies' b_undecided; //value should be undecided
+	Boolean b_true_implies_undefined is b_true 'implies' b_undefined; //value should be false
+	//Second row
+	Boolean b_false_implies_true is b_false 'implies' b_true; //value should be true
+	Boolean b_false_implies_false is b_false 'implies' b_false; //value should be true
+	Boolean b_false_implies_undecided is b_false 'implies' b_undecided; //value should be true
+	Boolean b_false_implies_undefined is b_false 'implies' b_undefined; //value should be true
+	//Third row
+	Boolean b_undecided_implies_true is b_undecided 'implies' b_true; //value should be true
+	Boolean b_undecided_implies_false is b_undecided 'implies' b_false; //value should be undecided
+	Boolean b_undecided_implies_undecided is b_undecided 'implies' b_undecided; //value should be undecided
+	Boolean b_undecided_implies_undefined is b_undecided 'implies' b_undefined; //value should be undecided
+	//Fourth row
+	Boolean b_undefined_implies_true is b_undefined 'implies' b_true; //value should be true
+	Boolean b_undefined_implies_false is b_undefined 'implies' b_false; //value should be false
+	Boolean b_undefined_implies_undecided is b_undefined 'implies' b_undecided; //value should be undecided
+	Boolean b_undefined_implies_undefined is b_undefined 'implies' b_undefined; //value should be undefined
+
+};

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

@@ -0,0 +1,12 @@
+model TemplateXor is {
+	// Definition of disjunction of two Booleans.
+	Template b1 'or' b2 = not(not b1 and not b2);	
+
+	// Definition of exclusivee disjunction
+	Template b1 'xor' b2 = (b1 'or' b2) and ( not( b1 and b2 ) );
+
+	// Example of function call
+	Boolean b1 is external;
+	Boolean b2 is external;
+	Boolean b1_xor_b2 is b1 'xor' b2;
+};

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

@@ -0,0 +1,38 @@
+model TemplateXor_no_ext is {
+	// Definition of disjunction of two Booleans.
+	Template b1 'or' b2 = not ( (not b1) and (not b2) );
+
+	// Definition of exclusive disjunction of two Booleans.
+	Template b1 'xor' b2 = (b1 'or' b2) and not (b1 and b2);
+
+	// Example of function call
+	Boolean b_true is true;
+	Boolean b_false is false;
+	Boolean b_undecided is undecided;
+	Boolean b_undefined is undefined;
+
+	//Test truth table for the exclusive logical disjunction
+	//Values should be the same as for the built-in xor operator
+
+	//First row
+	Boolean b_true_xor_true is b_true 'xor' b_true; //value should be false
+	Boolean b_true_xor_false is b_true 'xor' b_false; //value should be true
+	Boolean b_true_xor_undecided is b_true 'xor' b_undecided; //value should be undecided
+	Boolean b_true_xor_undefined is b_true 'xor' b_undefined; //value should be true
+	//Second row
+	Boolean b_false_xor_true is b_false 'xor' b_true; //value should be true
+	Boolean b_false_xor_false is b_false 'xor' b_false; //value should be false
+	Boolean b_false_xor_undecided is b_false 'xor' b_undecided; //value should be undecided
+	Boolean b_false_xor_undefined is b_false 'xor' b_undefined; //value should be true
+	//Third row
+	Boolean b_undecided_xor_true is b_undecided 'xor' b_true; //value should be undecided
+	Boolean b_undecided_xor_false is b_undecided 'xor' b_false; //value should be undecided
+	Boolean b_undecided_xor_undecided is b_undecided 'xor' b_undecided; //value should be undecided
+	Boolean b_undecided_xor_undefined is b_undecided 'xor' b_undefined; //value should be undecided
+	//Fourth row
+	Boolean b_undefined_xor_true is b_undefined 'xor' b_true; //value should be true
+	Boolean b_undefined_xor_false is b_undefined 'xor' b_false; //value should be true
+	Boolean b_undefined_xor_undecided is b_undefined 'xor' b_undecided; //value should be undecided
+	Boolean b_undefined_xor_undefined is b_undefined 'xor' b_undefined; //value should be undefined
+
+};