/* Without POR : 64K states
   With    POR : 511 states, because
    the cycle proviso (C3 condition of Clarke et al, Chapter 10)
    is avoided. */
    
active proctype p1()
{ byte x; /* Also init to 0 */
 do
 :: x < 255 -> x++
 :: x = 255
 od
}

active proctype p2()
{ byte y; /* Also init to 0 */
 do
 :: y < 255 -> y++
 :: y = 255 
 od
}