A forum for Spin users
You are not logged in.
Pages: 1
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
I wish to announce the publication of a tutorial on the use of search diversity in Spin:
Mordechai (Moti) Ben-Ari and Fatima Kaloti-Hallak. Demonstrating random and parallel algorithms with Spin. ACM Inroads 3, 3 (September 2012), 36-38. http://doi.acm.org/10.1145/2339055.2339069
This joins the earlier tutorial:
Mordechai (Moti) Ben-Ari. A primer on model checking. ACM Inroads 1, 1 (March 2010), 40-47. http://doi.acm.org/10.1145/1721933.1721950
I'd be interested in hearing about the use of this material in teaching!
Moti
I have released new versions of the Erigone model checker (a Spin-compatible model checker intended for teaching) and its GUI called EUI. This was done to clean up the treatment of internal LTL specifications. For Erigone the changes are minor, but for EUI:
1. For simplicity, only internal LTL specifications are supported.
2. Named specifications are now supported:
ltl mutex { []!(csp && csq) }
ltl nostarve { []<>csp && []<>csq }
and you can interactively specify which one to use in a field called "LTL name".
Download at:
http://code.google.com/p/erigone/
http://code.google.com/p/jspin/
Thanks
Moti
I'm not sure that I understand your model but there are a few problems:
1. When I tried to run Spin, the preprocessor failed.
I don't know enough C to know why ...
By substituting the "define"s manually,
I received assertion errors.
2. The correct mode for checking assertion errors is "Safety".
"Acceptance" is used when there is a "cycle"
usually within a never-claim or a one derived from an LTL formula.
3. In your monitor, a nondeterministic choice is made between
the two assertions. You probably want to check both of them
so they should be in the same alternative.
I hope this helps,
Moti
Version 3.1.0 of the Erigone Model Checker includes a postprocessor VMC which generates graphs showing the model checking process step-by-step: the creation and search of the state space. It's hard to explain so I've prepared a short video demonstration (pardon my lack of radiophonic talent!):
http://screencast.com/t/HNQ5l1lijXsJ
Erigone is a Spin-compatible model checker intended for educational purposes and can be downloaded from Google Code:
http://code.google.com/p/erigone/
Moti
> A typo in the ACM Inroads: " A Primer on Model Checking" by Mordechai (Moti) Ben-Ari
> page 44: counter == 10 not counter = 10
Correct, this is a typo.
My apologies.
Moti
Erigone is a Spin-compatible model checker designed for educational purposes:
* It is single executable file so installation and use are trivial.
* Erigone produces a detailed, customizable trace of the model-checking algorithms in a keyword-based format that can be directly read or used by other tools.
* The source code is documented in detail.
Version 3 now supports almost all of Promela.
For more detail see:
[url]http://stwww.weizmann.ac.il/g-cs/benari/erigone/index.html[/url]
Download from:
[url]http://code.google.com/p/erigone/[/url]
Discussions on the mailing list:
[url]http://groups.google.com/group/Erigone[/url]
Moti
I have prepared a short document explaining the new features of Promela in Spin 6. It is intended to supplement my textbook: Principles of the Spin Model Checker. Springer, 2008. In addition, there are versions of the programs in the book that were modified to use the new features.
The document and the program archive can be downloaded for free from my website:
[url]http://stwww.weizmann.ac.il/g-cs/benari/books/index.html#spin[/url]
or from the book's page on Springer's website:
[url]http://www.springer.com/978-1-84628-769-5[/url]
Moti Ben-Ari
The output format of Spin 6.0.0 is changed and this makes it incompatible
with the jSpin development environment. A new version (jSpin 5.0) has been
created and is available at:
[url]http://code.google.com/p/jspin/[/url]
This version also enables the user to specify interactively which one of a set
of named internal ltl formulas will be used for a verification.
Please contact me if there are any problems.
Moti
Pages: 1