A forum for Spin users
You are not logged in.
Pages: 1
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
Offline
Pages: 1