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