Multithreading in SPIN model checker

Question

How do we parametrize the SPIN model with the number of threads? I am using the standard SPIN model checker. Does it have options to set the number of parallel threads? I checked the reference but didn't find anything useful

Answer 1

You can dynamically spawn a Promela process using the run operator. You can thus iterate as:

#define TRY_COUNT 5
byte index = 0;
do
:: index == TRY_COUNT -> break
:: else -> index++; run theProcess()
od

You can also define a file like:

active [TRY_COUNT] proctype foo () {
  printf ("PID: %d\n", _pid);
  assert (true)
}

init {
  assert (true)
}

and then run a SPIN simulation:

$ spin -DTRY_COUNT=4 bar.pml
              PID: 2
      PID: 0
          PID: 1
                  PID: 3
5 processes created

or a verification

$ spin -DTRY_COUNT=4 -a bar.pml
$ gcc -o bar pan.c
$ ./bar
hint: this search is more efficient if pan.c is compiled -DSAFETY

(Spin Version 6.3.2 -- 17 May 2014)
    + Partial Order Reduction
...