Skip to content

Commit

Permalink
Merge pull request #75 from audrey-jardin/main
Browse files Browse the repository at this point in the history
Fix for CRML.mo, some reference test results and traffic-light example
  • Loading branch information
lenaRB committed Apr 22, 2024
2 parents 68c4687 + 0e6ab40 commit 79b9de0
Show file tree
Hide file tree
Showing 36 changed files with 353 additions and 193 deletions.
14 changes: 13 additions & 1 deletion resources/crml_tutorial/traffic_light/Spec_simplified.crml
Original file line number Diff line number Diff line change
Expand Up @@ -62,12 +62,24 @@ model Spec is {
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);

//Option 2:
Operator [ Boolean ] Periods P 'ensure' Boolean b
= ('check' ('count' (b 'becomes true') == 0) 'over' P) and (P 'check anytime' b);
= (Periods P 'check count' (b 'becomes true') '==' 0) 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);
Expand Down
65 changes: 48 additions & 17 deletions resources/modelica_libraries/CRML.mo
Original file line number Diff line number Diff line change
Expand Up @@ -4,12 +4,17 @@
class Overview "Overview of CRML"

annotation (Documentation(info="<html>
<p>CRML(Common Requirement Modeling Language) is a language for the simulation of temporal requirements on cyber-physical systems.</p>
<p>CRML(Common Requirement Modeling Language) is a language for the simulation of temporal requirements on cyber-physical systems.</p>
<p>This library is a Modelica implementation of CRML.</p>
<p>For more information, please consult the following references:</p>
<p><span style=\"font-family: Wingdings; color: #fe5815;\">&sect; </span></span><span style=\"font-family: Arial;\">Bouskela D., Nguyen T. and Jardin A. (2017), &ldquo;Toward a Rigorous Approach for Verifying Cyber-Physical Systems Against Requirements,&rdquo; Canadian J. of Electrical and Computer Engineering, Vol. 40-2, pp. 66-73. </p>
<ul>
<li><span style=\"font-family: Arial;\">Bouskela D., Nguyen T. and Jardin A. (2017), &ldquo;Toward a Rigorous Approach for Verifying Cyber-Physical Systems Against Requirements,&rdquo; Canadian J. of Electrical and Computer Engineering, Vol. 40-2, pp. 66-73. </span></li>
<li><span style=\"font-family: Arial;\">Bouskela D., Buffoni L., Jardin A., Molnar V., Pop A. and Zavada A. (2023), &quot;The Common Requirement Modeling Language&quot;, Proceedings of the 15th International Modelica Conference 2023, Aachen, October 9-11.</span></li>
</ul>
<p>Regarding the RandomFailure block in package Blocks.Events, please consult the following reference:</p>
<p><span style=\"font-family: Wingdings; color: #fe5815;\">&sect; </span></span><span style=\"font-family: Arial;\">Bouissou M. and Buffoni L. (2020), &ldquo;Generic Method to Transform a Modelica Simulation into a Dynamic Reliability Model,&rdquo; IMdR, Institut pour la ma&icirc;trise des Risques, 22e Congr&egrave;s de Ma&icirc;trise des Risques et S&ucirc;ret&eacute; de Fonctionnement. </p>
<ul>
<li><span style=\"font-family: Arial;\">Bouissou M. and Buffoni L. (2020), &ldquo;Generic Method to Transform a Modelica Simulation into a Dynamic Reliability Model,&rdquo; IMdR, Institut pour la ma&icirc;trise des Risques, 22e Congr&egrave;s de Ma&icirc;trise des Risques et S&ucirc;ret&eacute; de Fonctionnement. </span></li>
</ul>
</html>"), Icon(graphics={
Ellipse(
lineColor={75,138,73},
Expand All @@ -31,7 +36,7 @@

end Overview;

class ReqSysProLicense "License"
class CrmlLicense "License"

annotation (Documentation(info="<html>
<p><b><span style=\"font-size: 12pt; color: #008000;\">The CRML License </span></b></p>
Expand All @@ -56,7 +61,7 @@
fillPattern=FillPattern.Solid,
extent={{-12.5,-12.5},{12.5,12.5}})}));

end ReqSysProLicense;
end CrmlLicense;

package ReleaseNotes "Release notes"

Expand Down Expand Up @@ -109,6 +114,38 @@
fillPattern=FillPattern.Solid,
extent={{-12.5,-12.5},{12.5,12.5}})}));
end Version_0_2;

