PROBPLUGIN - ProB 1 for Rodin - Execute with Custom Guard Issues
Description
Environment
None
Attachments
1
- 20 Dec 2013, 08:58 AM
Gliffy Diagrams
Activity
Show:
Jenkins Build Server December 20, 2013 at 12:56 PM
SUCCESS: Integrated in
ProB_eclipse_develop #1252
fixed https://probjira.atlassian.net/browse/PROBPLUGIN-88#icft=PROBPLUGIN-88 (jens: rev 389c98f635a552ff1e3cdd0704bbc12c383420c8)
de.prob.ui/plugin.xml
de.prob.ui/src/de/prob/ui/operationview/GetOperationByPredicateCommand2.java
de.prob.ui/src/de/prob/ui/operationview/CustomPreconditionInputDialog.java
de.prob.ui/src/de/prob/ui/operationview/EventBInputValidator.java
Fixed
Details
Details
Assignee
Jens Bendisposto
Jens BendispostoReporter
Michael Leuschel
Michael LeuschelPriority
Created December 20, 2013 at 8:58 AM
Updated December 20, 2013 at 12:56 PM
Resolved December 20, 2013 at 12:54 PM
Hi,
When I type something like
p = 2^8
into the custom guard then nothing happens and an exception occurs on the console log (see below).
With p=256 it works.
The event is the following one:
event largechoice any p sqrt where
@grd p∈1‥2^20
@grd2 sqrt ∗ sqrt = p
end
Im also unable to type something like
p=256 & x>0
as guard.
The dialog box shows the message “No Event-B Predicate”.
If I paste in the unicode and (∧) instead of & it works.
Michael
!ENTRY org.eclipse.ui 4 0 2013-12-20 09:52:44.431
!MESSAGE Unhandled event loop exception
!STACK 0
java.lang.NullPointerException
at de.prob.core.command.ExecuteOperationCommand.<init>(ExecuteOperationCommand.java:35)
at de.prob.core.command.ExecuteOperationCommand.<init>(ExecuteOperationCommand.java:28)
at de.prob.core.command.ExecuteOperationCommand.executeOperation(ExecuteOperationCommand.java:43)
at de.prob.ui.operationview.CustomPreconditionInputDialog.getCustomOperation(CustomPreconditionInputDialog.java:53)
at de.prob.ui.operationview.CustomPreconditionInputDialog.getOperation(CustomPreconditionInputDialog.java:69)
at de.prob.ui.operationview.CustomPreconditionDialogHandler.execute(CustomPreconditionDialogHandler.java:37)
at org.eclipse.ui.internal.handlers.HandlerProxy.execute(HandlerProxy.java:293)
at org.eclipse.core.commands.Command.executeWithChecks(Command.java:476)
at org.eclipse.core.commands.ParameterizedCommand.executeWithChecks(ParameterizedCommand.java:508)
at org.eclipse.ui.internal.handlers.HandlerService.executeCommand(HandlerService.java:169)
at org.eclipse.ui.internal.handlers.SlaveHandlerService.executeCommand(SlaveHandlerService.java:241)
at org.eclipse.ui.internal.handlers.SlaveHandlerService.executeCommand(SlaveHandlerService.java:241)
at org.eclipse.ui.menus.CommandContributionItem.handleWidgetSelection(CommandContributionItem.java:829)
at org.eclipse.ui.menus.CommandContributionItem.access$19(CommandContributionItem.java:815)
at org.eclipse.ui.menus.CommandContributionItem$5.handleEvent(CommandContributionItem.java:805)
at org.eclipse.swt.widgets.EventTable.sendEvent(EventTable.java:84)
at org.eclipse.swt.widgets.Display.sendEvent(Display.java:4128)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1457)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1480)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1465)
at org.eclipse.swt.widgets.Widget.notifyListeners(Widget.java:1270)
at org.eclipse.swt.widgets.Display.runDeferredEvents(Display.java:3974)
at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3613)
at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2701)
at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2665)
at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2499)
at org.eclipse.ui.internal.Workbench$7.run(Workbench.java:679)
at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)
at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:668)
at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
at org.eclipse.ui.internal.ide.application.IDEApplication.start(IDEApplication.java:123)
at org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:196)
at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)
at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)
at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:344)
at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)
at java.lang.reflect.Method.invoke(Method.java:597)
at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:622)
at org.eclipse.equinox.launcher.Main.basicRun(Main.java:577)
at org.eclipse.equinox.launcher.Main.run(Main.java:1410)