How to prevent a monitor to receive an unexpected event

[ghost]

In this spec we can see an Init state that handles the eMonitor_AtomicityInitialize event and a state WaitForEvents for the rest. And it seems to work fine.

When I do the same in my code, I arrive to faulty schedulers where the monitor didn't move yet to the WaitForEvents state, receives an unexpected event and fails. Events in monitors cannot be deferred, how can I handle this situation? is it normal that I encounter this or it could be related to a bug in my code?

[ankushdesai]

Hi, I didnt completely understand your question. Can you please paste the code that is leading to an error. Note that Monitors automatically receive events that it is observing.

[ghost]

Let's assume the following monitor:

spec SomeInvariant observes eInit, eMessage
{
start state Init {
on eInit goto WaitForEvents {
...
}
}

state WaitForEvents {
on eMessage do {
...
}
}
}

and this schedule happens:

Monitor enter state Init
Machine(1) announce eMessage
Monitor fails, cannot handle eMessage on state Init

So this happens because the monitor didn't change to state WaitForEvents "on time".

This is easy solved making Init state to handle all events, but I'm wondering why this works in the tutorial spec.

[ankushdesai]

Note that a spec machine is observing a sequence of events happening in the system. Another way to think about monitors is also that a monitor accepts a set of sequences of events that can happen in the system (events that lead to unhandled event exception are sequence or executions that are rejected by the Monitor). So the execution you mentioned above is not accepted by your monitor and hence leads to an error. It is required that a monitor accepts all executions (over the events observed) that can happen in the system.

Hope this helps!