// dummy module M x : [0..1] init 0; [] x=0 -> true; endmodule