# test quantifiers on processes
# note: order of output is nondeterministic

resource a()

   process simple [ i=1 to 2 ] {
      write(i)
   }

   const int N = 3
   process p0  {
      write("in p0")
   }

   process p1  {
      write("in p1")
   }

   process p2 [ i=1 to N ] {
      write("in p2")
   }

   process p3 [ i=0 to 1,j=-1 downto -2 ] {
      write("in p3",i,j)
   }

   process p4 [ i=1 to 5 st i != 3,j= 1 to 4 st i <= j ] {
      write("in p4",i,j)
   }

end