diff --git a/resources/crml_tutorial/pumping_system/pumping_system.crml b/resources/crml_tutorial/pumping_system/pumping_system.crml index a7b0e3e3..6a1390c9 100644 --- a/resources/crml_tutorial/pumping_system/pumping_system.crml +++ b/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") }; -}; \ No newline at end of file + }; \ No newline at end of file diff --git a/resources/crml_tutorial/traffic_light/Spec.crml b/resources/crml_tutorial/traffic_light/Spec.crml index 147e0106..0f78a51e 100644 --- a/resources/crml_tutorial/traffic_light/Spec.crml +++ b/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; + }; diff --git a/resources/crml_tutorial/traffic_light/Spec_crossroad.crml b/resources/crml_tutorial/traffic_light/Spec_crossroad.crml index 6129d0e9..9b9556fc 100644 --- a/resources/crml_tutorial/traffic_light/Spec_crossroad.crml +++ b/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 ; -}; \ No newline at end of file + // 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 ; + }; \ No newline at end of file diff --git a/resources/crml_tutorial/traffic_light/Spec_simplified.crml b/resources/crml_tutorial/traffic_light/Spec_simplified.crml index 58bc872e..658db279 100644 --- a/resources/crml_tutorial/traffic_light/Spec_simplified.crml +++ b/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; + }; diff --git a/resources/crml_tutorial/traffic_light/TrafficLightSpec_simplified.crml b/resources/crml_tutorial/traffic_light/TrafficLightSpec_simplified.crml index cd79b247..b42969b0 100644 --- a/resources/crml_tutorial/traffic_light/TrafficLightSpec_simplified.crml +++ b/resources/crml_tutorial/traffic_light/TrafficLightSpec_simplified.crml @@ -1,117 +1,38 @@ -model TrafficLightSpecification is { -// Requirement model for the traffic light example - - // 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); - - // 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) == 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; -}; +model TrafficLightSpecification_simplified is + // Libraries import + 'ETL' union + 'FORML' union + + // Traffic Light (Simplified) Requirement model + { + // User-defined types and operators + // Definition of Requirement type + //Type Requirement is Boolean; + + // 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; + } +; diff --git a/resources/crml_tutorial/traffic_light/TrafficLightSpecification_articleModelicaConf2025.crml b/resources/crml_tutorial/traffic_light/TrafficLightSpecification_articleModelicaConf2025.crml index cf7da48b..67e8d4bb 100644 --- a/resources/crml_tutorial/traffic_light/TrafficLightSpecification_articleModelicaConf2025.crml +++ b/resources/crml_tutorial/traffic_light/TrafficLightSpecification_articleModelicaConf2025.crml @@ -1,54 +1,57 @@ model TrafficLightSpecification_article is - // Import of libraries - flatten {ETL, FORM_L} - union { - // List of external variables - Boolean red is external; - Boolean yellow is external; - Boolean green is external; - - Boolean operation is external; - Boolean night_mode is external; - Boolean day_mode is not night_mode; + // Libraries import + 'ETL' union + 'FORML' union - // Definition of requirements - // req0: "During operation, no more than one light should be on (a flashing mode could be specified later)" - Boolean{} lights is {red, yellow, green}; - Integer n_lights_on is card { filter lights (element == true) }; - - Requirement req0 is - ('during' operation) ('check anytime' (n_lights_on <= 1) ); - - // Day_mode - // req1: "After green, next step is yellow" - Requirement req1 is - (( 'after' ( green 'becomes true' ) 'before' ( yellow 'becomes true' )) while day_mode) - ('check count' (red 'becomes true') '==' 0); + // TrafficLightSpecification model + { + // List of external variables + Boolean red is external; + Boolean yellow is external; + Boolean green is external; + + Boolean operation is external; + Boolean night_mode is external; + Boolean day_mode is not night_mode; - // req2: "Step green should stay active for at least 30 seconds" - Requirement req2 is - (( 'after' (green 'becomes true') 'for' 30) while day_mode) - ('ensure' green); + // Definition of requirements + // req0: "During operation, no more than one light should be on (a flashing mode could be specified later)" + Boolean{} lights is {red, yellow, green}; + Integer n_lights_on is card { filter lights (element == true) }; + + Requirement req0 is + ('during' operation) ('check anytime' (n_lights_on <= 1) ); + + // Day_mode + // req1: "After green, next step is yellow" + Requirement req1 is + (( 'after' ( green 'becomes true' ) 'before' ( yellow 'becomes true' )) while day_mode) + ('check count' (red 'becomes true') '==' 0); - // 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) while day_mode) - ('check at end' yellow); - - // Night_mode - // req4: "During night, yellow should only be used" - Requirement req4 is - ('during' night_mode) - ('check count' ( (red or green) 'becomes true') '==' 0); - // req5: "During night, yellow should flash every 2 seconds" - Requirement req5a is - ('during' night_mode) - ('check count' ( yellow 'becomes true') '<>' 0); - Requirement req5b is - ('after' ( yellow 'becomes true') 'within' 2) while night_mode) - ('ensure' yellow); - Requirement req5c is - ('after' ( yellow 'becomes true') 'for' 2) while night_mode) - ('check at end' not yellow); - Requirement req5 is req5a and req5b and req5c; -}; \ No newline at end of file + // req2: "Step green should stay active for at least 30 seconds" + Requirement req2 is + (( 'after' (green 'becomes true') 'for' 30) while day_mode) + ('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) while day_mode) + ('check at end' yellow); + + // Night_mode + // req4: "During night, yellow should only be used" + Requirement req4 is + ('during' night_mode) + ('check count' ( (red or green) 'becomes true') '==' 0); + // req5: "During night, yellow should flash every 2 seconds" + Requirement req5a is + ('during' night_mode) + ('check count' ( yellow 'becomes true') '<>' 0); + Requirement req5b is + ('after' ( yellow 'becomes true') 'within' 2) while night_mode) + ('ensure' yellow); + Requirement req5c is + ('after' ( yellow 'becomes true') 'for' 2) while night_mode) + ('check at end' not yellow); + Requirement req5 is req5a and req5b and req5c; + }; \ No newline at end of file diff --git a/resources/crml_tutorial/typical_requirement.crml b/resources/crml_tutorial/typical_requirement.crml index aeb025ff..5eac877c 100644 --- a/resources/crml_tutorial/typical_requirement.crml +++ b/resources/crml_tutorial/typical_requirement.crml @@ -1,34 +1,41 @@ -class TypicalRequirement is ETL union FORM_L union { +class TypicalRequirement is + // Libraries import + 'ETL' union + 'FORML' union + + // TypicalRequirement Model + { - type Requirement is Boolean forbid { *, +, integrate }; + type Requirement is Boolean forbid { *, +, integrate }; - Boolean inOperation is external; - Boolean inNormalDomain is external; - Boolean inBackupDomain is external; - Boolean inSystemOperatingLife is external; - - Real x, y is external; - Integer n is external; - - Real p is 0.99; - - // r1 is “During operation, the system should stay within its normal domain." - Requirement r1 is 'during' inOperation 'ensure' inNormalDomain; - - // r2 is “If the system fails to stay within its operating domain, then it should not stay outside of its normal domain for more than x minutes." - Requirement r2 is 'during' inOperation 'ensure' (not inNormalDomain 'implies' r2_outside); - Requirement r2_outside is 'during' [inNormalDomain 'becomes false', inNormalDomain 'becomes false' + x mn] 'check at end' b; - Boolean b is inOperation 'implies' inNormalDomain; + Boolean inOperation is external; + Boolean inNormalDomain is external; + Boolean inBackupDomain is external; + Boolean inSystemOperatingLife is external; - // r3 is "The system should not go outside its normal domain more than n times per year.” - Requirement r3 is 'count' ((b 'becomes false') on [b 'becomes false', b 'becomes false' + 1 year] <= n; - - // r4 is “If (r1 and r2 and r3) fail, then the system should go to its backup domain within y minutes as soon as the failure is detected.” - Requirement r4 is not (r1 and r2 and r3) 'implies' - 'during' [(r1 and r2 and r3) 'becomes false', (r1 and r2 and r3) 'becomes false' + y mn] 'check at end' inBackupDomain; - - // R is “During system operating life, r1 and r2 and r3 and r4 should be satisfied with a probability of success of p%.” - Real prob is estimator Probability (r1 and r2 and r3 and r4) at inSystemOperatingLife 'becomes false'; - Requirement R is 'during' inSystemOperatingLife 'check at end prob' > p; -}; + Real x, y is external; + Integer n is external; + + Real p is 0.99; + + // r1 is “During operation, the system should stay within its normal domain." + Requirement r1 is 'during' inOperation 'ensure' inNormalDomain; + + // r2 is “If the system fails to stay within its operating domain, then it should not stay outside of its normal domain for more than x minutes." + Requirement r2 is 'during' inOperation 'ensure' (not inNormalDomain 'implies' r2_outside); + Requirement r2_outside is 'during' [inNormalDomain 'becomes false', inNormalDomain 'becomes false' + x mn] 'check at end' b; + Boolean b is inOperation 'implies' inNormalDomain; + + // r3 is "The system should not go outside its normal domain more than n times per year.” + Requirement r3 is 'count' ((b 'becomes false') on [b 'becomes false', b 'becomes false' + 1 year] <= n; + + // r4 is “If (r1 and r2 and r3) fail, then the system should go to its backup domain within y minutes as soon as the failure is detected.” + Requirement r4 is not (r1 and r2 and r3) 'implies' + 'during' [(r1 and r2 and r3) 'becomes false', (r1 and r2 and r3) 'becomes false' + y mn] 'check at end' inBackupDomain; + + // R is “During system operating life, r1 and r2 and r3 and r4 should be satisfied with a probability of success of p%.” + Real prob is estimator Probability (r1 and r2 and r3 and r4) at inSystemOperatingLife 'becomes false'; + Requirement R is 'during' inSystemOperatingLife 'check at end prob' > p; + } +; diff --git a/resources/use_cases/cooling_system/ics_reqs.crml b/resources/use_cases/cooling_system/ics_reqs.crml index 571229dd..0811f2e7 100644 --- a/resources/use_cases/cooling_system/ics_reqs.crml +++ b/resources/use_cases/cooling_system/ics_reqs.crml @@ -1,226 +1,68 @@ // ICS requirement model -model ics_reqs is { - - // ETL library - - // Operators on Boolean - // Logical disjunction - Template b1 'or' b2 = not (not b1 and not b2); - - // Exclusive logical disjunction - Template b1 'xor' b2 = (b1 'or' b2) and not (b1 and b2); - - // Logical inference - Template b1 'implies' b2 = not b1 'or' b2; - - // Operators on clocks - // 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)); - - // Count the occurrences of events inside a time period - Operator [ Integer ] 'count' Clock C 'inside' Period P = card (C 'inside' P); - - // Operators on events - // Events generated when a Boolean becomes true - Operator [ Clock ] Boolean b 'becomes true' = new Clock b; - - // Events generated when a Boolean becomes false - Operator [ Clock] Boolean b 'becomes false' = not b 'becomes true'; - - // Events generated when a Boolean becomes true inside a time period - Operator [ Clock] Boolean b 'becomes true inside' Period P - = (b 'becomes true') 'inside' P; - - // Events generated when a Boolean becomes false inside a time period - Operator [ Clock] Boolean b 'becomes false inside' Period P - = (b 'becomes false') 'inside' P; - - // Decide - // Operator 'decide' is - Operator [ Boolean ] 'decide' Boolean phi 'over' Period P - = phi 'or' new Boolean (P end); - - // 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); - - Category increasing_int = { (>, >), (>=, >=), (<, >=), (<=, >), (==, >), (<>, >) }; - Category increasing_real = { (>, >), (>=, >=), (<, >=), (<=, >) }; - Operator [ Boolean ] Integer x '>_int' Integer n = apply increasing_int on ( x > n ); - Operator [ Boolean ] Integer x '>=_int' Integer n = apply increasing_int on ( x >= n ); - Operator [ Boolean ] Integer x '<_int' Integer n = apply increasing_int on ( x < n ); - Operator [ Boolean ] Integer x '<=_int' Integer n = apply increasing_int on ( x <= n ); - Operator [ Boolean ] Integer x '==_int' Integer n = apply increasing_int on ( x == n ); - Operator [ Boolean ] Integer x '<>_int' Integer n = apply increasing_int on ( x <> n ); - Operator [ Boolean ] Real x '>_real' Real d = apply increasing_real on ( x > d ); - Operator [ Boolean ] Real x '>=_real' Real d = apply increasing_real on ( x >= d ); - Operator [ Boolean ] Real x '<_real' Real d = apply increasing_real on ( x < d ); - Operator [ Boolean ] Real x '<=_real' Real d = apply increasing_real on ( x <= d ); - - - Operator [ Boolean ] 'id' Boolean b = b; - Operator [ Boolean ] 'cte_false' Boolean b = false; - Operator [ Boolean ] 'cte_true' Boolean b = true; - - Category varying1 = { ('id', 'cte_false') }; - Category varying2 = { ('id', 'cte_true') }; - Operator [ Boolean ] 'set to false' Boolean b = apply varying1 on ( 'id' b ); - Operator [ Boolean ] 'set to true' Boolean b = apply varying2 on ( 'id' b ); - +model ics_reqs is + ///////////////// + // Libraries import + /////////////////// + 'ETL' union + 'FORML' union + { + /////////////////////////////////////////////////////////////////////////////// + // ICS (Intermediate Cooling System) model /////////////////////////////////////////////////////////////////////////////// - // FORM-L library - // include "ETL.crml" - - // Operators to define time periods - // From events occur - Operator [ Periods ] 'from' Clock ev = new Periods [ ev, new Clock false ]; - - // After events occur - Operator [ Periods ] 'after' Clock ev = new Periods ] ev, new Clock false ]; - - // Before events occur - Operator [ Periods ] 'before' Clock ev = new Periods [ new Clock false, ev [; - - // Until events occur - Operator [ Periods ] 'until' Clock ev = new Periods [ new Clock false, ev ]; - - // While a Boolean is true - Operator [ Periods ] 'during' Boolean b = new Periods [ new Clock b, new Clock not b ]; - - // After events occur and before events occur - Operator [ Periods ] 'after' Clock ev1 'before' Clock ev2 = new Periods ] ev1, ev2 [; - - // After events occur and until events occur - Operator [ Periods ] 'after' Clock ev1 'until' 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 ]; - - // After events occur and within an elapsed time - Operator [ Periods ] 'after' Clock ev 'within' Real d = new Periods ] ev, ev + d [; - - // From events occur and before events occur - Operator [ Periods ] 'from' Clock ev1 'before' Clock ev2 = new Periods [ ev1, ev2 [; - - // From events occur and until events occur - Operator [ Periods ] 'from' Clock ev1 'until' Clock ev2 = new Periods [ ev1, ev2 ]; - - // From events occur and for an elapsed time - Operator [ Periods ] 'from' Clock ev 'for' Real d = new Periods [ ev, ev + d ]; - - // From events occur and within an elapsed time - Operator [ Periods ] 'from' Clock ev 'within' Real d = new Periods [ ev, ev + d [; - - // When events occurs - Operator [ Periods ] 'when' Clock ev = new Periods [ ev, ev ]; - - // Operators for the evaluation of requirements - - // Checking that a requirement is satisfied at the end of a time period - Operator [ Boolean ] Periods P 'check at end' Boolean b - = 'check' ('set to false' b) 'over' P; - - // Checking that a requirement is satisfied at any time instant of a time period - Operator [ Boolean ] Periods P 'check anytime' Boolean b - = 'check' ('set to true' b) 'over' P; + // Temperature requirements + // NL : "The ICS temperature should be maintained between 16°C and 30°C." + // SNL: "During normal normal operation, the ICS system shall have a temperature between 16°C and 30°C." + Boolean normal_operation is external; + Real T is external; + Boolean T_in_range is ((T >= 16) and (T <= 30)); //remark: not done yet but units should be specified + Boolean R1_T is ('during' normal_operation) 'ensure' T_in_range ; - // Following operators cannot be implemented because "count inside" is implemented only on period and not periods (which would have no meaning) ! - - // Checking that the number of event occurrences at the end of a time period is lower or higher than a threshold - //Operator [ Boolean ] Periods P 'check count' Clock E '<' Integer n - // = 'check' (('count' E 'inside' P) '<_int' n) 'over' P; - //Operator [ Boolean ] Periods P 'check count' Clock E '<=' Integer n - // = 'check'(('count' E 'inside' P) '<=_int' n) 'over' P; - //Operator [ Boolean ] Periods P 'check count' Clock E '>' Integer n - // = 'check'(('count' E 'inside' P) '>_int' n) 'over' P; - //Operator [ Boolean ] Periods P 'check count' Clock E '>=' Integer n - // = 'check'(('count' E 'inside' P) '>=_int' n) 'over' P; - //Operator [ Boolean ] Periods P 'check count' Clock E '==' Integer n - // = 'check'(('count' E 'inside' P) '==_int' n) 'over' P; - //Operator [ Boolean ] Periods P 'check count' Clock E '<>' Integer n - // = 'check'(('count' E 'inside' P) '<>_int' n) 'over' P; - - // Ensuring that a requirement is satisfied all along a time period - //Operator [ Boolean ] Periods P 'ensure' Boolean b - // = (P 'check count' (b 'becomes true') '==' 0) and (P 'check anytime' b); - - - // Following operators cannot been implemented because "duration on" is not implemented yet in the compiler. - - // Checking that the duration of a condition at the end of a time period is lower or higher than a threshold - //Operator [ Boolean ] Periods P 'check duration' Boolean b '<' Real d - // = 'check' (('duration' b 'on' P) '<_real' d) 'over' P; - //Operator [ Boolean ] Periods P 'check duration' Boolean b '<=' Real d - // = 'check' (('duration' b 'on' P) '<=_real' d) 'over' P; - //Operator [ Boolean ] Periods P 'check duration' Boolean b '>' Real d - // = 'check' (('duration' b 'on' P) '>_real' d) 'over' P; - //Operator [ Boolean ] Periods P 'check duration' Boolean b '>=' Real d - // = 'check' (('duration' b 'on' P) '>=_real' d) 'over' P; - - /////////////////////////////////////////////////////////////////////////////// - // Finally, the SRI model - - // Temperature requirements - // NL : "La température du SRI doit être maintenue entre 16°C et 30°C." - // SNL: "En fonctionnement normal, le système SRI doit avoir une température entre 16°C et 30°C." - Boolean normal_operation is external; - Real T is external; - Boolean T_in_range is ((T >= 16) and (T <= 30)); //remark: not done yet but units should be specified - Boolean R1_T is ('during' normal_operation) 'ensure' T_in_range ; - - // NL : "Si la température dépasse ces limites, elle doit être revenue dans l'intervalle au bout d'une minute." - // SNL : "Lorsque le système SRI a une température qui dépasse les limites du fonctionnement normal, - // le système SRI doit avoir une température à nouveau dans l'intervalle autorisé en fonctionnement normal - // au bout d'une minute." - Boolean R2_T is ('from' (new Clock (not R1_T)) 'for' 60.0) 'check at end' T_in_range ; //remark: 'implies' could be used instead - Boolean R_T is R1_T and R2_T ; - - // Speed requirements for heat exchangers - // NL : "Afin de limiter les phénomènes d'érosion et de corrosion, la vitesse du fluide dans les échangeurs ne doit pas dépasser 6 m/s." - // SNL1 : "En fonctionnement normal, chaque échangeur de chaleur doit avoir une vitesse de fluide inférieure ou égale à 6m/s" - // SNL2 : "Lorsque l'échangeur a une vitesse de fluide supérieure à 6 m/s, le système SRI doit garantir que la durée cumulée pendant laquelle la vitesse reste supérieure à 6 m/s - // n’excède pas 10 secondes sur les 3600 secondes suivant cet événement." - // SNL3 : "Lorsque l'échangeur a une vitesse de fluide supérieure à 6 m/s, le système SRI doit garantir que le nombre d’occurrences distinctes de dépassement de 6 m/s - // n’excède pas 2 sur les 3600 secondes suivant cet événement." - class Req_speed is { - Real v is external; - Boolean v_too_high is (v > 6.0) ; // m/s - Clock v_too_high_clock is (new Clock v_too_high) ; - Boolean R1_v is ('from' v_too_high_clock 'for' 3600.0) 'check duration' v_too_high '<=_real' 10.0 ; - Boolean R2_v is ('from' v_too_high_clock 'for' 3600.0) 'check count' v_too_high_clock '<=_int' 2 ; - Boolean R_v is R1_v and R2_v ; - }; - Real v1 is external; - Real v2 is external; - Req_speed Req_speed1(v = v1), Req_speed2(v = v2); - Boolean R_speed_all is Req_speed1.R_v and Req_speed2.R_v ; - - // Flow requirements for pumps - // NL : Les pompes du système ne doivent pas caviter. - // SNL : Lorsque une pompe du SRI est en service, le système SRI doit garantir que le débit associée à cette pompe - // est supérieur ou égal à 70 tonnes par heure. - class Req_flow is { - Real flow is external ; - Boolean pump_in_service is external ; - Boolean f_over_fmin is (f >= 700) ; // t/h - Boolean R_f is ('during' pump_in_service) 'ensure' f_over_fmin ; + // NL : "If the temperature exceed these limits, it must return to within the normal operating range within one minute." + // SNL : "When the ICS system's temperature exceeds the normal operating limits, + // the ICS system shall return to within the normal operating range + // within one minute." + Boolean R2_T is ('from' (new Clock (not R1_T)) 'for' 60.0) 'check at end' T_in_range ; //remark: 'implies' could be used instead + Boolean R_T is R1_T and R2_T ; + + // Speed requirements for heat exchangers + // NL : "To limit erosion and corrosion, the fluid velocity in heat exchangers must not exceed 6 m/s." + // SNL1 : "During normal operation, the fluid velocity in each heat exchanger shall be less than or equal to 6 m/s" + // SNL2 : "When the heat exchanger has a fluid velocity greater than 6 m/s, the SRI system shall ensure that the cumulative duration during which the velocity remains above 6 m/s + // does not exceed 10 seconds over the 3600 seconds following this event." + // SNL3 : "When the heat exchanger has a fluid velocity greater than 6 m/s, the SRI system shall ensure that the number of distinct occurrences where the velocity exceeds 6 m/s + // does not exceed 2 during the 3,600 seconds following this event." + class Req_speed is { + Real v is external; + Boolean v_too_high is (v > 6.0) ; // m/s + Clock v_too_high_clock is (new Clock v_too_high) ; + Boolean R1_v is ('from' v_too_high_clock 'for' 3600.0) 'check duration' v_too_high '<=_real' 10.0 ; + Boolean R2_v is ('from' v_too_high_clock 'for' 3600.0) 'check count' v_too_high_clock '<=_int' 2 ; + Boolean R_v is R1_v and R2_v ; + }; + Real v1 is external; + Real v2 is external; + Req_speed Req_speed1(v = v1), Req_speed2(v = v2); + Boolean R_speed_all is Req_speed1.R_v and Req_speed2.R_v ; + + // Flow requirements for pumps + // NL : The system's pumps must not cavitate. + // SNL : When an ICS pump is in operation, the ICS system shall ensure that the flow rate associated with that pump + // is greater than or equal to 70 tonnes per hour. + class Req_flow is { + Real flow is external ; + Boolean pump_in_service is external ; + Boolean f_over_fmin is (f >= 700) ; // t/h + Boolean R_f is ('during' pump_in_service) 'ensure' f_over_fmin ; + }; + Boolean pump_in_service1 is external; + Boolean pump_in_service2 is external; + Boolean pump_in_service3 is external; + Real flow1 is external; + Real flow2 is external; + Real flow3 is external; + Req_flow Req_flow1(pump_in_service=pump_in_service1,flow=flow1); + Req_flow Req_flow2(pump_in_service=pump_in_service2,flow=flow2); + Req_flow Req_flow3(pump_in_service=pump_in_service3,flow=flow3); + Boolean R_flow_all is Req_flow1.R_f and Req_flow2.R_f and Req_flow3.R_f; }; - Boolean pump_in_service1 is external; - Boolean pump_in_service2 is external; - Boolean pump_in_service3 is external; - Real flow1 is external; - Real flow2 is external; - Real flow3 is external; - Req_flow Req_flow1(pump_in_service=pump_in_service1,flow=flow1); - Req_flow Req_flow2(pump_in_service=pump_in_service2,flow=flow2); - Req_flow Req_flow3(pump_in_service=pump_in_service3,flow=flow3); - Boolean R_flow_all is Req_flow1.R_f and Req_flow2.R_f and Req_flow3.R_f; - -}; diff --git a/submodules/test-resources/src/main/resources/testModels/libraries/FORM-L.crml b/submodules/test-resources/src/main/resources/testModels/libraries/FORM-L.crml index c16dcfd9..05b96937 100644 --- a/submodules/test-resources/src/main/resources/testModels/libraries/FORM-L.crml +++ b/submodules/test-resources/src/main/resources/testModels/libraries/FORM-L.crml @@ -1,84 +1,87 @@ -// FORM-L library -// include "ETL.crml" +library FORML is + // Other Libraries dependencies + 'ETL' union -library FORM_L is ETL union { - // Operators to define time periods - // From events occur - Operator [ Periods ] 'from' Clock ev = Periods [ ev, new Clock false ]; - - // After events occur - Operator [ Periods ] 'after' Clock ev = Periods ] ev, new Clock false ]; - - // Before events occur - Operator [ Periods ] 'before' Clock ev = Periods [ new Clock false, ev [; - - // Until events occur - Operator [ Periods ] 'until' Clock ev = Periods [ new Clock false, ev ]; - - // While a Boolean is true - Operator [ Periods ] 'during' Boolean b = Periods [ Clock b, Clock not b ]; - - // After events occur and before events occur - Operator [ Periods ] 'after' Clock ev1 'before' Clock ev2 = Periods ] ev1, ev2 [; - - // After events occur and until events occur - Operator [ Periods ] 'after' Clock ev1 'until' Clock ev2 = Periods ] ev1, ev2 ]; - - // After events occur and for an elapsed time - Operator [ Periods ] 'after' Clock ev 'for' Real d = Periods ] ev, ev + d ]; - - // After events occur and within an elapsed time - Operator [ Periods ] 'after' Clock ev 'within' Real d = Periods ] ev, ev + d [; - - // From events occur and before events occur - Operator [ Periods ] 'from' Clock ev1 'before' Clock ev2 = Periods [ ev1, ev2 [; - - // From events occur and until events occur - Operator [ Periods ] 'from' Clock ev1 'until' Clock ev2 = Periods [ ev1, ev2 ]; - - // From events occur and for an elapsed time - Operator [ Periods ] 'from' Clock ev 'for' Real d = Periods [ ev, ev + d ]; - - // From events occur and within an elapsed time - Operator [ Periods ] 'from' Clock ev 'within' Real d = Periods [ ev, ev + d [; - - // When events occur - Operator [ Periods ] 'when' Clock ev = Periods [ ev, ev ]; + // FORML Operators + { + // Operators to define time periods + // From events occur + Operator [ Periods ] 'from' Clock ev = Periods [ ev, new Clock false ]; + + // After events occur + Operator [ Periods ] 'after' Clock ev = Periods ] ev, new Clock false ]; + + // Before events occur + Operator [ Periods ] 'before' Clock ev = Periods [ new Clock false, ev [; + + // Until events occur + Operator [ Periods ] 'until' Clock ev = Periods [ new Clock false, ev ]; + + // While a Boolean is true + Operator [ Periods ] 'during' Boolean b = Periods [ Clock b, Clock not b ]; + + // After events occur and before events occur + Operator [ Periods ] 'after' Clock ev1 'before' Clock ev2 = Periods ] ev1, ev2 [; + + // After events occur and until events occur + Operator [ Periods ] 'after' Clock ev1 'until' Clock ev2 = Periods ] ev1, ev2 ]; + + // After events occur and for an elapsed time + Operator [ Periods ] 'after' Clock ev 'for' Real d = Periods ] ev, ev + d ]; + + // After events occur and within an elapsed time + Operator [ Periods ] 'after' Clock ev 'within' Real d = Periods ] ev, ev + d [; + + // From events occur and before events occur + Operator [ Periods ] 'from' Clock ev1 'before' Clock ev2 = Periods [ ev1, ev2 [; + + // From events occur and until events occur + Operator [ Periods ] 'from' Clock ev1 'until' Clock ev2 = Periods [ ev1, ev2 ]; + + // From events occur and for an elapsed time + Operator [ Periods ] 'from' Clock ev 'for' Real d = Periods [ ev, ev + d ]; + + // From events occur and within an elapsed time + Operator [ Periods ] 'from' Clock ev 'within' Real d = Periods [ ev, ev + d [; + + // When events occur + Operator [ Periods ] 'when' Clock ev = Periods [ ev, ev ]; - // Operators for the evaluation of requirements - - // 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; - - // Checking that a requirement is satisfied at any time instant of a time period - Operator [ Boolean ] Periods P 'check anytime' Boolean b = 'check' varying2 'id' b 'over' P; - - // Ensuring that a requirement is satisfied all along a time period - Operator [ Boolean ] Periods P 'ensure' Boolean b - = ('check' ('count' (b 'becomes true') == 0) 'over' P) and (P 'check anytime' b); - - // Checking that the number of event occurrences at the end of a time period is lower or higher than a threshold - Operator [ Boolean ] Periods P 'check count' Clock E '<' constant Integer n - = 'check'(('count' E 'inside' P) increasing1 '<' n) 'over' P; - Operator [ Boolean ] Periods P 'check count' Clock E '<=' constant Integer n - = 'check'(('count' E 'inside' P) increasing1 '<=' n) 'over' P; - Operator [ Boolean ] Periods P 'check count' Clock E '>' constant Integer n - = 'check'(('count' E 'inside' P) increasing1 '>' n) 'over' P; - Operator [ Boolean ] Periods P 'check count' Clock E '>=' constant Integer n - = 'check'(('count' E 'inside' P) increasing1 '>=' n) 'over' P; - Operator [ Boolean ] Periods P 'check count' Clock E '==' constant Integer n - = 'check'(('count' E 'inside' P) increasing1 '==' n) 'over' P; - Operator [ Boolean ] Periods P 'check count' Clock E '<>' constant Integer n - = 'check'(('count' E 'inside' P) increasing1 '<>' n) 'over' P; + // Operators for the evaluation of requirements + + // 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; + + // Checking that a requirement is satisfied at any time instant of a time period + Operator [ Boolean ] Periods P 'check anytime' Boolean b = 'check' varying2 'id' b 'over' P; + + // Ensuring that a requirement is satisfied all along a time period + Operator [ Boolean ] Periods P 'ensure' Boolean b + = ('check' ('count' (b 'becomes true') == 0) 'over' P) and (P 'check anytime' b); + + // Checking that the number of event occurrences at the end of a time period is lower or higher than a threshold + Operator [ Boolean ] Periods P 'check count' Clock E '<' constant Integer n + = 'check'(('count' E 'inside' P) increasing1 '<' n) 'over' P; + Operator [ Boolean ] Periods P 'check count' Clock E '<=' constant Integer n + = 'check'(('count' E 'inside' P) increasing1 '<=' n) 'over' P; + Operator [ Boolean ] Periods P 'check count' Clock E '>' constant Integer n + = 'check'(('count' E 'inside' P) increasing1 '>' n) 'over' P; + Operator [ Boolean ] Periods P 'check count' Clock E '>=' constant Integer n + = 'check'(('count' E 'inside' P) increasing1 '>=' n) 'over' P; + Operator [ Boolean ] Periods P 'check count' Clock E '==' constant Integer n + = 'check'(('count' E 'inside' P) increasing1 '==' n) 'over' P; + Operator [ Boolean ] Periods P 'check count' Clock E '<>' constant Integer n + = 'check'(('count' E 'inside' P) increasing1 '<>' n) 'over' P; - // Checking that the duration of a condition at the end of a time period is lower or higher than a threshold - Operator [ Boolean ] Periods P 'check duration' Boolean b '<' constant Real d - = 'check' (('duration' b 'on' P) increasing2 '<' d) 'over' P; - Operator [ Boolean ] Periods P 'check duration' Boolean b '<=' constant Real d - = 'check' (('duration' b 'on' P) increasing2 '<=' d) 'over' P; - Operator [ Boolean ] Periods P 'check duration' Boolean b '>' constant Real d - = 'check' (('duration' b 'on' P) increasing2 '>' d) 'over' P; - Operator [ Boolean ] Periods P 'check duration' Boolean b '>=' constant Real d - = 'check' (('duration' b 'on' P) increasing2 '>=' d) 'over' P; -}; + // Checking that the duration of a condition at the end of a time period is lower or higher than a threshold + Operator [ Boolean ] Periods P 'check duration' Boolean b '<' constant Real d + = 'check' (('duration' b 'on' P) increasing2 '<' d) 'over' P; + Operator [ Boolean ] Periods P 'check duration' Boolean b '<=' constant Real d + = 'check' (('duration' b 'on' P) increasing2 '<=' d) 'over' P; + Operator [ Boolean ] Periods P 'check duration' Boolean b '>' constant Real d + = 'check' (('duration' b 'on' P) increasing2 '>' d) 'over' P; + Operator [ Boolean ] Periods P 'check duration' Boolean b '>=' constant Real d + = 'check' (('duration' b 'on' P) increasing2 '>=' d) 'over' P; + } +;