Commit 049b1f11 authored by Ferdie Reijnen's avatar Ferdie Reijnen
Browse files

Merge branch '364-cif-data-based-synthesis-performance-test-models' into 'develop'

#364 CIF data-based synthesis performance test models

See merge request !317
parents 6ff666c3 b7fae404
Pipeline #4130 passed with stage
in 0 seconds
...@@ -59,7 +59,7 @@ For each change to the CIF language, follow these steps: ...@@ -59,7 +59,7 @@ For each change to the CIF language, follow these steps:
* Update type checker (`org.eclipse.escet.cif.typechecker`). * Update type checker (`org.eclipse.escet.cif.typechecker`).
** Add new constraints to the error and problem messages (`ErrMsg.java`). ** Add new constraints to the error and problem messages (`ErrMsg.java`).
** Verify the implementation by running `chk.bash`. ** Verify the implementation by running `chk.bash`.
* Update example models for changed syntax and constraints (`org.eclipse.escet.cif.examples`). * Update example and benchmark models for changed syntax and constraints (`org.eclipse.escet.cif.examples`).
* Update pretty printer including set of keywords (`org.eclipse.escet.cif.prettyprinter`). * Update pretty printer including set of keywords (`org.eclipse.escet.cif.prettyprinter`).
* Update common methods (`org.eclipse.escet.cif.common`). * Update common methods (`org.eclipse.escet.cif.common`).
* Update CIF to CIF transformations and other tools. * Update CIF to CIF transformations and other tools.
......
...@@ -18,12 +18,12 @@ indexterm:[examples] ...@@ -18,12 +18,12 @@ indexterm:[examples]
[[examples-chapter-index]] [[examples-chapter-index]]
== CIF examples == CIF examples
CIF ships with several examples. CIF ships with several examples and benchmark models.
To obtain these examples, follow these steps: To obtain these examples, follow these steps:
* Start the Eclipse ESCET IDE. * Start the Eclipse ESCET IDE.
* Click menu:File[New > Example...]. * Click menu:File[New > Example...].
* Select _CIF Examples_ and click btn:[Next]. * Select _CIF Examples_ or _CIF Benchmarks_ and click btn:[Next].
* Choose the name of the new project that will be created. * Choose the name of the new project that will be created.
* Choose a location for the new project, on your hard disk. * Choose a location for the new project, on your hard disk.
If you leave the _Use default location_ option enabled, the new project will be created in workspace directory. If you leave the _Use default location_ option enabled, the new project will be created in workspace directory.
......
//////////////////////////////////////////////////////////////////////////////
// Copyright (c) 2022 Contributors to the Eclipse Foundation
//
// See the NOTICE file(s) distributed with this work for additional
// information regarding copyright ownership.
//
// This program and the accompanying materials are made available
// under the terms of the MIT License which is available at
// https://opensource.org/licenses/MIT
//
// SPDX-License-Identifier: MIT
//////////////////////////////////////////////////////////////////////////////
Model source: Ferdie Reijnen, Martijn Goorden, Joanna van de Mortel-Fronczak, Michel Reniers and Jacobus Rooda,
"Application of Dependency Structure Matrices and Multilevel Synthesis to a Production Line" In: Proceedings of the IEEE
Conference on Control Technology and Applications, pages 458-464, 2018, doi: https://doi.org/10.1109/CCTA.2018.8511449.
Model repository: https://github.com/ffhreijnen/CCTAProductionLine.
//////////////////////////////////////////////////////////////////////////////
// Copyright (c) 2018, 2022 Contributors to the Eclipse Foundation
//
// See the NOTICE file(s) distributed with this work for additional
// information regarding copyright ownership.
//
// This program and the accompanying materials are made available
// under the terms of the MIT License which is available at
// https://opensource.org/licenses/MIT
//
// SPDX-License-Identifier: MIT
//////////////////////////////////////////////////////////////////////////////
import "stations12.cif";
import "stations34.cif";
import "station5.cif";
import "station6.cif";
//Testing - Handling combination
// Elevator is only allowed to ascend when it is safe.
requirement {A_elevator_up.c_on, A_elevator_down.c_off} needs S_transfer_athalfway.On;
requirement {A_elevator_up.c_on, A_elevator_down.c_off} needs S_reflective.Off;
// Transfer is allowed to move towards droppos when:
// - Currently at drop.
// - Currently at middle, testing is safe, testing is empty.
requirement A_transfer2droppos.c_on needs
(S_transfer_atpickup.On) or
(S_transfer_athalfway.On and S_elevator_down.On and S_capacitive.Off);
// Transfer is allowed to stop move towards droppos when:
// - Currently at droppos.
// - Currently at middle, testing is unsafe or non empty.
requirement A_transfer2droppos.c_off needs
(S_transfer_atdrop.On) or
(S_transfer_athalfway.On and (S_elevator_down.Off or S_capacitive.On));
// Buffer - Processing combination
// The separator is only allowed to release a product when the processing station has a free space.
requirement A_separator.c_off needs S_atinput.Off;
// The separator is only allowed to release a product when the processing station is in a valid position.
requirement A_separator.c_off needs S_turntable.On;
// Processing - Sorting combination
// Eject can enable when the sorting has sorted the last product.
requirement A_eject.c_off needs A_conveyer.Off;
// Testing - Buffering combination
// The air slide can only be enabled when the buffering station is not full.
requirement A_airslide.c_on needs S_atin.Off;
//////////////////////////////////////////////////////////////////////////////
// Copyright (c) 2018, 2022 Contributors to the Eclipse Foundation
//
// See the NOTICE file(s) distributed with this work for additional
// information regarding copyright ownership.
//
// This program and the accompanying materials are made available
// under the terms of the MIT License which is available at
// https://opensource.org/licenses/MIT
//
// SPDX-License-Identifier: MIT
//////////////////////////////////////////////////////////////////////////////
plant def TwoStateSensor(alg bool InitialOn):
uncontrollable u_on, u_off;
location On:
initial InitialOn;
marked InitialOn;
edge u_off goto Off;
location Off:
initial not InitialOn;
marked not InitialOn;
edge u_on goto On;
end
plant def TwoStateActuator(alg bool InitialOn):
controllable c_on, c_off;
location On:
initial InitialOn;
marked InitialOn;
edge c_off goto Off;
location Off:
initial not InitialOn;
marked not InitialOn;
edge c_on goto On;
end
plant def TwoStateActuator2(alg bool InitialOn):
controllable c_on, c_off;
location On:
initial InitialOn;
marked;
edge c_off goto Off;
location Off:
initial not InitialOn;
marked;
edge c_on goto On;
end
plant def Button():
uncontrollable u_push, u_release;
location Released:
initial; marked;
edge u_push goto Pushed;
location Pushed:
edge u_release goto Released;
end
//////////////////////////////////////////////////////////////////////////////
// Copyright (c) 2018, 2022 Contributors to the Eclipse Foundation
//
// See the NOTICE file(s) distributed with this work for additional
// information regarding copyright ownership.
//
// This program and the accompanying materials are made available
// under the terms of the MIT License which is available at
// https://opensource.org/licenses/MIT
//
// SPDX-License-Identifier: MIT
//////////////////////////////////////////////////////////////////////////////
import "definitions.cif";
// PROCESSING
// Plant:
// Sensors
S_atinput : TwoStateSensor(false);
S_attest : TwoStateSensor(false);
S_atdrill : TwoStateSensor(false);
S_atexit : TwoStateSensor(false);
S_clamp : TwoStateSensor(false);
S_test_ok : TwoStateSensor(false);
S_drill_up : TwoStateSensor(true);
S_drill_down : TwoStateSensor(false);
S_turntable : TwoStateSensor(true);
S_Pinitialized : TwoStateSensor(false);
// Actuators
A_drill : TwoStateActuator(false);
A_turntable : TwoStateActuator(false);
A_drilldown : TwoStateActuator(false);
A_drillup : TwoStateActuator(true);
A_clamp : TwoStateActuator(false);
A_tester : TwoStateActuator(false);
A_eject : TwoStateActuator(false);
plant PTimer:
controllable c_on, c_reset; uncontrollable u_timeout;
location Off:
initial; marked;
edge c_on goto Running;
location Running:
edge u_timeout goto Timeout;
edge c_reset goto Off;
location Timeout:
edge c_reset goto Off;
end
// Dynamics
// Drill dynamics, sensors are mutually exclusive.
plant S_drill_up.u_on needs S_drill_down.Off;
plant S_drill_down.u_on needs S_drill_up.Off;
// Requirements
// Initialization
// The actuators can only activate when the station is initialized.
requirement {A_drill.c_on, A_drill.c_off, A_turntable.c_on, A_turntable.c_off,
A_drilldown.c_on, A_drillup.c_off, A_clamp.c_on, A_clamp.c_off,
A_tester.c_on, A_tester.c_off, A_eject.c_on, A_eject.c_off, PTimer.c_on, PTimer.c_reset}
needs S_Pinitialized.On;
// A timer that makes sure that the turntable is at stand-still for x seconds, such that sensor measurements can be
// performed.
requirement PTimer.c_on needs S_turntable.On;
requirement PTimer.c_reset needs S_turntable.Off;
// Turn table
// The turn table is only allowed to enable at a valid positions.
requirement A_turntable.c_on needs S_turntable.On;
requirement A_turntable.c_on needs PTimer.Timeout;
// The turntable actuator can be disabled when the turntable leaves the valid position.
requirement A_turntable.c_off needs S_turntable.Off;
// The turntable can only rotate when the other actuators are in a safe position.
requirement A_turntable.c_on needs S_drill_up.On;
requirement A_turntable.c_on needs S_clamp.Off;
requirement A_turntable.c_on needs A_eject.Off;
requirement A_turntable.c_on needs A_drill.Off;
requirement A_turntable.c_on needs A_tester.Off;
// The turntable can only rotate when a new product has entered.
requirement A_turntable.c_on needs S_atinput.On;
// Tester
// The tester is only allowed to enable when the turntable is at standstill.
requirement A_tester.c_on needs S_turntable.On;
requirement A_tester.c_on needs A_turntable.Off;
requirement A_tester.c_on needs PTimer.Timeout;
// The tester is only allowed to enable when there is a product.
requirement A_tester.c_on needs S_attest.On;
// The tester can be disabled once the measurement is completed.
requirement A_tester.c_off needs S_test_ok.On;
// If there is a product at the testing location, it should be processed, before the turntable is activated again.
requirement Tester:
location One:
initial; marked;
edge A_turntable.c_on;
edge A_tester.c_on goto Two;
location Two:
edge A_tester.c_off goto Three;
location Three:
edge A_turntable.c_on goto One;
end
// Clamp
// The clamp is only allowed to enable when the turn table is at standstill.
requirement A_clamp.c_on needs S_turntable.On;
requirement A_clamp.c_on needs A_turntable.Off;
requirement A_clamp.c_on needs PTimer.Timeout;
// The clamp is only allowed to enable when a product is available.
requirement A_clamp.c_on needs S_atdrill.On;
// The clamp can only be released when the drill is up.
requirement A_clamp.c_off needs S_drill_up.On;
// The clamp can only be released when the drill is disabled.
requirement A_clamp.c_off needs A_drill.Off;
// Drill
// The drill is only allowed to enable at the upper position.
requirement A_drill.c_on needs S_drill_up.On;
// The drill is only allowed to activate when there is a clamped product.
requirement A_drill.c_on needs S_clamp.On;
// The drill is only allowed to disable at the upper position.
requirement A_drill.c_off needs S_drill_up.On;
// Drill movement
// The drill is only allowed to descend when it is fully ascended.
requirement {A_drillup.c_off, A_drilldown.c_on} needs S_drill_up.On;
// The drill is only allowed to ascend when it is fully descended.
requirement {A_drillup.c_on, A_drilldown.c_off} needs S_drill_down.On;
// The cycle at the drilling location should be as follows:
// Clamp product, activate drill, descend, ascend, deactivate drill, release product.
requirement ClampDrill:
location One:
initial; marked;
edge A_turntable.c_on;
edge A_clamp.c_on goto Two;
location Two:
edge A_drill.c_on goto Three;
location Three:
edge A_drillup.c_off goto Four;
location Four:
edge A_drilldown.c_on goto Five;
location Five:
edge A_drilldown.c_off goto Six;
location Six:
edge A_drillup.c_on goto seven;
location Seven:
edge A_drill.c_off goto Eight;
location Eight:
edge A_clamp.c_off goto Nine;
location Nine:
edge A_turntable.c_on goto One;
end
// Eject
// The ejector are only allowed to enable when the turntable is at stand-still.
requirement A_eject.c_on needs S_turntable.On;
requirement A_eject.c_on needs A_turntable.Off;
requirement A_eject.c_on needs PTimer.Timeout;
// The ejector is only allowed to enable when there is a product.
requirement A_eject.c_on needs S_atexit.On;
// The ejector can be retracted if the product is removed.
requirement A_eject.c_off needs S_atexit.Off;
//////////////////////////////////////////////////////////////////////////////
// Copyright (c) 2018, 2022 Contributors to the Eclipse Foundation
//
// See the NOTICE file(s) distributed with this work for additional
// information regarding copyright ownership.
//
// This program and the accompanying materials are made available
// under the terms of the MIT License which is available at
// https://opensource.org/licenses/MIT
//
// SPDX-License-Identifier: MIT
//////////////////////////////////////////////////////////////////////////////
import "definitions.cif";
// SORTING
// Plant:
// Sensors
S_product : TwoStateSensor(false);
S_inductive : TwoStateSensor(false);
S_optical : TwoStateSensor(false);
S_slidefull : TwoStateSensor(false);
S_gate1_opened : TwoStateSensor(true);
S_gate1_closed : TwoStateSensor(false);
S_gate2_opened : TwoStateSensor(true);
S_gate2_closed : TwoStateSensor(false);
S_Sinitialized : TwoStateSensor(false);
// Actuators
A_conveyer : TwoStateActuator(false);
A_gate1 : TwoStateActuator(false);
A_gate2 : TwoStateActuator(false);
A_stopperretract : TwoStateActuator(false);
plant STimer:
controllable c_on, c_reset; uncontrollable u_timeout;
location Off:
initial; marked;
edge c_on goto Running;
location Running:
edge u_timeout goto Timeout;
edge c_reset goto Off;
location Timeout:
edge c_reset goto Off;
end
// Dynamics
// Gate1 dynamics, sensors are mutually exclusive.
plant S_gate1_opened.u_on needs S_gate1_closed.Off;
plant S_gate1_closed.u_on needs S_gate1_opened.Off;
// Gate2 dynamics, sensors are mutually exclusive.
plant S_gate2_opened.u_on needs S_gate2_closed.Off;
plant S_gate2_closed.u_on needs S_gate2_opened.Off;
// Requirements
// Initialization
// Actuators are only allowed to enable/disable when the station is initialized.
requirement {A_conveyer.c_on, A_conveyer.c_off, A_gate1.c_on, A_gate1.c_off,
A_gate2.c_on, A_gate2.c_off, A_stopperretract.c_on, A_stopperretract.c_off}
needs S_Sinitialized.On;
// Timer that time out after x seconds, to make sure that a product is identified.
requirement STimer.c_on needs S_product.On;
requirement STimer.c_reset needs S_slidefull.On;
// Conveyer
// Conveyer is allowed to enable when there is a product.
requirement A_conveyer.c_on needs S_product.On;
// Conveyer is allowed to disable when product is in the slide.
requirement A_conveyer.c_off needs S_slidefull.On;
// Stopper
// Stopper is allowed to retract when:
// - There is a product that has been identified (Timeout).
// - The slide is not full.
requirement A_stopperretract.c_on needs STimer.Timeout;
requirement A_stopperretract.c_on needs S_slidefull.Off;
// Stopper is allowed to extend when the product entered the buffer.
requirement A_stopperretract.c_off needs S_slidefull.On;
// Gates
// The gates are only allowed to close when they are fully open.
requirement A_gate1.c_on needs S_gate1_opened.On;
requirement A_gate2.c_on needs S_gate2_opened.On;
// The gates are only allowed to open when they are fully closed.
requirement A_gate1.c_off needs S_gate1_closed.On;
requirement A_gate2.c_off needs S_gate2_closed.On;
// Gate1 is only allowed to close when there is a plastic product before the stopper.
requirement A_gate1.c_on needs S_optical.On;
requirement A_gate1.c_on needs S_inductive.Off;
requirement A_gate1.c_on needs STimer.Timeout;
// Gate1 is only allowed to open when product entered the buffer.
requirement A_gate1.c_off needs S_slidefull.On;
// Gate2 is only allowed to close when there is a metal product before the stopper.
requirement A_gate2.c_on needs S_optical.On;
requirement A_gate2.c_on needs S_inductive.On;
requirement A_gate2.c_on needs STimer.Timeout;
// Gate2 is only allowed to open when product entered the buffer.
requirement A_gate2.c_off needs S_slidefull.On;
// Gate1 and 2 are only allowed to actuate when the stopper is closed.
requirement {A_gate1.c_on, A_gate1.c_off} needs A_stopperretract.Off;
requirement {A_gate2.c_on, A_gate2.c_off} needs A_stopperretract.Off;
//////////////////////////////////////////////////////////////////////////////
// Copyright (c) 2018, 2022 Contributors to the Eclipse Foundation
//
// See the NOTICE file(s) distributed with this work for additional
// information regarding copyright ownership.
//
// This program and the accompanying materials are made available
// under the terms of the MIT License which is available at
// https://opensource.org/licenses/MIT
//
// SPDX-License-Identifier: MIT
//////////////////////////////////////////////////////////////////////////////
import "definitions.cif";
// DISTRIBUTING
// Plant:
// Sensors
S_product1 : TwoStateSensor(false);
S_product2 : TwoStateSensor(false);
S_product3 : TwoStateSensor(false);
S_pusher1_in : TwoStateSensor(true);
S_pusher1_out : TwoStateSensor(false);
S_stack1_filled : TwoStateSensor(true);
S_pusher2_in : TwoStateSensor(true);
S_pusher2_out : TwoStateSensor(false);
S_stack2_filled : TwoStateSensor(true);
S_pusher3_in : TwoStateSensor(true);
S_pusher3_out : TwoStateSensor(false);
S_stack3_filled : TwoStateSensor(true);
S_Dinitialized : TwoStateSensor(false);
// Actuators
A_pusher1 : TwoStateActuator(false);
A_pusher2 : TwoStateActuator(false);
A_pusher3 : TwoStateActuator(false);
// Dynamics
plant S_pusher1_in.u_on needs S_pusher1_out.Off;
plant S_pusher1_out.u_on needs S_pusher1_in.Off;
plant S_pusher2_in.u_on needs S_pusher2_out.Off;
plant S_pusher2_out.u_on needs S_pusher2_in.Off;
plant S_pusher3_in.u_on needs S_pusher3_out.Off;
plant S_pusher3_out.u_on needs S_pusher3_in.Off;
// Requirements
// Actuators are only allowed to actuate when the station is initialized.
requirement {A_pusher1.c_on, A_pusher1.c_off} needs S_Dinitialized.On;
requirement {A_pusher2.c_on, A_pusher2.c_off} needs S_Dinitialized.On;
requirement {A_pusher3.c_on, A_pusher3.c_off} needs S_Dinitialized.On;
// The Pusher is only allowed to move backwards/out when it is completely in.
requirement A_pusher1.c_on needs S_pusher1_in.On;
requirement A_pusher2.c_on needs S_pusher2_in.On;
requirement A_pusher3.c_on needs S_pusher3_in.On;
// The Pusher is only allowed to move forwards/in when it is completely out.
requirement A_pusher1.c_off needs S_pusher1_out.On;
requirement A_pusher2.c_off needs S_pusher2_out.On;
requirement A_pusher3.c_off needs S_pusher3_out.On;
// The Pusher is only allowed to move backwards/out when the product has been removed.
requirement A_pusher1.c_on needs S_product1.Off;
requirement A_pusher2.c_on needs S_product2.Off;
requirement A_pusher3.c_on needs S_product3.Off;
// The Pusher is only allowed to move forwards/in when there is a product in front of it.
requirement A_pusher1.c_off needs S_stack1_filled.On;
requirement A_pusher2.c_off needs S_stack2_filled.On;
requirement A_pusher3.c_off needs S_stack3_filled.On;
// The Pusher is only allowed to move forward when there is no product at the pickup position.
requirement A_pusher1.c_off needs S_product1.Off;
requirement A_pusher2.c_off needs S_product2.Off;
requirement A_pusher3.c_off needs S_product3.Off;
// HANDLING
// Plant:
// Sensors
S_product4 : TwoStateSensor(false);
S_xpos_at1 : TwoStateSensor(false);
S_xpos_at2 : TwoStateSensor(false);
S_xpos_at3 : TwoStateSensor(false);
S_xpos_atdrop : TwoStateSensor(true);
S_zpos_atup : TwoStateSensor(true);
S_zpos_atdown : TwoStateSensor(false);
S_gripper : TwoStateSensor(false);
S_transfer_atpickup : TwoStateSensor(false);
S_transfer_atdrop : TwoStateSensor(false);
S_transfer_athalfway : TwoStateSensor(true);
S_vacuum : TwoStateSensor(false);
S_Hinitialized : TwoStateSensor(false);
// Actuators
A_x2distributing : TwoStateActuator(true);
A_x2testing : TwoStateActuator(true);
A_zdown : TwoStateActuator(false);
A_gripperclose : TwoStateActuator(false);
A_transfer2pickpos : TwoStateActuator2(false);
A_transfer2droppos : TwoStateActuator2(false);
A_vacuum : TwoStateActuator(false);
A_ejectpulse : TwoStateActuator(false);
// Dynamics
// Xpos dynamics, sensors are mutually exclusive.
plant S_xpos_at1.u_on needs S_xpos_at2.Off and S_xpos_at3.Off and S_xpos_atdrop.Off;
plant S_xpos_at2.u_on needs S_xpos_at1.Off and S_xpos_at3.Off and S_xpos_atdrop.Off;
plant S_xpos_at3.u_on needs S_xpos_at1.Off and S_xpos_at2.Off and S_xpos_atdrop.Off;
plant S_xpos_atdrop.u_on needs S_xpos_at1.Off and S_xpos_at2.Off and S_xpos_at3.Off;
// Zpos dynamics, sensors are mutually exclusive.
plant S_zpos_atup.u_on needs S_zpos_atdown.Off;
plant S_zpos_atdown.u_on needs S_zpos_atup.Off;
// Transfer dynamics, sensors are mutually exclusive.
plant S_transfer_atpickup.u_on needs S_transfer_atdrop.Off and S_transfer_athalfway.Off;
plant S_transfer_atdrop.u_on needs S_transfer_atpickup.Off and S_transfer_athalfway.Off;
plant S_transfer_athalfway.u_on needs S_transfer_atdrop.Off and S_transfer_atpickup.Off;
// Requirements
// Actuators are only allowed to enable/disable when the station is initialized.
requirement {A_x2distributing.c_on, A_x2distributing.c_off, A_x2testing.c_on, A_x2testing.c_off,
A_zdown.c_on, A_zdown.c_off, A_gripperclose.c_on, A_gripperclose.c_off,
A_transfer2pickpos.c_on, A_transfer2pickpos.c_off, A_transfer2droppos.c_on, A_transfer2droppos.c_off,
A_vacuum.c_on, A_vacuum.c_off, A_ejectpulse.c_on, A_ejectpulse.c_off} needs S_Hinitialized.On;
// Gripper Y position:
// The gripper is only allowed to descend when it is fully ascended.
requirement A_zdown.c_on needs S_zpos_atup.On;
// The gripper is only allowed to ascend when it is fully descended.
requirement A_zdown.c_off needs S_zpos_atdown.On;
// The gripper is only allowed to descend when the gripper is at stand-still.
requirement A_zdown.c_on needs A_x2distributing.On and A_x2testing.On;
// The gripper is only allowed to descend when:
// - Is at station 1 while station 1 is filled, and the gripper is empty
// - Is at station 2 while station 2 is filled, and the gripper is empty
// - Is at station 3 while station 3 is filled, and the gripper is empty
// - Is at station 4 while station 4 is empty, and the gripper is filled.
requirement A_zdown.c_on needs
(S_xpos_at1.On and S_product1.On and S_gripper.Off) or
(S_xpos_at2.On and S_product2.On and S_gripper.Off) or
(S_xpos_at3.On and S_product3.On and S_gripper.Off) or
(S_xpos_atdrop.On and S_product4.Off and S_gripper.On);