Skip to content

Commit

Permalink
Merge pull request #45 from audrey-jardin/main
Browse files Browse the repository at this point in the history
updates of unit examples to test simplified ETL library
  • Loading branch information
lenaRB committed Nov 23, 2023
2 parents 5a7f642 + 6e8a1be commit b659ba1
Show file tree
Hide file tree
Showing 216 changed files with 3,065 additions and 185 deletions.
2 changes: 1 addition & 1 deletion project-run.bat
Original file line number Diff line number Diff line change
Expand Up @@ -2,5 +2,5 @@ REM run this to download the files and compile everything
@echo on

set GRADLE_USER_HOME=.\gradle-dependencies
call gradlew.bat build
call gradlew.bat test
pause
18 changes: 9 additions & 9 deletions resources/crml_tutorial/heated_tank/requirements_tank.crml
Original file line number Diff line number Diff line change
@@ -1,15 +1,15 @@
model requirements_tank is {

class TankModel is {
external Real level ;
external Real temperature;
};
class TankModel is {
Real level is external;
Real temperature is external;
};

TankModel tankm is new TankModel;
TankModel tankm is new TankModel;

Boolean R1 is tankm.level >= 7.5;
Boolean R2 is tankm.level >= 10;
Boolean R3 is R1 and (not R2);
Boolean R4 is tankm.temperature <= 100;
Boolean R1 is tankm.level >= 7.5;
Boolean R2 is tankm.level >= 10;
Boolean R3 is R1 and (not R2);
Boolean R4 is tankm.temperature <= 100;

};
Original file line number Diff line number Diff line change
@@ -1,12 +1,12 @@
within SysCon2018;
within SysCon2018;
model SysCon
parameter Integer n = 2;
CRML.TimeLocators.Continuous.During during_system_inOperation
annotation (Placement(transformation(extent={{-40,80},{-20,100}})));
CRML.Requirements.CheckCountLowerEqual
checkInPCount(threshold=n)
annotation (Placement(transformation(extent={{-40,50},{-20,70}})));
CRML.Blocks.Logical4.And4 and4
CRML.Blocks.Logical4.And4_n and4(N=3)
annotation (Placement(transformation(extent={{70,-10},{90,10}})));
CRML.ETL.Connectors.Boolean4Input system_inOperation
annotation (Placement(transformation(extent={{-120,80},{-100,100}})));
Expand All @@ -26,15 +26,25 @@ model SysCon
annotation (Placement(transformation(extent={{0,-60},{20,-40}})));
CRML.Blocks.Logical4.BooleanToBoolean4 booleanToBoolean4_1
annotation (Placement(transformation(extent={{-14,-84},{-6,-76}})));
CRML.TimeLocators.Continuous.AfterFor afterFor_r4
annotation (Placement(transformation(extent={{30,30},{50,50}})));
CRML.Blocks.Math.Constant T2(k=40)
annotation (Placement(transformation(extent={{-76,-46},{-60,-30}})));
CRML.Blocks.Math.Constant d1(k=900)
annotation (Placement(transformation(extent={{-76,24},{-60,40}})));
Modelica.Blocks.Logical.Less less1
annotation (Placement(transformation(extent={{-40,-40},{-20,-20}})));
CRML.Blocks.Logical4.BooleanToBoolean4 booleanToBoolean4_2
annotation (Placement(transformation(extent={{-12,6},{-4,14}})));
CRML.Blocks.Logical4.Not4 not4_1
annotation (Placement(transformation(extent={{0,0},{20,20}})));
CRML.Requirements.CheckDurationLower checkDurationLower_r4(threshold=60)
annotation (Placement(transformation(extent={{30,0},{50,20}})));
equation
connect(during_system_inOperation.y, checkInPCount.tl)
annotation (Line(points={{-30,80},{-30,70}}, color={0,0,255}));
connect(ensure.y, and4.u2) annotation (Line(points={{21,-80},{64,-80},{64,-8},
{69,-8}}, color={162,29,33}));
connect(during_pump_isStarted.y, ensure.tl)
annotation (Line(points={{10,-60},{10,-70}}, color={0,0,255}));
connect(checkInPCount.y, and4.u1) annotation (Line(points={{-19,60},{64,60},{64,
8},{69,8}}, color={162,29,33}));
connect(system_inOperation, during_system_inOperation.u)
annotation (Line(points={{-110,90},{-41,90}}, color={162,29,33}));
connect(pump_isStarted, checkInPCount.u) annotation (Line(points={{-110,0},{-80,
Expand All @@ -51,6 +61,28 @@ equation
annotation (Line(points={{-19,-80},{-14.4,-80}}, color={255,0,255}));
connect(ensure.u, booleanToBoolean4_1.y)
annotation (Line(points={{-1,-80},{-5.6,-80}}, color={162,29,33}));
connect(less1.u2, T2.y)
annotation (Line(points={{-42,-38},{-59.2,-38}}, color={0,0,127}));
connect(less1.u1, less.u1) annotation (Line(points={{-42,-30},{-52,-30},{-52,
-80},{-42,-80}}, color={0,0,127}));
connect(less1.y, booleanToBoolean4_2.u) annotation (Line(points={{-19,-30},{
-16,-30},{-16,10},{-12.4,10}}, color={255,0,255}));
connect(not4_1.y, checkDurationLower_r4.u)
annotation (Line(points={{21,10},{29,10}}, color={162,29,33}));
connect(afterFor_r4.duration, d1.y)
annotation (Line(points={{29,32},{-59.2,32}}, color={0,0,0}));
connect(checkInPCount.y, and4.u[1]) annotation (Line(points={{-19,60},{66,60},
{66,-0.666667},{69,-0.666667}}, color={162,29,33}));
connect(checkDurationLower_r4.y, and4.u[2]) annotation (Line(points={{51,10},
{66,10},{66,0},{69,0}}, color={162,29,33}));
connect(ensure.y, and4.u[3]) annotation (Line(points={{21,-80},{66,-80},{66,
0.666667},{69,0.666667}}, color={162,29,33}));
connect(booleanToBoolean4_2.y, not4_1.u)
annotation (Line(points={{-3.6,10},{-1,10}}, color={162,29,33}));
connect(checkDurationLower_r4.tl, afterFor_r4.y)
annotation (Line(points={{40,20},{40,30}}, color={0,0,255}));
connect(afterFor_r4.u, checkDurationLower_r4.u) annotation (Line(points={{29,
40},{26,40},{26,10},{29,10}}, color={162,29,33}));
annotation (Icon(coordinateSystem(preserveAspectRatio=false), graphics={
Rectangle(
extent={{-100,100},{100,-100}},
Expand Down Expand Up @@ -78,5 +110,25 @@ equation
Text(
extent={{86,20},{128,12}},
lineColor={28,108,200},
textString="requirement_value")}));
textString="requirement_value"),
Text(
extent={{-80,122},{32,104}},
lineColor={28,108,200},
textString="R1: While the sytem is in operation,
the pump must not be started more than twice.",
horizontalAlignment=TextAlignment.Left),
Text(
extent={{-80,-102},{40,-120}},
lineColor={28,108,200},
horizontalAlignment=TextAlignment.Left,
textString="R3: While the pump is in operation (i.e. started),
its temperature must always stay below 50°C"),
Text(
extent={{0,90},{154,60}},
lineColor={28,108,200},
horizontalAlignment=TextAlignment.Left,
textString="R4: While the system is in operation,
after the pump temperature rises above 40°C,
the temperature should not stay above this value
for a duration of more than 1 mn cumulated over the next 15 mn.")}));
end SysCon;
Original file line number Diff line number Diff line change
@@ -1,20 +1,19 @@
within SysCon2018;
model SysConMain
import ReqSysPro;
SysCon sysCon annotation (Placement(transformation(extent={{-10,0},{10,20}})));
ReqSysPro.Blocks.Logical.BooleanPulse system_inOperation(
CRML.Blocks.Logical.BooleanPulse system_inOperation(
width=3600,
startTime=60,
period=4000)
annotation (Placement(transformation(extent={{-80,40},{-60,60}})));
ReqSysPro.Blocks.Logical.BooleanPulse pump_isStarted1(
CRML.Blocks.Logical.BooleanPulse pump_isStarted1(
width=1140,
period=1200,
startTime=600)
annotation (Placement(transformation(extent={{-80,0},{-60,20}})));
ReqSysPro.Blocks.Math.Constant pump_temperature(k=40)
CRML.Blocks.Math.Constant pump_temperature(k=40)
annotation (Placement(transformation(extent={{-80,-40},{-60,-20}})));
ReqSysPro.PropertyStatus.ShowPropertyStatus showValue
CRML.Blocks.Logical4.ShowBoolean4 showValue
annotation (Placement(transformation(extent={{40,0},{60,20}})));
Modelica.Blocks.Logical.And pump_isStarted
annotation (Placement(transformation(extent={{-42,6},{-34,14}})));
Expand All @@ -26,7 +25,8 @@ equation
connect(pump_temperature.y, sysCon.pump_temperature) annotation (Line(points={{-59,-30},
{-26,-30},{-26,2},{-11,2}}, color={0,0,0}));
connect(sysCon.requirement_value, showValue.u)
annotation (Line(points={{11,10},{39,10}}, color={162,29,33}));
annotation (Line(points={{11,10},{39.5,10}},
color={162,29,33}));
connect(pump_isStarted1.y, pump_isStarted.u2) annotation (Line(points={{-59,
10},{-50,10},{-50,6.8},{-42.8,6.8}}, color={255,0,128}));
connect(system_inOperation.y, pump_isStarted.u1) annotation (Line(points={{
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,57 @@
within SysCon2018;
model SysConMain1
SysCon sysCon annotation (Placement(transformation(extent={{-10,0},{10,20}})));
CRML.Blocks.Logical.BooleanPulse system_inOperation(
width=3600,
startTime=60,
period=4000)
annotation (Placement(transformation(extent={{-80,40},{-60,60}})));
Modelica.Blocks.Sources.Sine
pump_temperature(
freqHz=1/600,
offset=39,
amplitude=1.1)
annotation (Placement(transformation(extent={{-80,-40},{-60,-20}})));
CRML.Blocks.Logical.BooleanPulse pump_isStarted1(
width=1140,
period=1200,
startTime=600)
annotation (Placement(transformation(extent={{-80,0},{-60,20}})));
CRML.Blocks.Logical4.ShowBoolean4 showValue
annotation (Placement(transformation(extent={{40,0},{60,20}})));
Modelica.Blocks.Logical.And pump_isStarted
annotation (Placement(transformation(extent={{-42,6},{-34,14}})));
CRML.Blocks.Logical4.BooleanToBoolean4 booleanToBoolean4_1
annotation (Placement(transformation(extent={{-28,16},{-20,24}})));
CRML.Blocks.Logical4.BooleanToBoolean4 booleanToBoolean4_2
annotation (Placement(transformation(extent={{-28,6},{-20,14}})));
equation
connect(pump_temperature.y, sysCon.pump_temperature) annotation (Line(points={{-59,-30},
{-26,-30},{-26,2},{-11,2}}, color={0,0,0}));
connect(sysCon.requirement_value, showValue.u)
annotation (Line(points={{11,10},{39.5,10}},
color={162,29,33}));
connect(pump_isStarted1.y, pump_isStarted.u2) annotation (Line(points={{-59,
10},{-50,10},{-50,6.8},{-42.8,6.8}}, color={255,0,128}));
connect(system_inOperation.y, pump_isStarted.u1) annotation (Line(points={{
-59,50},{-46,50},{-46,10},{-42.8,10}}, color={255,0,128}));
connect(system_inOperation.y, booleanToBoolean4_1.u) annotation (Line(points=
{{-59,50},{-40,50},{-40,20},{-28.4,20}}, color={217,67,180}));
connect(sysCon.system_inOperation, booleanToBoolean4_1.y) annotation (Line(
points={{-11,19},{-11,18.5},{-19.6,18.5},{-19.6,20}}, color={162,29,33}));
connect(pump_isStarted.y, booleanToBoolean4_2.u)
annotation (Line(points={{-33.6,10},{-28.4,10}}, color={255,0,255}));
connect(sysCon.pump_isStarted, booleanToBoolean4_2.y)
annotation (Line(points={{-11,10},{-19.6,10}}, color={162,29,33}));
annotation (Icon(coordinateSystem(preserveAspectRatio=false), graphics={
Ellipse(lineColor = {75,138,73},
fillColor={255,255,255},
fillPattern = FillPattern.Solid,
extent={{-100,-100},{100,100}}),
Polygon(lineColor = {0,0,255},
fillColor = {75,138,73},
pattern = LinePattern.None,
fillPattern = FillPattern.Solid,
points={{-36,60},{64,0},{-36,-60},{-36,60}})}), Diagram(
coordinateSystem(preserveAspectRatio=false)));
end SysConMain1;
Original file line number Diff line number Diff line change
@@ -1,2 +1,3 @@
SysConMain
SysConMain1
SysCon
11 changes: 7 additions & 4 deletions resources/crml_tutorial/traffic_light/Spec_simplified.crml
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ model Spec is {

// Filter clock ticks inside a time period
Operator [ Clock ] Clock C 'inside' Period P
= C filter ((tick >= (P start)) and (tick <= (P end)));
= C filter ((tick C >= (P start)) and (tick C <= (P end)));

// Operators on clocks
// Count the occurrences of events inside a time period
Expand Down Expand Up @@ -82,18 +82,21 @@ model Spec is {

// Definition of requirements
// req1: "After green, next step is yellow"
Requirement req1 is
// 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
// 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
// Requirement req3 is
Boolean req3 is
'after' (green 'becomes true' + 30) 'for' 0.2
'check at end' yellow;
};
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
within CRML_test.ETL.BecomesTrue;
partial model BecomesTrue
Utilities.Boolean4Connector b1
annotation (Placement(transformation(extent={{-120,10},{-100,-10}})));
Utilities.ClockConnector c_b1_becomes_true
annotation (Placement(transformation(extent={{100,10},{120,-10}})));
CRML.Blocks.Events.ClockEvent clockEvent
annotation (Placement(transformation(extent={{-6,-6},{6,6}})));
CRML.Blocks.Events.Event4ToEvent event4ToEvent
annotation (Placement(transformation(extent={{-54,-4},{-46,4}})));
equation
connect(clockEvent.y, c_b1_becomes_true) annotation (Line(
points={{6.6,0},{110,0}},
color={175,175,175},
pattern=LinePattern.Dot,
thickness=0.5));
connect(b1, event4ToEvent.u)
annotation (Line(points={{-110,0},{-54.4,0}}, color={0,0,0}));
connect(clockEvent.u, event4ToEvent.y)
annotation (Line(points={{-6.6,0},{-45.6,0}}, color={217,67,180}));
annotation (Icon(coordinateSystem(preserveAspectRatio=false)), Diagram(
coordinateSystem(preserveAspectRatio=false)));
end BecomesTrue;
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
within CRML_test.ETL.BecomesTrue;
model BecomesTrue_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}})));
CRML.Blocks.Logical4.BooleanToBoolean4 booleanToBoolean4_1
annotation (Placement(transformation(extent={{-4,-4},{4,4}})));
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 (Icon(coordinateSystem(preserveAspectRatio=false)), Diagram(
coordinateSystem(preserveAspectRatio=false)));
end BecomesTrue_externals;
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
within CRML_test.ETL.BecomesTrue;
model BecomesTrue_verif
extends BecomesTrue;
BecomesTrue_externals externals
annotation (Placement(transformation(extent={{-200,0},{-140,60}})));
CRML.Blocks.Events.ShowEvent show_c_b1_becomes_true
annotation (Placement(transformation(extent={{52,-44},{60,-36}})));
equation
// Bindings
b1 = externals.b1;
connect(show_c_b1_becomes_true.u, event4ToEvent.y) annotation (Line(points={{
51.6,-40},{-20,-40},{-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}},
initialScale=0.1), graphics={
Ellipse(lineColor = {75,138,73},
fillColor={255,255,255},
fillPattern = FillPattern.Solid,
extent = {{-100,-100},{100,100}}),
Polygon(lineColor = {0,0,255},
fillColor = {75,138,73},
pattern = LinePattern.None,
fillPattern = FillPattern.Solid,
points = {{-36,60},{64,0},{-36,-60},{-36,60}})}), Diagram(
coordinateSystem(preserveAspectRatio=false,
extent={{-200,-100},{100,100}},
initialScale=0.1)),
experiment(StopTime=14));
end BecomesTrue_verif;
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
within CRML_test.ETL;
package BecomesTrue
end BecomesTrue;
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
BecomesTrue
BecomesTrue_externals
BecomesTrue_verif
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
within CRML_test.ETL.TemplateOr;
partial model TemplateOr
Utilities.Boolean4Connector b1
annotation (Placement(transformation(extent={{-120,40},{-100,20}})));
Utilities.Boolean4Connector b2
annotation (Placement(transformation(extent={{-120,-20},{-100,-40}})));
Utilities.Boolean4Connector b1_or_b2
annotation (Placement(transformation(extent={{100,10},{120,-10}})));
equation
b1_or_b2 = CRML.Blocks.Logical4.or4(b1, b2);
annotation (Icon(coordinateSystem(preserveAspectRatio=false)), Diagram(
coordinateSystem(preserveAspectRatio=false)));
end TemplateOr;
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
within CRML_test.ETL.TemplateOr;
model TemplateOr_externals
CRML.Blocks.Logical4.Boolean4Constant boolean4Constant1(K=CRML.ETL.Types.Boolean4.true4)
annotation (Placement(transformation(extent={{-60,40},{-40,60}})));
CRML.Blocks.Logical4.Boolean4Constant boolean4Constant2(K=CRML.ETL.Types.Boolean4.undecided)
annotation (Placement(transformation(extent={{-60,-60},{-40,-40}})));
CRML.ETL.Connectors.Boolean4Output b1
annotation (Placement(transformation(extent={{100,40},{120,60}})));
CRML.ETL.Connectors.Boolean4Output b2
annotation (Placement(transformation(extent={{100,-60},{120,-40}})));
equation
connect(boolean4Constant1.y, b1)
annotation (Line(points={{-39,50},{110,50}}, color={162,29,33}));
connect(boolean4Constant2.y, b2)
annotation (Line(points={{-39,-50},{110,-50}}, color={162,29,33}));
annotation (Icon(coordinateSystem(preserveAspectRatio=false)), Diagram(
coordinateSystem(preserveAspectRatio=false)));
end TemplateOr_externals;
Loading

0 comments on commit b659ba1

Please sign in to comment.