Spinroot

benari

Member

Registered: 2010-11-24

Posts: 9

Sokoban solver in Promela

I implemented a naive Sokoban solver in Promela. Solving a Sokoban puzzle is very difficult and a naive solver can solve only the simplest puzzles. I hope that this program will be useful for experimenting the Spin's facilities for improving the efficiency of model checking: hash functions, bitstate verification, multicore search diversity.

For convenience the zip file is stored on my jSpin site:
https://code.google.com/p/jspin/

Moti