Bug: ETL property consisting only of quantification over def throws IllegalStateException
When trying to verify an ETL property that consists only of a quantification over a def, an IllegalStateException is thrown. For example:
def sub(i): <any formula>
check phi: forall (i: 1 ... 1) sub(i)
It seems this happens because the MtlFormula
of the check ("phi") instantiated with a specific parameter value, and the MtlFormula
of the def ("sub") instantiated with that parameter value are the same. When adding "phi", formula2name
in org.eclipse.trace4cps.tl.VerificationResult
already contains the formula (for "sub(1)"), so the exception is thrown.
Minimal test case:
Trace file:
E 0 0 ; a=1
ETL file:
def sub(i): {'a'=i}
check phi: forall (i: 1 ... 1) sub(i)
The error and stacktrace:
!ENTRY org.eclipse.ui 4 0 2023-03-21 12:10:05.676
!MESSAGE Unhandled event loop exception
!STACK 0
java.lang.IllegalStateException
at org.eclipse.trace4cps.tl.VerificationResult.add(VerificationResult.java:53)
at org.eclipse.trace4cps.tl.FormulaBuilder.create(FormulaBuilder.java:97)
at org.eclipse.trace4cps.tl.VerificationHelper.<init>(VerificationHelper.java:72)
at org.eclipse.trace4cps.ui.view.action.VerifyAction.doRun(VerifyAction.java:67)
at org.eclipse.trace4cps.ui.view.action.AbstractTraceViewAction.run(AbstractTraceViewAction.java:56)
at org.eclipse.jface.action.Action.runWithEvent(Action.java:474)
at org.eclipse.jface.action.ActionContributionItem.handleWidgetSelection(ActionContributionItem.java:579)
at org.eclipse.jface.action.ActionContributionItem.lambda$5(ActionContributionItem.java:452)
at org.eclipse.swt.widgets.EventTable.sendEvent(EventTable.java:89)
at org.eclipse.swt.widgets.Display.sendEvent(Display.java:4213)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1037)
at org.eclipse.swt.widgets.Display.runDeferredEvents(Display.java:4030)
at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3630)
at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine$5.run(PartRenderingEngine.java:1158)
at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:338)
at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine.run(PartRenderingEngine.java:1047)
at org.eclipse.e4.ui.internal.workbench.E4Workbench.createAndRunUI(E4Workbench.java:155)
at org.eclipse.ui.internal.Workbench.lambda$3(Workbench.java:658)
at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:338)
at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:557)
at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:154)
at org.eclipse.ui.internal.ide.application.IDEApplication.start(IDEApplication.java:150)
at org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:203)
at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:137)
at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:107)
at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:401)
at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:255)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
at java.lang.reflect.Method.invoke(Method.java:498)
at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:657)
at org.eclipse.equinox.launcher.Main.basicRun(Main.java:594)
at org.eclipse.equinox.launcher.Main.run(Main.java:1447)
at org.eclipse.equinox.launcher.Main.main(Main.java:1420)
Edited by Edo Mangelaars