search

hhu-stups / prob-issues

ProB issues (for probcli, ProB Tcl/Tk, ProB2, ProB2UI)
6 stars 0 forks source link

Deadlock check causes subsequent error messages #348

Open ukaea-chah opened 4 months ago

ukaea-chah commented 4 months ago

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 commented 4 months ago

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

ukaea-chah commented 4 months ago

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.