This is the Solitaire Game Solver, version 1.0 (16.07.2004). The homepage of the game solver, with news and updates, is at . Questions about the program should be directed to: ############################################################################ INFORMATION: The Solitaire Game Solver offers two classic solitaire games: * Peg Solitaire: The game is played on a board with 32 holes. Holes may be occupied with pegs. Pegs are allowed to jump over adjacent pegs, provided that the hole they end up in is empty. The peg that has been jumped over is removed. The goal is to remove all the pegs except for one that should end up in the centre hole. * 15-puzzle: The game is played on a 4x4 board. One cell of the board is empty, all others contain pieces. A piece adjacent to the hole may slide into the hole. The object of the game is to bring the pieces into a predefined order. In this implementation, you may either play the game on your own, or you can ask the computer for help. You may also define your own starting configuration and ask the computer to solve it. In the 15-puzzle, you also have the opportunity to play against the computer. The Solitaire Game Solver demonstrates how tools used for the verification of hardware or software systems (i.e. model checkers) can be used to solve solitaire games. The typical task of a model checker is to search for faulty executions in a system. Since the state space of a realistic system may be rather large, model- checkers need to employ efficient search techniques. This makes model checkers suitable to solve solitaire games: Solitaire games have a large solution space (e.g. the number of potential configurations in the 15-puzzle is 16*15*...*1), and searching for a solution is analogous to finding an "faulty" execution in a system. Here, solutions are found using some of the model checkers supported by the Model-Checking Kit. In particular, Spin is used to solve the Peg Solitaire game, and LoLA is used to solve the 15-puzzle. ############################################################################ PREREQUISITES: The Solitaire Game Solver is written in Java. To compile and to run the programs, you need the Java 1.4 compiler and appletviewer, respectively. These are part of the Java 2 SDK and Runtime Environment, available from . The "java" executable needs to be in a directory included in your PATH variable. ############################################################################ INSTALLATION: 1. Extract the tar.gz file to a directory of your choice. 2. The Java sources consist of two parts: a server, and two game applets. The applets and the server need to communicate. The communication setup depends on whether you want to run the applets in Java's appletviewer, or in your Internet browser. Check out src/config.java and and adjust the settings there if necessary. 3. If you changed config.java in the previous step, recompile it using javac and copy the file config.class to the applets/ directory. 4. If you choose to run the applets in your browser, install the script cgi-bin/proxy.pl on your WWW server. More information is contained within the script. 5. Download Spin from . Compile, and copy the spin executable to mckit/tools/. ############################################################################ RUNNING: 1. Change to the applets/ directory and run the server, e.g. "java Server". 2. (a) Using the appletviewer: Change to the applets/ directory and run the appletviewer on * peg.html (for Peg Solitaire) * 15puzzle-a.html (for the 15-puzzle) (substitute -a for -b, -c, or -d for other backgrounds) (b) Using your Internet browser: Point your browser to applets/index.html and proceed from there. ############################################################################ AUTHORS: The Solitaire Game Solver was created by Mario Bittner, Peter Reimann, and Patrick Schaffroth as a student programming project at the Institute for Formal Methods in Computer Science, University of Stuttgart. The project was supervised by Javier Esparza and Stefan Schwoon. The model-checking tools used to find solutions to the games are LoLA by Karsten Schmidt and Spin by Gerard Holzmann et al.