class Version_0_3 "Version 0.3"

annotation (DocumentationClass=true, Documentation(info="<html>
<p><b><span style=\"font-size: 10pt; color: #008000;\">Version 0.3 (in progress, 2024)</span></b></p>
<p>This is the third beta release of the library. </p>
<p>Minor updates:</p>
<ul>
<li>Package &quot;Blocks.Events&quot;: declaration of x as public (and not protected) for setting start value</li>
<li>Package &quot;Examples&quot;: deletion of dependency with the Modelica_StateGraph2 library in &quot;traffic light&quot; example</li>
</ul>
<p>Major updates:</p>
<p>- </p>
</html>"),Icon(graphics={
Ellipse(
lineColor={75,138,73},
fillColor={75,138,73},
pattern=LinePattern.None,
fillPattern=FillPattern.Solid,
extent={{-100,-100},{100,100}}),
Polygon(origin={-10.167,-15},
fillColor={255,255,255},
pattern=LinePattern.None,
fillPattern=FillPattern.Solid,
points={{-15.833,20.0},{-15.833,30.0},{14.167,40.0},{24.167,20.0},{4.167,-30.0},{14.167,-30.0},{24.167,-30.0},{24.167,-40.0},{-5.833,-50.0},{-15.833,-30.0},{4.167,20.0},{-5.833,20.0}},
smooth=Smooth.Bezier),
Ellipse(origin={1.5,56.5},
fillColor={255,255,255},
pattern=LinePattern.None,
fillPattern=FillPattern.Solid,
extent={{-12.5,-12.5},{12.5,12.5}})}));
end Version_0_3;
annotation (Icon(graphics={
Polygon(
points={{-80,-100},{-80,100},{0,100},{0,20},{80,20},{80,-100},{-80,-100}},
Expand Down Expand Up @@ -164,16 +201,9 @@
fillColor={241,241,241},
fillPattern=FillPattern.Solid)}), Documentation(info="<html>
<p><b><span style=\"font-size: 12pt; color: #008000;\">Contacts </span></b></p>
<dd>Daniel Bouskela</dd>
<dd>Audrey Jardin</dd>
<dd>Yulu Dong<br></dd>
<dd>EDF Lab - PRISME</dd>
<dd>6, quai Watier</dd>
<dd>F-78401 Chatou Cedex</dd>
<dd>France<br></dd>
<dd>email: <a href=\"mailto:daniel.bouskela@edf.fr\">daniel.bouskela@edf.fr</a></dd>
<dd>email: <a href=\"mailto:audrey.jardin@edf.fr\">audrey.jardin@edf.fr</a></dd>
<dd>email: <a href=\"mailto:yulu.dong@edf.fr\">yulu.dong@edf.fr</a><br></dd>
<p style=\"margin-left: 30px;\">Daniel Bouskela</p><p style=\"margin-left: 30px;\">Audrey Jardin</p><p style=\"margin-left: 30px;\">Yulu Dong</p>
<p style=\"margin-left: 30px;\">EDF Lab - PRISME</p><p style=\"margin-left: 30px;\">6, quai Watier</p><p style=\"margin-left: 30px;\">F-78401 Chatou Cedex</p><p style=\"margin-left: 30px;\">France</p>
<p style=\"margin-left: 30px;\"><br>email: <a href=\"mailto:audrey.jardin@edf.fr\">audrey.jardin@edf.fr</a></p>
</html>"));
end Contacts;
annotation (Icon(graphics={
Expand Down Expand Up @@ -3793,14 +3823,15 @@ The usage is demonstrated, e.g., in example
block Event4ToEvent
import CRML.ETL.Types.Boolean4;

protected
Boolean x(start=false, fixed=true) = (u == Boolean4.true4);
// protected
Boolean x(start=false, fixed=true) = (u == Boolean4.true4);

public
ETL.Connectors.Boolean4Input u
annotation (Placement(transformation(extent={{-120,-10},{-100,10}})));
ETL.Connectors.BooleanOutput y(start=false, fixed=true)
annotation (Placement(transformation(extent={{100,-10},{120,10}})));

equation

y = edge(x);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -23,5 +23,7 @@ equation
connect(b1, not4_1.u)
annotation (Line(points={{-110,0},{-89,0}}, color={0,0,0}));
annotation (Icon(coordinateSystem(preserveAspectRatio=false)), Diagram(
coordinateSystem(preserveAspectRatio=false)));
coordinateSystem(preserveAspectRatio=false)),
Documentation(info="<html>
</html>"));
end BecomesFalse;
Original file line number Diff line number Diff line change
@@ -1,16 +1,20 @@
within CRML_test.ETL.BecomesFalse;
model BecomesFalse_externals
CRML.Blocks.Events.EventPeriodic boolean4Constant1(period=3, startTime=2)
CRML.Blocks.Events.EventPeriodic eventPeriodic_1(period=3, startTime=2)
annotation (Placement(transformation(extent={{-60,-10},{-40,10}})));
CRML.ETL.Connectors.Boolean4Output b1
annotation (Placement(transformation(extent={{100,-10},{120,10}})));
CRML.Blocks.Logical4.BooleanToBoolean4 booleanToBoolean4_1
annotation (Placement(transformation(extent={{-4,-4},{4,4}})));
CRML.Blocks.Events.ShowEvent showEvent_eventPeriodic_b1
annotation (Placement(transformation(extent={{-20,-44},{-12,-36}})));
equation
connect(boolean4Constant1.y, booleanToBoolean4_1.u)
connect(eventPeriodic_1.y, booleanToBoolean4_1.u)
annotation (Line(points={{-39,0},{-4.4,0}}, color={217,67,180}));
connect(booleanToBoolean4_1.y, b1)
annotation (Line(points={{4.4,0},{110,0}}, color={162,29,33}));
connect(eventPeriodic_1.y, showEvent_eventPeriodic_b1.u) annotation (Line(
points={{-39,0},{-28,0},{-28,-40},{-20.4,-40}}, color={217,67,180}));
annotation (Icon(coordinateSystem(preserveAspectRatio=false)), Diagram(
coordinateSystem(preserveAspectRatio=false)));
end BecomesFalse_externals;
Original file line number Diff line number Diff line change
@@ -1,15 +1,15 @@
within CRML_test.ETL.BecomesFalse;
model BecomesFalse_verif
extends BecomesFalse;
extends BecomesFalse(event4ToEvent(x(start=true)));
BecomesFalse_externals externals
annotation (Placement(transformation(extent={{-200,0},{-140,60}})));
CRML.Blocks.Events.ShowEvent show_c_b1_becomes_false
annotation (Placement(transformation(extent={{52,-44},{60,-36}})));
CRML.Blocks.Events.ShowEvent showEvent_c_b1_becomes_false
annotation (Placement(transformation(extent={{60,-74},{68,-66}})));
equation
// Bindings
b1 = externals.b1;
connect(show_c_b1_becomes_false.u, event4ToEvent.y) annotation (Line(points={{
51.6,-40},{-20,-40},{-20,0},{-45.6,0}}, color={217,67,180}));
connect(showEvent_c_b1_becomes_false.u, event4ToEvent.y) annotation (Line(
points={{59.6,-70},{-20,-70},{-20,0},{-45.6,0}}, color={217,67,180}));
annotation (Placement(transformation(extent={{0,-20},{60,40}})),
Icon(coordinateSystem(preserveAspectRatio=false,
extent={{-200,-100},{100,100}},
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ within CRML_test.ETL.BecomesFalse_no_ext;
model BecomesFalse_no_ext
CRML.Blocks.Events.ClockEvent c1
annotation (Placement(transformation(extent={{24,44},{36,56}})));
CRML.Blocks.Events.Event4ToEvent event4ToEvent
CRML.Blocks.Events.Event4ToEvent event4ToEvent(x(start=true))
annotation (Placement(transformation(extent={{-4,46},{4,54}})));
CRML.Blocks.Logical.BooleanTable b1(
y0=false,
Expand All @@ -15,7 +15,7 @@ model BecomesFalse_no_ext
annotation (Placement(transformation(extent={{56,32},{64,40}})));
CRML.Blocks.Events.ClockEvent c2
annotation (Placement(transformation(extent={{24,4},{36,16}})));
CRML.Blocks.Events.Event4ToEvent event4ToEvent1
CRML.Blocks.Events.Event4ToEvent event4ToEvent1(x(start=true))
annotation (Placement(transformation(extent={{-4,6},{4,14}})));
CRML.Blocks.Logical.BooleanConstant b2
annotation (Placement(transformation(extent={{-80,0},{-60,20}})));
Expand All @@ -25,7 +25,7 @@ model BecomesFalse_no_ext
annotation (Placement(transformation(extent={{56,-8},{64,0}})));
CRML.Blocks.Events.ClockEvent c3
annotation (Placement(transformation(extent={{24,-36},{36,-24}})));
CRML.Blocks.Events.Event4ToEvent event4ToEvent2
CRML.Blocks.Events.Event4ToEvent event4ToEvent2(x(start=true))
annotation (Placement(transformation(extent={{-4,-34},{4,-26}})));
CRML.Blocks.Logical.BooleanConstant b3(K=false)
annotation (Placement(transformation(extent={{-80,-40},{-60,-20}})));
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -6,11 +6,15 @@ model BecomesTrue_externals
annotation (Placement(transformation(extent={{100,-10},{120,10}})));
CRML.Blocks.Logical4.BooleanToBoolean4 booleanToBoolean4_1
annotation (Placement(transformation(extent={{-4,-4},{4,4}})));
CRML.Blocks.Events.ShowEvent showEvent_eventPeriodic_b1
annotation (Placement(transformation(extent={{-20,-44},{-12,-36}})));
equation
connect(boolean4Constant1.y, booleanToBoolean4_1.u)
annotation (Line(points={{-39,0},{-4.4,0}}, color={217,67,180}));
connect(booleanToBoolean4_1.y, b1)
annotation (Line(points={{4.4,0},{110,0}}, color={162,29,33}));
connect(showEvent_eventPeriodic_b1.u, boolean4Constant1.y) annotation (Line(
points={{-20.4,-40},{-30,-40},{-30,0},{-39,0}}, color={217,67,180}));
annotation (Icon(coordinateSystem(preserveAspectRatio=false)), Diagram(
coordinateSystem(preserveAspectRatio=false)));
end BecomesTrue_externals;
Original file line number Diff line number Diff line change
Expand Up @@ -4,28 +4,28 @@ partial model BecomesTrueInside
annotation (Placement(transformation(extent={{-120,10},{-100,-10}})));
Utilities.ClockConnector c_b1_becomes_true_inside_p1
annotation (Placement(transformation(extent={{100,10},{120,-10}})));
CRML.Blocks.Events.Event4ToEvent event4ToEvent
annotation (Placement(transformation(extent={{-54,-4},{-46,4}})));
replaceable ETL.Inside.Inside inside
annotation (Placement(transformation(extent={{4,-50},{24,-30}})));
CRML.Blocks.Events.Event4ToEvent event4ToEvent_1
annotation (Placement(transformation(extent={{-64,-4},{-56,4}})));
replaceable Inside.Inside2 inside
annotation (Placement(transformation(extent={{2,-50},{22,-30}})));
Utilities.Boolean4Connector b2
annotation (Placement(transformation(extent={{-10,10},{10,-10}},
rotation=-90,
origin={-110,-60})));
CRML.Blocks.Events.Event4ToEvent event4ToEvent1
annotation (Placement(transformation(extent={{-66,-64},{-58,-56}})));
CRML.Blocks.Events.Event4ToEvent event4ToEvent_2
annotation (Placement(transformation(extent={{-64,-64},{-56,-56}})));
equation
connect(b1, event4ToEvent.u)
annotation (Line(points={{-110,0},{-54.4,0}}, color={0,0,0}));
connect(b2, event4ToEvent1.u)
annotation (Line(points={{-110,-60},{-66.4,-60}}, color={0,0,0}));
connect(event4ToEvent1.y, inside.b1) annotation (Line(points={{-57.6,-60},{
-22,-60},{-22,-43},{3,-43}}, color={217,67,180}));
connect(event4ToEvent.y, inside.b2) annotation (Line(points={{-45.6,0},{-22,0},
{-22,-37},{3,-37}}, color={217,67,180}));
connect(b1, event4ToEvent_1.u)
annotation (Line(points={{-110,0},{-64.4,0}}, color={0,0,0}));
connect(b2, event4ToEvent_2.u)
annotation (Line(points={{-110,-60},{-64.4,-60}}, color={0,0,0}));
connect(event4ToEvent_2.y, inside.b1) annotation (Line(points={{-55.6,-60},{
-22,-60},{-22,-43},{1,-43}}, color={217,67,180}));
connect(event4ToEvent_1.y, inside.b2) annotation (Line(points={{-55.6,0},{-22,
0},{-22,-37},{1,-37}}, color={217,67,180}));
connect(inside.c_filtered_ticks_of_c1_inside_p1, c_b1_becomes_true_inside_p1)
annotation (Line(
points={{25,-40},{64,-40},{64,0},{110,0}},
points={{23,-40},{64,-40},{64,0},{110,0}},
color={175,175,175},
pattern=LinePattern.Dot,
thickness=0.5));
Expand Down
Original file line number Diff line number Diff line change
@@ -1,16 +1,34 @@
within CRML_test.ETL.BecomesTrueInside;
model BecomesTrueInside_externals
CRML.Blocks.Events.EventPeriodic boolean4Constant1(period=3, startTime=2)
annotation (Placement(transformation(extent={{-60,-10},{-40,10}})));
CRML.ETL.Connectors.Boolean4Output b1
annotation (Placement(transformation(extent={{100,-10},{120,10}})));
annotation (Placement(transformation(extent={{100,30},{120,50}})));
CRML.Blocks.Logical4.BooleanToBoolean4 booleanToBoolean4_1
annotation (Placement(transformation(extent={{-4,-4},{4,4}})));
annotation (Placement(transformation(extent={{-4,36},{4,44}})));
public
CRML.Blocks.Logical.BooleanTable booleanTable_b1(
y0=false,
option_width=false,
instant={2,5,7.5,9})
annotation (Placement(transformation(extent={{-60,30},{-40,50}})));
CRML.Blocks.Logical.BooleanTable booleanTable_b2(
y0=false,
option_width=false,
instant={3.5,4.5})
annotation (Placement(transformation(extent={{-60,-50},{-40,-30}})));
CRML.Blocks.Logical4.BooleanToBoolean4 booleanToBoolean4_2
annotation (Placement(transformation(extent={{-4,-44},{4,-36}})));
CRML.ETL.Connectors.Boolean4Output b2
annotation (Placement(transformation(extent={{100,-50},{120,-30}})));
equation
connect(boolean4Constant1.y, booleanToBoolean4_1.u)
annotation (Line(points={{-39,0},{-4.4,0}}, color={217,67,180}));
connect(booleanToBoolean4_1.y, b1)
annotation (Line(points={{4.4,0},{110,0}}, color={162,29,33}));
annotation (Line(points={{4.4,40},{110,40}},
color={162,29,33}));
connect(booleanTable_b1.y, booleanToBoolean4_1.u)
annotation (Line(points={{-39,40},{-4.4,40}}, color={217,67,180}));
connect(booleanTable_b2.y, booleanToBoolean4_2.u)
annotation (Line(points={{-39,-40},{-4.4,-40}}, color={217,67,180}));
connect(booleanToBoolean4_2.y, b2)
annotation (Line(points={{4.4,-40},{110,-40}}, color={162,29,33}));
annotation (Icon(coordinateSystem(preserveAspectRatio=false)), Diagram(
coordinateSystem(preserveAspectRatio=false)));
end BecomesTrueInside_externals;
Loading

0 comments on commit 79b9de0

Please sign in to comment.