SETUP_CONSTANTS not executed in ProB2-UI when initialisation fails

[leuschel]

When the INITITIALISATION fails then SETUP_CONSTANTS is not executed in ProB2-UI. Also, after manually going forward, one cannot execute the INITIALISATION by predicate (to obtain a visualisation of why it fails).

Example model:

MACHINE InitIF_Fails
SETS
 ID={aa,bb}
DEFINITIONS SET_PREF_TRACE_INFO == TRUE
CONSTANTS iv
PROPERTIES
 iv = aa
VARIABLES xx,yy
INVARIANT
 xx:ID & yy:ID
INITIALISATION 
   xx:=iv ;
   IF xx=iv THEN yy :: {iv}-{xx} 
            ELSE yy := iv END
END

The Compute Unsat Core command analyses the PROPERTIES, not the INITIALISATION here.

[iTitus]

SETUP_CONSTANTS fails with the following (uncaught) error:

de.prob.exception.ProBError: ProB reported Errors
ProB returned error messages:
Error: Initialisation statement fails:  yy :: {iv} - {xx} (...\InitIF_Fails.mch:14:17 to 14:33)
    at de.prob.animator.command.AbstractCommand.processErrorResult(AbstractCommand.java:123)
    at de.prob.animator.AnimatorImpl.execute(AnimatorImpl.java:197)
    at de.prob.animator.ReusableAnimator.execute(ReusableAnimator.java:189)
    at de.prob.animator.ReusableAnimator$InternalAnimator.execute(ReusableAnimator.java:60)
    at de.prob.statespace.StateSpace.execute(StateSpace.java:703)
    at de.prob.animator.IAnimator.execute(IAnimator.java:35)
    at de.prob.statespace.State.explore(State.java:469)
    at de.prob.statespace.State.exploreIfNeeded(State.java:506)
    at de.prob.statespace.Trace.add(Trace.java:197)
    at de.prob2.ui.operations.OperationsView.lambda$executeOperationIfPossible$11(OperationsView.java:370)
    at java.base/java.util.concurrent.Executors$RunnableAdapter.call(Executors.java:572)
    at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:317)
    at de.prob2.ui.internal.executor.CompletableFutureTask.run(CompletableFutureTask.java:40)
    at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1144)
    at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:642)
    at java.base/java.lang.Thread.run(Thread.java:1583)

After that one can click SETUP_CONSTANTS again and the error popup is not shown again. But the No valid constants/initialisation found warning is shown.

So this could also be a Prolog or Kernel problem?

[leuschel]

The initalisation failure errors are now added as state errors. This partly solves this problem.

There is still a small issues that: 1) we show the compute unsat core button (which debugs the PROPERTIES), 2) we do not specify exactly to the user whether it is constants/initialisation that fails, 3) we show a list of disabled events (even though only INITIALISATION should be shown as disabled). For 1) we could either remove the button for INITIALISATION or adapt it to extract the span_predicate from the state_error or similar.

[leuschel]

In ProB Tcl/Tk this now looks like this:

After clicking on the state error: and then clicking on visualise: