Skip to content

add reference models and results for testing SRI example #6

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
audrey-jardin merged 2 commits into from
Oct 20, 2025
Merged

add reference models and results for testing SRI example #6

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
5c51ede
add reference models and results for testing SRI example
audrey-jardin Oct 14, 2025
d4c9679
update icons for Units package
audrey-jardin Oct 20, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion resources/modelica_libraries/CRML.mo
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4325,7 +4325,9 @@ which is only valid in the rotor-fixed coordinate system.
end xSI;
annotation(
Documentation(info = "<html>
</html>"));
</html>"),
Diagram(graphics),
Icon(graphics = {Rectangle(lineColor = {200, 200, 200}, fillColor = {248, 248, 248}, fillPattern = FillPattern.HorizontalCylinder, extent = {{-100, -100}, {100, 100}}, radius = 25), Text(extent = {{-64, 36}, {58, -32}}, textString = "Units")}));
end Units;

package ETL
Expand Down
Binary file added src/test/resources/refResults/use-cases/ics_educational/Reqs_sri_CRML_verif_res.mat
View file
Open in desktop
Binary file not shown.
220 changes: 220 additions & 0 deletions src/test/resources/testModels/use-cases/ics_educational/Reqs_sri_CRML.crml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,220 @@
// SRI requirement model
model Reqs_sri_CRML 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 );

///////////////////////////////////////////////////////////////////////////////
// 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;

// 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

// Always ??? Not sure operator without parameter is admitted.
Operator [ Periods ] 'always' = 'during' true;

// Temperature requirements
Real T is external;

// 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 T_in_range is ((T >= 16) and (T <= 30)); //remark: not done yet but units should be specified
Boolean R1_T is ('always') '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
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
class Req_flow is {
Real f 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_flow1(pump_in_service=pump_in_service2,flow=flow2);
Req_flow Req_flow1(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;

};
Loading
Loading