search

hhu-stups / prob-issues

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

Exception when trying to visualise failed execute by predicate in ProB2-UI #362

Open leuschel opened 3 weeks ago

leuschel commented 3 weeks ago

When right-clicking on a disabled event and selecting "Execute by Predicate..." and then after the failed execution trying to click on visualise, we get an exception:

Screenshot 2024-08-19 at 14 24 20

leuschel commented 3 weeks ago

Here is the exception:

de.prob.animator.command.ExecuteOperationException: Executing operation ... with additional predicate produced errors: Could not execute operation evc_acq_message_ma in state 2
        at de.prob.statespace.StateSpace.transitionFromPredicate(StateSpace.java:257)
        at de.prob.statespace.StateSpace.transitionFromPredicate(StateSpace.java:277)
        at de.prob2.ui.operations.ExecuteByPredicateStage.executeSync(ExecuteByPredicateStage.java:159)
        at java.base/java.util.concurrent.Executors$RunnableAdapter.call(Executors.java:539)
        at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264)
        at de.prob2.ui.internal.executor.CompletableFutureTask.run(CompletableFutureTask.java:40)
        at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1136)
        at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:635)
        at java.base/java.lang.Thread.run(Thread.java:833)
[ERROR] Uncaught exception on thread Thread[JavaFX Application Thread,5,main]
java.lang.RuntimeException: java.lang.reflect.InvocationTargetException
        at javafx.fxml@22.0.2/javafx.fxml.FXMLLoader$MethodHandler.invoke(FXMLLoader.java:1863)
        at javafx.fxml@22.0.2/javafx.fxml.FXMLLoader$ControllerMethodEventHandler.handle(FXMLLoader.java:1731)
        at javafx.base@22.0.2/com.sun.javafx.event.CompositeEventHandler.dispatchBubblingEvent(CompositeEventHandler.java:86)
        at javafx.base@22.0.2/com.sun.javafx.event.EventHandlerManager.dispatchBubblingEvent(EventHandlerManager.java:232)
        at javafx.base@22.0.2/com.sun.javafx.event.EventHandlerManager.dispatchBubblingEvent(EventHandlerManager.java:189)
        at javafx.base@22.0.2/com.sun.javafx.event.CompositeEventDispatcher.dispatchBubblingEvent(CompositeEventDispatcher.java:59)
        at javafx.base@22.0.2/com.sun.javafx.event.BasicEventDispatcher.dispatchEvent(BasicEventDispatcher.java:58)
        at javafx.base@22.0.2/com.sun.javafx.event.EventDispatchChainImpl.dispatchEvent(EventDispatchChainImpl.java:114)
        at javafx.base@22.0.2/com.sun.javafx.event.BasicEventDispatcher.dispatchEvent(BasicEventDispatcher.java:56)
        at javafx.base@22.0.2/com.sun.javafx.event.EventDispatchChainImpl.dispatchEvent(EventDispatchChainImpl.java:114)
        at javafx.base@22.0.2/com.sun.javafx.event.BasicEventDispatcher.dispatchEvent(BasicEventDispatcher.java:56)
        at javafx.base@22.0.2/com.sun.javafx.event.EventDispatchChainImpl.dispatchEvent(EventDispatchChainImpl.java:114)
        at javafx.base@22.0.2/com.sun.javafx.event.EventUtil.fireEventImpl(EventUtil.java:74)
        at javafx.base@22.0.2/com.sun.javafx.event.EventUtil.fireEvent(EventUtil.java:49)
        at javafx.base@22.0.2/javafx.event.Event.fireEvent(Event.java:198)
        at javafx.graphics@22.0.2/javafx.scene.Node.fireEvent(Node.java:8917)
        at javafx.controls@22.0.2/javafx.scene.control.Button.fire(Button.java:203)
        at javafx.controls@22.0.2/com.sun.javafx.scene.control.behavior.ButtonBehavior.mouseReleased(ButtonBehavior.java:207)
        at javafx.controls@22.0.2/com.sun.javafx.scene.control.inputmap.InputMap.handle(InputMap.java:274)
        at javafx.base@22.0.2/com.sun.javafx.event.CompositeEventHandler$NormalEventHandlerRecord.handleBubblingEvent(CompositeEventHandler.java:247)
        at javafx.base@22.0.2/com.sun.javafx.event.CompositeEventHandler.dispatchBubblingEvent(CompositeEventHandler.java:80)
        at javafx.base@22.0.2/com.sun.javafx.event.EventHandlerManager.dispatchBubblingEvent(EventHandlerManager.java:232)
        at javafx.base@22.0.2/com.sun.javafx.event.EventHandlerManager.dispatchBubblingEvent(EventHandlerManager.java:189)
        at javafx.base@22.0.2/com.sun.javafx.event.CompositeEventDispatcher.dispatchBubblingEvent(CompositeEventDispatcher.java:59)
        at javafx.base@22.0.2/com.sun.javafx.event.BasicEventDispatcher.dispatchEvent(BasicEventDispatcher.java:58)
        at javafx.base@22.0.2/com.sun.javafx.event.EventDispatchChainImpl.dispatchEvent(EventDispatchChainImpl.java:114)
        at javafx.base@22.0.2/com.sun.javafx.event.BasicEventDispatcher.dispatchEvent(BasicEventDispatcher.java:56)
        at javafx.base@22.0.2/com.sun.javafx.event.EventDispatchChainImpl.dispatchEvent(EventDispatchChainImpl.java:114)
        at javafx.base@22.0.2/com.sun.javafx.event.BasicEventDispatcher.dispatchEvent(BasicEventDispatcher.java:56)
        at javafx.base@22.0.2/com.sun.javafx.event.EventDispatchChainImpl.dispatchEvent(EventDispatchChainImpl.java:114)
        at javafx.base@22.0.2/com.sun.javafx.event.EventUtil.fireEventImpl(EventUtil.java:74)
        at javafx.base@22.0.2/com.sun.javafx.event.EventUtil.fireEvent(EventUtil.java:54)
        at javafx.base@22.0.2/javafx.event.Event.fireEvent(Event.java:198)
        at javafx.graphics@22.0.2/javafx.scene.Scene$MouseHandler.process(Scene.java:3985)
        at javafx.graphics@22.0.2/javafx.scene.Scene.processMouseEvent(Scene.java:1891)
        at javafx.graphics@22.0.2/javafx.scene.Scene$ScenePeerListener.mouseEvent(Scene.java:2709)
        at javafx.graphics@22.0.2/com.sun.javafx.tk.quantum.GlassViewEventHandler$MouseEventNotification.run(GlassViewEventHandler.java:411)
        at javafx.graphics@22.0.2/com.sun.javafx.tk.quantum.GlassViewEventHandler$MouseEventNotification.run(GlassViewEventHandler.java:301)
        at java.base/java.security.AccessController.doPrivileged(AccessController.java:399)
        at javafx.graphics@22.0.2/com.sun.javafx.tk.quantum.GlassViewEventHandler.lambda$handleMouseEvent$2(GlassViewEventHandler.java:450)
        at javafx.graphics@22.0.2/com.sun.javafx.tk.quantum.QuantumToolkit.runWithoutRenderLock(QuantumToolkit.java:430)
        at javafx.graphics@22.0.2/com.sun.javafx.tk.quantum.GlassViewEventHandler.handleMouseEvent(GlassViewEventHandler.java:449)
        at javafx.graphics@22.0.2/com.sun.glass.ui.View.handleMouseEvent(View.java:551)
        at javafx.graphics@22.0.2/com.sun.glass.ui.View.notifyMouse(View.java:937)
        at javafx.graphics@22.0.2/com.sun.glass.ui.mac.MacView.notifyMouse(MacView.java:127)
