// **************************************************************************
//
//    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
//
// **************************************************************************

package Theseus;

macro line = 6;
macro column = 6;

module Play(
    nat{line+1} line_theseus,
    nat{line+1} line_minotaur,
    nat{column+1} col_theseus,
    nat{column+1} col_minotaur,
    [line+1][column]bool horizontal_walls,
    [line][column+1]bool vertical_walls,
    nat{4} direction,
    event !theseus_plays,
    event theseus_has_won,
    event minotaur_has_won
) {
    weak abort { {
            loop {
                emit (theseus_plays);
                MoveTheseus(direction, horizontal_walls, vertical_walls, line_theseus, col_theseus);
                pause;
                MoveMinotaur(line_theseus, col_theseus, horizontal_walls, vertical_walls, line_minotaur, col_minotaur);
                pause;
                MoveMinotaur(line_theseus, col_theseus, horizontal_walls, vertical_walls, line_minotaur, col_minotaur);
                pause;
            }
        } || {
            loop {
                HasWon(line_theseus, col_theseus, theseus_has_won);
                pause;
            }
        } || {
            loop {
                HasLost(line_theseus, col_theseus, line_minotaur, col_minotaur, minotaur_has_won);
                pause;
            }
        }
    } when ( theseus_has_won | minotaur_has_won );
}