spin
Spin is a model checker. Use promella (.pml) format to create state machines for which spin can "check" properties, validity, etc.
How to check a trace:
How to check a property written in the file given the property is assocated as such:
then check the property with:
Some more basic tools:
• Interactive mode (
• Properties and counterexamples (e.g. say "this state is never reached" and then see if it finds a counterexample)
•
•
http://spinroot.com/spin/Man/ for specific man-based information
spinroot.com for more info
How to check a trace:
spin -t0 -s -r the-file.pml
How to check a property written in the file given the property is assocated as such:
ltl property {
always (something = something else)
}
spin -run -a -DNOREDUCE sctp.pml
Some more basic tools:
• Interactive mode (
spin -i)
• Properties and counterexamples (e.g. say "this state is never reached" and then see if it finds a counterexample)
•
spin -run without arguments checks for deadlocks
•
spin -- will give you a list of spin commands / params (like a shitty man page missing lots of info)
http://spinroot.com/spin/Man/ for specific man-based information
spinroot.com for more info