testing traffic light example

lenaRB · Nov 27, 2023 · 9d216f3 · 9d216f3
1 parent 4317a99
commit 9d216f3
Show file tree

Hide file tree

Showing 4 changed files with 11 additions and 9 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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