trunk/verif/Spin/Test/loops

   1 active proctype loop()
   2 {       byte a, b;
   3
   4         do
   5         :: a = (a+1)%3;
   6                 if
   7                 :: b = 2*a; skip
   8                 :: b = 2*a; accept: skip
   9                 fi;
  10 progress:       b--
  11         od
  12 }