diff --git a/resources/modelica_libraries/CRML_test/Examples/TrafficLight/Spec.mo b/resources/modelica_libraries/CRML_test/Examples/TrafficLight/Spec.mo new file mode 100644 index 0000000..d6fb481 --- /dev/null +++ b/resources/modelica_libraries/CRML_test/Examples/TrafficLight/Spec.mo @@ -0,0 +1,127 @@ +within CRML_test.Examples.TrafficLight; + +model Spec + CRML.TimeLocators.Continuous.AfterBefore afterBefore annotation( + Placement(transformation(extent = {{-40, 64}, {-20, 84}}))); + CRML.Requirements.CheckCountEqual checkInPCount(threshold = 0) annotation( + Placement(transformation(extent = {{-40, 24}, {-20, 44}}))); + CRML.TimeLocators.Continuous.AfterFor afterFor annotation( + Placement(transformation(extent = {{-40, -40}, {-20, -20}}))); + CRML.Blocks.Math.Constant const(k = 30) annotation( + Placement(transformation(extent = {{-80, -60}, {-60, -40}}))); + CRML.Requirements.Ensure checkBoolean annotation( + Placement(transformation(extent = {{-40, -80}, {-20, -60}}))); + CRML.TimeLocators.Continuous.AfterFor When annotation( + Placement(transformation(extent = {{100, 70}, {120, 90}}))); + CRML.Blocks.Math.Constant const1(k = 0.2) annotation( + Placement(transformation(extent = {{20, 14}, {40, 34}}))); + CRML.Requirements.CheckAtEnd checkInPCount1 annotation( + Placement(transformation(extent = {{100, 0}, {120, 20}}))); + CRML.Blocks.Math.Constant const2(k = 30) annotation( + Placement(transformation(extent = {{22, 50}, {42, 70}}))); + CRML.ETL.Connectors.BooleanInput red "External Boolean variable" annotation( + Placement(transformation(extent = {{-120, 70}, {-100, 90}}))); + CRML.ETL.Connectors.BooleanInput green annotation( + Placement(transformation(extent = {{-120, -90}, {-100, -70}}))); + CRML.ETL.Connectors.BooleanInput yellow "Boolean condition" annotation( + Placement(transformation(extent = {{-120, -10}, {-100, 10}}))); + CRML.Blocks.Logical4.ShowBoolean4 show_req1 annotation( + Placement(transformation(extent = {{-8, 20}, {14, 48}}))); + CRML.Blocks.Logical4.ShowBoolean4 show_req2 annotation( + Placement(transformation(extent = {{-10, -82}, {14, -58}}))); + CRML.Blocks.Logical4.ShowBoolean4 show_req3 annotation( + Placement(transformation(origin = {-2, 14}, extent = {{140, -2}, {162, 22}}))); + CRML.Blocks.Logical4.And4 and4_1 annotation( + Placement(transformation(extent = {{20, -58}, {40, -38}}))); + CRML.Blocks.Logical4.And4 and4_2 annotation( + Placement(transformation(extent = {{112, -50}, {132, -30}}))); + CRML.Blocks.Logical4.ShowBoolean4 show_req annotation( + Placement(transformation(extent = {{138, -52}, {160, -28}}))); + CRML.Blocks.Logical4.BooleanToBoolean4 booleanToBoolean4_1 annotation( + Placement(transformation(extent = {{-84, 76}, {-76, 84}}))); + CRML.Blocks.Logical4.BooleanToBoolean4 booleanToBoolean4_2 annotation( + Placement(transformation(extent = {{-84, 62}, {-76, 70}}))); + CRML.Blocks.Logical4.BooleanToBoolean4 booleanToBoolean4_3 annotation( + Placement(transformation(extent = {{-84, -84}, {-76, -76}}))); + CRML.Blocks.Logical4.BooleanToBoolean4 booleanToBoolean4_4 annotation( + Placement(transformation(extent = {{-84, -4}, {-76, 4}}))); + CRML.Blocks.Events.EventDelay booleanDelay annotation( + Placement(transformation(extent = {{58, 70}, {78, 90}}))); + CRML.Blocks.Logical4.BooleanToBoolean4 booleanToBoolean4_5 annotation( + Placement(transformation(extent = {{84, 76}, {92, 84}}))); + CRML.Blocks.Events.Event4ToEvent event4ToEvent annotation( + Placement(transformation(extent = {{42, 76}, {50, 84}}))); + CRML.ETL.Connectors.Boolean4Output req1 annotation( + Placement(transformation(origin = {170, 60}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {170, 60}, extent = {{-10, -10}, {10, 10}}))); + CRML.ETL.Connectors.Boolean4Output req2 annotation( + Placement(transformation(origin = {170, 0}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {170, 0}, extent = {{-10, -10}, {10, 10}}))); + CRML.ETL.Connectors.Boolean4Output req3 annotation( + Placement(transformation(origin = {170, -60}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {170, -60}, extent = {{-10, -10}, {10, 10}}))); +equation + connect(afterBefore.y, checkInPCount.tl) annotation( + Line(points = {{-30, 64}, {-30, 44}}, color = {0, 0, 255})); + connect(const.y, afterFor.duration) annotation( + Line(points = {{-59, -50}, {-50, -50}, {-50, -38}, {-41, -38}}, color = {0, 0, 0})); + connect(afterFor.y, checkBoolean.tl) annotation( + Line(points = {{-30, -40}, {-30, -60}}, color = {0, 0, 255})); + connect(const1.y, When.duration) annotation( + Line(points = {{41, 24}, {90, 24}, {90, 72}, {99, 72}}, color = {0, 0, 0})); + connect(checkInPCount.y, show_req1.u) annotation( + Line(points = {{-19, 34}, {-8.55, 34}}, color = {162, 29, 33})); + connect(checkBoolean.y, show_req2.u) annotation( + Line(points = {{-19, -70}, {-10.6, -70}}, color = {162, 29, 33})); + connect(checkBoolean.y, and4_1.u2) annotation( + Line(points = {{-19, -70}, {-16, -70}, {-16, -56}, {19, -56}}, color = {162, 29, 33})); + connect(checkInPCount.y, and4_1.u1) annotation( + Line(points = {{-19, 34}, {-16, 34}, {-16, -40}, {19, -40}}, color = {162, 29, 33})); + connect(and4_2.y, show_req.u) annotation( + Line(points = {{133, -40}, {137.45, -40}}, color = {162, 29, 33})); + connect(and4_1.y, and4_2.u2) annotation( + Line(points = {{41, -48}, {111, -48}}, color = {162, 29, 33})); + connect(checkInPCount.u, booleanToBoolean4_1.y) annotation( + Line(points = {{-41, 34}, {-72, 34}, {-72, 80}, {-75.6, 80}}, color = {162, 29, 33})); + connect(booleanToBoolean4_1.u, red) annotation( + Line(points = {{-84.4, 80}, {-110, 80}}, color = {217, 67, 180})); + connect(yellow, booleanToBoolean4_2.u) annotation( + Line(points = {{-110, 0}, {-94, 0}, {-94, 66}, {-84.4, 66}}, color = {217, 67, 180})); + connect(booleanToBoolean4_2.y, afterBefore.u2) annotation( + Line(points = {{-75.6, 66}, {-41, 66}}, color = {162, 29, 33})); + connect(green, booleanToBoolean4_3.u) annotation( + Line(points = {{-110, -80}, {-84.4, -80}}, color = {217, 67, 180})); + connect(booleanToBoolean4_3.y, checkBoolean.u) annotation( + Line(points = {{-75.6, -80}, {-52, -80}, {-52, -70}, {-41, -70}}, color = {162, 29, 33})); + connect(booleanToBoolean4_3.y, afterFor.u) annotation( + Line(points = {{-75.6, -80}, {-52, -80}, {-52, -30}, {-41, -30}}, color = {162, 29, 33})); + connect(booleanToBoolean4_3.y, afterBefore.u1) annotation( + Line(points = {{-75.6, -80}, {-52, -80}, {-52, 74}, {-41, 74}}, color = {162, 29, 33})); + connect(checkInPCount1.u, booleanToBoolean4_4.y) annotation( + Line(points = {{99, 10}, {90, 10}, {90, 0}, {-75.6, 0}}, color = {162, 29, 33})); + connect(booleanToBoolean4_4.u, yellow) annotation( + Line(points = {{-84.4, 0}, {-110, 0}}, color = {217, 67, 180})); + connect(When.y, checkInPCount1.tl) annotation( + Line(points = {{110, 70}, {110, 20}}, color = {0, 0, 255})); + connect(const2.y, booleanDelay.delay) annotation( + Line(points = {{43, 60}, {50, 60}, {50, 72}, {57, 72}}, color = {0, 0, 0})); + connect(checkInPCount1.y, show_req3.u) annotation( + Line(points = {{121, 10}, {129, 10}, {129, 24}, {137, 24}}, color = {162, 29, 33})); + connect(checkInPCount1.y, and4_2.u1) annotation( + Line(points = {{121, 10}, {128, 10}, {128, -22}, {98, -22}, {98, -32}, {111, -32}}, color = {162, 29, 33})); + connect(booleanDelay.y, booleanToBoolean4_5.u) annotation( + Line(points = {{79, 80}, {83.6, 80}}, color = {217, 67, 180})); + connect(booleanToBoolean4_5.y, When.u) annotation( + Line(points = {{92.4, 80}, {99, 80}}, color = {162, 29, 33})); + connect(event4ToEvent.y, booleanDelay.u) annotation( + Line(points = {{50.4, 80}, {57, 80}}, color = {217, 67, 180})); + connect(booleanToBoolean4_3.y, event4ToEvent.u) annotation( + Line(points = {{-75.6, -80}, {-52, -80}, {-52, 88}, {28, 88}, {28, 80}, {41.6, 80}}, color = {162, 29, 33})); + connect(checkInPCount.y, req1) annotation( + Line(points = {{-18, 34}, {-10, 34}, {-10, 100}, {140, 100}, {140, 60}, {170, 60}}, color = {162, 29, 33})); + connect(checkBoolean.y, req2) annotation( + Line(points = {{-18, -70}, {-12, -70}, {-12, -20}, {140, -20}, {140, 0}, {170, 0}}, color = {162, 29, 33})); + connect(checkInPCount1.y, req3) annotation( + Line(points = {{122, 10}, {128, 10}, {128, -22}, {98, -22}, {98, -60}, {170, -60}}, color = {162, 29, 33})); + annotation( + Icon(coordinateSystem(preserveAspectRatio = false, extent = {{-100, -100}, {160, 100}}), graphics = {Rectangle(origin = {30, 0},lineColor = {28, 108, 200}, fillColor = {215, 215, 215}, fillPattern = FillPattern.Solid, extent = {{-130, 100}, {130, -100}}), Ellipse(origin = {32, 0},lineColor = {238, 46, 47}, fillColor = {238, 46, 47}, fillPattern = FillPattern.Solid, extent = {{-20, 98}, {20, 58}}), Ellipse(origin = {32, 0},lineColor = {244, 125, 35}, fillColor = {244, 125, 35}, fillPattern = FillPattern.Solid, extent = {{-20, 18}, {20, -20}}), Ellipse(origin = {32, 0},lineColor = {0, 140, 72}, fillColor = {0, 140, 72}, fillPattern = FillPattern.Solid, extent = {{-20, -60}, {20, -98}}), Text(textColor = {28, 108, 200}, extent = {{-92, 126}, {90, 108}}, textString = "%name")}), + Diagram(coordinateSystem(preserveAspectRatio = false, extent = {{-100, -100}, {160, 100}}), graphics = {Rectangle(lineColor = {28, 108, 200}, fillColor = {255, 255, 170}, fillPattern = FillPattern.Solid, extent = {{-86, -16}, {-14, -94}}), Rectangle(lineColor = {28, 108, 200}, fillColor = {255, 255, 170}, fillPattern = FillPattern.Solid, extent = {{-86, 96}, {-14, -10}}), Text(textColor = {28, 108, 200}, extent = {{-72, -2}, {-30, -6}}, textString = "After green, next step is yellow"), Text(textColor = {28, 108, 200}, extent = {{-82, -82}, {-16, -94}}, textString = "Step green should stay active for at least 30 seconds"), Rectangle(lineColor = {28, 108, 200}, fillColor = {255, 255, 170}, fillPattern = FillPattern.Solid, extent = {{16, 96}, {134, -16}}), Text(textColor = {28, 108, 200}, extent = {{24, -4}, {76, -8}}, textString = "After green becomes active + 30 seconds,"), Text(textColor = {28, 108, 200}, extent = {{25, -8}, {81, -14}}, textString = "next step should turn yellow within 0.2 seconds"), Text(textColor = {28, 108, 200}, extent = {{-126, 100}, {-96, 92}}, textString = "red"), Text(textColor = {28, 108, 200}, extent = {{-126, -58}, {-96, -66}}, textString = "green"), Text(textColor = {28, 108, 200}, extent = {{-126, 22}, {-96, 14}}, textString = "yellow"), Text(textColor = {28, 108, 200}, extent = {{-84, 96}, {-58, 86}}, textString = "req1"), Text(textColor = {28, 108, 200}, extent = {{28, 96}, {54, 86}}, textString = "req3"), Text(textColor = {28, 108, 200}, extent = {{-84, -18}, {-58, -28}}, textString = "req2")}), + experiment(StopTime = 100)); +end Spec; diff --git a/resources/modelica_libraries/CRML_test/Examples/TrafficLight/Spec_externals.mo b/resources/modelica_libraries/CRML_test/Examples/TrafficLight/Spec_externals.mo new file mode 100644 index 0000000..85c9662 --- /dev/null +++ b/resources/modelica_libraries/CRML_test/Examples/TrafficLight/Spec_externals.mo @@ -0,0 +1,55 @@ +within CRML_test.Examples.TrafficLight; + +model Spec_externals + Modelica.Blocks.Sources.RealExpression greenObserver(y = phys.greenLamp.i) annotation( + Placement(transformation(extent = {{56, 10}, {30, 30}}))); + Modelica.Blocks.Logical.GreaterEqualThreshold oGreen(threshold = 9) annotation( + Placement(transformation(extent = {{12, 16}, {4, 24}}))); + Modelica.Blocks.Sources.RealExpression yellowObservor(y = phys.yellowLamp.i) annotation( + Placement(transformation(extent = {{56, 30}, {30, 50}}))); + Modelica.Blocks.Logical.GreaterEqualThreshold oYellow(threshold = 9) annotation( + Placement(transformation(extent = {{12, 36}, {4, 44}}))); + Modelica.Blocks.Sources.RealExpression redObserver(y = phys.redLamp.i) annotation( + Placement(transformation(extent = {{56, 50}, {30, 70}}))); + CRML.Examples.TrafficLight.Log2 log annotation( + Placement(transformation(extent = {{148, 30}, {128, 50}}))); + Modelica.Blocks.Logical.GreaterEqualThreshold oRed(threshold = 9) annotation( + Placement(transformation(extent = {{12, 56}, {4, 64}}))); + CRML.Examples.TrafficLight.Phys1 phys annotation( + Placement(transformation(extent = {{108, 30}, {88, 50}}))); + Modelica.Blocks.Sources.BooleanExpression green_active(y = oGreen.y) annotation( + Placement(transformation(extent = {{-30, 10}, {-50, 30}}))); + Modelica.Blocks.Sources.BooleanExpression yellow_active(y = oYellow.y) annotation( + Placement(transformation(extent = {{-30, 30}, {-50, 50}}))); + Modelica.Blocks.Sources.BooleanExpression red_active(y = oRed.y) annotation( + Placement(transformation(extent = {{-30, 50}, {-50, 70}}))); + Modelica.Blocks.Interfaces.BooleanOutput red annotation( + Placement(transformation(origin = {-72, 60}, extent = {{10, -10}, {-10, 10}}), iconTransformation(origin = {-110, 60}, extent = {{-10, -10}, {10, 10}}))); + Modelica.Blocks.Interfaces.BooleanOutput yellow annotation( + Placement(transformation(origin = {-72, 40}, extent = {{10, -10}, {-10, 10}}), iconTransformation(origin = {-110, 0}, extent = {{-10, -10}, {10, 10}}))); + Modelica.Blocks.Interfaces.BooleanOutput green annotation( + Placement(transformation(origin = {-72, 20}, extent = {{10, -10}, {-10, 10}}), iconTransformation(origin = {-110, -60}, extent = {{-10, -10}, {10, 10}}))); +equation + connect(greenObserver.y, oGreen.u) annotation( + Line(points = {{28.7, 20}, {12.8, 20}}, color = {0, 0, 127})); + connect(yellowObservor.y, oYellow.u) annotation( + Line(points = {{28.7, 40}, {12.8, 40}}, color = {0, 0, 127})); + connect(redObserver.y, oRed.u) annotation( + Line(points = {{28.7, 60}, {12.8, 60}}, color = {0, 0, 127})); + connect(phys.green, log.y_green) annotation( + Line(points = {{109, 32}, {114, 32}, {114, 32}, {118, 32}, {118, 32}, {127, 32}}, color = {217, 67, 180})); + connect(phys.yellow, log.y_yellow) annotation( + Line(points = {{109, 40}, {127, 40}}, color = {217, 67, 180})); + connect(phys.red, log.y_red) annotation( + Line(points = {{109, 48}, {114, 48}, {114, 48}, {118, 48}, {118, 48}, {127, 48}}, color = {217, 67, 180})); + connect(red_active.y, red) annotation( + Line(points = {{-50, 60}, {-72, 60}}, color = {255, 0, 255})); + connect(yellow_active.y, yellow) annotation( + Line(points = {{-50, 40}, {-72, 40}}, color = {255, 0, 255})); + connect(green_active.y, green) annotation( + Line(points = {{-50, 20}, {-72, 20}}, color = {255, 0, 255})); + annotation( + Icon(coordinateSystem(preserveAspectRatio = false, extent = {{-100, -100}, {100, 100}})), + Diagram(coordinateSystem(preserveAspectRatio = false, extent = {{-100, -100}, {100, 100}}), graphics = {Rectangle(lineColor = {28, 108, 200}, fillColor = {215, 215, 215}, fillPattern = FillPattern.Solid, extent = {{-150, 90}, {172, -30}}), Rectangle(lineColor = {28, 108, 200}, fillColor = {170, 255, 213}, fillPattern = FillPattern.Solid, extent = {{80, 80}, {158, 0}}), Text(textColor = {28, 108, 200}, extent = {{84, 14}, {156, 4}}, textString = "Behavioral model"), Rectangle(lineColor = {28, 108, 200}, fillColor = {170, 255, 255}, fillPattern = FillPattern.Solid, extent = {{-4, 80}, {60, 0}}), Text(textColor = {28, 108, 200}, extent = {{-10, 12}, {64, 4}}, textString = "Observation model"), Text(textColor = {28, 108, 200}, extent = {{116, 64}, {156, 56}}, textString = "I&C"), Text(textColor = {28, 108, 200}, extent = {{80, 64}, {120, 56}}, textString = "Physical"), Rectangle(lineColor = {28, 108, 200}, fillColor = {255, 213, 170}, fillPattern = FillPattern.Solid, extent = {{-54, 80}, {-26, 0}}), Text(textColor = {28, 108, 200}, extent = {{-76, 12}, {-4, 4}}, textString = "Bindings"), Text(textColor = {28, 108, 200}, extent = {{-66, -8}, {78, -26}}, textString = "Model for computing externals")}), + experiment(StopTime = 100)); +end Spec_externals; diff --git a/resources/modelica_libraries/CRML_test/Examples/TrafficLight/Spec_verif.mo b/resources/modelica_libraries/CRML_test/Examples/TrafficLight/Spec_verif.mo new file mode 100644 index 0000000..4f00294 --- /dev/null +++ b/resources/modelica_libraries/CRML_test/Examples/TrafficLight/Spec_verif.mo @@ -0,0 +1,61 @@ +within CRML_test.Examples.TrafficLight; + +model Spec_verif + Modelica.Blocks.Sources.RealExpression greenObserver(y = phys.greenLamp.i) annotation( + Placement(transformation(extent = {{56, 10}, {30, 30}}))); + Modelica.Blocks.Logical.GreaterEqualThreshold oGreen(threshold = 9) annotation( + Placement(transformation(extent = {{12, 16}, {4, 24}}))); + Modelica.Blocks.Sources.RealExpression yellowObservor(y = phys.yellowLamp.i) annotation( + Placement(transformation(extent = {{56, 30}, {30, 50}}))); + Modelica.Blocks.Logical.GreaterEqualThreshold oYellow(threshold = 9) annotation( + Placement(transformation(extent = {{12, 36}, {4, 44}}))); + Modelica.Blocks.Sources.RealExpression redObserver(y = phys.redLamp.i) annotation( + Placement(transformation(extent = {{56, 50}, {30, 70}}))); + CRML.Examples.TrafficLight.Log2 log annotation( + Placement(transformation(extent = {{148, 30}, {128, 50}}))); + Modelica.Blocks.Logical.GreaterEqualThreshold oRed(threshold = 9) annotation( + Placement(transformation(extent = {{12, 56}, {4, 64}}))); + CRML.Examples.TrafficLight.Phys1 phys annotation( + Placement(transformation(extent = {{108, 30}, {88, 50}}))); + Modelica.Blocks.Sources.BooleanExpression green_active(y = oGreen.y) annotation( + Placement(transformation(extent = {{-30, 10}, {-50, 30}}))); + Modelica.Blocks.Sources.BooleanExpression yellow_active(y = oYellow.y) annotation( + Placement(transformation(extent = {{-30, 30}, {-50, 50}}))); + Modelica.Blocks.Sources.BooleanExpression red_active(y = oRed.y) annotation( + Placement(transformation(extent = {{-30, 50}, {-50, 70}}))); + Modelica.Blocks.Interfaces.BooleanOutput red annotation( + Placement(transformation(origin = {-72, 60}, extent = {{10, -10}, {-10, 10}}, rotation = -0), iconTransformation(origin = {-68, 58}, extent = {{-10, -10}, {10, 10}}))); + Modelica.Blocks.Interfaces.BooleanOutput yellow annotation( + Placement(transformation(origin = {-72, 40}, extent = {{10, -10}, {-10, 10}}), iconTransformation(origin = {-58, 68}, extent = {{-10, -10}, {10, 10}}))); + Modelica.Blocks.Interfaces.BooleanOutput green annotation( + Placement(transformation(origin = {-72, 20}, extent = {{10, -10}, {-10, 10}}), iconTransformation(origin = {-48, 78}, extent = {{-10, -10}, {10, 10}}))); + Spec spec annotation( + Placement(transformation(origin = {-110, 40}, extent = {{13, -10}, {-13, 10}}, rotation = -0))); +equation + // Bindings + spec.red = red; + spec.green = green; + spec.yellow = yellow; + connect(greenObserver.y, oGreen.u) annotation( + Line(points = {{28.7, 20}, {12.8, 20}}, color = {0, 0, 127})); + connect(yellowObservor.y, oYellow.u) annotation( + Line(points = {{28.7, 40}, {12.8, 40}}, color = {0, 0, 127})); + connect(redObserver.y, oRed.u) annotation( + Line(points = {{28.7, 60}, {12.8, 60}}, color = {0, 0, 127})); + connect(phys.green, log.y_green) annotation( + Line(points = {{109, 32}, {114, 32}, {114, 32}, {118, 32}, {118, 32}, {127, 32}}, color = {217, 67, 180})); + connect(phys.yellow, log.y_yellow) annotation( + Line(points = {{109, 40}, {127, 40}}, color = {217, 67, 180})); + connect(phys.red, log.y_red) annotation( + Line(points = {{109, 48}, {114, 48}, {114, 48}, {118, 48}, {118, 48}, {127, 48}}, color = {217, 67, 180})); + connect(red_active.y, red) annotation( + Line(points = {{-50, 60}, {-72, 60}}, color = {255, 0, 255})); + connect(yellow_active.y, yellow) annotation( + Line(points = {{-50, 40}, {-72, 40}}, color = {255, 0, 255})); + connect(green_active.y, green) annotation( + Line(points = {{-50, 20}, {-72, 20}}, color = {255, 0, 255})); + annotation( + Icon(coordinateSystem(preserveAspectRatio = false, extent = {{-160, -40}, {180, 100}}), graphics = {Rectangle(extent = {{-160, 100}, {180, -40}}, lineColor = {28, 108, 200}), Line(points = {{-40, 28}, {0, -30}, {62, 96}}, color = {0, 127, 0}, smooth = Smooth.None, thickness = 1)}), + Diagram(coordinateSystem(preserveAspectRatio = false, extent = {{-160, -40}, {180, 100}}), graphics = {Rectangle(lineColor = {28, 108, 200}, fillColor = {215, 215, 215}, fillPattern = FillPattern.Solid, extent = {{-150, 90}, {172, -30}}), Rectangle(lineColor = {28, 108, 200}, fillColor = {170, 255, 213}, fillPattern = FillPattern.Solid, extent = {{80, 80}, {158, 0}}), Text(textColor = {28, 108, 200}, extent = {{84, 14}, {156, 4}}, textString = "Behavioral model"), Rectangle(lineColor = {28, 108, 200}, fillColor = {170, 255, 255}, fillPattern = FillPattern.Solid, extent = {{-4, 80}, {60, 0}}), Text(textColor = {28, 108, 200}, extent = {{-10, 12}, {64, 4}}, textString = "Observation model"), Text(textColor = {28, 108, 200}, extent = {{116, 64}, {156, 56}}, textString = "I&C"), Text(textColor = {28, 108, 200}, extent = {{80, 64}, {120, 56}}, textString = "Physical"), Rectangle(lineColor = {28, 108, 200}, fillColor = {255, 213, 170}, fillPattern = FillPattern.Solid, extent = {{-54, 80}, {-26, 0}}), Text(textColor = {28, 108, 200}, extent = {{-76, 12}, {-4, 4}}, textString = "Bindings"), Text(textColor = {28, 108, 200}, extent = {{-66, -8}, {78, -26}}, textString = "Model for computing externals")}), + experiment(StopTime = 100)); +end Spec_verif; diff --git a/resources/modelica_libraries/CRML_test/Examples/TrafficLight/package.mo b/resources/modelica_libraries/CRML_test/Examples/TrafficLight/package.mo new file mode 100644 index 0000000..277dc1b --- /dev/null +++ b/resources/modelica_libraries/CRML_test/Examples/TrafficLight/package.mo @@ -0,0 +1,4 @@ +within CRML_test.Examples; + +package TrafficLight +end TrafficLight; diff --git a/resources/modelica_libraries/CRML_test/Examples/TrafficLight/package.order b/resources/modelica_libraries/CRML_test/Examples/TrafficLight/package.order new file mode 100644 index 0000000..d731db0 --- /dev/null +++ b/resources/modelica_libraries/CRML_test/Examples/TrafficLight/package.order @@ -0,0 +1,3 @@ +Spec +Spec_externals +Spec_verif diff --git a/resources/modelica_libraries/CRML_test/Examples/package.mo b/resources/modelica_libraries/CRML_test/Examples/package.mo new file mode 100644 index 0000000..1f19cd2 --- /dev/null +++ b/resources/modelica_libraries/CRML_test/Examples/package.mo @@ -0,0 +1,7 @@ +within CRML_test; + +package Examples + annotation( + 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 = {{-42, 38}, {44, -30}}, textString = "", fontName = "Symbol"), Rectangle(lineColor = {128, 128, 128}, extent = {{-100, -100}, {100, 100}}, radius = 25)})); +end Examples; diff --git a/resources/modelica_libraries/CRML_test/Examples/package.order b/resources/modelica_libraries/CRML_test/Examples/package.order new file mode 100644 index 0000000..1a142bd --- /dev/null +++ b/resources/modelica_libraries/CRML_test/Examples/package.order @@ -0,0 +1 @@ +TrafficLight diff --git a/resources/modelica_libraries/CRML_test/package.order b/resources/modelica_libraries/CRML_test/package.order index ee8f110..b3f309d 100644 --- a/resources/modelica_libraries/CRML_test/package.order +++ b/resources/modelica_libraries/CRML_test/package.order @@ -2,3 +2,4 @@ ETL FORML Spec_doc Utilities +Examples diff --git a/src/test/resources/refResults/crml-modelica-library-examples/TrafficLight/Spec_verif_ref.mat b/src/test/resources/refResults/crml-modelica-library-examples/TrafficLight/Spec_verif_ref.mat new file mode 100644 index 0000000..7333f68 Binary files /dev/null and b/src/test/resources/refResults/crml-modelica-library-examples/TrafficLight/Spec_verif_ref.mat differ diff --git a/src/test/resources/testModels/crml-modelica-library-examples/TrafficLight/Spec.crml b/src/test/resources/testModels/crml-modelica-library-examples/TrafficLight/Spec.crml new file mode 100644 index 0000000..7d89f12 --- /dev/null +++ b/src/test/resources/testModels/crml-modelica-library-examples/TrafficLight/Spec.crml @@ -0,0 +1,33 @@ +model Spec is { + // Import of libraries + flatten {ETL, FORM_L} + union { + + // Requirement model for the traffic light example + + // 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; + + // 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; + + // 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/src/test/resources/testModels/crml-modelica-library-examples/TrafficLight/Spec_simplified.crml b/src/test/resources/testModels/crml-modelica-library-examples/TrafficLight/Spec_simplified.crml new file mode 100644 index 0000000..e6a06f6 --- /dev/null +++ b/src/test/resources/testModels/crml-modelica-library-examples/TrafficLight/Spec_simplified.crml @@ -0,0 +1,117 @@ +model Spec_simplified 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; +}; + diff --git a/src/test/resources/verificationModels/crml-modelica-library-examples/TrafficLight/Spec_externals.mo b/src/test/resources/verificationModels/crml-modelica-library-examples/TrafficLight/Spec_externals.mo new file mode 100644 index 0000000..d46c5f5 --- /dev/null +++ b/src/test/resources/verificationModels/crml-modelica-library-examples/TrafficLight/Spec_externals.mo @@ -0,0 +1,53 @@ +model Spec_externals + Modelica.Blocks.Sources.RealExpression greenObserver(y = phys.greenLamp.i) annotation( + Placement(transformation(extent = {{56, 10}, {30, 30}}))); + Modelica.Blocks.Logical.GreaterEqualThreshold oGreen(threshold = 9) annotation( + Placement(transformation(extent = {{12, 16}, {4, 24}}))); + Modelica.Blocks.Sources.RealExpression yellowObservor(y = phys.yellowLamp.i) annotation( + Placement(transformation(extent = {{56, 30}, {30, 50}}))); + Modelica.Blocks.Logical.GreaterEqualThreshold oYellow(threshold = 9) annotation( + Placement(transformation(extent = {{12, 36}, {4, 44}}))); + Modelica.Blocks.Sources.RealExpression redObserver(y = phys.redLamp.i) annotation( + Placement(transformation(extent = {{56, 50}, {30, 70}}))); + CRML.Examples.TrafficLight.Log2 log annotation( + Placement(transformation(extent = {{148, 30}, {128, 50}}))); + Modelica.Blocks.Logical.GreaterEqualThreshold oRed(threshold = 9) annotation( + Placement(transformation(extent = {{12, 56}, {4, 64}}))); + CRML.Examples.TrafficLight.Phys1 phys annotation( + Placement(transformation(extent = {{108, 30}, {88, 50}}))); + Modelica.Blocks.Sources.BooleanExpression green_active(y = oGreen.y) annotation( + Placement(transformation(extent = {{-30, 10}, {-50, 30}}))); + Modelica.Blocks.Sources.BooleanExpression yellow_active(y = oYellow.y) annotation( + Placement(transformation(extent = {{-30, 30}, {-50, 50}}))); + Modelica.Blocks.Sources.BooleanExpression red_active(y = oRed.y) annotation( + Placement(transformation(extent = {{-30, 50}, {-50, 70}}))); + Modelica.Blocks.Interfaces.BooleanOutput red annotation( + Placement(transformation(origin = {-72, 60}, extent = {{10, -10}, {-10, 10}}), iconTransformation(origin = {-110, 60}, extent = {{-10, -10}, {10, 10}}))); + Modelica.Blocks.Interfaces.BooleanOutput yellow annotation( + Placement(transformation(origin = {-72, 40}, extent = {{10, -10}, {-10, 10}}), iconTransformation(origin = {-110, 0}, extent = {{-10, -10}, {10, 10}}))); + Modelica.Blocks.Interfaces.BooleanOutput green annotation( + Placement(transformation(origin = {-72, 20}, extent = {{10, -10}, {-10, 10}}), iconTransformation(origin = {-110, -60}, extent = {{-10, -10}, {10, 10}}))); +equation + connect(greenObserver.y, oGreen.u) annotation( + Line(points = {{28.7, 20}, {12.8, 20}}, color = {0, 0, 127})); + connect(yellowObservor.y, oYellow.u) annotation( + Line(points = {{28.7, 40}, {12.8, 40}}, color = {0, 0, 127})); + connect(redObserver.y, oRed.u) annotation( + Line(points = {{28.7, 60}, {12.8, 60}}, color = {0, 0, 127})); + connect(phys.green, log.y_green) annotation( + Line(points = {{109, 32}, {114, 32}, {114, 32}, {118, 32}, {118, 32}, {127, 32}}, color = {217, 67, 180})); + connect(phys.yellow, log.y_yellow) annotation( + Line(points = {{109, 40}, {127, 40}}, color = {217, 67, 180})); + connect(phys.red, log.y_red) annotation( + Line(points = {{109, 48}, {114, 48}, {114, 48}, {118, 48}, {118, 48}, {127, 48}}, color = {217, 67, 180})); + connect(red_active.y, red) annotation( + Line(points = {{-50, 60}, {-72, 60}}, color = {255, 0, 255})); + connect(yellow_active.y, yellow) annotation( + Line(points = {{-50, 40}, {-72, 40}}, color = {255, 0, 255})); + connect(green_active.y, green) annotation( + Line(points = {{-50, 20}, {-72, 20}}, color = {255, 0, 255})); + annotation( + Icon(coordinateSystem(preserveAspectRatio = false, extent = {{-100, -100}, {100, 100}})), + Diagram(coordinateSystem(preserveAspectRatio = false, extent = {{-100, -100}, {100, 100}}), graphics = {Rectangle(lineColor = {28, 108, 200}, fillColor = {215, 215, 215}, fillPattern = FillPattern.Solid, extent = {{-150, 90}, {172, -30}}), Rectangle(lineColor = {28, 108, 200}, fillColor = {170, 255, 213}, fillPattern = FillPattern.Solid, extent = {{80, 80}, {158, 0}}), Text(textColor = {28, 108, 200}, extent = {{84, 14}, {156, 4}}, textString = "Behavioral model"), Rectangle(lineColor = {28, 108, 200}, fillColor = {170, 255, 255}, fillPattern = FillPattern.Solid, extent = {{-4, 80}, {60, 0}}), Text(textColor = {28, 108, 200}, extent = {{-10, 12}, {64, 4}}, textString = "Observation model"), Text(textColor = {28, 108, 200}, extent = {{116, 64}, {156, 56}}, textString = "I&C"), Text(textColor = {28, 108, 200}, extent = {{80, 64}, {120, 56}}, textString = "Physical"), Rectangle(lineColor = {28, 108, 200}, fillColor = {255, 213, 170}, fillPattern = FillPattern.Solid, extent = {{-54, 80}, {-26, 0}}), Text(textColor = {28, 108, 200}, extent = {{-76, 12}, {-4, 4}}, textString = "Bindings"), Text(textColor = {28, 108, 200}, extent = {{-66, -8}, {78, -26}}, textString = "Model for computing externals")}), + experiment(StopTime = 100)); +end Spec_externals; diff --git a/src/test/resources/verificationModels/crml-modelica-library-examples/TrafficLight/Spec_verif.mo b/src/test/resources/verificationModels/crml-modelica-library-examples/TrafficLight/Spec_verif.mo new file mode 100644 index 0000000..9fb5c45 --- /dev/null +++ b/src/test/resources/verificationModels/crml-modelica-library-examples/TrafficLight/Spec_verif.mo @@ -0,0 +1,59 @@ +model Spec_verif + Modelica.Blocks.Sources.RealExpression greenObserver(y = phys.greenLamp.i) annotation( + Placement(transformation(extent = {{56, 10}, {30, 30}}))); + Modelica.Blocks.Logical.GreaterEqualThreshold oGreen(threshold = 9) annotation( + Placement(transformation(extent = {{12, 16}, {4, 24}}))); + Modelica.Blocks.Sources.RealExpression yellowObservor(y = phys.yellowLamp.i) annotation( + Placement(transformation(extent = {{56, 30}, {30, 50}}))); + Modelica.Blocks.Logical.GreaterEqualThreshold oYellow(threshold = 9) annotation( + Placement(transformation(extent = {{12, 36}, {4, 44}}))); + Modelica.Blocks.Sources.RealExpression redObserver(y = phys.redLamp.i) annotation( + Placement(transformation(extent = {{56, 50}, {30, 70}}))); + CRML.Examples.TrafficLight.Log2 log annotation( + Placement(transformation(extent = {{148, 30}, {128, 50}}))); + Modelica.Blocks.Logical.GreaterEqualThreshold oRed(threshold = 9) annotation( + Placement(transformation(extent = {{12, 56}, {4, 64}}))); + CRML.Examples.TrafficLight.Phys1 phys annotation( + Placement(transformation(extent = {{108, 30}, {88, 50}}))); + Modelica.Blocks.Sources.BooleanExpression green_active(y = oGreen.y) annotation( + Placement(transformation(extent = {{-30, 10}, {-50, 30}}))); + Modelica.Blocks.Sources.BooleanExpression yellow_active(y = oYellow.y) annotation( + Placement(transformation(extent = {{-30, 30}, {-50, 50}}))); + Modelica.Blocks.Sources.BooleanExpression red_active(y = oRed.y) annotation( + Placement(transformation(extent = {{-30, 50}, {-50, 70}}))); + Modelica.Blocks.Interfaces.BooleanOutput red annotation( + Placement(transformation(origin = {-72, 60}, extent = {{10, -10}, {-10, 10}}, rotation = -0), iconTransformation(origin = {-68, 58}, extent = {{-10, -10}, {10, 10}}))); + Modelica.Blocks.Interfaces.BooleanOutput yellow annotation( + Placement(transformation(origin = {-72, 40}, extent = {{10, -10}, {-10, 10}}), iconTransformation(origin = {-58, 68}, extent = {{-10, -10}, {10, 10}}))); + Modelica.Blocks.Interfaces.BooleanOutput green annotation( + Placement(transformation(origin = {-72, 20}, extent = {{10, -10}, {-10, 10}}), iconTransformation(origin = {-48, 78}, extent = {{-10, -10}, {10, 10}}))); + Spec spec annotation( + Placement(transformation(origin = {-110, 40}, extent = {{13, -10}, {-13, 10}}, rotation = -0))); +equation + // Bindings + spec.red = red; + spec.green = green; + spec.yellow = yellow; + connect(greenObserver.y, oGreen.u) annotation( + Line(points = {{28.7, 20}, {12.8, 20}}, color = {0, 0, 127})); + connect(yellowObservor.y, oYellow.u) annotation( + Line(points = {{28.7, 40}, {12.8, 40}}, color = {0, 0, 127})); + connect(redObserver.y, oRed.u) annotation( + Line(points = {{28.7, 60}, {12.8, 60}}, color = {0, 0, 127})); + connect(phys.green, log.y_green) annotation( + Line(points = {{109, 32}, {114, 32}, {114, 32}, {118, 32}, {118, 32}, {127, 32}}, color = {217, 67, 180})); + connect(phys.yellow, log.y_yellow) annotation( + Line(points = {{109, 40}, {127, 40}}, color = {217, 67, 180})); + connect(phys.red, log.y_red) annotation( + Line(points = {{109, 48}, {114, 48}, {114, 48}, {118, 48}, {118, 48}, {127, 48}}, color = {217, 67, 180})); + connect(red_active.y, red) annotation( + Line(points = {{-50, 60}, {-72, 60}}, color = {255, 0, 255})); + connect(yellow_active.y, yellow) annotation( + Line(points = {{-50, 40}, {-72, 40}}, color = {255, 0, 255})); + connect(green_active.y, green) annotation( + Line(points = {{-50, 20}, {-72, 20}}, color = {255, 0, 255})); + annotation( + Icon(coordinateSystem(preserveAspectRatio = false, extent = {{-160, -40}, {180, 100}}), graphics = {Rectangle(extent = {{-160, 100}, {180, -40}}, lineColor = {28, 108, 200}), Line(points = {{-40, 28}, {0, -30}, {62, 96}}, color = {0, 127, 0}, smooth = Smooth.None, thickness = 1)}), + Diagram(coordinateSystem(preserveAspectRatio = false, extent = {{-160, -40}, {180, 100}}), graphics = {Rectangle(lineColor = {28, 108, 200}, fillColor = {215, 215, 215}, fillPattern = FillPattern.Solid, extent = {{-150, 90}, {172, -30}}), Rectangle(lineColor = {28, 108, 200}, fillColor = {170, 255, 213}, fillPattern = FillPattern.Solid, extent = {{80, 80}, {158, 0}}), Text(textColor = {28, 108, 200}, extent = {{84, 14}, {156, 4}}, textString = "Behavioral model"), Rectangle(lineColor = {28, 108, 200}, fillColor = {170, 255, 255}, fillPattern = FillPattern.Solid, extent = {{-4, 80}, {60, 0}}), Text(textColor = {28, 108, 200}, extent = {{-10, 12}, {64, 4}}, textString = "Observation model"), Text(textColor = {28, 108, 200}, extent = {{116, 64}, {156, 56}}, textString = "I&C"), Text(textColor = {28, 108, 200}, extent = {{80, 64}, {120, 56}}, textString = "Physical"), Rectangle(lineColor = {28, 108, 200}, fillColor = {255, 213, 170}, fillPattern = FillPattern.Solid, extent = {{-54, 80}, {-26, 0}}), Text(textColor = {28, 108, 200}, extent = {{-76, 12}, {-4, 4}}, textString = "Bindings"), Text(textColor = {28, 108, 200}, extent = {{-66, -8}, {78, -26}}, textString = "Model for computing externals")}), + experiment(StopTime = 100)); +end Spec_verif; diff --git a/src/test/resources/verificationModels/use-cases/ics_educational/Reqs_sri_CRML_externals.mo b/src/test/resources/verificationModels/use-cases/ics_educational/Reqs_sri_CRML_externals.mo index 48d7025..1621eef 100644 --- a/src/test/resources/verificationModels/use-cases/ics_educational/Reqs_sri_CRML_externals.mo +++ b/src/test/resources/verificationModels/use-cases/ics_educational/Reqs_sri_CRML_externals.mo @@ -1,5 +1,3 @@ -within cooling_system.Verification; - model Reqs_sri_CRML_externals import cooling_system; Modelica.Blocks.Sources.RealExpression Q_echangeur_1(y = SRI_corrige.EchangeurAPlaques1D1.Ec.Q) annotation( @@ -61,23 +59,23 @@ model Reqs_sri_CRML_externals Modelica.Blocks.Sources.RealExpression T_output_sf(y = SRI_corrige.EchangeurAPlaques1D2.Tsf) annotation( Placement(transformation(origin = {27, -190}, extent = {{-17, -14}, {17, 14}}))); Modelica.Blocks.Interfaces.RealOutput v1 annotation( - Placement(transformation(origin = {270, 60}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {270, 60}, extent = {{-10, -10}, {10, 10}}))); + Placement(transformation(origin = {270, 60}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {290, 60}, extent = {{-10, -10}, {10, 10}}))); Modelica.Blocks.Interfaces.RealOutput v2 annotation( - Placement(transformation(origin = {270, 40}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {270, 20}, extent = {{-10, -10}, {10, 10}}))); + Placement(transformation(origin = {270, 40}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {290, 20}, extent = {{-10, -10}, {10, 10}}))); Modelica.Blocks.Interfaces.BooleanOutput pump_in_service1 annotation( - Placement(transformation(origin = {270, 10}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {270, -60}, extent = {{-10, -10}, {10, 10}}))); + Placement(transformation(origin = {270, 10}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {290, -60}, extent = {{-10, -10}, {10, 10}}))); Modelica.Blocks.Interfaces.BooleanOutput pump_in_service2 annotation( - Placement(transformation(origin = {270, -46}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {270, -120}, extent = {{-10, -10}, {10, 10}}))); + Placement(transformation(origin = {270, -46}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {290, -120}, extent = {{-10, -10}, {10, 10}}))); Modelica.Blocks.Interfaces.BooleanOutput pump_in_service3 annotation( - Placement(transformation(origin = {270, -100}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {270, -180}, extent = {{-10, -10}, {10, 10}}))); + Placement(transformation(origin = {270, -100}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {290, -180}, extent = {{-10, -10}, {10, 10}}))); Modelica.Blocks.Interfaces.RealOutput flow1 annotation( - Placement(transformation(origin = {270, -12}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {270, -80}, extent = {{-10, -10}, {10, 10}}))); + Placement(transformation(origin = {270, -12}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {290, -80}, extent = {{-10, -10}, {10, 10}}))); Modelica.Blocks.Interfaces.RealOutput flow2 annotation( - Placement(transformation(origin = {270, -70}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {270, -140}, extent = {{-10, -10}, {10, 10}}))); + Placement(transformation(origin = {270, -70}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {290, -140}, extent = {{-10, -10}, {10, 10}}))); Modelica.Blocks.Interfaces.RealOutput flow3 annotation( - Placement(transformation(origin = {270, -130}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {270, -200}, extent = {{-10, -10}, {10, 10}}))); + Placement(transformation(origin = {270, -130}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {290, -200}, extent = {{-10, -10}, {10, 10}}))); Modelica.Blocks.Interfaces.RealOutput T annotation( - Placement(transformation(origin = {270, -200}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {270, -240}, extent = {{-10, -10}, {10, 10}}))); + Placement(transformation(origin = {270, -200}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {290, -240}, extent = {{-10, -10}, {10, 10}}))); equation connect(Q_echangeur_1.y, flowToSpeed.u) annotation( Line(points = {{45.7, 64}, {57.4, 64}, {57.4, 65.2}, {66, 65.2}}, color = {0, 0, 127})); @@ -123,6 +121,6 @@ equation Line(points = {{270, 60}, {178, 60}, {178, 66}, {90, 66}}, color = {0, 0, 127})); annotation( Diagram(graphics = {Rectangle(origin = {56, -70}, fillColor = {143, 240, 164}, fillPattern = FillPattern.Solid, extent = {{-52, 166}, {52, -166}}), Text(origin = {53, 87}, extent = {{-27, 9}, {27, -9}}, textString = "Observers"), Rectangle(origin = {-127, 0}, fillColor = {255, 190, 111}, fillPattern = FillPattern.Solid, extent = {{-67, 96}, {67, -96}}), Text(origin = {-131, 87}, extent = {{-35, 7}, {35, -7}}, textString = "Scenarios")}, coordinateSystem(extent = {{-200, 100}, {260, -240}})), - Icon(coordinateSystem(extent = {{-200, -300}, {260, 100}})), + Icon(coordinateSystem(extent = {{-200, 100}, {280, -300}}), graphics = {Rectangle(origin = {39, -104}, fillColor = {255, 255, 255}, fillPattern = FillPattern.Solid, extent = {{-241, 204}, {241, -196}}), Text(origin = {70, -38}, extent = {{-14, -102}, {-96, -2}}, textString = "%name")}), experiment(StartTime = 0, StopTime = 1000, Tolerance = 1e-06, Interval = 2)); end Reqs_sri_CRML_externals; diff --git a/src/test/resources/verificationModels/use-cases/ics_educational/Reqs_sri_CRML_verif.mo b/src/test/resources/verificationModels/use-cases/ics_educational/Reqs_sri_CRML_verif.mo index 69305f3..9e4412a 100644 --- a/src/test/resources/verificationModels/use-cases/ics_educational/Reqs_sri_CRML_verif.mo +++ b/src/test/resources/verificationModels/use-cases/ics_educational/Reqs_sri_CRML_verif.mo @@ -1,8 +1,6 @@ -within cooling_system.Verification; - model Reqs_sri_CRML_verif Reqs_sri_CRML_externals externals annotation( - Placement(transformation(origin = {-206, 40}, extent = {{-23, -20}, {23, 20}}))); + Placement(transformation(origin = {-216, 20}, extent = {{-23, -20}, {23, 20}}))); inner CRML.TimeLocators.Continuous.Master master annotation( Placement(transformation(origin = {-392, 168}, extent = {{232, -228}, {252, -208}}))); CRML.Blocks.Logical.BooleanPulse booleanPulse(period = 1000, startTime = 10, width = 980) annotation( @@ -10,9 +8,9 @@ model Reqs_sri_CRML_verif CRML.Blocks.Logical4.BooleanToBoolean4 booleanToBoolean4_1 annotation( Placement(transformation(origin = {-402, 168}, extent = {{218, -222}, {226, -214}}))); Reqs_sri_CRML reqs annotation( - Placement(transformation(origin = {-130, 4}, extent = {{-14, -13}, {14, 13}}))); + Placement(transformation(origin = {-154, 20}, extent = {{-14, -13}, {14, 13}}))); equation - // Bindings +// Bindings reqs.v1 = externals.v1; reqs.v2 = externals.v2; reqs.pump_in_service1 = externals.pump_in_service1; @@ -21,12 +19,13 @@ equation reqs.flow1 = externals.flow1; reqs.flow2 = externals.flow2; reqs.flow3 = externals.flow3; - reqs.T = externals.T ; + reqs.T = externals.T; connect(booleanPulse.y, booleanToBoolean4_1.u) annotation( Line(points = {{-199, -50}, {-184, -50}}, color = {217, 67, 180})); connect(master.u, booleanToBoolean4_1.y) annotation( Line(points = {{-161, -50}, {-176, -50}}, color = {162, 29, 33})); - -annotation( - Diagram(coordinateSystem(extent = {{-240, 60}, {-140, -60}}))); + annotation( + Diagram(coordinateSystem(extent = {{-240, 60}, {-140, -60}}), graphics), + Icon(graphics = {Rectangle(fillColor = {255, 255, 255}, fillPattern = FillPattern.Solid, extent = {{-100, 100}, {100, -100}}), 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}})}), + experiment(StartTime = 0, StopTime = 1000, Tolerance = 1e-06, Interval = 2)); end Reqs_sri_CRML_verif; diff --git a/src/test/resources/verificationModels/use-cases/ics_educational/lib/SRI_v4_EI/cooling_system/Verification/Reqs_sri_CRML.mo b/src/test/resources/verificationModels/use-cases/ics_educational/lib/SRI_v4_EI/cooling_system/Verification/Reqs_sri_CRML.mo index d95831f..6bc0ae5 100644 --- a/src/test/resources/verificationModels/use-cases/ics_educational/lib/SRI_v4_EI/cooling_system/Verification/Reqs_sri_CRML.mo +++ b/src/test/resources/verificationModels/use-cases/ics_educational/lib/SRI_v4_EI/cooling_system/Verification/Reqs_sri_CRML.mo @@ -2,15 +2,15 @@ within cooling_system.Verification; model Reqs_sri_CRML Modelica.Blocks.Interfaces.RealInput T annotation( - Placement(transformation(origin = {-160, -140}, extent = {{-20, -20}, {20, 20}}), iconTransformation(origin = {-120, -100}, extent = {{-20, -20}, {20, 20}}))); + Placement(transformation(origin = {-160, -140}, extent = {{-20, -20}, {20, 20}}), iconTransformation(origin = {-200, -100}, extent = {{-20, -20}, {20, 20}}))); CRML.ETL.Connectors.Boolean4Output R_speed_all annotation( - Placement(transformation(origin = {140, -20}, extent = {{100, 40}, {120, 60}}), iconTransformation(extent = {{100, 40}, {120, 60}}))); + Placement(transformation(origin = {140, -20}, extent = {{100, 40}, {120, 60}}), iconTransformation(origin = {60, 70}, extent = {{100, 40}, {120, 60}}))); CRML.ETL.Connectors.Boolean4Output R_flow_all annotation( - Placement(transformation(origin = {140, -48}, extent = {{100, 8}, {120, 28}}), iconTransformation(origin = {0, 54}, extent = {{100, -54}, {120, -34}}))); + Placement(transformation(origin = {140, -48}, extent = {{100, 8}, {120, 28}}), iconTransformation(origin = {60, 104}, extent = {{100, -54}, {120, -34}}))); outer CRML.TimeLocators.Continuous.Master master annotation( Placement(transformation(origin = {70, 76}, extent = {{-10, -10}, {10, 10}}))); CRML.ETL.Connectors.Boolean4Output R_T annotation( - Placement(transformation(origin = {140, -148}, extent = {{100, 8}, {120, 28}}), iconTransformation(origin = {0, -12}, extent = {{100, -54}, {120, -34}}))); + Placement(transformation(origin = {140, -148}, extent = {{100, 8}, {120, 28}}), iconTransformation(origin = {60, -16}, extent = {{100, -54}, {120, -34}}))); Verification.Requirements.Req_speed_all_CRML req_speed_all_CRML annotation( Placement(transformation(origin = {-172, -22}, extent = {{212, 42}, {232, 62}}))); Verification.Requirements.Req_flow_all_CRML req_flow_all_CRML annotation( @@ -18,21 +18,21 @@ model Reqs_sri_CRML Verification.Requirements.Req_Tsri_CRML req_Tsri_CRML annotation( Placement(transformation(origin = {-170, 20}, extent = {{210, -158}, {230, -138}}))); Modelica.Blocks.Interfaces.RealInput v1 annotation( - Placement(transformation(origin = {-160, 60}, extent = {{-20, -20}, {20, 20}}), iconTransformation(origin = {-120, 100}, extent = {{-20, -20}, {20, 20}}))); + Placement(transformation(origin = {-160, 60}, extent = {{-20, -20}, {20, 20}}), iconTransformation(origin = {-200, 200}, extent = {{-20, -20}, {20, 20}}))); Modelica.Blocks.Interfaces.RealInput v2 annotation( - Placement(transformation(origin = {-160, 40}, extent = {{-20, -20}, {20, 20}}), iconTransformation(origin = {-120, 80}, extent = {{-20, -20}, {20, 20}}))); + Placement(transformation(origin = {-160, 40}, extent = {{-20, -20}, {20, 20}}), iconTransformation(origin = {-200, 180}, extent = {{-20, -20}, {20, 20}}))); Modelica.Blocks.Interfaces.RealInput flow1 annotation( - Placement(transformation(origin = {-160, -10}, extent = {{-20, -20}, {20, 20}}), iconTransformation(origin = {-120, 20}, extent = {{-20, -20}, {20, 20}}))); + Placement(transformation(origin = {-160, -10}, extent = {{-20, -20}, {20, 20}}), iconTransformation(origin = {-200, 20}, extent = {{-20, -20}, {20, 20}}))); Modelica.Blocks.Interfaces.RealInput flow2 annotation( - Placement(transformation(origin = {-160, -60}, extent = {{-20, -20}, {20, 20}}), iconTransformation(origin = {-120, -20}, extent = {{-20, -20}, {20, 20}}))); + Placement(transformation(origin = {-160, -60}, extent = {{-20, -20}, {20, 20}}), iconTransformation(origin = {-200, -20}, extent = {{-20, -20}, {20, 20}}))); Modelica.Blocks.Interfaces.RealInput flow3 annotation( - Placement(transformation(origin = {-160, -110}, extent = {{-20, -20}, {20, 20}}), iconTransformation(origin = {-120, -60}, extent = {{-20, -20}, {20, 20}}))); + Placement(transformation(origin = {-160, -110}, extent = {{-20, -20}, {20, 20}}), iconTransformation(origin = {-200, -60}, extent = {{-20, -20}, {20, 20}}))); Modelica.Blocks.Interfaces.BooleanInput pump_in_service1 annotation( - Placement(transformation(origin = {-160, 10}, extent = {{-20, -20}, {20, 20}}), iconTransformation(origin = {-120, 40}, extent = {{-20, -20}, {20, 20}}))); + Placement(transformation(origin = {-160, 10}, extent = {{-20, -20}, {20, 20}}), iconTransformation(origin = {-200, 140}, extent = {{-20, -20}, {20, 20}}))); Modelica.Blocks.Interfaces.BooleanInput pump_in_service2 annotation( - Placement(transformation(origin = {-160, -40}, extent = {{-20, -20}, {20, 20}}), iconTransformation(origin = {-120, 0}, extent = {{-20, -20}, {20, 20}}))); + Placement(transformation(origin = {-160, -40}, extent = {{-20, -20}, {20, 20}}), iconTransformation(origin = {-200, 100}, extent = {{-20, -20}, {20, 20}}))); Modelica.Blocks.Interfaces.BooleanInput pump_in_service3 annotation( - Placement(transformation(origin = {-160, -90}, extent = {{-20, -20}, {20, 20}}), iconTransformation(origin = {-120, -40}, extent = {{-20, -20}, {20, 20}}))); + Placement(transformation(origin = {-160, -90}, extent = {{-20, -20}, {20, 20}}), iconTransformation(origin = {-200, 60}, extent = {{-20, -20}, {20, 20}}))); equation connect(R_flow_all, R_flow_all) annotation( Line(points = {{250, -30}, {250, -30}}, color = {162, 29, 33})); @@ -63,6 +63,6 @@ equation connect(req_Tsri_CRML.R_T, R_T) annotation( Line(points = {{58, -134}, {250, -134}, {250, -130}}, color = {162, 29, 33})); annotation( - Icon(graphics = {Rectangle(fillColor = {128, 0, 255}, fillPattern = FillPattern.Solid, extent = {{-100, 100}, {100, -100}}), Text(origin = {-6, 124}, extent = {{-136, 30}, {136, -30}}, textString = "%name")}, coordinateSystem(extent = {{-140, 160}, {140, -100}})), + Icon(graphics = {Rectangle(origin = {-10, 60},fillColor = {128, 0, 255}, fillPattern = FillPattern.Solid, extent = {{-170, 160}, {170, -160}}), Text(origin = {-30, 244}, extent = {{-136, 30}, {136, -30}}, textString = "%name")}, coordinateSystem(extent = {{-180, 220}, {160, -100}})), Diagram(coordinateSystem(extent = {{-180, 80}, {260, -160}}))); end Reqs_sri_CRML; diff --git a/src/test/resources/verificationModels/use-cases/ics_educational/lib/SRI_v4_EI/cooling_system/Verification/Reqs_sri_CRML_externals.mo b/src/test/resources/verificationModels/use-cases/ics_educational/lib/SRI_v4_EI/cooling_system/Verification/Reqs_sri_CRML_externals.mo index 48d7025..e7c894c 100644 --- a/src/test/resources/verificationModels/use-cases/ics_educational/lib/SRI_v4_EI/cooling_system/Verification/Reqs_sri_CRML_externals.mo +++ b/src/test/resources/verificationModels/use-cases/ics_educational/lib/SRI_v4_EI/cooling_system/Verification/Reqs_sri_CRML_externals.mo @@ -61,23 +61,23 @@ model Reqs_sri_CRML_externals Modelica.Blocks.Sources.RealExpression T_output_sf(y = SRI_corrige.EchangeurAPlaques1D2.Tsf) annotation( Placement(transformation(origin = {27, -190}, extent = {{-17, -14}, {17, 14}}))); Modelica.Blocks.Interfaces.RealOutput v1 annotation( - Placement(transformation(origin = {270, 60}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {270, 60}, extent = {{-10, -10}, {10, 10}}))); + Placement(transformation(origin = {270, 60}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {290, 60}, extent = {{-10, -10}, {10, 10}}))); Modelica.Blocks.Interfaces.RealOutput v2 annotation( - Placement(transformation(origin = {270, 40}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {270, 20}, extent = {{-10, -10}, {10, 10}}))); + Placement(transformation(origin = {270, 40}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {290, 20}, extent = {{-10, -10}, {10, 10}}))); Modelica.Blocks.Interfaces.BooleanOutput pump_in_service1 annotation( - Placement(transformation(origin = {270, 10}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {270, -60}, extent = {{-10, -10}, {10, 10}}))); + Placement(transformation(origin = {270, 10}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {290, -60}, extent = {{-10, -10}, {10, 10}}))); Modelica.Blocks.Interfaces.BooleanOutput pump_in_service2 annotation( - Placement(transformation(origin = {270, -46}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {270, -120}, extent = {{-10, -10}, {10, 10}}))); + Placement(transformation(origin = {270, -46}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {290, -120}, extent = {{-10, -10}, {10, 10}}))); Modelica.Blocks.Interfaces.BooleanOutput pump_in_service3 annotation( - Placement(transformation(origin = {270, -100}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {270, -180}, extent = {{-10, -10}, {10, 10}}))); + Placement(transformation(origin = {270, -100}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {290, -180}, extent = {{-10, -10}, {10, 10}}))); Modelica.Blocks.Interfaces.RealOutput flow1 annotation( - Placement(transformation(origin = {270, -12}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {270, -80}, extent = {{-10, -10}, {10, 10}}))); + Placement(transformation(origin = {270, -12}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {290, -80}, extent = {{-10, -10}, {10, 10}}))); Modelica.Blocks.Interfaces.RealOutput flow2 annotation( - Placement(transformation(origin = {270, -70}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {270, -140}, extent = {{-10, -10}, {10, 10}}))); + Placement(transformation(origin = {270, -70}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {290, -140}, extent = {{-10, -10}, {10, 10}}))); Modelica.Blocks.Interfaces.RealOutput flow3 annotation( - Placement(transformation(origin = {270, -130}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {270, -200}, extent = {{-10, -10}, {10, 10}}))); + Placement(transformation(origin = {270, -130}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {290, -200}, extent = {{-10, -10}, {10, 10}}))); Modelica.Blocks.Interfaces.RealOutput T annotation( - Placement(transformation(origin = {270, -200}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {270, -240}, extent = {{-10, -10}, {10, 10}}))); + Placement(transformation(origin = {270, -200}, extent = {{-10, -10}, {10, 10}}), iconTransformation(origin = {290, -240}, extent = {{-10, -10}, {10, 10}}))); equation connect(Q_echangeur_1.y, flowToSpeed.u) annotation( Line(points = {{45.7, 64}, {57.4, 64}, {57.4, 65.2}, {66, 65.2}}, color = {0, 0, 127})); @@ -123,6 +123,6 @@ equation Line(points = {{270, 60}, {178, 60}, {178, 66}, {90, 66}}, color = {0, 0, 127})); annotation( Diagram(graphics = {Rectangle(origin = {56, -70}, fillColor = {143, 240, 164}, fillPattern = FillPattern.Solid, extent = {{-52, 166}, {52, -166}}), Text(origin = {53, 87}, extent = {{-27, 9}, {27, -9}}, textString = "Observers"), Rectangle(origin = {-127, 0}, fillColor = {255, 190, 111}, fillPattern = FillPattern.Solid, extent = {{-67, 96}, {67, -96}}), Text(origin = {-131, 87}, extent = {{-35, 7}, {35, -7}}, textString = "Scenarios")}, coordinateSystem(extent = {{-200, 100}, {260, -240}})), - Icon(coordinateSystem(extent = {{-200, -300}, {260, 100}})), + Icon(coordinateSystem(extent = {{-200, 100}, {280, -300}}), graphics = {Rectangle(origin = {39, -104}, fillColor = {255, 255, 255}, fillPattern = FillPattern.Solid, extent = {{-241, 204}, {241, -196}}), Text(origin = {70, -38}, extent = {{-14, -102}, {-96, -2}}, textString = "%name")}), experiment(StartTime = 0, StopTime = 1000, Tolerance = 1e-06, Interval = 2)); end Reqs_sri_CRML_externals; diff --git a/src/test/resources/verificationModels/use-cases/ics_educational/lib/SRI_v4_EI/cooling_system/Verification/Reqs_sri_CRML_verif.mo b/src/test/resources/verificationModels/use-cases/ics_educational/lib/SRI_v4_EI/cooling_system/Verification/Reqs_sri_CRML_verif.mo index 69305f3..341ea01 100644 --- a/src/test/resources/verificationModels/use-cases/ics_educational/lib/SRI_v4_EI/cooling_system/Verification/Reqs_sri_CRML_verif.mo +++ b/src/test/resources/verificationModels/use-cases/ics_educational/lib/SRI_v4_EI/cooling_system/Verification/Reqs_sri_CRML_verif.mo @@ -2,7 +2,7 @@ within cooling_system.Verification; model Reqs_sri_CRML_verif Reqs_sri_CRML_externals externals annotation( - Placement(transformation(origin = {-206, 40}, extent = {{-23, -20}, {23, 20}}))); + Placement(transformation(origin = {-216, 20}, extent = {{-23, -20}, {23, 20}}))); inner CRML.TimeLocators.Continuous.Master master annotation( Placement(transformation(origin = {-392, 168}, extent = {{232, -228}, {252, -208}}))); CRML.Blocks.Logical.BooleanPulse booleanPulse(period = 1000, startTime = 10, width = 980) annotation( @@ -10,9 +10,9 @@ model Reqs_sri_CRML_verif CRML.Blocks.Logical4.BooleanToBoolean4 booleanToBoolean4_1 annotation( Placement(transformation(origin = {-402, 168}, extent = {{218, -222}, {226, -214}}))); Reqs_sri_CRML reqs annotation( - Placement(transformation(origin = {-130, 4}, extent = {{-14, -13}, {14, 13}}))); + Placement(transformation(origin = {-154, 20}, extent = {{-14, -13}, {14, 13}}))); equation - // Bindings +// Bindings reqs.v1 = externals.v1; reqs.v2 = externals.v2; reqs.pump_in_service1 = externals.pump_in_service1; @@ -21,12 +21,13 @@ equation reqs.flow1 = externals.flow1; reqs.flow2 = externals.flow2; reqs.flow3 = externals.flow3; - reqs.T = externals.T ; + reqs.T = externals.T; connect(booleanPulse.y, booleanToBoolean4_1.u) annotation( Line(points = {{-199, -50}, {-184, -50}}, color = {217, 67, 180})); connect(master.u, booleanToBoolean4_1.y) annotation( Line(points = {{-161, -50}, {-176, -50}}, color = {162, 29, 33})); - -annotation( - Diagram(coordinateSystem(extent = {{-240, 60}, {-140, -60}}))); + annotation( + Diagram(coordinateSystem(extent = {{-240, 60}, {-140, -60}}), graphics), + Icon(graphics = {Rectangle(fillColor = {255, 255, 255}, fillPattern = FillPattern.Solid, extent = {{-100, 100}, {100, -100}}), 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}})}), + experiment(StartTime = 0, StopTime = 1000, Tolerance = 1e-06, Interval = 2)); end Reqs_sri_CRML_verif; diff --git a/src/test/resources/verificationModels/use-cases/ics_educational/lib/SRI_v4_EI/cooling_system/Verification/package.order b/src/test/resources/verificationModels/use-cases/ics_educational/lib/SRI_v4_EI/cooling_system/Verification/package.order index b9180c6..432f78a 100644 --- a/src/test/resources/verificationModels/use-cases/ics_educational/lib/SRI_v4_EI/cooling_system/Verification/package.order +++ b/src/test/resources/verificationModels/use-cases/ics_educational/lib/SRI_v4_EI/cooling_system/Verification/package.order @@ -1,8 +1,8 @@ Scenarios Observers Requirements -Reqs_sri_CRML Verif Verif_corrige -Reqs_sri_CRML_verif +Reqs_sri_CRML Reqs_sri_CRML_externals +Reqs_sri_CRML_verif