IllegalArgumentException in B Console for symbolic return values
Description
Environment
None
Activity
Show:
Michael Leuschel November 10, 2020 at 12:14 PM
get_error_messages now returns the empty list when there are no warnings and no errors, commit
0793c25bac7ec256ebe6af1992386989593c7aa9
There is, however, still the issue that if warnings occur during evaluation of an expression, we get the result string as first part of the error term, which would still lead to an illegal argument exception. Ideally, we should make the code in Java more robust and also extend it to include messages / warnings.
Michael Leuschel November 10, 2020 at 11:21 AM
This is possibly due to the fact that messages are now passed to ProB2; in b_interpreter.pl we have:
Msg = 'Keeping comprehension-set symbolic (you may want to use the /*@symbolic*/ pragma to prevent this message, unless it was due to a WD-Error), identifiers: ',
add_message(b_compute_comprehension_set,Msg,P,B),Fixed
Details
Details
Assignee
Unassigned
UnassignedReporter
Michael Leuschel
Michael LeuschelPriority
MajorCreated November 10, 2020 at 11:11 AM
Updated November 16, 2020 at 11:16 AM
Resolved November 16, 2020 at 11:16 AM
When typing the following into the B Console
{x|x:NATURAL & not(x:NAT)}
I get this exception:
[2020-11-10 12:08:40,081, 824701 ms] "JavaFX Application Thread" [ERROR] de.prob2.ui.ProB2.lambda$startInBackground$5(ProB2.java:188): Uncaught exception on thread Thread[JavaFX Application Thread,5,main] java.lang.IllegalArgumentException: Unknown error type: /*@symbolic*/ {x|x : NATURAL & x /: {0,1,2,3}} at de.prob.animator.domainobjects.EvalResult.getEvalResult(EvalResult.java:182) at de.prob.animator.command.EvaluateFormulasCommand.processResult(EvaluateFormulasCommand.java:50) at de.prob.animator.AnimatorImpl.execute(AnimatorImpl.java:90) at de.prob.statespace.StateSpace.execute(StateSpace.java:577) at de.prob.statespace.State.evalFormulas(State.java:230) at de.prob.statespace.State.eval(State.java:246) at de.prob.statespace.State.eval(State.java:206) at de.prob.statespace.Trace.evalCurrent(Trace.java:88) at de.prob2.ui.consoles.b.BInterpreter.exec(BInterpreter.java:136) at de.prob2.ui.consoles.Console.handleEnter(Console.java:282) at de.prob2.ui.consoles.Console.lambda$setEvents$15(Console.java:119) at org.fxmisc.wellbehaved.event.InputMap.lambda$consume$2(InputMap.java:256) at java.base/java.util.Optional.map(Optional.java:258) at org.fxmisc.wellbehaved.event.PatternActionMap.lambda$forEachEventType$1(InputMap.java:414) at org.fxmisc.wellbehaved.event.InputHandlerMap.lambda$null$0(InputHandlerMap.java:22) at org.fxmisc.wellbehaved.event.InputHandler.handle(InputHandler.java:50) at javafx.base/com.sun.javafx.event.CompositeEventHandler$NormalEventHandlerRecord.handleBubblingEvent(CompositeEventHandler.java:218) at javafx.base/com.sun.javafx.event.CompositeEventHandler.dispatchBubblingEvent(CompositeEventHandler.java:80) at javafx.base/com.sun.javafx.event.EventHandlerManager.dispatchBubblingEvent(EventHandlerManager.java:238) at javafx.base/com.sun.javafx.event.EventHandlerManager.dispatchBubblingEvent(EventHandlerManager.java:191) at javafx.base/com.sun.javafx.event.CompositeEventDispatcher.dispatchBubblingEvent(CompositeEventDispatcher.java:59) at javafx.base/com.sun.javafx.event.BasicEventDispatcher.dispatchEvent(BasicEventDispatcher.java:58) at javafx.base/com.sun.javafx.event.EventDispatchChainImpl.dispatchEvent(EventDispatchChainImpl.java:114) at javafx.base/com.sun.javafx.event.BasicEventDispatcher.dispatchEvent(BasicEventDispatcher.java:56) at javafx.base/com.sun.javafx.event.EventDispatchChainImpl.dispatchEvent(EventDispatchChainImpl.java:114) at javafx.base/com.sun.javafx.event.BasicEventDispatcher.dispatchEvent(BasicEventDispatcher.java:56) at javafx.base/com.sun.javafx.event.EventDispatchChainImpl.dispatchEvent(EventDispatchChainImpl.java:114) at javafx.base/com.sun.javafx.event.BasicEventDispatcher.dispatchEvent(BasicEventDispatcher.java:56) at javafx.base/com.sun.javafx.event.EventDispatchChainImpl.dispatchEvent(EventDispatchChainImpl.java:114) at javafx.base/com.sun.javafx.event.BasicEventDispatcher.dispatchEvent(BasicEventDispatcher.java:56) at javafx.base/com.sun.javafx.event.EventDispatchChainImpl.dispatchEvent(EventDispatchChainImpl.java:114) at javafx.base/com.sun.javafx.event.BasicEventDispatcher.dispatchEvent(BasicEventDispatcher.java:56) at javafx.base/com.sun.javafx.event.EventDispatchChainImpl.dispatchEvent(EventDispatchChainImpl.java:114) at javafx.base/com.sun.javafx.event.BasicEventDispatcher.dispatchEvent(BasicEventDispatcher.java:56) at javafx.base/com.sun.javafx.event.EventDispatchChainImpl.dispatchEvent(EventDispatchChainImpl.java:114) at javafx.base/com.sun.javafx.event.EventUtil.fireEventImpl(EventUtil.java:74) at javafx.base/com.sun.javafx.event.EventUtil.fireEvent(EventUtil.java:54) at javafx.base/javafx.event.Event.fireEvent(Event.java:198) at javafx.graphics/javafx.scene.Scene$KeyHandler.process(Scene.java:4058) at javafx.graphics/javafx.scene.Scene$KeyHandler.access$1500(Scene.java:4004) at javafx.graphics/javafx.scene.Scene.processKeyEvent(Scene.java:2121) at javafx.graphics/javafx.scene.Scene$ScenePeerListener.keyEvent(Scene.java:2595) at javafx.graphics/com.sun.javafx.tk.quantum.GlassViewEventHandler$KeyEventNotification.run(GlassViewEventHandler.java:217) at javafx.graphics/com.sun.javafx.tk.quantum.GlassViewEventHandler$KeyEventNotification.run(GlassViewEventHandler.java:149) at java.base/java.security.AccessController.doPrivileged(AccessController.java:391) at javafx.graphics/com.sun.javafx.tk.quantum.GlassViewEventHandler.lambda$handleKeyEvent$1(GlassViewEventHandler.java:248) at javafx.graphics/com.sun.javafx.tk.quantum.QuantumToolkit.runWithoutRenderLock(QuantumToolkit.java:390) at javafx.graphics/com.sun.javafx.tk.quantum.GlassViewEventHandler.handleKeyEvent(GlassViewEventHandler.java:247) at javafx.graphics/com.sun.glass.ui.View.handleKeyEvent(View.java:547) at javafx.graphics/com.sun.glass.ui.View.notifyKey(View.java:971)