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

// Check if we can move left from (l, c)

module CanMoveLeft(
    nat{line+1} l,
    nat{column+1} c,
    [line+1][column()]bool h_walls,
    [line][column()+1]bool v_walls,
    event !granted
) {
    if ( not(v_walls[l-1][c-1]) ) emit (granted);
}