local x, y : int where x = 0, y = 0 P1 :: [ await x < y ]
If-then-else statement: local x, y : int where x = 0, y = 0 P1 :: [if x < y then x := x + 1 else y := y - x ]
local x, y : int where x = 0, y = 0 P1 :: [if x < y then x := x + 1 else y := y - x ]