Lets say we have this piece of code:
int x = 3;
int y = 5;
int z = 0;
active proctype P(){
if
:: x > y -> z = x
:: else -> z = y
fi
}
active proctype Q(){
x++
}
active proctype R(){
y = y - x
}
I don't understand what interleavings are. What exactly are interleaving and where and how many are there in my example above?
In Promela, a process with an executable instruction can be scheduled for execution at any given point in time, provided that no other process is currently executing a uninterruptible atomic sequence.
A single instruction, on its own, it is executed atomically. In order to have multiple instructions in the same atomic sequence, one can use either atomic { } or d_step { }. I refer you to this other question on the topic for learning the difference among the two.
In your case, a possible execution trace is:
x++ // Q(), x := 4
z = y // P(), z := 5
y = y - x // R(), y := 1
Another, totally admissible, possible execution trace is:
y = y - x // R(), y := 2
x++ // Q(), x := 4
z = x // P(), z := 4
The processes are interleaved with one another, meaning that after each instruction of some process P_i (which is not in an uninterruptible atomic sequence), the process P_i can be preempted and some other process P_j can be scheduled for execution (provided that it actually has to execute something).
It is is nothing different from what happens in a multi-tasking unix machine, in which processes are interleaved one another and compete for access to the CPU.