// ************************************************************************** // // 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; // Simply checks if (l1, c1) and (l2, c2) are in the same place module HasLost( nat{line+1} l1, nat{column+1} c1, nat{line+1} l2, nat{column+1} c2, event !has_lost ) { if ( ( l1 == l2 ) and ( c1 == c2 ) ) emit(has_lost); }