BEGIN EXPECTED CONSTRAINT 0 < p & p <= 1 END EXPECTED CONSTRAINT (* This constraint is an expected result, and was manually written since IMITATOR is not able to infer a result on this model. This expected result is provided without any warranty. *)