Closed pglvdm closed 10 years ago
For a CML model like:
process Test = begin state m : map nat to nat:= {|->} operations Op(a: nat) r : nat frame rd m pre a in set dom m post r = m(a) @ Skip end
one gets a PO called:
(a in set (dom m))
but this should be seen in the context where the pre-condition is satusfied so one should get:
(a in set (dom m)) => (a in set (dom m))
which is probably will be possible to prove :-)
Fixed.
As with #223 , there is still an issue with collecting the state at the entry point of an operation. But the pre-condition is now correctly taken into account.
For a CML model like:
one gets a PO called:
but this should be seen in the context where the pre-condition is satusfied so one should get:
which is probably will be possible to prove :-)