// ************************************************************************** // // 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; module Play( nat{line+1} line_theseus, nat{line+1} line_minotaur, nat{column+1} col_theseus, nat{column+1} col_minotaur, [line+1][column]bool horizontal_walls, [line][column+1]bool vertical_walls, nat{4} direction, event !theseus_plays, event theseus_has_won, event minotaur_has_won ) { weak abort { { loop { emit (theseus_plays); MoveTheseus(direction, horizontal_walls, vertical_walls, line_theseus, col_theseus); pause; MoveMinotaur(line_theseus, col_theseus, horizontal_walls, vertical_walls, line_minotaur, col_minotaur); pause; MoveMinotaur(line_theseus, col_theseus, horizontal_walls, vertical_walls, line_minotaur, col_minotaur); pause; } } || { loop { HasWon(line_theseus, col_theseus, theseus_has_won); pause; } } || { loop { HasLost(line_theseus, col_theseus, line_minotaur, col_minotaur, minotaur_has_won); pause; } } } when ( theseus_has_won | minotaur_has_won ); }