Davide,
Thank you for the clarification. My error was to interpret the "not"
operator as an existential function (ie: "there is no such object that
exists") and viewing the object as a unit, rather than, as you pointed out,
logically manipulable.
In light of that, the logical OR in place of the co
Both should fire when there is no message.
This said, the two are not equivalent.
The negation of
Message( sent == true, status != INITIALIZED )
is:
Message( sent == false *||* status == INITIALIZED )
That is, by deMorgan's laws, you need to negate
the operators AND flip the and/or connectives.
I
Are the two following statements not equivalent?
forall($msg:Message()
Message(this==$msg, sent==true, status!=State._INITIALIZED)
)
not( Message(sent==false, status==State._INITIALIZED) )
My understanding is that they both ensure that there are no Message objects
in WM
