-- NAS model as described in Tino Teige, Andreas Eggers, Martin Fränzle, -- "Constraint-Based Analysis of Concurrent Probabilistic Hybrid Systems: An -- Application to Networked Automation Systems, Nonlinear Analysis: Hybrid -- Systems, 5(2):343-366, 2011. DECL -- Scale of model: -- 1 length unit = 0.01 mm. -- 1 time unit = 1 ms. -- Environment parameters. define START_POS = 1000; define MIN_POS = -300000; define POS_SENSOR_A = 699; define POS_SENSOR_B = 470; define NORMAL_SPEED = 24; define SLOW_SPEED = 4; define DECELARATE_A = 2; define DECELARATE_B = 4; define DELAY_NETWORK1 = 1; define DELAY_NETWORK2 = 2; define PLC_IO_CYCLE = 10; define PLC_CYCLE = 7; -- Gives the maximum time of whole model. define MAX_TIME = 1000000000; define MAX_TIME_STEP = 1000; define MIN_TIME_STEP = 1; -- Disabling value for quantified variables. define OFF = -1; -- Safe interval representation of 1/24. define ONE_BY_24_LB = 0.04166666; define ONE_BY_24_UB = 0.04166667; -- Safe interval representation of 1/7. define ONE_BY_7_LB = 0.14285714; define ONE_BY_7_UB = 0.14285715; boole initialized; float [0, MAX_TIME] time; float [0, MAX_TIME_STEP] dt; -- Object. boole obj_preA; boole obj_betwAB; boole obj_postB; float [MIN_POS, START_POS] obj_pos; boole obj_sA_reached; boole obj_sB_reached; float [0, MAX_TIME] obj_next_event; float [-1, MAX_TIME_STEP] obj_step; int [-1, MAX_TIME_STEP] obj_step_int; boole obj_next_event_now; -- Transport unit. boole tu_init; boole tu_decA; boole tu_slowspeed; boole tu_decB; boole tu_stop; float [0, NORMAL_SPEED] tu_speed; float [0, DECELARATE_B] tu_dec; float [0, MAX_TIME] tu_next_event; float [-1, MAX_TIME_STEP] tu_step; int [-1, MAX_TIME_STEP] tu_step_int; boole tu_next_event_now; -- Network sensor data. -- Network sA. boole net_sA_init; boole net_sA_send; boole net_sA_compl; float [0, MAX_TIME] net_sA_next_event; float [-1, MAX_TIME_STEP] net_sA_step; boole net_sA_next_event_now; boole net_sA_stable; -- Network sB. boole net_sB_init; boole net_sB_send; boole net_sB_compl; float [0, MAX_TIME] net_sB_next_event; float [-1, MAX_TIME_STEP] net_sB_step; boole net_sB_next_event_now; boole net_sB_stable; -- Network actuator data. -- Network DECA. boole net_DECA_init; boole net_DECA_send; boole net_DECA_compl; float [0, MAX_TIME] net_DECA_next_event; float [-1, MAX_TIME_STEP] net_DECA_step; boole net_DECA_next_event_now; -- Network DECB. boole net_DECB_init; boole net_DECB_send; boole net_DECB_compl; float [0, MAX_TIME] net_DECB_next_event; float [-1, MAX_TIME_STEP] net_DECB_step; boole net_DECB_next_event_now; -- IO card. -- IO in. boole io_in_sA_ready; -- flag set by IO for PLC boole io_in_sB_ready; -- flag set by IO for PLC float [0, MAX_TIME] io_in_next_event; float [-1, MAX_TIME_STEP] io_in_step; boole io_in_next_event_now; boole io_in_stable; -- IO out. boole io_out_send_DECA; -- flag set by IO for net boole io_out_send_DECB; -- flag set by IO for net float [0, MAX_TIME] io_out_next_event; float [-1, MAX_TIME_STEP] io_out_step; boole io_out_next_event_now; -- PLC. boole plc_init; boole plc_comp_DECA; boole plc_comp_DECB; boole plc_DECA_finished; boole plc_DECB_finished; boole plc_send_DECA; -- flag set by PLC for IO boole plc_send_DECB; -- flag set by PLC for IO float [0, MAX_TIME] plc_next_event; float [-1, MAX_TIME_STEP] plc_step; boole plc_next_event_now; boole plc_stable; INIT !initialized; time = 0; -- Object. obj_preA; !obj_betwAB; !obj_postB; -- obj_pos will be set after a probabilistic choice (and thus in the TRANS -- part but affects the 0th unwinding of obj_pos). -- Determine the point of time when the object reaches sensor A. Then is the -- time of the next event for this object. POS_SENSOR_A = obj_pos - (obj_next_event - time) * tu_speed + 0.5 * (obj_next_event - time)^2 * tu_dec; -- Transport unit. tu_init; !tu_decA; !tu_slowspeed; !tu_decB; !tu_stop; tu_speed = NORMAL_SPEED; tu_dec = 0; tu_next_event = MAX_TIME; -- Network sensor data. -- Network sA. net_sA_init; !net_sA_send; !net_sA_compl; net_sA_next_event = MAX_TIME; -- Network sB. net_sB_init; !net_sB_send; !net_sB_compl; net_sB_next_event = MAX_TIME; -- Network actuator data. -- Network DECA. net_DECA_init; !net_DECA_send; !net_DECA_compl; net_DECA_next_event = MAX_TIME; -- Network DECB. net_DECB_init; !net_DECB_send; !net_DECB_compl; net_DECB_next_event = MAX_TIME; -- IO card. !io_in_sA_ready; !io_in_sB_ready; !io_out_send_DECA; !io_out_send_DECB; -- PLC. plc_init; !plc_comp_DECA; !plc_comp_DECB; !plc_DECA_finished; !plc_DECB_finished; !plc_send_DECA; !plc_send_DECB; DISTR R. prob_init_dist p = [ OFF -> 1, 1 -> [ONE_BY_24_LB,ONE_BY_24_UB], 2 -> [ONE_BY_24_LB,ONE_BY_24_UB], 3 -> [ONE_BY_24_LB,ONE_BY_24_UB], 4 -> [ONE_BY_24_LB,ONE_BY_24_UB], 5 -> [ONE_BY_24_LB,ONE_BY_24_UB], 6 -> [ONE_BY_24_LB,ONE_BY_24_UB], 7 -> [ONE_BY_24_LB,ONE_BY_24_UB], 8 -> [ONE_BY_24_LB,ONE_BY_24_UB], 9 -> [ONE_BY_24_LB,ONE_BY_24_UB], 10 -> [ONE_BY_24_LB,ONE_BY_24_UB], 11 -> [ONE_BY_24_LB,ONE_BY_24_UB], 12 -> [ONE_BY_24_LB,ONE_BY_24_UB], 13 -> [ONE_BY_24_LB,ONE_BY_24_UB], 14 -> [ONE_BY_24_LB,ONE_BY_24_UB], 15 -> [ONE_BY_24_LB,ONE_BY_24_UB], 16 -> [ONE_BY_24_LB,ONE_BY_24_UB], 17 -> [ONE_BY_24_LB,ONE_BY_24_UB], 18 -> [ONE_BY_24_LB,ONE_BY_24_UB], 19 -> [ONE_BY_24_LB,ONE_BY_24_UB], 20 -> [ONE_BY_24_LB,ONE_BY_24_UB], 21 -> [ONE_BY_24_LB,ONE_BY_24_UB], 22 -> [ONE_BY_24_LB,ONE_BY_24_UB], 23 -> [ONE_BY_24_LB,ONE_BY_24_UB], 24 -> [ONE_BY_24_LB,ONE_BY_24_UB] ]: R. net_sA_delay p = [ OFF -> 1, 1 -> 0.9, 2 -> 0.1 ]: R. net_sB_delay p = [ OFF -> 1, 1 -> 0.9, 2 -> 0.1 ]: R. net_DECA_delay p = [ OFF -> 1, 1 -> 0.9, 2 -> 0.1 ]: R. net_DECB_delay p = [ OFF -> 1, 1 -> 0.9, 2 -> 0.1 ]: R. io_cycle_offset p = [ OFF -> 1, 0 -> 0.1, 1 -> 0.1, 2 -> 0.1, 3 -> 0.1, 4 -> 0.1, 5 -> 0.1, 6 -> 0.1, 7 -> 0.1, 8 -> 0.1, 9 -> 0.1 ]: R. plc_cycle_offset p = [ OFF -> 1, 0 -> [ONE_BY_7_LB,ONE_BY_7_UB], 1 -> [ONE_BY_7_LB,ONE_BY_7_UB], 2 -> [ONE_BY_7_LB,ONE_BY_7_UB], 3 -> [ONE_BY_7_LB,ONE_BY_7_UB], 4 -> [ONE_BY_7_LB,ONE_BY_7_UB], 5 -> [ONE_BY_7_LB,ONE_BY_7_UB], 6 -> [ONE_BY_7_LB,ONE_BY_7_UB] ]: TRANS -- After the first step, also the probabilistic initializations have been -- performed. initialized'; -- Object. obj_preA' + obj_betwAB' + obj_postB' = 1; -- Randomly initialize starting position in the first unwinding. !initialized -> obj_pos = START_POS - prob_init_dist; !initialized -> prob_init_dist != OFF; initialized -> prob_init_dist = OFF; obj_next_event_now <-> (time >= obj_next_event); ( obj_preA and !obj_next_event_now) -> ( obj_preA' and obj_pos' = obj_pos - dt * tu_speed + 0.5 * dt^2 * tu_dec and obj_next_event' = obj_next_event and obj_step = obj_next_event - time and !obj_sA_reached and !obj_sB_reached); ( obj_preA and obj_next_event_now) -> ( obj_betwAB' and obj_pos' = obj_pos and POS_SENSOR_B = obj_pos - (obj_next_event'- time) * tu_speed + 0.5 * (obj_next_event' - time)^2 * tu_dec and obj_step = 0 and obj_sA_reached and !obj_sB_reached); ( obj_betwAB and !obj_next_event_now) -> ( obj_betwAB' and obj_pos' = obj_pos - dt * tu_speed + 0.5 * dt^2 * tu_dec and obj_next_event' = obj_next_event and obj_step = obj_next_event - time and obj_sA_reached and !obj_sB_reached); ( obj_betwAB and obj_next_event_now) -> ( obj_postB' and obj_pos' = obj_pos and obj_next_event' = MAX_TIME and obj_step = 0 and obj_sA_reached and obj_sB_reached); obj_postB -> ( obj_postB' and obj_pos' = obj_pos - dt * tu_speed + 0.5 * dt^2 * tu_dec and obj_next_event' = MAX_TIME and obj_step = MAX_TIME_STEP and obj_sA_reached and obj_sB_reached); -- Transport unit. tu_init' + tu_decA' + tu_slowspeed' + tu_decB' + tu_stop' = 1; tu_next_event_now <-> (time >= tu_next_event); ( tu_init and !net_DECA_compl and !net_DECB_compl) -> ( tu_init' and tu_speed' = tu_speed and tu_dec' = tu_dec and tu_next_event' = tu_next_event and tu_step = MAX_TIME_STEP); ( tu_init and net_DECA_compl and !net_DECB_compl) -> ( tu_decA' and tu_speed' = tu_speed and tu_dec' = DECELARATE_A and SLOW_SPEED = tu_speed - (tu_next_event' - time) * DECELARATE_A and tu_step = 0); ( tu_init and net_DECB_compl) -> ( tu_decB' and tu_speed' = tu_speed and tu_dec' = DECELARATE_B and 0 = tu_speed - (tu_next_event' - time) * DECELARATE_B and tu_step = 0); ( tu_decA and net_DECB_compl) -> ( tu_decB' and tu_speed' = tu_speed and tu_dec' = DECELARATE_B and 0 = tu_speed - (tu_next_event' - time) * DECELARATE_B and tu_step = 0); ( tu_decA and !net_DECB_compl and !tu_next_event_now) -> ( tu_decA' and tu_speed' = max(tu_speed - dt * tu_dec, SLOW_SPEED) and tu_dec' = tu_dec and tu_next_event' = tu_next_event and tu_step = tu_next_event - time); ( tu_decA and !net_DECB_compl and tu_next_event_now) -> ( tu_slowspeed' and tu_speed' = tu_speed and tu_dec' = 0 and tu_next_event' = MAX_TIME and tu_step = 0); ( tu_slowspeed and !net_DECB_compl) -> ( tu_slowspeed' and tu_speed' = tu_speed and tu_dec' = tu_dec and tu_next_event' = MAX_TIME and tu_step = MAX_TIME_STEP); ( tu_slowspeed and net_DECB_compl) -> ( tu_decB' and tu_speed' = tu_speed and tu_dec' = DECELARATE_B and 0 = tu_speed - (tu_next_event' - time) * DECELARATE_B and tu_step = 0); ( tu_decB and !tu_next_event_now) -> ( tu_decB' and tu_speed' = max(tu_speed - dt * tu_dec, 0) and tu_dec' = tu_dec and tu_next_event' = tu_next_event and tu_step = tu_next_event - time); ( tu_decB and tu_next_event_now) -> ( tu_stop' and tu_speed' = 0 and tu_dec' = 0 and tu_next_event' = MAX_TIME and tu_step = 0); tu_stop -> ( tu_stop' and tu_speed' = 0 and tu_dec' = 0 and tu_next_event' = MAX_TIME and tu_step = 0); -- stop time at the end of the trajectory. -- Network sensor data. -- Network sA. net_sA_init' + net_sA_send' + net_sA_compl' = 1; net_sA_next_event_now <-> (time >= net_sA_next_event); net_sA_stable <-> (net_sA_step > 0); ( net_sA_init and !obj_sA_reached) -> ( net_sA_init' and net_sA_next_event' = MAX_TIME and net_sA_step = MAX_TIME_STEP and net_sA_delay = OFF); ( net_sA_init and obj_sA_reached) -> ( net_sA_send' and net_sA_next_event' = time + net_sA_delay and net_sA_step = 0 and net_sA_delay != OFF); ( net_sA_send and !net_sA_next_event_now) -> ( net_sA_send' and net_sA_next_event' = net_sA_next_event and net_sA_step = net_sA_next_event - time and net_sA_delay = OFF); ( net_sA_send and net_sA_next_event_now) -> ( net_sA_compl' and net_sA_next_event' = MAX_TIME and net_sA_step = 0 and net_sA_delay = OFF); net_sA_compl -> ( net_sA_compl' and net_sA_next_event' = MAX_TIME and net_sA_step = MAX_TIME_STEP and net_sA_delay = OFF); -- Network sB. net_sB_init' + net_sB_send' + net_sB_compl' = 1; net_sB_next_event_now <-> (time >= net_sB_next_event); net_sB_stable <-> (net_sB_step > 0); ( net_sB_init and !obj_sB_reached) -> ( net_sB_init' and net_sB_next_event' = MAX_TIME and net_sB_step = MAX_TIME_STEP and net_sB_delay = OFF); ( net_sB_init and obj_sB_reached) -> ( net_sB_send' and net_sB_next_event' = time + net_sB_delay and net_sB_step = 0 and net_sB_delay != OFF); ( net_sB_send and !net_sB_next_event_now) -> ( net_sB_send' and net_sB_next_event' = net_sB_next_event and net_sB_step = net_sB_next_event - time and net_sB_delay = OFF); ( net_sB_send and net_sB_next_event_now) -> ( net_sB_compl' and net_sB_next_event' = MAX_TIME and net_sB_step = 0 and net_sB_delay = OFF); net_sB_compl -> ( net_sB_compl' and net_sB_next_event' = MAX_TIME and net_sB_step = MAX_TIME_STEP and net_sB_delay = OFF); -- Network actuator data. -- Network DECA. net_DECA_init' + net_DECA_send' + net_DECA_compl' = 1; net_DECA_next_event_now <-> (time >= net_DECA_next_event); ( net_DECA_init and !io_out_send_DECA') -> ( net_DECA_init' and net_DECA_next_event' = MAX_TIME and net_DECA_step = MAX_TIME_STEP and net_DECA_delay = OFF); ( net_DECA_init and io_out_send_DECA') -> ( net_DECA_send' and net_DECA_next_event' = time + net_DECA_delay and net_DECA_step = 0 and net_DECA_delay != OFF); ( net_DECA_send and !net_DECA_next_event_now) -> ( net_DECA_send' and net_DECA_next_event' = net_DECA_next_event and net_DECA_step = net_DECA_next_event - time and net_DECA_delay = OFF); ( net_DECA_send and net_DECA_next_event_now) -> ( net_DECA_compl' and net_DECA_next_event' = MAX_TIME and net_DECA_step = 0 and net_DECA_delay = OFF); net_DECA_compl -> ( net_DECA_compl' and net_DECA_next_event' = MAX_TIME and net_DECA_step = MAX_TIME_STEP and net_DECA_delay = OFF); -- Network DECB. net_DECB_init' + net_DECB_send' + net_DECB_compl' = 1; net_DECB_next_event_now <-> (time >= net_DECB_next_event); ( net_DECB_init and !io_out_send_DECB') -> ( net_DECB_init' and net_DECB_next_event' = MAX_TIME and net_DECB_step = MAX_TIME_STEP and net_DECB_delay = OFF); ( net_DECB_init and io_out_send_DECB') -> ( net_DECB_send' and net_DECB_next_event' = time + net_DECB_delay and net_DECB_step = 0 and net_DECB_delay != OFF); ( net_DECB_send and !net_DECB_next_event_now) -> ( net_DECB_send' and net_DECB_next_event' = net_DECB_next_event and net_DECB_step = net_DECB_next_event - time and net_DECB_delay = OFF); ( net_DECB_send and net_DECB_next_event_now) -> ( net_DECB_compl' and net_DECB_next_event' = MAX_TIME and net_DECB_step = 0 and net_DECB_delay = OFF); net_DECB_compl -> ( net_DECB_compl' and net_DECB_next_event' = MAX_TIME and net_DECB_step = MAX_TIME_STEP and net_DECB_delay = OFF); -- IO card input and output initialization. -- Initialization with randomized cycle offset (phaseshift). !initialized -> io_in_next_event = time + io_cycle_offset; !initialized -> io_out_next_event = time + io_cycle_offset; !initialized -> io_cycle_offset != OFF; initialized -> io_cycle_offset = OFF; -- IO card in. io_in_next_event_now <-> (time >= io_in_next_event); io_in_stable <-> (io_in_step > 0); ( !io_in_next_event_now or !net_sA_stable or !net_sB_stable) -> ( io_in_next_event' = io_in_next_event and io_in_step = io_in_next_event - time and (io_in_sA_ready' <-> io_in_sA_ready) and (io_in_sB_ready' <-> io_in_sB_ready)); ( io_in_next_event_now and net_sA_stable and net_sB_stable) -> ( io_in_next_event' = time + PLC_IO_CYCLE and io_in_step = 0 and (io_in_sA_ready' <-> net_sA_compl) and (io_in_sB_ready' <-> net_sB_compl)); -- IO card out. io_out_next_event_now <-> (time >= io_out_next_event); ( !io_out_next_event_now or !plc_stable) -> ( io_out_next_event' = io_out_next_event and io_out_step = io_out_next_event - time and (io_out_send_DECA' <-> io_out_send_DECA) and (io_out_send_DECB' <-> io_out_send_DECB)); ( io_out_next_event_now and plc_stable) -> ( io_out_next_event' = time + PLC_IO_CYCLE and io_out_step = 0 and (io_out_send_DECA' <-> plc_send_DECA') and (io_out_send_DECB' <-> plc_send_DECB')); -- PLC. -- Initialization with randomized cycle offset (phaseshift). !initialized -> plc_next_event = time + plc_cycle_offset; !initialized -> plc_cycle_offset != OFF; initialized -> plc_cycle_offset = OFF; plc_init' + plc_comp_DECA' + plc_comp_DECB' + plc_DECA_finished' + plc_DECB_finished' = 1; plc_next_event_now <-> (time >= plc_next_event); plc_stable <-> (plc_step > 0); ( plc_init and ( !plc_next_event_now or !io_in_stable)) -> ( plc_init' and plc_next_event' = plc_next_event and plc_step = plc_next_event - time and (plc_send_DECA' <-> plc_send_DECA) and (plc_send_DECB' <-> plc_send_DECB)); ( plc_init and plc_next_event_now and io_in_stable and !io_in_sA_ready' and !io_in_sB_ready') -> ( plc_init' and plc_next_event' = time + PLC_CYCLE and plc_step = 0 and (plc_send_DECA' <-> plc_send_DECA) and (plc_send_DECB' <-> plc_send_DECB)); ( plc_init and plc_next_event_now and io_in_stable and io_in_sA_ready' and !io_in_sB_ready') -> ( plc_comp_DECA' and plc_next_event' = time + PLC_CYCLE and plc_step = 0 and (plc_send_DECA' <-> plc_send_DECA) and (plc_send_DECB' <-> plc_send_DECB)); ( plc_init and plc_next_event_now and io_in_stable and io_in_sB_ready') -> ( plc_comp_DECB' and plc_next_event' = time + PLC_CYCLE and plc_step = 0 and (plc_send_DECA' <-> plc_send_DECA) and (plc_send_DECB' <-> plc_send_DECB)); ( plc_comp_DECA and ( !plc_next_event_now or !io_in_stable)) -> ( plc_comp_DECA' and plc_next_event' = plc_next_event and plc_step = plc_next_event - time and (plc_send_DECA' <-> plc_send_DECA) and (plc_send_DECB' <-> plc_send_DECB)); ( plc_comp_DECA and plc_next_event_now and io_in_stable and !io_in_sB_ready') -> ( plc_DECA_finished' and plc_next_event' = time + PLC_CYCLE and plc_step = 0 and plc_send_DECA' and (plc_send_DECB' <-> plc_send_DECB)); ( plc_comp_DECA and plc_next_event_now and io_in_stable and io_in_sB_ready') -> ( plc_comp_DECB' and plc_next_event' = time + PLC_CYCLE and plc_step = 0 and plc_send_DECA' and (plc_send_DECB' <-> plc_send_DECB)); ( plc_DECA_finished and ( !plc_next_event_now or !io_in_stable)) -> ( plc_DECA_finished' and plc_next_event' = plc_next_event and plc_step = plc_next_event - time and (plc_send_DECA' <-> plc_send_DECA) and (plc_send_DECB' <-> plc_send_DECB)); ( plc_DECA_finished and plc_next_event_now and io_in_stable and !io_in_sB_ready') -> ( plc_DECA_finished' and plc_next_event' = time + PLC_CYCLE and plc_step = 0 and (plc_send_DECA' <-> plc_send_DECA) and (plc_send_DECB' <-> plc_send_DECB)); ( plc_DECA_finished and plc_next_event_now and io_in_stable and io_in_sB_ready') -> ( plc_comp_DECB' and plc_next_event' = time + PLC_CYCLE and plc_step = 0 and (plc_send_DECA' <-> plc_send_DECA) and (plc_send_DECB' <-> plc_send_DECB)); ( plc_comp_DECB and !plc_next_event_now) -> ( plc_comp_DECB' and plc_next_event' = plc_next_event and plc_step = plc_next_event - time and (plc_send_DECA' <-> plc_send_DECA) and (plc_send_DECB' <-> plc_send_DECB)); ( plc_comp_DECB and plc_next_event_now) -> ( plc_DECB_finished' and plc_next_event' = MAX_TIME and plc_step = 0 and (plc_send_DECA' <-> plc_send_DECA) and plc_send_DECB'); plc_DECB_finished -> ( plc_DECB_finished' and plc_next_event' = MAX_TIME and plc_step = MAX_TIME_STEP and (plc_send_DECA' <-> plc_send_DECA) and (plc_send_DECB' <-> plc_send_DECB)); -- Cast Object and transport unit steps to integer. obj_step_int >= obj_step; obj_step_int < obj_step + 1; tu_step_int >= tu_step; tu_step_int < tu_step + 1; -- Scheduled event and time handling. dt = max(0, min(obj_step_int, min(tu_step_int, min(net_sA_step, min(net_sB_step, min(net_DECA_step, min(net_DECB_step, min(io_in_step, min(io_out_step, plc_step))))))))); time' = time + dt; TARGET tu_stop and obj_pos <= 100 and obj_pos >= 0;