Commit a1cc0d2f authored by Ferdie Reijnen's avatar Ferdie Reijnen
Browse files

#364 Added CIF FESTO benchmark model.

parent 364665a6
Pipeline #3922 passed with stage
in 0 seconds
//////////////////////////////////////////////////////////////////////////////
// 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
//////////////////////////////////////////////////////////////////////////////
import "stations12.cif";
import "stations34.cif";
import "station5.cif";
import "station6.cif";
//////////////////////////////////////////////////////////////////////////////
// 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
//////////////////////////////////////////////////////////////////////////////
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) 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
// This is a more concise notation of the FSA in Figure 6.
plant S_drill_up.u_on needs S_drill_down.Off;
plant S_drill_down.u_on needs S_drill_up.Off;
// Requirements
// Initialization
// (R1) 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;
// (R4) The turntable actuator can be disabled when the turntable leaves the valid position.
requirement A_turntable.c_off needs S_turntable.Off;
// (R2) 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;
// (R3) The turntable can only rotate when a new product has entered.
requirement A_turntable.c_on needs S_atinput.On;
// Tester
// (R5) 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;
// (R5) The tester is only allowed to enable when there is a product
requirement A_tester.c_on needs S_attest.On;
// (R9) The tester can be disabled once the measurement is completed
requirement A_tester.c_off needs S_test_ok.On;
// (R10) 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
// (R5) 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;
// (R5) The clamp is only allowed to enable when a product is available
requirement A_clamp.c_on needs S_atdrill.On;
// (R6) The clamp can only be released when the drill is up
requirement A_clamp.c_off needs S_drill_up.On;
// (R6) The clamp can only be released when the drill is disabled
requirement A_clamp.c_off needs A_drill.Off;
// Dril
// (R11) The cycle at the drilling location should be as follows:
// The drill is only allowed to enable at the upper position
requirement A_drill.c_on needs S_drill_up.On;
// (R7) The drill is only allowed to activate when there is a clamped product.
requirement A_drill.c_on needs S_clamp.On;
// (R11) The cycle at the drilling location should be as follows:
// The drill is only allowed to disable at the upper position
requirement A_drill.c_off needs S_drill_up.On;
// Drill movement
// (R11) The cycle at the drilling location should be as follows:
// 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;
// (R11) The cycle at the drilling location should be as follows:
// 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;
// (R10) / (R11) 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
// (R5) 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;
// (R5) The ejector is only allowed to enable when there is a product
requirement A_eject.c_on needs S_atexit.On;
// (R8) The ejector can be retracted if the product is removed.
requirement A_eject.c_off needs S_atexit.Off;
//////////////////////////////////////////////////////////////////////////////
// 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
//////////////////////////////////////////////////////////////////////////////
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;
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) 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);
// The gripper is only allowed to ascend when:
// - Is at station 1 while the gripper is closed, and a product is detected
// - Is at station 2 while the gripper is closed, and a product is detected
// - Is at station 3 while the gripper is closed, and a product is detected
// - Is at station 4 while the gripper is open.
requirement A_zdown.c_off needs
(S_xpos_at1.On and A_gripperclose.On and S_gripper.On) or // Not sure if product is not detected when gripper is open
(S_xpos_at2.On and A_gripperclose.On and S_gripper.On) or
(S_xpos_at3.On and A_gripperclose.On and S_gripper.On) or
(S_xpos_atdrop.On and A_gripperclose.Off);
// Griper Open/Close:
// Gripper is only allowed to close/open when it is down
requirement {A_gripperclose.c_on, A_gripperclose.c_off} needs S_zpos_atdown.On;
// Gripper is only allowed to close at station 1, 2 or 3;
requirement A_gripperclose.c_on needs S_xpos_at1.On or S_xpos_at2.On or S_xpos_at3.On;
// Gripper is only allowed to open at station 4;
requirement A_gripperclose.c_off needs S_xpos_atdrop.On;
// Gripper X position:
// Gripper is only allowed to move in x when it is fully ascended
requirement {A_x2distributing.c_off, A_x2testing.c_off} needs S_zpos_atup.On;
// Gripper is never allowed to have both actuators off, rest position is both on
requirement A_x2distributing.c_off needs A_x2testing.On;
requirement A_x2testing.c_off needs A_x2distributing.On;
// Control strategy:
// - Wait at drop until either 1, 2 or 3 is filled. Priority 3 > 2 > 1
// Assumptions:
// - Products at 3, 2, and 1 are never removed
// - Whenever the gripper starts moving towards handling, it stops at the first filled position.
// - Lead time is not important, dropper does not have to move for the transfer unit
// Gripper is allowed to move to the dist when
// - currently at drop with no product, (to make room for transfer).
// - currently at 3 with no product, 3 empty, and 2 or 3 filled
// - currently at 2 with no product, 2 empty, and 1 filled
requirement A_x2testing.c_off needs
(S_xpos_atdrop.On and S_gripper.Off) or
(S_xpos_at3.On and S_gripper.Off and (S_product1.On or S_product2.On) and S_product3.Off) or
(S_xpos_at2.On and S_gripper.Off and S_product1.On and S_product2.Off);
// Gripper is allowed to stop when moving to dist when
// - currently at 3 with 3 filled;
// - currently at 3 with 1 and 2 empty;
// - currently at 2 with 2 filled;
// - currently at 1; Moving beyond this point is dangerous!
requirement A_x2testing.c_on needs
(S_xpos_at3.On and S_product3.On) or
(S_xpos_at3.On and S_product2.Off and S_product1.Off) or
(S_xpos_at2.On and S_product2.On) or
(S_xpos_at1.On);
// Gripper is allowed to move to test when
// - currently at 1 with a product
// - currently at 2 with a product
// - currently at 3 with a product and the transfer is in a safe position
requirement A_x2distributing.c_off needs
(S_xpos_at1.On and S_gripper.On) or
(S_xpos_at2.On and S_gripper.On) or
(S_xpos_at3.On and S_gripper.On and S_product4.Off and S_transfer_athalfway.On);
// Gripper is allowed to stop when moving to test when
// - currently at 3 while the transfer is at a dangerous position
// - currently at 3 while 4 is filled;
// - currently at drop; Moving beyond this point is dangerous!
requirement A_x2distributing.c_on needs
(S_xpos_at3.On and S_transfer_athalfway.Off) or