-------------------------------------------------------------------------------- -- -- ETCS model from ICONS08 paper. -- -- Author : Christian Herde -- -- Last Modified : -- Wed Apr 14 10:23:00 CEST 2004 -- -------------------------------------------------------------------------------- DECL -- Definition of symbolic constants. define dt = 2.0; -- time advances in steps of dt seconds define n = 3; -- messages are sent every n + 1 steps of the model define s = 400.0; -- safety distance added to braking distance define len = 200.0; -- length of a train (m) define a_min = -1.4; -- maximal deceleration define a_nom = -0.7; -- nominal deceleration define a_max = 0.7; -- maximal acceleration define v_max = 83.4; -- maximum speed of a train (m/s) define x_max = 5000.0; -- length of track define param_on = 0.7; -- switch on point of relay block define param_off = 0.3; -- switch off point of relay block -- Train 1. static float [a_nom, a_max] a_free1; -- acceleration in 'free running' mode float [a_min, a_max] a1; -- acceleration (m/s^2) float [0.0, x_max] xr1; -- position of the rear of the train (m) float [0.0, v_max] v1; -- speed of train 1 (m/s) -- Train 2. boole brake, p; int [0, n] clk; float [0.0, v_max] i1, o1, o1_mem; float [0.0, x_max] i2, o2, o2_mem; float [0.0, x_max] i3, o3, o3_mem; float [0.0, 7000] h1; float [-1000, 10000] h2; float [-10.0, 10.0] h3; float [0.0, -a_min] h4; float [a_min, 0.0] a_brake; -- deceleration when in 'braking' mode static float [a_nom, a_max] a_free2; -- acceleration in 'free running' mode float [0.0, x_max] xr2; -- position of the rear of the train (m) float [0.0, v_max] v2; -- speed of train 1 (m/s) float [a_min, a_max] a2; -- acceleration (m/s^2) INIT -- Initially trains are stopped and have a distance of 1000 meters. v1 = 0; v2 = 0; xr1 = xr2 + len + 1000; xr2 = 0.0; -- Initialize state-holding blocks. clk = 0; o1_mem = i1; o2_mem = i2; o3_mem = i3; !p; TRANS -- Dynamics of train 1. -- Euler approximation of integrators. Integrator of a1 has -- 0.0 as lower and v_max as upper saturation limit. a1 = a_free1; xr1' = xr1 + dt * v1; (v1' = v1 + dt * a1 or (v1' = 0.0 and v1 + dt * a1 <= 0.0) or (v1' = v_max and v1 + dt * a1 >= v_max)); -- Dynamics of train 2. -- Wiring. i1 = v2; i2 = xr2 + len; i3 = xr1; -- Timer subsystem (clk = n) -> (clk' = 0); (clk < n) -> (clk' = clk + 1); (clk = 0) -> [(o1 = i1) and (o2 = i2) and (o3 = i3) and (o1_mem' = i1) and (o2_mem' = i2) and (o3_mem' = o3)]; (clk > 0) -> [(o1 = o1_mem) and (o2 = o2_mem) and (o3 = o3_mem) and (o1_mem' = o1_mem) and (o2_mem' = o2_mem) and (o3_mem' = o3_mem)]; -- Compute deceleration h1 = o1^2; h2 = o3 - o2 - s; 2.0 * h3 * h2 = h1; -- Saturation block: When the input signal is within the range -- specified by the Lower limit and Upper limit parameters, the input -- signal passes through unchanged. When the input signal is outside -- these bounds, the signal is clipped to the upper or lower bound. (h3 <= 0.0) -> h4 = 0.0; (h3 >= -a_min) -> h4 = -a_min; (h3 > 0.0 and h3 < -a_min) -> h4 = h3; -- Gain block a_brake = -1.0 * h4; -- Relay block: When the relay is on, it remains on until the input -- drops below the value of the switch off point parameter. When the -- relay is off, it remains off until the input exceeds the value of -- the switch on point parameter. (!p and h4 >= param_on ) -> ( p' and brake); (!p and h4 < param_on ) -> (!p' and !brake); ( p and h4 <= param_off) -> (!p' and !brake); ( p and h4 > param_off) -> ( p' and brake); -- Switch brake -> a2 = a_brake; !brake -> a2 = a_free2; -- Euler approximation of integrators. Integrator of a2 has -- 0.0 as lower and v_max as upper saturation limit. xr2' = xr2 + dt * v2; (v2' = v2 + dt * a2 or (v2' = 0.0 and v2 + dt * a2 <= 0.0) or (v2' = v_max and v2 + dt * a2 >= v_max)); TARGET -- Can trains collide? xr1 - (xr2 + len) <= 0.0;