Search code examples
promela

How do I model a boolean AND-evaluation in Promela non-atomically?

How do I model a boolean AND-evaluation in Promela non-atomically ?

I want to model the statement while (flag[j] == true && victim == i) where the AND-evaluation should be done non-atomically.

How is this possible?

Solution 
  • loop:
if 
:: flag[j] != true -> goto done
:: else
fi;

if 
:: victim != i -> goto done
:: else
fi;

/* body of 'while' */

goto loop;
done:

/* after 'while' */

    Note, although I don't have a Spin environment in front of me, what makes you think the conditional is atomic in the first place? I'd test with something like:

    byte i = 0

i++ >= 0 && i-- >= 0

never { assert (1 == i) }

    But, either way, the first code above shows how to make it non-atomic if need be.