Commit 199c6b8f authored by Ferdie Reijnen's avatar Ferdie Reijnen
Browse files

#364 Updated FESTO model.

parent a1cc0d2f
Pipeline #3960 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
//////////////////////////////////////////////////////////////////////////////
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) 2022 Contributors to the Eclipse Foundation
// Copyright (c) 2018, 2022 Contributors to the Eclipse Foundation
//
// See the NOTICE file(s) distributed with this work for additional
// information regarding copyright ownership.
......@@ -15,3 +15,41 @@ 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;
\ No newline at end of file
//////////////////////////////////////////////////////////////////////////////
// Copyright (c) 2022 Contributors to the Eclipse Foundation
// Copyright (c) 2018, 2022 Contributors to the Eclipse Foundation
//
// See the NOTICE file(s) distributed with this work for additional
// information regarding copyright ownership.
......
//////////////////////////////////////////////////////////////////////////////
// Copyright (c) 2022 Contributors to the Eclipse Foundation
// Copyright (c) 2018, 2022 Contributors to the Eclipse Foundation
//
// See the NOTICE file(s) distributed with this work for additional
// information regarding copyright ownership.
......@@ -17,171 +17,166 @@ import "definitions.cif";
// 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);
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);
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;
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.
// 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
// (R1) The actuators can only activate when the station is initialized.
// 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
// 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
// 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.
// 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
// 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.
// 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
// 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
// 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
// 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
// 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;
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
// 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
// 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
// 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
// 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
// Drill
// 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.
// 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
// 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
// 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
// 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
// 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;
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;
// 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
// 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.
// 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
// Copyright (c) 2018, 2022 Contributors to the Eclipse Foundation
//
// See the NOTICE file(s) distributed with this work for additional
// information regarding copyright ownership.
......@@ -17,15 +17,15 @@ import "definitions.cif";
// 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);
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);
......@@ -34,28 +34,29 @@ 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;
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
// 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
// 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;
......@@ -65,49 +66,49 @@ 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
// 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
// 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
// - 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
// 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
// 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
// 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
// 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
// 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
// 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
// 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
// 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
// Copyright (c) 2018, 2022 Contributors to the Eclipse Foundation
//
// See the NOTICE file(s) distributed with this work for additional
// information regarding copyright ownership.
......@@ -20,25 +20,21 @@ import "definitions.cif";
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);
A_pusher1 : TwoStateActuator(false);
A_pusher2 : TwoStateActuator(false);
A_pusher3 : TwoStateActuator(false);
// Dynamics
plant S_pusher1_in.u_on needs S_pusher1_out.Off;
......@@ -51,17 +47,17 @@ 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
// 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
// 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
// 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;
......@@ -76,7 +72,7 @@ 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
// 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;
......@@ -87,57 +83,47 @@ requirement A_pusher3.c_off needs S_product3.Off;
// 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);
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
// 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
// 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
// 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
// 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,
......@@ -145,13 +131,13 @@ requirement {A_x2distributing.c_on, A_x2distributing.c_off, A_x2testing.c_on, A_
// Gripper Y position:
// The gripper is only allowed to descend when it is fully ascended
// 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
// 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
// The gripper is only allowed to descend when the gripper is at stand-still.