// **************************************************************************
//
//    eses                   eses
//   eses                     eses
//  eses    eseses  esesese    eses   Embedded Systems Group
//  ese    ese  ese ese         ese
//  ese    eseseses eseseses    ese   Department of Computer Science
//  eses   eses          ese   eses
//   eses   eseses  eseseses  eses    University of Kaiserslautern
//    eses                   eses
//
// **************************************************************************
//
//  Name:        Theseus and the Minotaur
//
//  References:  http://www.logicmazes.com/theseus.html
//
//  Theseus must escape from a maze. There is also a mechanical Minotaur. For
//  every turn that Theseus takes, the Minotaur takes two turns. The Minotaur
//  follows this program for each of his two turns: First he tests if he can
//  move horizontally and get closer to Theseus. If he can, he will move one
//  square horizontally. If he can't, he will test if he could move vertically
//  and get closer to Theseus. If he can, he will move one square vertically.
//  If he can't move either horizontally or vertically, then he just skips that
//  turn.
//
//  Walls are encoded by a 2D array of horizontal walls (boolean) and a 2D
//  array of vertical walls (boolean).
//  Theseus possible positions are [0..line+1] x [0..column+1]. Theseus is
//  inside the maze if is position is in [1..line] x [1..column]
//
//  maze of Level3:
//
//         #############
//         #           #
//         ##### ##### #
//         # # #   #t  #
//         # # ### ### #
//         #       # # #
//         ### ### # # #
//         #     #     #
//         #   #####   #
//         #     #   #m#
//         # ####### ###
//         #
//         #############
//
// **************************************************************************

package Theseus;

macro line = 6;
macro column = 6;


module Level3 (
    nat{4} direction,
    event theseus_has_won,
    event minotaur_has_won
) {
    event theseus_plays,
    nat{line+1} line_theseus,
    nat{line+1} line_minotaur,
    nat{column+1} col_theseus,
    nat{column+1} col_minotaur,
    [line+1][column]bool h_walls,
    [line][column+1]bool v_walls;

    // initialize maze
  h_walls[0][0] = true;
  h_walls[0][1] = true;
  h_walls[0][2] = true;
  h_walls[0][3] = true;
  h_walls[0][4] = true;
  h_walls[0][5] = true;
  h_walls[1][0] = true;
  h_walls[1][1] = true;
  h_walls[1][2] = false;
  h_walls[1][3] = true;
  h_walls[1][4] = true;
  h_walls[1][5] = false;
  h_walls[2][0] = false;
  h_walls[2][1] = false;
  h_walls[2][2] = true;
  h_walls[2][3] = false;
  h_walls[2][4] = true;
  h_walls[2][5] = false;
  h_walls[3][0] = true;
  h_walls[3][1] = false;
  h_walls[3][2] = true;
  h_walls[3][3] = false;
  h_walls[3][4] = false;
  h_walls[3][5] = false;
  h_walls[4][0] = false;
  h_walls[4][1] = false;
  h_walls[4][2] = true;
  h_walls[4][3] = true;
  h_walls[4][4] = false;
  h_walls[4][5] = false;
  h_walls[5][0] = false;
  h_walls[5][1] = true;
  h_walls[5][2] = true;
  h_walls[5][3] = true;
  h_walls[5][4] = false;
  h_walls[5][5] = true;
  h_walls[6][0] = true;
  h_walls[6][1] = true;
  h_walls[6][2] = true;
  h_walls[6][3] = true;
  h_walls[6][4] = true;
  h_walls[6][5] = true;
  v_walls[0][0] = true;
  v_walls[0][1] = false;
  v_walls[0][2] = false;
  v_walls[0][3] = false;
  v_walls[0][4] = false;
  v_walls[0][5] = false;
  v_walls[0][6] = true;
  v_walls[1][0] = true;
  v_walls[1][1] = true;
  v_walls[1][2] = true;
  v_walls[1][3] = false;
  v_walls[1][4] = true;
  v_walls[1][5] = false;
  v_walls[1][6] = true;
  v_walls[2][0] = true;
  v_walls[2][1] = false;
  v_walls[2][2] = false;
  v_walls[2][3] = false;
  v_walls[2][4] = true;
  v_walls[2][5] = true;
  v_walls[2][6] = true;
  v_walls[3][0] = true;
  v_walls[3][1] = false;
  v_walls[3][2] = false;
  v_walls[3][3] = true;
  v_walls[3][4] = false;
  v_walls[3][5] = false;
  v_walls[3][6] = true;
  v_walls[4][0] = true;
  v_walls[4][1] = false;
  v_walls[4][2] = false;
  v_walls[4][3] = true;
  v_walls[4][4] = false;
  v_walls[4][5] = true;
  v_walls[4][6] = true;
  v_walls[5][0] = true;
  v_walls[5][1] = false;
  v_walls[5][2] = false;
  v_walls[5][3] = false;
  v_walls[5][4] = false;
  v_walls[5][5] = false;
  v_walls[5][6] = false;
  line_theseus  = 2;
  col_theseus  = 5;
  line_minotaur = 5;
  col_minotaur = 6;
  pause;

    Play(
        line_theseus, line_minotaur, col_theseus, col_minotaur,
        h_walls, v_walls,
        direction, theseus_plays,
        theseus_has_won, minotaur_has_won
    );

} satisfies {
    TheseusWins[DisProveA]: assert A G !theseus_has_won;
}