--------------------------
-- NAVIGATION BENCHMARK --
--------------------------

-- / -1.2	0.1	\
-- \ 0.1	-1.2	/

-- x0 in [2,3]
-- y0 in [1,2]
-- vx in [-0.3,0.3]
-- vy in [-0.3,0]

-- | B | 2 | 4 |
-- | 4 | 3 | 4 |
-- | 2 | 2 | A |


automaton nav

var x,y,vx,vy      : analog;
    x0,y0,vx0,vy0  : parameter;

synclabs: east, west, north, south;

loc Q_hub: while True wait {x'=0 & y'=0 & vx'=0 & vy'=0}
  when x >= 0 & x < 1 & y >= 0 & y < 1 do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_0_0;
  when x >= 0 & x < 1 & y >= 1 & y < 2 do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_0_1;
  when x >= 0 & x < 1 & y >= 2 & y < 3 do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_bad;
  when x >= 1 & x < 2 & y >= 0 & y < 1 do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_1_0;
  when x >= 1 & x < 2 & y >= 1 & y < 2 do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_1_1;
  when x >= 1 & x < 2 & y >= 2 & y < 3 do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_1_2;
  when x >= 2 & x < 3 & y >= 0 & y < 1 do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_safe;
  when x >= 2 & x < 3 & y >= 1 & y < 2 do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_2_1;
  when x >= 2 & x < 3 & y >= 2 & y < 3 do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_2_2;

loc Q_safe: while True wait {x'=0 & y'=0 & vx'=0 & vy'=0}
  when True do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_safe;
loc Q_bad: while True wait {x'=0 & y'=0 & vx'=0 & vy'=0}
  when True do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_bad;
loc Q_0_0: while vx in [-1,1] & vy in [-1,1] & x in [0,1] & y in[0,1] wait {
    vx' = -1.2 * vx + 0.1 * vy + 1.2 &
    vy' = 0.1 * vx + -1.2 * vy -0.1 &
    x' = vx & y' = vy }
  when x = 1 & vx >= 0 sync east do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_1_0;
  when x = 0 & vx <= 0 sync west do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_bad;
  when y = 1 & vy >= 0 sync north do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_0_1;
  when y = 0 & vy <= 0 sync south do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_bad;

loc Q_0_1: while vx in [-1,1] & vy in [-1,1] & x in [0,1] & y in[1,2] wait {
    vx' = -1.2 * vx + 0.1 * vy + 0.1 &
    vy' = 0.1 * vx + -1.2 * vy -1.2 &
    x' = vx & y' = vy }
  when x = 1 & vx >= 0 sync east do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_1_1;
  when x = 0 & vx <= 0 sync west do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_bad;
  when y = 2 & vy >= 0 sync north do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_bad;
  when y = 1 & vy <= 0 sync south do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_0_0;


loc Q_1_0: while vx in [-1,1] & vy in [-1,1] & x in [1,2] & y in[0,1] wait {
    vx' = -1.2 * vx + 0.1 * vy + 1.2 &
    vy' = 0.1 * vx + -1.2 * vy -0.1 &
    x' = vx & y' = vy }
  when x = 2 & vx >= 0 sync east do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_safe;
  when x = 1 & vx <= 0 sync west do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_0_0;
  when y = 1 & vy >= 0 sync north do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_1_1;
  when y = 0 & vy <= 0 sync south do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_bad;

loc Q_1_1: while vx in [-1,1] & vy in [-1,1] & x in [1,2] & y in[1,2] wait {
    vx' = -1.2 * vx + 0.1 * vy + 0.919238815542512 &
    vy' = 0.1 * vx + -1.2 * vy -0.919238815542512 &
    x' = vx & y' = vy }
  when x = 2 & vx >= 0 sync east do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_2_1;
  when x = 1 & vx <= 0 sync west do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_0_1;
  when y = 2 & vy >= 0 sync north do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_1_2;
  when y = 1 & vy <= 0 sync south do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_1_0;

loc Q_1_2: while vx in [-1,1] & vy in [-1,1] & x in [1,2] & y in[2,3] wait {
    vx' = -1.2 * vx + 0.1 * vy + 1.2 &
    vy' = 0.1 * vx + -1.2 * vy -0.1 &
    x' = vx & y' = vy }
  when x = 2 & vx >= 0 sync east do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_2_2;
  when x = 1 & vx <= 0 sync west do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_bad;
  when y = 3 & vy >= 0 sync north do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_bad;
  when y = 2 & vy <= 0 sync south do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_1_1;


loc Q_2_1: while vx in [-1,1] & vy in [-1,1] & x in [2,3] & y in[1,2] wait {
    vx' = -1.2 * vx + 0.1 * vy + 0.1 &
    vy' = 0.1 * vx + -1.2 * vy -1.2 &
    x' = vx & y' = vy }
  when x = 3 & vx >= 0 sync east do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_bad;
  when x = 2 & vx <= 0 sync west do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_1_1;
  when y = 2 & vy >= 0 sync north do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_2_2;
  when y = 1 & vy <= 0 sync south do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_safe;

loc Q_2_2: while vx in [-1,1] & vy in [-1,1] & x in [2,3] & y in[2,3] wait {
    vx' = -1.2 * vx + 0.1 * vy + 0.1 &
    vy' = 0.1 * vx + -1.2 * vy -1.2 &
    x' = vx & y' = vy }
  when x = 3 & vx >= 0 sync east do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_bad;
  when x = 2 & vx <= 0 sync west do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_1_2;
  when y = 3 & vy >= 0 sync north do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_bad;
  when y = 2 & vy <= 0 sync south do {x'=x,y'=y,vx'=vx,vy'=vy} goto Q_2_1;

end

var init: region;
init := loc[nav] = Q_hub
  & x=x0
  & y=y0
  & vx=vx0
  & vy=vy0

--  & x0 >= 2 & x0 < 3
--  & y0 >= 1 & y0 < 2
--  & vx0 in [-0.3,0.3]
--  & vy0 in [-0.3,0]
  
  & x0 = 2.5
  & y0 = 1.5
  & vx0 = 0 
  & vy0 = 0
  ;

var bad: region;
bad := loc[nav] = Q_bad;