69 update traffic light and cooling system use cases with import feature

resources/crml_tutorial/pumping_system/pumping_system.crml

@@ -1,8 +1,11 @@
-
-
-model PumpingSystem is flatten {Units, FORM_L}
+model PumpingSystem is
+	// Libraries import
+	flatten 'Units' union
+	'ETL' union 
+	'FORML' union
 
-	union {
+	// PumpingSystem model
+	{
 		// type Requirement is Boolean forbid { *, +, integrate };
 
 		class Pump is {
@@ -32,4 +35,4 @@ model PumpingSystem is flatten {Units, FORM_L}
 		};
 
 		System system is System{ Pump (ident = "PO1"),  Pump (ident = "PO2"), Pump (ident = "PO3") };
-};
+	};

resources/crml_tutorial/traffic_light/Spec.crml

@@ -1,30 +1,33 @@
-model Spec is //ETL union FORM_L union 
-{
-// Requirement model for the traffic light example
+model Spec is
+  // Libraries import
+  'ETL' union
+  'FORML' union
+  'Units' union
+
+  // Requirement model for the traffic light example
+  {
+  // Definition of Requirement type
+  // Type Requirement is Boolean ;//forbid { *, +, integrate };
 
- // Definition of Requirement type
- // Type Requirement is Boolean ;//forbid { *, +, integrate };
+    // List of external variables
+    Boolean red is external;
+    Boolean yellow is external;
+    Boolean green is external;
 
-  // List of external variables
-  Boolean red is external;
-  Boolean yellow is external;
-  Boolean green is external;
+    // 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 );
 
-  // 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 );
+    // req2: "Step green should stay active for at least 30 seconds"
+    Requirement req2 is
+      "after" (green "becomes true") "for" 30
+      "ensure" green;
 
-  // req2: "Step green should stay active for at least 30 seconds"
-  Requirement req2 is
-    "after" (green "becomes true") "for" 30
-    "ensure" green;
-
-  // req3: "After green becomes active + 30 seconds,
-  //        next step should turn yellow within 0.2 seconds"
-  Requirement req3 is
-    "after" (green "becomes true" + 30) "for" 0.2
-    "check at end" yellow; 
-
-};
+    // req3: "After green becomes active + 30 seconds,
+    //        next step should turn yellow within 0.2 seconds"
+    Requirement req3 is
+      "after" (green "becomes true" + 30) "for" 0.2
+      "check at end" yellow; 
+  };

resources/crml_tutorial/traffic_light/Spec_crossroad.crml

