-------------------------------------------------------------------------------- -- -- HYSAT sample input file. -- -- Author : Christian Herde -- -- Last Modified : -- Wed Apr 14 10:23:00 CEST 2004 -- -------------------------------------------------------------------------------- DECL -- Lane. define x0 = 0.0; define x1 = 1.0; define x2 = 3.0; define x3 = 4.0; define y0 = 0.0; define y1 = 4.0; define y2 = 5.0; define y3 = 9.0; -- Teeing-off area. define xl = 1.5; define yd = 0.75; define xr = 2.5; define yu = 1.25; -- Position of hole. define xh = 2.0; define yh = 8.0; -- Position of ball. float [x0, x3] x; float [y0, y3] y; -- Horizontal component of velocity. -- Negative values: left. Positive values: right. float [-20, 20] vx; -- Vertical component of velocity. -- Negative values: down. Positive values: up. float [-20, 20] vy; -- Duration of a flow. float [0.0, 10.0] dt; -- Locations. boole s1, s2, s3; -- To jump or not to jump? boole jump; -- Minium duration of a flow. To exclude zeno trajectories. define flow_min = 0.01; -- By setting fg to a small negative value it is possible to slightly -- tilt the lane such that the hole is on a higher level than the -- teeing-off field. define fg = -1.8; -- If fl equals 1.0, the ball loses no energy when colliding with -- a boundary or an obstacle. Setting it to 0.9, e.g., will cause a -- loss of 10 per cent in the respective component of the velocity vector. define fl = 0.6; INIT -- Ball is within the teeing-off area. xl <= x; x <= xr; yd <= y; y <= yu; -- x = 2.0; -- y = 1.0; -- Motion starts with a flow in location s3. !jump; !s1 and !s2 and s3; TRANS -- At any time control is at exactly in one location. s1' + s2' + s3' = 1; -- The components of the velocity vector are non-zero throughout. vx != 0 and vy != 0; -- Jumps and flows alternate. jump <-> !jump'; -- Jumps don't consume time. Flows do. jump -> dt = 0; !jump -> dt > flow_min; -- Evolution of continuous variables during a flow. !jump -> (x' = x + dt * vx and y' = y + dt * vy + 0.5 * fg * dt^2 and vx' = vx and vy' = vy + dt * fg); -- Flows have to preserve the location invariants. !jump -> (x0 <= x' and x' <= x3); (!jump and s1) -> (y2 <= y' and y' <= y3); (!jump and s2) -> (y1 <= y' and y' <= y2); (!jump and s3) -> (y0 <= y' and y' <= y1); -- The transition relation only talks about start- and endpoints -- of trajectories, not about the states in-between. We have to make -- sure that a trajectory does not leave the region defined by the -- location invariants, thereafter returning to it. !(!jump and s3 and y' = y1 and vy' < 0); !(!jump and s2 and y' = y2 and vy' < 0); !(!jump and s1 and y' = y3 and vy' < 0); -- Flows do not change the location. (!jump and s1) -> s1'; (!jump and s2) -> s2'; (!jump and s3) -> s3'; -- Jumps do not change the position of the ball. jump -> (x' = x and y' = y); -- Jumps only happen on boundaries. (jump and s1) -> (x = x0 or x = x3 or y = y3 or y = y2); (jump and s2) -> (x = x0 or x = x3 or y = y2 or y = y1); (jump and s3) -> (x = x0 or x = x3 or y = y1 or y = y0); -- We cannot jump from s1 to s3 or from s3 to s1. (jump and s1) -> (s1' or s2'); (jump and s3) -> (s3' or s2'); -- How do jumps modify the state? -- Horizontal component. (jump and x = x0 and vx < 0) -> vx' = -fl * vx; (jump and x = x3 and vx > 0) -> vx' = -fl * vx; (jump and x0 < x and x < x3) -> vx' = vx; -- We never hit a lower boundary while moving upward. (jump and s1 and y = y2 and vy > 0) -> false; (jump and s2 and y = y1 and vy > 0) -> false; (jump and s3 and y = y0 and vy > 0) -> false; -- We never hit an upper boundary while moving downward. (jump and s1 and y = y3 and vy < 0) -> false; (jump and s2 and y = y2 and vy < 0) -> false; (jump and s3 and y = y1 and vy < 0) -> false; -- How do jumps modify the state? -- Vertical component. (jump and s1 and y = y3 and vy > 0) -> (s1' and vy' = -fl * vy); (jump and s1 and y = y2 and vy < 0 and x <= x2) -> (s1' and vy' = -fl * vy); (jump and s1 and y = y2 and vy < 0 and x > x2) -> (s2' and vy' = vy); (jump and s1 and y2 < y and y < y3) -> (s1' and vy' = vy); (jump and s2 and y = y2 and vy > 0 and x > x2) -> (s1' and vy' = vy); (jump and s2 and y = y2 and vy > 0 and x <= x2) -> (s2' and vy' = -fl * vy); (jump and s2 and y = y1 and vy < 0 and x >= x1) -> (s2' and vy' = -fl * vy); (jump and s2 and y = y1 and vy < 0 and x < x1) -> (s3' and vy' = vy); (jump and s2 and y1 < y and y < y2) -> (s2' and vy' = vy); (jump and s3 and y = y1 and vy > 0 and x < x1) -> (s2' and vy' = vy); (jump and s3 and y = y1 and vy > 0 and x >= x1) -> (s3' and vy' = -fl * vy); (jump and s3 and y = y0 and vy < 0) -> (s3' and vy' = -fl * vy); (jump and s3 and y0 < y and y < y1) -> (s3' and vy' = vy); TARGET x = xh; y = yh;