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

// Theseus makes a move (according to walls)

module MoveTheseus(
    nat{4} dir,
    [line+1][column()]bool h_walls,
    [line][column()+1]bool v_walls,
    nat{line+1} l,
    nat{column+1} c
) {
    event granted;
    if ( dir == 1 ) {
        CanMoveDown(l, c, h_walls, v_walls, granted);
        if ( granted ) next(l) = l + 1;
    } else if ( dir == 2 ) {
        CanMoveUp(l, c, h_walls, v_walls, granted);
        if ( granted ) next(l) = l - 1;
    } else if ( dir == 3 ) {
        CanMoveRight(l, c, h_walls, v_walls, granted);
        if ( granted ) next(c) = c + 1;
    } else if ( dir == 4 ) {
        CanMoveLeft(l, c, h_walls, v_walls, granted);
        if ( granted ) next(c) = c - 1;
    }
}