Thank you!
]]>-RSN
Use N as a seed for the random number generator.
Can be used in combination with compilation directives -DT_RAND and -DP_RAND (defined under experimental options below) to randomize the search process. N can be any non-negative integer value.
I will test and see if this works.
To be clear, what I am looking for is an option XXX such that given some tmp.pml, running
spin -run -a XXX tmp.pml
... will create the same trail file every time, if the property is violated.
]]>$ g3 [input]
and then in turn g3 makes a new Promela file **tmp.pml**, the contents of which differ depending on the [input], and runs
$ spin -run -a tmp.pml
g3 then processes the piped output and prints a result. I have unit tests for my code. When I run my code, I can run it 4 times in a row, and have it pass, fail, fail, pass. I am quite confident the reason has to do with Spin: I think Spin is finding a different trail file (a different path to the violation of the property in tmp.pml) each time I run it. I tried making Spin find the shortest trail file using the -i option but this made my tool very slow for larger inputs. I also tried manually setting the seed (I think the option was -nX where X is the seed) but this did not solve the problem.
How can I make Spin run deterministically, in order to make debugging my tool that invokes Spin easier?
]]>