IllegalArgumentException in B Console for symbolic return values

Description

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)

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

Assignee

Reporter

Priority

Created November 10, 2020 at 11:11 AM
Updated November 16, 2020 at 11:16 AM
Resolved November 16, 2020 at 11:16 AM