Interleaving possibilities in Promela

Question

I am new to Promela and I'm having some difficulties understanding how to calculate the interleaving possibilities of a model. Which one of the statements is counted in the calculation (how do I know which one to take)? Does process P have 5, as well as Q?

  #define N 2
  proctype P(){
           int counter = 0
           do
           :: counter<N -> printf("P␣"); counter++
  
          :: else -> break
          od
  }
 
  proctype Q(){
           int counter = 0
           do
           :: counter<N -> printf("Q␣"); counter++
           :: else -> break
           od
  }
 
  init {
      atomic{   run P();
                run Q();}
  }```

1. Run the model in random and interactive mode. How many interleaving possibilities does
the program have and which?
2. How many possibilities are there for arbitrary values of N?

Answer 1

To calculate the interleaving possibilities of a model in Promela, you need to consider the non-deterministic choices made by the processes during execution. In this case, the processes P and Q run concurrently, and each process has two choices: either to execute the statement inside the loop (if the counter is less than N) or to break out of the loop.

1. The interleaving possibilities for the given program with N set to 2 are :
2. P and Q are running concurrently, and they have their own local counters (counter) starting from 0.
3. Both P and Q can increment their counters inside the loop while the condition counter<N is true.
4. If the counter reaches N in a process, it will break out of the loop.

Here are the possible interleavings:

1. P␣P␣Q␣Q␣ (Both P and Q increment their counters twice before breaking out of the loop.)
2. P␣Q␣P␣Q␣ (One P increments its counter, then Q increments its counter, and this continues.)

The interleaving possibilities are only two because the processes are running concurrently, and they have a deterministic choice to increment their counters until the condition counter<N is satisfied.

For your second question The number of possibilities for arbitrary values of N can be calculated as follows:

• Both P and Q can interleave in any order until their counters reach N.
• Since there are two processes (P and Q), each having N choices (increment the counter or break out), the total number of interleaving possibilities is 2^N * 2^N = 4^N.

So, for arbitrary values of N, there are 4^N possible interleaving execution sequences.