```// **************************************************************************
//
//    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 Level1:
//
//      ######### ###
//      #t        # #
//      ### #   # # #
//      #   #   # # #
//      # ### # ### #
//      # # # #  m  #
//      # # ### ### #
//      # #     #   #
//      # # ### #   #
//      # # #       #
//      # # #       #
//      #           #
//      #############
//
// **************************************************************************

package Theseus;

macro line = 6;
macro column = 6;

module Level1 (
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] = false;
h_walls[0][5] = true;
h_walls[1][0] = true;
h_walls[1][1] = false;
h_walls[1][2] = false;
h_walls[1][3] = false;
h_walls[1][4] = false;
h_walls[1][5] = false;
h_walls[2][0] = false;
h_walls[2][1] = true;
h_walls[2][2] = false;
h_walls[2][3] = false;
h_walls[2][4] = true;
h_walls[2][5] = false;
h_walls[3][0] = false;
h_walls[3][1] = false;
h_walls[3][2] = true;
h_walls[3][3] = false;
h_walls[3][4] = true;
h_walls[3][5] = false;
h_walls[4][0] = false;
h_walls[4][1] = false;
h_walls[4][2] = true;
h_walls[4][3] = false;
h_walls[4][4] = false;
h_walls[4][5] = false;
h_walls[5][0] = false;
h_walls[5][1] = false;
h_walls[5][2] = false;
h_walls[5][3] = false;
h_walls[5][4] = false;
h_walls[5][5] = false;
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] = true;
v_walls[0][6] = true;
v_walls[1][0] = true;
v_walls[1][1] = false;
v_walls[1][2] = true;
v_walls[1][3] = false;
v_walls[1][4] = true;
v_walls[1][5] = true;
v_walls[1][6] = true;
v_walls[2][0] = true;
v_walls[2][1] = true;
v_walls[2][2] = true;
v_walls[2][3] = true;
v_walls[2][4] = false;
v_walls[2][5] = false;
v_walls[2][6] = true;
v_walls[3][0] = true;
v_walls[3][1] = true;
v_walls[3][2] = false;
v_walls[3][3] = false;
v_walls[3][4] = true;
v_walls[3][5] = false;
v_walls[3][6] = true;
v_walls[4][0] = true;
v_walls[4][1] = true;
v_walls[4][2] = true;
v_walls[4][3] = false;
v_walls[4][4] = false;
v_walls[4][5] = false;
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] = true;
line_theseus  = 1;
col_theseus  = 1;
line_minotaur = 3;
col_minotaur = 5;
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;
}
```