diff --git a/resources/crml_tutorial/traffic_light/Spec.crml b/resources/crml_tutorial/traffic_light/Spec.crml index 10e6e87..147e010 100644 --- a/resources/crml_tutorial/traffic_light/Spec.crml +++ b/resources/crml_tutorial/traffic_light/Spec.crml @@ -3,7 +3,7 @@ model Spec is //ETL union FORM_L union // Requirement model for the traffic light example // Definition of Requirement type - Type Requirement is Boolean ;//forbid { *, +, integrate }; + // Type Requirement is Boolean ;//forbid { *, +, integrate }; // List of external variables Boolean red is external; @@ -13,8 +13,8 @@ model Spec is //ETL union FORM_L union // Definition of requirements // req1: "After green, next step is yellow" Requirement req1 is - "after" (green "becomes true") "before" (yellow "becomes true") - "check count" (red "becomes true") "==" 0; + ( "after" ( green "becomes true" ) "before" ( yellow "becomes true" ) + "check count" (red "becomes true") "==" 0 ); // req2: "Step green should stay active for at least 30 seconds" Requirement req2 is diff --git a/resources/crml_tutorial/traffic_light/Spec_simplified.crml b/resources/crml_tutorial/traffic_light/Spec_simplified.crml index a0269bd..51164ce 100644 --- a/resources/crml_tutorial/traffic_light/Spec_simplified.crml +++ b/resources/crml_tutorial/traffic_light/Spec_simplified.crml @@ -70,10 +70,10 @@ model Spec is { = ('check' ('count' (b 'becomes true') == 0) 'over' P) and (P 'check anytime' b); // Checking that a requirement is satisfied at any time instant of a time period - Operator [ Boolean ] Periods P 'check anytime' Boolean b = apply varying2 'check' 'id' b 'over' P; + Operator [ Boolean ] Periods P 'check anytime' Boolean b = apply varying2 on '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 = apply varying1 'check' 'id' b 'over' P; + Operator [ Boolean ] Periods P 'check at end' Boolean b = apply varying1 on 'check' 'id' b 'over' P; // List of external variables Boolean red is external; diff --git a/src/main/antlr/grammar/crml.g4 b/src/main/antlr/grammar/crml.g4 index 8435847..bee76f4 100644 --- a/src/main/antlr/grammar/crml.g4 +++ b/src/main/antlr/grammar/crml.g4 @@ -76,9 +76,9 @@ when_exp : 'when' when_e=exp 'then' then_e=exp; integrate : 'integrate' exp 'on' exp; -tick : 'tick'; +tick : 'tick' id; - exp : id | constant | sub_exp | constructor | sum |trim | proj | period_op + exp : sub_exp | id | constant | constructor | sum |trim | proj | period_op | uright=user_keyword right=exp | left=exp ubinary=user_keyword right=exp | left=exp uleft=user_keyword | left=exp binary=builtin_op right=exp | right=exp runary=builtin_op | lunary=builtin_op left=exp | 'element' | 'terminate' | when_exp | exp 'at' at=exp @@ -95,7 +95,7 @@ op : builtin_op|user_keyword builtin_op : 'and' | '*' | '+' | '-' | '/' | 'with' | 'master' | 'on' | 'filter' | '<=' | '<' | '>=' | '>' | '<>' | 'par' | '==' | - 'pre' | 'not'| '-' | 'card' | 'and' | 'or' | '^' | + 'pre' | 'not'| '-' | 'card' | 'or' | '^' | 'start' | 'end' | 'mod' | 'exp' | 'log' | 'log10' | 'cos' |'acos' | 'sin' | 'asin' ; diff --git a/src/main/java/crml/translator/crmlVisitorImpl.java b/src/main/java/crml/translator/crmlVisitorImpl.java index 99a13e0..e18b5b2 100644 --- a/src/main/java/crml/translator/crmlVisitorImpl.java +++ b/src/main/java/crml/translator/crmlVisitorImpl.java @@ -490,8 +490,10 @@ else if (ctx.uninstantiated_def()!=null) } // if the expression is in parenthesis - if(ctx.sub_exp()!=null) + if(ctx.sub_exp()!=null){ + System.out.println("SUB EXPRESSION FOUND"); return visit(ctx.sub_exp().exp()); + } // expression is a tick