Skip to content

Commit

Permalink
more sophisticated unit test for category
Browse files Browse the repository at this point in the history
  • Loading branch information
audrey-jardin committed Apr 26, 2024
1 parent 74fce40 commit 75371f2
Show file tree
Hide file tree
Showing 2 changed files with 71 additions and 0 deletions.
36 changes: 36 additions & 0 deletions src/test/resources/testModels/libraries/FORML_test/CheckAtEnd.crml
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
model CheckAtEnd is ETL union {
// Decide
// Option1
// Operator [ Boolean ] 'decide' Boolean phi 'over' Period P = phi or (P end); //With or defined as the built-in disjunction operator
// Option2
Template b1 'or' b2 = not (not b1 and not b2);
Operator [ Boolean ] 'decide' Boolean phi 'over' Period P = phi 'or' new Boolean (P end); //With 'or' as a user-defined disjunction operator for Booleans (only)

// Evaluate
Operator [ Boolean ] 'evaluate' Boolean phi 'over' Period P
= integrate (('decide' phi 'over' P) * phi) on P;

// Check
Operator [ Boolean ] 'check' Boolean phi 'over' Periods P
= and ('evaluate' phi 'over' P);

// Category
Operator [ Boolean ] 'id' Boolean b = b;
Operator [ Boolean ] 'cte_false' Boolean b = false;
Category varying1 = { ('id', 'cte_false') };

// Operator for checking that a requirement is satisfied at the end of a time period
Operator [ Boolean ] Periods P 'check at end' Boolean b = 'check' (varying1 ('id' b)) 'over' P;

// Example of function call
Event e1 is external;
Event e2 is external;
Boolean u is external;
Period P1 is ] e1, e2 [;

Boolean b_check_at_end is {P1} 'check at end' u;




};
Original file line number Diff line number Diff line change
@@ -0,0 +1,35 @@
model CheckAtEnd is ETL union {
// Decide
// Option1
// Operator [ Boolean ] 'decide' Boolean phi 'over' Period P = phi or (P end); //With or defined as the built-in disjunction operator
// Option2
Template b1 'or' b2 = not (not b1 and not b2);
Operator [ Boolean ] 'decide' Boolean phi 'over' Period P = phi 'or' new Boolean (P end); //With 'or' as a user-defined disjunction operator for Booleans (only)

// Evaluate
Operator [ Boolean ] 'evaluate' Boolean phi 'over' Period P
= integrate (('decide' phi 'over' P) * phi) on P;

// Check
Operator [ Boolean ] 'check' Boolean phi 'over' Periods P
= and ('evaluate' phi 'over' P);

// Category
Operator [ Boolean ] 'id' Boolean b = b;
Operator [ Boolean ] 'cte_false' Boolean b = false;
Category varying1 = { ('id', 'cte_false') };

// Operator for checking that a requirement is satisfied at the end of a time period
Operator [ Boolean ] Periods P 'check at end' Boolean b = 'check' (varying1 ('id' b)) 'over' P;

// Example of function call
Boolean u is if (2.0 < time) and (time < 3.5) then undecided 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 b_check_at_end is {P1} 'check at end' u; // value should start undefined, turns undecided at 2.5s then false at 3.5s




};

0 comments on commit 75371f2

Please sign in to comment.