dReachTempFile.drh

// Variables for the actual X and Y position of the car
[0, 10] x;
[0, 10] y;

// Variables for the invt of the car in any given state
// these variables cannot be hard coded because of the
// way that templating works
[0, 10] x_last;
[0, 10] y_last;

[0, 100] time;

// Dummy state for the final resting place of the car
{
  mode 1;

  invt:
    true;

  flow:
    d/dt[x] = 0;
    d/dt[y] = 0;
    d/dt[x_last] = 0;
    d/dt[y_last] = 0;
  jump:
    false ==> @1 true;
}



{
  
  // Super State: 1
  // Direction: 1
  mode 2;

  invt:
      // Right turn north
      (y <= y_last + 1);
      (x <= x_last + 1);
  flow:
      d/dt[y] = 1;
      d/dt[x] = 1;
      d/dt[x_last] = 0;
      d/dt[y_last] = 0;
  jump:
      // Right turn north
      (and (y >= y_last + 1) (x >= x_last + 1)) ==> @7 (and (x_last' = x) (y_last' = y) (x' = x) (y' = y));
}
{
  
  // Super State: 1
  // Direction: 2
  mode 3;

  invt:
      // Right turn east
      (y >= y_last - 1);
      (x <= x_last + 1);
  flow:
      d/dt[y] = -1;
      d/dt[x] = 1;
      d/dt[x_last] = 0;
      d/dt[y_last] = 0;
  jump:
      // Right turn east
      (and (y <= y_last - 1) (x >= x_last + 1)) ==> @8 (and (x_last' = x) (y_last' = y) (x' = x) (y' = y));
}
{
  
  // Super State: 1
  // Direction: 3
  mode 4;

  invt:
      // Right turn south
      (y >= y_last - 1);
      (x >= x_last - 1);
  flow:
      d/dt[y] = -1;
      d/dt[x] = -1;
      d/dt[x_last] = 0;
      d/dt[y_last] = 0;
  jump:
      // Right turn south
      (and (y <= y_last - 1) (x <= x_last - 1)) ==> @5 (and (x_last' = x) (y_last' = y) (x' = x) (y' = y));
}
{
  
  // Super State: 1
  // Direction: 0
  mode 5;

  invt:
      // Right turn west
      (y <= y_last + 1);
      (x >= x_last - 1);
  flow:
      d/dt[y] = 1;
      d/dt[x] = -1;
      d/dt[x_last] = 0;
      d/dt[y_last] = 0;
  jump:
      // Right turn west
      (and (y >= y_last + 1) (x <= x_last - 1)) ==> @6 (and (x_last' = x) (y_last' = y) (x' = x) (y' = y));
}

{
  
  // Super State: 2
  // Direction: 1
  mode 6;

  invt:
      // Left turn north
      (y <= y_last + 1);
      (x >= x_last - 1);
  flow:
      d/dt[y] = 1;
      d/dt[x] = -1;
      d/dt[x_last] = 0;
      d/dt[y_last] = 0;
  jump:
      // Left turn north
      (and (y >= y_last + 1) (x <= x_last - 1)) ==> @9 (and (x_last' = x) (y_last' = y) (x' = x) (y' = y));
}
{
  
  // Super State: 2
  // Direction: 2
  mode 7;

  invt:
      // Left turn east
      (y <= y_last + 1);
      (x <= x_last + 1);
  flow:
      d/dt[y] = 1;
      d/dt[x] = 1;
      d/dt[x_last] = 0;
      d/dt[y_last] = 0;
  jump:
      // Left turn east
      (and (y >= y_last + 1) (x >= x_last + 1)) ==> @10 (and (x_last' = x) (y_last' = y) (x' = x) (y' = y));
}
{
  
  // Super State: 2
  // Direction: 3
  mode 8;

  invt:
      // Left turn south
      (y >= y_last - 1);
      (x <= x_last + 1);
  flow:
      d/dt[y] = -1;
      d/dt[x] = 1;
      d/dt[x_last] = 0;
      d/dt[y_last] = 0;
  jump:
      // Left turn south
      (and (y <= y_last - 1) (x >= x_last + 1)) ==> @11 (and (x_last' = x) (y_last' = y) (x' = x) (y' = y));
}
{
  
  // Super State: 2
  // Direction: 0
  mode 9;

  invt:
      // Left turn west
      (y >= y_last - 1);
      (x >= x_last - 1);
  flow:
      d/dt[y] = -1;
      d/dt[x] = -1;
      d/dt[x_last] = 0;
      d/dt[y_last] = 0;
  jump:
      // Left turn west
      (and (y <= y_last - 1) (x <= x_last - 1)) ==> @12 (and (x_last' = x) (y_last' = y) (x' = x) (y' = y));
}

{
  
  // Super State: 3
  // Direction: 1
  mode 10;

  invt:
      // Straight north
      (y <= y_last + 1);
  flow:
      d/dt[y] = 1;
      d/dt[x] = 0;
      d/dt[x_last] = 0;
      d/dt[y_last] = 0;
  jump:
      // Straight north
      (y >= y_last + 1) ==> @1 (and (x_last' = x) (y_last' = y) (x' = x) (y' = y));
}
{
  
  // Super State: 3
  // Direction: 2
  mode 11;

  invt:
      // Straight east
      (x <= x_last + 1);
  flow:
      d/dt[y] = 0;
      d/dt[x] = 1;
      d/dt[x_last] = 0;
      d/dt[y_last] = 0;
  jump:
      // Straight east
      (x >= x_last + 1) ==> @1 (and (x_last' = x) (y_last' = y) (x' = x) (y' = y));
}
{
  
  // Super State: 3
  // Direction: 3
  mode 12;

  invt:
      // Straight south
      (y >= y_last - 1);
  flow:
      d/dt[y] = -1;
      d/dt[x] = 0;
      d/dt[x_last] = 0;
      d/dt[y_last] = 0;
  jump:
      // Straight south
      (y <= y_last - 1) ==> @1 (and (x_last' = x) (y_last' = y) (x' = x) (y' = y));
}
{
  
  // Super State: 3
  // Direction: 0
  mode 13;

  invt:
      // Straight west
      (x >= x_last - 1);
  flow:
      d/dt[y] = 0;
      d/dt[x] = -1;
      d/dt[x_last] = 0;
      d/dt[y_last] = 0;
  jump:
      // Straight west
      (x <= x_last - 1) ==> @1 (and (x_last' = x) (y_last' = y) (x' = x) (y' = y));
}

init:
  @2 (and (y = 0) (x = 0) (x_last = 0) (y_last = 0));

goal:
  @1 true;