-------------------------------------------------------------------------------- -- -- Roundabout collision-avoidance manoeuver in air-traffic management. -- Adapted from the protocol presented by Tomlin et al. -- -- Author : Christian Herde -- -- Last Modified : -- Tue May 22 15:22:34 CEST 2007 -- -------------------------------------------------------------------------------- DECL -- Aircraft 1. define v1 = 6; -- velocity float [-10.0, 10.0] p1; -- angle float [0.0, 1000.0] x1; -- x position float [0.0, 1000.0] y1; -- y position -- Aircraft 2. define v2 = 6; -- velocity float [-10.0, 10.0] p2; -- angle float [0.0, 1000.0] x2; -- x position float [0.0, 1000.0] y2; -- y position -- Further declarations. define d = 1000000; -- square of minimal initial distance (1000) define a = 160000; -- square of alert distance (400) define c = 78400; -- square of critical distance (280) define w = -0.02; -- angular velocity when being in circular flight define m = -50.0; -- reciprocal of w boole jump; boole cruise; float [0.0, 500.0] dt; float [0.0, 500.0] t; INIT -- Initially the aircrafts are at least 1000 units away from each other. (x1 - x2)^2 + (y1 - y2)^2 >= d; -- They are in cruise mode. !jump; cruise; -- Reset global time. t = 0.0; TRANS jump' <-> !jump; -- Transition from mode 'cruise' to 'collision avoidance'. jump and cruise -> ( (x1 - x2)^2 + (y1 - y2)^2 <= a and !cruise' and dt = 0.0 and p1' = p1 + 1.570796 and x1' = x1 and y1' = y1 and p2' = p2 + 1.570796 and x2' = x2 and y2' = y2); -- Mode 'collision avoidance' has no outgoing transition. jump and !cruise -> false; -- Cruise mode. Angular velocity is zero, i.e. angle remains constant. !jump and cruise -> ( cruise' and dt > 0.0 and (x1' - x2')^2 + (y1' - y2')^2 >= a and p1' = p1 and x1' = v1 * cos(p1) * dt + x1 and y1' = v1 * sin(p1) * dt + y1 and p2' = p2 and x2' = v2 * cos(p2) * dt + x2 and y2' = v2 * sin(p2) * dt + y2); -- Collision avoidance mode. !jump and !cruise -> ( !cruise' and dt > 0.0 and dt * -w <= 3.1415926 and p1' = p1 + w * dt and x1' = m * [v1 * sin(p1 + w * dt) - v1 * sin(p1) + x1 * w] and y1' = m * [-v1 * cos(p1 + w * dt) + v1 * cos(p1) + y1 * w] and p2' = p2 + w * dt and x2' = m * [v2 * sin(p2 + w * dt) - v2 * sin(p2) + x2 * w] and y2' = m * [-v2 * cos(p2 + w * dt) + v2 * cos(p2) + y2 * w]); -- Update global time. t' = t + dt; TARGET -- Characterization of state to be reached. (x1 - x2)^2 + (y1 - y2)^2 <= c;