@@ -1,60 +1,64 @@
-model TrafficLight_Spec is ETL union FORM_L union 
-{
-// Requirement model for the traffic light example
+model TrafficLight_Spec is
+	// Libraries import
+	'ETL' union
+	'FORML' union 
 
- // Definition of Requirement type
-  Type Requirement is Boolean ;//forbid { *, +, integrate };
-
-  // Extension of FORM_L library
-  // Checking that the duration of a condition at the end of a time period is between two threshold (could be declined with '>' and '<' relations)
-  Operator [ Boolean ] Periods P 'check duration' Boolean b 'between' constant Real d1 'and' constant Real d2
-		= (P 'check duration' b '>=' d1) and (P 'check duration' b '<=' d2);
-	// Checking that the transitional regime between two states does not spend too much time.
-	// In 'relaxed' mode, there is no imposed order.
-	Operator [ Boolean ] Boolean b1 'relaxed switches to' Boolean b2 'within' constant Real d
-		= 'after' (b1 'becomes false' 'or' b2 'becomes true') 'within' d 						// time locator
-			'check at end' not b1 and b2 ;																			// condition
-
-	class Lamp is {
-		Boolean current ;
-		Boolean next ;
-		Real minTime ;
-		Real maxTime ;
+	{
+	// Requirement model for the traffic light example
+
+		// Definition of Requirement type
+		Type Requirement is Boolean ;//forbid { *, +, integrate };
 
-		constant Real switchingTime = 0.2;
-
-		// Functional requirement
-		// req1: "The lamp should light during a continuous time between minTime and maxTime."
-		Requirement req1 is
-			'during' current 																									// time locator
-			'check duration' current 'between' minTime 'and' maxTime ;							// condition
+		// Extension of FORM_L library
+		// Checking that the duration of a condition at the end of a time period is between two threshold (could be declined with '>' and '<' relations)
+		Operator [ Boolean ] Periods P 'check duration' Boolean b 'between' constant Real d1 'and' constant Real d2
+				= (P 'check duration' b '>=' d1) and (P 'check duration' b '<=' d2);
+			// Checking that the transitional regime between two states does not spend too much time.
+			// In 'relaxed' mode, there is no imposed order.
+			Operator [ Boolean ] Boolean b1 'relaxed switches to' Boolean b2 'within' constant Real d
+				= 'after' (b1 'becomes false' 'or' b2 'becomes true') 'within' d 						// time locator
+					'check at end' not b1 and b2 ;																			// condition
+
+		class Lamp is {
+			Boolean current ;
+			Boolean next ;
+			Real minTime ;
+			Real maxTime ;
 
-		// req2: "after current step, current lamp should turn off, and next one should turn on within 0.2 seconds (whatever the order)"
-		Requirement req2 is current 'relaxed switches to' next 'within' switchingTime ;
-	};
-
-	class TrafficLight is {
-		// List of external variables
-		Boolean red is external;
-		Boolean yellow is external;
-		Boolean green is external;
+			constant Real switchingTime = 0.2;
 
-		Boolean simulationTime is external ;
+			// Functional requirement
+			// req1: "The lamp should light during a continuous time between minTime and maxTime."
+			Requirement req1 is
+				'during' current 																									// time locator
+				'check duration' current 'between' minTime 'and' maxTime ;							// condition
+
+			// req2: "after current step, current lamp should turn off, and next one should turn on within 0.2 seconds (whatever the order)"
+			Requirement req2 is current 'relaxed switches to' next 'within' switchingTime ;
+		};
+
+		class TrafficLight is {
+			// List of external variables
+			Boolean red is external;
+			Boolean yellow is external;
+			Boolean green is external;
+
+			Boolean simulationTime is external ;
 
-		// Instantiate the three lamps
-		Lamp      red_lamp is new Lamp ( current =  red,      next = green,  minTime = 30, maxTime = 40);
-		Lamp  green_lamp is new Lamp ( current =  green,  next = yellow, minTime = 30, maxTime = 40);
-		Lamp yellow_lamp is new Lamp ( current =  yellow, next = red,     minTime = 5,   maxTime = 10);
+			// Instantiate the three lamps
+			Lamp      red_lamp is new Lamp ( current =  red,      next = green,  minTime = 30, maxTime = 40);
+			Lamp  green_lamp is new Lamp ( current =  green,  next = yellow, minTime = 30, maxTime = 40);
+			Lamp yellow_lamp is new Lamp ( current =  yellow, next = red,     minTime = 5,   maxTime = 10);
 
-		// Shadow requirement (only to eliminate a "null solution" where all lamps never light)
-		Requirement req_init is 'during' simulationTime 'check count' red_lamp '>=' 1 ;
-	};
+			// Shadow requirement (only to eliminate a "null solution" where all lamps never light)
+			Requirement req_init is 'during' simulationTime 'check count' red_lamp '>=' 1 ;
+		};
 
-	// instantiate two traffic lights in a crossroads
-	TrafficLight t1 is new TrafficLight ;
-	TrafficLight t2 is new TrafficLight ;
-
-	// Crossroad safety requirements 
-	Requirement req_crossroad1 is 'during' t1.green 'ensure' t2.red ;
-	Requirement req_crossroad2 is 'during' t2.green 'ensure' t1.red ;
-};
+		// instantiate two traffic lights in a crossroads
+		TrafficLight t1 is new TrafficLight ;
+		TrafficLight t2 is new TrafficLight ;
+		
+		// Crossroad safety requirements 
+		Requirement req_crossroad1 is 'during' t1.green 'ensure' t2.red ;
+		Requirement req_crossroad2 is 'during' t2.green 'ensure' t1.red ;
+	};

resources/crml_tutorial/traffic_light/Spec_simplified.crml

