Skip to content

Commit

Permalink
update to category syntax
Browse files Browse the repository at this point in the history
  • Loading branch information
lenaRB committed Oct 20, 2023
1 parent ebc56a8 commit 5a7f642
Show file tree
Hide file tree
Showing 3 changed files with 11 additions and 10 deletions.
2 changes: 1 addition & 1 deletion resources/crml_tutorial/traffic_light/Spec_simplified.crml
Original file line number Diff line number Diff line change
Expand Up @@ -73,7 +73,7 @@ model Spec is {
Operator [ Boolean ] Periods P 'check anytime' Boolean b = apply varying2 'check' 'id' b 'over' P;

// 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;
Operator [ Boolean ] Periods P 'check at end' Boolean b = apply varying1 'check' 'id' b 'over' P;

// List of external variables
Boolean red is external;
Expand Down
2 changes: 1 addition & 1 deletion src/main/antlr/grammar/crml.g4
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ template : 'Template' (id | user_keyword)+ '=' exp ';' ;

class_params : '(' (id '=' exp)+ ')';

operator_def : (type id | user_keyword)+ '=' ('apply' assoc=id)? exp ;
operator_def : (type id | user_keyword)+ '=' ('apply' assoc=id 'on')? exp ;

type_def : 'type' id ('extends' type arg_list? id?)? ('{' class_var_def * '}' )? ;

Expand Down
Original file line number Diff line number Diff line change
@@ -1,25 +1,26 @@
model CategoryAssociationExample1 is {
// Operators' definition
Operator 'decide' is
Operator [ Boolean ] 'decide' Boolean phi 'over' Period P = phi 'or' (P end));
Template b1 'or' b2 = not (not b1 and not b2);

Operator [ Boolean ] 'decide' Boolean phi 'over' Period P = phi 'or' (P end);
Operator [ Boolean ] 'id' Boolean b = b;
Operator [ Boolean ] 'cte_false' Boolean b = false;
Operator [ Boolean ] 'cte_true' Boolean b = true;

// Category definition as an operator on the operators previously defined
Category c3 is Category varying1 = { ('id', 'cte_false') };
Category c4 is Category varying1 = { ('id', 'cte_true') };
Category varying1 = { ('id', 'cte_false') };
Category varying2 = { ('id', 'cte_true') };

// Association of categories with operators
Category {} C3 is associate varying1 with 'decide';
Category {} C4 is associate varying2 with 'decide';
//Category {} C3 is associate varying1 with 'decide';
//Category {} C4 is associate varying2 with 'decide';

// Definition of new operators using association previously defined
// Decide that decision event to evaluate requirement is the end of a time period
Operator [ Boolean ] Period P 'decide at end' Boolean b = 'decide' varying1 'id' b 'over' P;
Operator [ Boolean ] Period P 'decide at end' Boolean b = apply varying1 on 'decide' 'id' b 'over' P;

// Decide that decision event to evaluate requirement is any time instant of a time period
Operator [ Boolean ] Periods P 'decide anytime' Boolean b = 'decide' varying2 'id' b 'over' P;
Operator [ Boolean ] Periods P 'decide anytime' Boolean b = apply varying2 on 'decide' 'id' b 'over' P;

// Example of operator calls
Boolean b1 is time > 1.0;
Expand Down

0 comments on commit 5a7f642

Please sign in to comment.