Caused by: java.lang.reflect.InvocationTargetException: null
        at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
        at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:77)
        at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
        at java.base/java.lang.reflect.Method.invoke(Method.java:568)
        at com.sun.javafx.reflect.Trampoline.invoke(MethodUtil.java:72)
        at jdk.internal.reflect.GeneratedMethodAccessor2.invoke(Unknown Source)
        at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
        at java.base/java.lang.reflect.Method.invoke(Method.java:568)
        at javafx.base@22.0.2/com.sun.javafx.reflect.MethodUtil.invoke(MethodUtil.java:270)
        at javafx.fxml@22.0.2/com.sun.javafx.fxml.MethodHelper.invoke(MethodHelper.java:84)
        at javafx.fxml@22.0.2/javafx.fxml.FXMLLoader$MethodHandler.invoke(FXMLLoader.java:1860)
        ... 44 common frames omitted
Caused by: java.lang.NullPointerException: Cannot invoke "de.prob.model.representation.BEvent.getChildrenOfType(java.lang.Class)" because "operation" is null
        at de.prob2.ui.operations.ExecuteByPredicateStage.buildInnerPredicate(ExecuteByPredicateStage.java:244)
        at de.prob2.ui.operations.ExecuteByPredicateStage.buildVisualizationPredicate(ExecuteByPredicateStage.java:285)
        at de.prob2.ui.operations.ExecuteByPredicateStage.visualizePredicate(ExecuteByPredicateStage.java:211)
        ... 55 common frames omitted
leuschel commented 3 weeks ago

The error does not seem to occur always. Sometimes a wrong visualisation predicate is generated, e.g., for the event get below we try to visualise #x2.(1=1), if we disable the SHOW_EVENTB_ANY... preference, we visualise (1=1) which is also incorrect:

MACHINE InitIF_Fails
SETS
 ID={aa,bb}
DEFINITIONS 
  SET_PREF_SHOW_EVENTB_ANY_VALUES == TRUE; 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
OPERATIONS
 get = ANY x2 WHERE x2=xx & x2=bb THEN skip END
END
iTitus commented 3 weeks ago

The wrong predicate #x2.(1=1) is caused by not adding a value for x2 in the predicate builder. 1=1 is the fallback predicate.

When given a valid value it looks like this: image #x2.(x2=bb) (or aa) The predicate is still missing the WHERE clause because it is not treated as a guard, this might have to be fixed in the Kernel.

Without the preference, the ANY variables are not treated as parameters and thus there are no predicates to be built - fallback to 1=1. Sadly it is not possible to set a value for x2 from the outside: image