Spinroot

Maxvonhippel

Member

Registered: 2019-09-13

Posts: 20

[SOLVED ... it is deterministic] Make Spin output deterministic

I am working on a tool that invokes Spin.  Let's call my tool g3.  So, the user runs

$ 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?

Last edited by Maxvonhippel (2020-02-17 22:50:02)

Maxvonhippel

Member

Registered: 2019-09-13

Posts: 20

Re: [SOLVED ... it is deterministic] Make Spin output deterministic

I suspect possibly the setting I want is this:

-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.

Last edited by Maxvonhippel (2020-01-29 17:33:04)

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: [SOLVED ... it is deterministic] Make Spin output deterministic

Spin verification runs should be deterministic, unless you specify some form of randomization or vary other parameters (like search depth, hashtable size in bitstate hashing, or things like -DT_RAND or -DP_RAND)
So, I suspect there's something else that's happening?

Maxvonhippel

Member

Registered: 2019-09-13

Posts: 20

Re: [SOLVED ... it is deterministic] Make Spin output deterministic

You're right, there was a bug elsewhere in my code, unrelated to Spin

Thank you!

Maxvonhippel

Member

Registered: 2019-09-13

Posts: 20

Re: [SOLVED ... it is deterministic] Make Spin output deterministic

By the way, for anyone who has this issue and comes across this post in the future - this bug is caused when you write code that uses Spin as a backend, but you don't make sure that your code deletes whatever models it wrote (and any trail files or other files output by Spin) after each execution of Spin.  It's just a side-effect bug from extra files lying around.  (So, not Spin's fault, basically automated user error.)