spinlock model: Simplify state-space

spinlock model: Simplify state-space

Remove useless busy-looping, useless in Promela. Same semantic as the
new code:

Quoting Michel Dagenais <michel.dagenais@polymtl.ca>:

> http://spinroot.com/spin/Man/condition.html
> In Promela , a standalone expression is a valid statement. Execution
> of a condition statement is blocked until the expression evaluates to
> a non-zero value (or, equivalently, to the boolean value true ).
>
> http://spinroot.com/spin/Man/separators.html
> The semicolon and the arrow are equivalent statement separators in
> Promela. The convention is to reserve the use of the arrow separator
> to follow condition statements. The arrow symbol can thus be used to
> visually identify those points in the code where execution could
> block.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>