// ************************************************************************** // // 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 // // ************************************************************************** // // Sokoban (倉庫番, Japanese for "warehouse keeper") is a transport // puzzle in which the player pushes boxes around a maze, viewed // from above, and tries to put them in designated locations. Only // one box may be pushed at a time, not two, and boxes cannot be // pulled. // // Sokoban was created in 1980 by Hiroyuki Imabayashi, and was // published in 1982 by Thinking Rabbit, a software house based in // Takarazuka, Japan. // // It is known that Sokoban is PSPACE-complete. For references see // many resources in the web like http://en.wikipedia.org/wiki/Sokoban. // // To use this Quartz description, you have to define static // constants "rows" and "cols" before including this file, // a further module "InitialField" to initialize the // field, and a specification "SokobanSpec" that defines the // fields where the boxes should be finally moved to. // // ************************************************************************** package Sokoban; macro cols = 8; macro rows = 8; // objects that may occupy a field macro EMPTY = 0b00; macro WALL = 0b11; macro BOX = 0b01; macro ROBOT = 0b10; // move instructions to the robot macro UP = 0b00; macro DOWN = 0b01; macro LEFT = 0b10; macro RIGHT = 0b11; module Play( bv{2} ?mv, [cols][rows]bv{2} f, nat{cols} robot_x, nat{rows} robot_y ) { // InitialField(f); loop { case (mv==UP) do { if(robot_y<=rows-3 & f[robot_x][robot_y+1]==BOX & f[robot_x][robot_y+2]==EMPTY()) { next(f[robot_x][robot_y]) = EMPTY; next(f[robot_x][robot_y+1]) = ROBOT; next(f[robot_x][robot_y+2]) = BOX; next(robot_y) = robot_y+1; } if(robot_y<=rows-2 & f[robot_x][robot_y+1]==EMPTY) { next(f[robot_x][robot_y]) = EMPTY; next(f[robot_x][robot_y+1]) = ROBOT; next(robot_y) = robot_y+1; } } (mv==DOWN) do { if(robot_y>=2 & f[robot_x][robot_y-1]==BOX & f[robot_x][robot_y-2]==EMPTY) { next(f[robot_x][robot_y]) = EMPTY; next(f[robot_x][robot_y-1]) = ROBOT; next(f[robot_x][robot_y-2]) = BOX; next(robot_y) = robot_y-1; } if(robot_y>=1 & f[robot_x][robot_y-1]==EMPTY) { next(f[robot_x][robot_y]) = EMPTY; next(f[robot_x][robot_y-1]) = ROBOT; next(robot_y) = robot_y-1; } } (mv==LEFT) do { if(robot_x>=2 & f[robot_x-1][robot_y]==BOX & f[robot_x-2][robot_y]==EMPTY) { next(f[robot_x][robot_y]) = EMPTY; next(f[robot_x-1][robot_y]) = ROBOT; next(f[robot_x-2][robot_y]) = BOX; next(robot_x) = robot_x-1; } if(robot_x>=1 & f[robot_x-1][robot_y]==EMPTY) { next(f[robot_x][robot_y]) = EMPTY; next(f[robot_x-1][robot_y]) = ROBOT; next(robot_x) = robot_x-1; } } (mv==RIGHT) do { if(robot_x<=cols-3 & f[robot_x+1][robot_y]==BOX & f[robot_x+2][robot_y]==EMPTY()) { next(f[robot_x][robot_y]) = EMPTY; next(f[robot_x+1][robot_y]) = ROBOT; next(f[robot_x+2][robot_y]) = BOX; next(robot_x) = robot_x+1; } if(robot_x<=cols-2 & f[robot_x+1][robot_y]==EMPTY) { next(f[robot_x][robot_y]) = EMPTY; next(f[robot_x+1][robot_y]) = ROBOT; next(robot_x) = robot_x+1; } } default nothing; pause; } }