diff --git a/src/test/resources/testModels/libraries/ETL_test/BecomesFalse.crml b/src/test/resources/testModels/libraries/ETL_test/BecomesFalse.crml new file mode 100644 index 00000000..1ddaf524 --- /dev/null +++ b/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'; +}; \ No newline at end of file diff --git a/src/test/resources/testModels/libraries/ETL_test/BecomesFalse_no_ext.crml b/src/test/resources/testModels/libraries/ETL_test/BecomesFalse_no_ext.crml new file mode 100644 index 00000000..f0c7ab6e --- /dev/null +++ b/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 + +}; \ No newline at end of file diff --git a/src/test/resources/testModels/libraries/ETL_test/BecomesTrueInside.crml b/src/test/resources/testModels/libraries/ETL_test/BecomesTrueInside.crml new file mode 100644 index 00000000..ccef4f06 --- /dev/null +++ b/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; +}; \ No newline at end of file diff --git a/src/test/resources/testModels/libraries/ETL_test/BecomesTrueInside_no_ext.crml b/src/test/resources/testModels/libraries/ETL_test/BecomesTrueInside_no_ext.crml new file mode 100644 index 00000000..62d9993f --- /dev/null +++ b/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 + +}; \ No newline at end of file diff --git a/src/test/resources/testModels/libraries/ETL_test/Implies.crml b/src/test/resources/testModels/libraries/ETL_test/Implies.crml new file mode 100644 index 00000000..9760e9df --- /dev/null +++ b/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; +}; \ No newline at end of file diff --git a/src/test/resources/testModels/libraries/ETL_test/Implies_no_ext.crml b/src/test/resources/testModels/libraries/ETL_test/Implies_no_ext.crml new file mode 100644 index 00000000..311d6f56 --- /dev/null +++ b/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 + +}; \ No newline at end of file diff --git a/src/test/resources/testModels/libraries/ETL_test/TemplateXor.crml b/src/test/resources/testModels/libraries/ETL_test/TemplateXor.crml new file mode 100644 index 00000000..053ab7dd --- /dev/null +++ b/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; +}; \ No newline at end of file diff --git a/src/test/resources/testModels/libraries/ETL_test/TemplateXor_no_ext.crml b/src/test/resources/testModels/libraries/ETL_test/TemplateXor_no_ext.crml new file mode 100644 index 00000000..92bbef7b --- /dev/null +++ b/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 + +}; \ No newline at end of file