% Evader/pursuer game (from Alur, Henzinger, Wong-Toi. Symbolic Analysis of
% Hybrid Systems. CDC 97)
% Variant: Pursuer used fixed speeds 6m/s and -0.5m/s; DT observable.

:- multifile r/5, implicit_updates/0, var2names/2, preds/2, cube_size/1, start/1, refinement/1, error/1.

refinement(inter).


% Variables:
%
% T  - time (in seconds)
% P  - pursuer position (in meters, modulo 40)
% E  - evader position (in meters, modulo 40)
% DT - time difference
% DP - pursuer position difference
% DE - evader position difference

var2names(p(_, data(T, P, E, DT)), [(T, 't'), (P, 'p'), (E, 'e'), (DT, 'dt')]).

preds(p(_, data(T, P, E, DT)), []).			%initial predicates

cube_size(1).

implicit_updates.       % if unspecified, values do not change

% locations
% rescued   - evader has reached helicopter
% clockwise - evader goes clockwise
% counter   - evader goes counterclockwise


% initial state
r(p(pc(start),      data(T, P, E, DT)),
  p(pc(init), data(T1, P1, E1, DT1)),
  [],
  [],
  100).

r(p(pc(init),      data(T, P, E, DT)),
  p(pc(clockwise), data(T1, P1, E1, DT1)),
  [T = 2, P = 10, E = 20, DT>=0],
  [],
  0).


% continous transitions
r(p(pc(clockwise), data(T,  P,  E,  DT)),
  p(pc(clockwise), data(T1, P1, E1, DT1)),
  [E >= 0, E =< 40, T >= 0, T < 2, P >= 0, P =< 40, DT >= 0, T + DT =< 2, E + 5 * DT =< 40, P - 0.5 * DT >= 0],
  [E1 = E + 5 * DT, T1 = T + DT, P1 = P - 0.5 * DT, DT1 = ?],
  1).

r(p(pc(clockwise), data(T,  P,  E,  DT)),
  p(pc(clockwise), data(T1, P1, E1, DT1)),
  [E >= 0, E =< 40, T >= 0, T < 2, P >= 0, P =< 40, DT >= 0, T + DT =< 2, E + 5 * DT =< 40, P + 6 * DT =< 40],
  [E1 = E + 5 * DT, T1 = T + DT, P1 = P + 6 * DT, DT1 = ?],
  2).

r(p(pc(counter), data(T,  P,  E,  DT)),
  p(pc(counter), data(T1, P1, E1, DT1)),
  [E >= 0, E =< 40, T >= 0, T < 2, P >= 0, P =< 40, DT >= 0, T + DT =< 2, E - 5 * DT >= 0, P - 0.5 * DT >= 0],
  [E1 = E - 5 * DT, T1 = T + DT, P1 = P - 0.5 * DT, DT1 = ?],
  3).

r(p(pc(counter), data(T,  P,  E,  DT)),
  p(pc(counter), data(T1, P1, E1, DT1)),
  [E >= 0, E =< 40, T >= 0, T < 2, P >= 0, P =< 40, DT >= 0, T + DT =< 2, E - 5 * DT >= 0, P + 6 * DT =< 40],
  [E1 = E - 5 * DT, T1 = T + DT, P1 = P + 6 * DT, DT1 = ?],
  4).


r(p(pc(rescued), data(T, P, E, DT)),
  p(pc(rescued), data(T1, P1, E1, DT1)),
  [E=0],
  [],
  3).


% discrete transitions, modulo 40 switches for P and E
r(p(pc(clockwise), data(T, P,  E, DT)),
  p(pc(clockwise), data(T1, P1, E1, DT1)),
  [P = 40],
  [P1 = 0],
  5).

r(p(pc(clockwise), data(T, P, E, DT)),
  p(pc(clockwise), data(T1, P1, E1, DT1)),
  [P = 0],
  [P1 = 40],
  6).

r(p(pc(clockwise), data(T, P, E, DT)),
  p(pc(clockwise), data(T1, P1, E1, DT1)),
  [E = 40],
  [E1 = 0],
  7).

r(p(pc(counter), data(T, P, E, DT)),
  p(pc(counter), data(T1, P1, E1, DT1)),
  [P = 40],
  [P1 = 0],
  8).

r(p(pc(counter), data(T, P, E, DT)),
  p(pc(counter), data(T1, P1, E1, DT1)),
  [P = 0],
  [P1 = 40],
  9).

r(p(pc(counter), data(T, P, E, DT)),
  p(pc(counter), data(T1, P1, E1, DT1)),
  [E = 40],
  [E1 = 0],
  10).


% discrete transitions, evader rescued
r(p(pc(clockwise), data(T, P, E, DT)),
  p(pc(rescued),  data(T1, P1, E1, DT1)),
  [E = 0],
  [],
  11).

r(p(pc(counter), data(T, P, E, DT)),
  p(pc(rescued), data(T1, P1, E1, DT1)),
  [E = 0],
  [],
  12).


% discrete transitions, evader mode switches
r(p(pc(clockwise), data(T, P, E, DT)),
  p(pc(clockwise), data(T1, P1, E1, DT1)),
  [T = 2,E > 0, E < 40, (40 - E)/5 < (40 - P)/6],
  [T1 = 0],
  13).

r(p(pc(clockwise), data(T, P, E, DT)),
  p(pc(counter),   data(T1, P1, E1, DT1)),
  [T = 2, E > 0, E < 40, (40 - E)/5 >= (40 - P)/6],
  [T1 = 0],
  14).

r(p(pc(counter),   data(T, P, E, DT)),
  p(pc(clockwise), data(T1, P1, E1, DT1)),
  [T = 2, E > 0, E < 40, (40 - E)/5 < (40 - P)/6],
  [T1 = 0],
  15).

r(p(pc(counter), data(T,  P, E, DT)),
  p(pc(counter), data(T1, P1, E1, DT1)),
  [T = 2, E > 0, E < 40, (40 - E)/5 >= (40 - P)/6],
  [Tp = 0],
  16).


% discrete transitions to error state
r(p(pc(counter), data(T,  P, E, DT)),
  p(pc(error), data(T1, P1, E1, DT1)),
  [E = P],
  [],
  17).

r(p(pc(clockwise), data(T,  P, E, DT)),
  p(pc(error), data(T1, P1, E1, DT1)),
  [E = P],
  [],
  18).

%start
start(pc(start)).
error(pc(error)).