Interpreter: When reaching a deadlock it would be nice to see what events are rejected

[pglvdm]

When reaching a deadlock it would be nice to see what events are rejected In this way it would be possible to get an understanding of the status of the different actions.

[lausdahl]

Please give a small example of such a model and what events for that model that should be shown

[joey-coleman]

In the example below, the Process will synchronise with the environment (user) on a, then go on to the parallel in the parens. In the parallel, the left branch offers to synchronise on b.true, while the right offers c.1, so we reach deadlock.

It would be useful to produce a list of synchronisations that were offered but were "unmatched"/refused, in this case the set {b.true, c.1}.

channels
  a
  b : bool
  c : nat

process P = begin
@
  a -> (
    b.true -> Skip
    [| {b, c} |]
    c.1 -> Skip
  )
end

The console output for this model, choosing to synchronize on a, is:

Top CML behavior: WAITING_EVENT
Waiting for environment on : a, tock
Executing: a
Top CML behavior: RUNNING
Top CML behavior: WAITING_CHILD
DEADLOCKED

It would be good to have the final output be:

...
DEADLOCKED
Refused synchronisations: {b.true, c.1}

[lausdahl]

The design of the interpreter does not seem to support this. I think it is filtered such that a deadlock means that the transition sets are empty at top level so no information is available to why it became empty.

[joey-coleman]

Closing; we'll reopen in case we have a chance to redesign the interpreter.