// ************************************************************************** // // 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 right from (l, c) module CanMoveRight( 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]) ) emit (granted); }