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

// Minotaur moves according to the rules

module MoveMinotaur(
    nat{line+1} l_theseus,
    nat{column+1} c_theseus,
    [line+1][column]bool h_walls,
    [line][column+1]bool v_walls,
    nat{line+1} l_minotaur,
    nat{column+1} c_minotaur
) {
    event granted_h;
    event granted_v;
    if ( c_theseus < c_minotaur ) {
        //  should go left
        CanMoveLeft(l_minotaur, c_minotaur, h_walls, v_walls, granted_h);
        if ( granted_h ) next(c_minotaur) = c_minotaur - 1;
    } else if ( c_theseus > c_minotaur ) {
        //  should go right
        CanMoveRight(l_minotaur, c_minotaur, h_walls, v_walls, granted_h);
        if ( granted_h ) next(c_minotaur) = c_minotaur + 1;
    }
    if ( not(granted_h) ) {
        if ( l_theseus < l_minotaur ) {
            //  should go up
            CanMoveUp(l_minotaur, c_minotaur, h_walls, v_walls, granted_v);
            if ( granted_v ) next(l_minotaur) = l_minotaur - 1;
        } else if ( l_theseus > l_minotaur ) {
            //  should go down
            CanMoveDown(l_minotaur, c_minotaur, h_walls, v_walls, granted_v);
            if ( granted_v ) next(l_minotaur) = l_minotaur + 1;
        }
    }
}