workcell.pepa
// This file is an input file for the PEPA Eclipse Plug-ina1_T1 = 1.16083347843752;
a1_T2 = 0.63318189732955;
xi = 100;
r_1 = 0.232774674115456;
r_2 = 2.17256362507759;
a2_T1 = 0.648735319687359;
r_3 = 0.407355679702048;
a2_T2 = 1.63530586106703;
a2_T3 = 0.464475281577689;
r_4 = 0.724187875025864;
f_T = 0.503524672708963;
f_B = 0.857632933104631;
t_T = 0.353232073472271;
p_b2m = 0.965250965250965;
p_m2t2b = 0.317258883248731;
d_B = 0.713266761768902;
d_T = 0.34965034965035;
c_H = 0.141924496168039;
c_V = 0.372300819061802;
Robot =
(ready_to_pick,infty).BlankFromTable;
BlankFromTable =
(pick_posn_arm_1,a1_T1).(ready_to_pick,xi).
(safe_posn_arm_1,a1_T2).Rot_2Press;
Rot_2Press =
(at_press_arm_2,r_2).UnloadPress;
UnloadPress =
(unload_blank,infty).(pick_posn_arm_2,a2_T1).Rot_2Belt;
Rot_2Belt =
(unload_blank, xi).(at_belt_arm_2,r_3).BlankToDBelt;
BlankToDBelt =
(dbelt_ready,infty).(put_posn_arm_2,a2_T2).
(dbelt_ready,xi).(safe_posn_arm_2,a2_T3).Rot_1Press;
Rot_1Press = (at_press_arm_1,r_4).LoadPress;
LoadPress =
(load_blank,infty).(put_posn_arm_1,a1_T2).
(safe_posn_arm_1,a1_T2).(load_blank,xi).Rot_1Table;
Rot_1Table = (at_table_arm_1,r_1).Robot;
Belt =
(b_sensor_On, f_T).(ready_to_put, infty).
(b_sensor_Off, f_B).(ready_to_put, xi).Belt;
Table =
(move_table, t_T).(ready_to_put, xi).(ready_to_put, infty).
(move_table, t_T).(ready_to_pick, xi).(ready_to_pick, infty).Table ;
Press =
(unload_blank, xi).(unload_blank, infty).(move_press, p_b2m).
(load_blank, xi).(load_blank, infty).(move_press, p_m2t2b).Press ;
DBelt_1 =
(dbelt_ready, xi).(dbelt_ready, infty).(delay, d_B).DBelt_2;
DBelt_2 =
(dbelt_ready, xi).(dbelt_ready, infty).(delay, d_B).DBelt_3 +
(d_Sensor_On,d_T).(d_Sensor_Off,d_B).(blank_ready,xi).(blank_ready,infty).DBelt_1;
DBelt_3 =
(d_Sensor_On,d_T).(d_Sensor_Off,d_B).
(blank_ready,xi).(blank_ready,infty).DBelt_2;
Crane =
(mag_u, c_V).(over_belt2, c_H).(blank_ready, infty).
(mag_d, c_V).(blank_ready,xi).(mag_u, c_V).
(over_belt1, c_H).(can_accept, xi).(mag_d, c_V).Crane ;
// The following expression invokes instances of the PEPA components
// which were defined above. In order to make models with larger
// state spaces try altering the term `Pressa to `(Press <> Press)'
// or change other components to be two copies in parallel similarly.
Robot <ready_to_pick, unload_blank, dbelt_ready, load_blank>
((Belt <ready_to_put> Table) <> Press <> (DBelt_1 <blank_ready> Crane))