Deadlock check causes subsequent error messages

[ukaea-chah]

With my model loaded, I ran Checks -> Constraint Based Checks -> Deadlock Freedom (with no extra predicate). It reported No Deadlock Found. But then when trying to run any event (SETUP_CONTEXT, INITIALISATION or any subsequent event) I get an error dialog:

ProB Problem

An Error occured
Reason:
ProB could not find valid constants wich satisfy the properties.
The properties were satisfiable

Since the deadlock check had been completed successfully, I don't expect it to cause repeated error reports.

Restarting the animation seemed to clear the error state.

This is with ProB 3.1.1.202402271349 in Rodin 3.8.0 or 3.9.0rc1.

[leuschel]

Thanks for the report. Can you send us the model which caused the problem?

[ukaea-chah]

Attached is a simple model which exhibits the behaviour for me. ex1.zip

The preamble to the above steps is: In Event-B explorer, right-click on mac0 then Start Animation / Model Checking.
An error "A timeout occured when finding constants after finding 3 solution(s)...." is reported, but I assume that this is normal for an unbounded set of possible initialisations. Click OK.