@@ -1,121 +1,39 @@
-//model TrafficLightSpecification is flatten ETLlibrary union {
-
 model TrafficLightSpecification is {
-// Requirement model for the traffic light example
-
-
+	// Libraries import
+	'ETL' union
+	'FORML' union
 
 	// User-defined types and operators
+	{
 		// Definition of Requirement type
 		//Type Requirement is Boolean;
-
-		// Extract of ETL library
-
-			// Operators on Boolean
-			// Logical disjunction
-			Template b1 'or' b2 = not ((not b1) and (not b2));
-
-			// Operators on events
-			// Events generated when a Boolean becomes true
-			Operator [ Clock ] Boolean b 'becomes true' = new Clock b;
-
-			// 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)));
-
-			// Decide
-			//Operator 'decide' is 
-			Operator [ Boolean ] 'decide' Boolean phi 'over' Period P = phi 'or' new Boolean((P end));
-
-			// Operators on clocks
-			// Count the occurrences of events inside a time period
-			Operator [ Integer ] 'count' Clock C 'inside' Period P = card (C 'inside' P);
-
-			// Evaluate
-			Operator [ Boolean ] 'evaluate' Boolean phi 'over' Period P 
-				= integrate (('decide' phi 'over' P) * phi) on P;
-
-			// Operators for the evaluation of requirements
-			// Check
-			Operator [ Boolean ] 'check' Boolean phi 'over' Periods P 
-				= and ('evaluate' phi 'over' P.element);
-
-			// Category c1 is Category increasing1 
-				//= { (>, >), (>=, >=), (<, >=), (<=, >), (==, >), (<>, >) };
-
-			Category increasing1 
-				= { (>, >), (>=, >=), (<, >=), (<=, >), (==, >), (<>, >) };
-			//Category {} C1 is associate increasing1 with 'decide';
-
-			Operator [ Boolean ] 'id' Boolean b = b;
-			Operator [ Boolean ] 'cte_false' Boolean b = false;
-			Operator [ Boolean ] 'cte_true' Boolean b = true;
-
-			// Category c3 is Category varying1 = { ('id', 'cte_false') };
-			Category varying1 = { ('id', 'cte_false') };
-			//Category {} C3 is associate varying1 with 'decide' 'over';
-
-			Category varying2 = { ('id', 'cte_true') };
-			//Category {} C4 is associate varying2 with 'decide' 'over';
-
-		// Extract of FORM_L library
-			// After events occur and before events occur
-			Operator [ Periods ] 'after' Clock ev1 'before' Clock ev2 = new Periods ] ev1, ev2 [;
-
-			// After events occur and for an elapsed time
-			Operator [ Periods ] 'after' Clock ev 'for' Real d = new Periods ] ev, (ev + d) ]; 	
-
-			// Checking that the number of event occurrences at the end of a time period is lower or higher than a threshold
-			// Option 1: without category
-			Operator [ Boolean ] Periods P 'check count' Clock E '==' Integer n 
-			= 'check'(('count' E 'inside' P.element) == n) 'over' P;
-
-			// // Option 2 (later support): with category
-			// Operator [ Boolean ] Periods P 'check count' Clock E '==' Integer n 
-			// = apply increasing1 on ('check'(('count' E 'inside' P) '==' n) 'over' P);
-
-
-			// Ensuring that a requirement is satisfied all along a time period
-			//Option 1:
-			// Operator [ Boolean ] Periods P 'ensure' Boolean b 
-				// = ('check' (('count' (b 'becomes true') 'inside' P) == 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 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 on ('check'  ('id' b) 'over' P);
-
-			//Option 2:
-			Operator [ Boolean ] Periods P 'ensure' Boolean b 
-				= (P 'check count' (b 'becomes true') '==' 0) and (P 'check anytime' b);
-
-
-	// List of external variables
-	Boolean red is external;
-	Boolean yellow is external;
-	Boolean green is external;
-
-	// Definition of requirements
-	// req1: "After green, next step is yellow"
-	// Requirement req1 is
-	Boolean req1 is
-		('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
-	Boolean req2 is
-		('after' (green 'becomes true') 'for' 30)
-		'ensure' green;
-
-	// req3: "After green becomes active + 30 seconds,
-	//        next step should turn yellow within 0.2 seconds"
-	// Requirement req3 is
-	Boolean req3 is
-		('after' ((green 'becomes true') + 30) 'for' 0.2)
-		'check at end' yellow;
-};
+	} union
+
+	// Requirement model for the traffic light example
+	{
+		// List of external variables
+		Boolean red is external;
+		Boolean yellow is external;
+		Boolean green is external;
+
+		// Definition of requirements
+		// req1: "After green, next step is yellow"
+		// Requirement req1 is
+		Boolean req1 is
+			('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
+		Boolean req2 is
+			('after' (green 'becomes true') 'for' 30)
+			'ensure' green;
+
+		// req3: "After green becomes active + 30 seconds,
+		//        next step should turn yellow within 0.2 seconds"
+		// Requirement req3 is
+		Boolean req3 is
+			('after' ((green 'becomes true') + 30) 'for' 0.2)
+			'check at end' yellow;
+	};