assume annotation on events

[shazqadeer]

Consider the following declaration in a P program:

event E3 assume 1;

The meaning is that in production assume acts as an assert but in testing it acts as an assume. One of the P regressions is currently failing. Upon debugging, it seems like PSharpTester is treating the assume annotation as an assert. But I can't be sure since I am not able to step into the PSharp code. Could you please check and clarify what is the PSharp behavior?

[akashlal]

You're right. This is a bug. Filed one to keep track: #396