Re: [tlaplus] Missing error trace on invariant violation

On Tue, Sep 26, 2017 at 11:52 PM, Markus Alexander Kuppe <tlaplus-go...@xxxxxxxxxxx> wrote:

On 27.09.2017 04:31, Lorin Hochstein wrote:
> Sometimes when I run the TLC Model Checker, it reports "Invariant Inv
> is violated", but there is no error-trace. Under what conditions does
> the checker not show an error trace?
>
> In some cases, when I reduce the size of the model, if the invariant
> is violated than a trace is available. However, in other cases I can't
> reproduce the error with a smaller model.
>
> Here's an example where this happens for me (The TLC model options I'm
> using appear at the bottom of the email):

Hi Lorin,

are you saying that with your ConcurrentUpdates spec and the given
model, the Toolbox never shows an error trace? Or does it fail to show
the trace intermittently hinting at a concurrency bug?

I tried you example ConcurrentUpdates locally with version 1.5.3 of the
Toolbox on Mac, Win and Linux and it showed an error trace every time.

Please provide more information about your environment (OS, Java
version, Toolbox version, ...).

Thanks

Markus

Hi Markus:

It consistently fails to show an error trace, it's perfectly reproducible on my machine (screen shot attached)

I'm running:

macOS 10.12.6

Java version: 1.8.0_131

Toolbox version: 1.5.3

I also have the vim bindings installed, as described here: https://groups.google.com/forum/#!topic/tlaplus/ZY2to27DhHU

The log also appears to indicate some exceptions were thrown:

java.lang.NullPointerException

at org.eclipse.core.runtime.Path.isPrefixOf(Path.java:701)

at org.lamport.tla.toolbox.tool.tlc.model.TLCSpec.getModels(TLCSpec.java:74)

at org.lamport.tla.toolbox.tool.tlc.ui.modelexplorer.ModelContentProvider.getChildren(ModelContentProvider.java:56)

at org.eclipse.ui.internal.navigator.extensions.SafeDelegateTreeContentProvider.getChildren(SafeDelegateTreeContentProvider.java:95)

at org.eclipse.ui.internal.navigator.extensions.SafeDelegateTreeContentProvider.getChildren(SafeDelegateTreeContentProvider.java:241)

at org.eclipse.ui.internal.navigator.extensions.SafeDelegateTreeContentProvider.getChildren(SafeDelegateTreeContentProvider.java:93)

at org.eclipse.ui.internal.navigator.NavigatorContentServiceContentProvider$1.run(NavigatorContentServiceContentProvider.java:157)

at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:42)

at org.eclipse.ui.internal.navigator.NavigatorContentServiceContentProvider.internalGetChildren(NavigatorContentServiceContentProvider.java:143)

at org.eclipse.ui.internal.navigator.NavigatorContentServiceContentProvider.getChildren(NavigatorContentServiceContentProvider.java:129)

at org.eclipse.jface.viewers.AbstractTreeViewer.getRawChildren(AbstractTreeViewer.java:1365)

at org.eclipse.jface.viewers.TreeViewer.getRawChildren(TreeViewer.java:353)

at org.eclipse.jface.viewers.StructuredViewer.getFilteredChildren(StructuredViewer.java:906)

at org.eclipse.jface.viewers.AbstractTreeViewer.getSortedChildren(AbstractTreeViewer.java:617)

at org.eclipse.jface.viewers.AbstractTreeViewer.updateChildren(AbstractTreeViewer.java:2645)

at org.eclipse.jface.viewers.AbstractTreeViewer.internalRefreshStruct(AbstractTreeViewer.java:1916)

at org.eclipse.jface.viewers.TreeViewer.internalRefreshStruct(TreeViewer.java:684)

at org.eclipse.jface.viewers.AbstractTreeViewer.internalRefreshStruct(AbstractTreeViewer.java:1923)

at org.eclipse.jface.viewers.TreeViewer.internalRefreshStruct(TreeViewer.java:684)

at org.eclipse.jface.viewers.AbstractTreeViewer.internalRefresh(AbstractTreeViewer.java:1891)

at org.eclipse.jface.viewers.AbstractTreeViewer.internalRefresh(AbstractTreeViewer.java:1848)

at org.eclipse.ui.navigator.CommonViewer.internalRefresh(CommonViewer.java:527)

at org.eclipse.jface.viewers.StructuredViewer$8.run(StructuredViewer.java:1554)

at org.eclipse.jface.viewers.StructuredViewer.preservingSelection(StructuredViewer.java:1462)

at org.eclipse.jface.viewers.TreeViewer.preservingSelection(TreeViewer.java:366)

at org.eclipse.jface.viewers.StructuredViewer.preservingSelection(StructuredViewer.java:1423)

at org.eclipse.jface.viewers.StructuredViewer.refresh(StructuredViewer.java:1551)

at org.eclipse.jface.viewers.ColumnViewer.refresh(ColumnViewer.java:534)

at org.eclipse.ui.navigator.CommonViewer.refresh(CommonViewer.java:347)

at org.eclipse.ui.navigator.CommonViewer.refresh(CommonViewer.java:490)

at org.eclipse.jface.viewers.StructuredViewer.refresh(StructuredViewer.java:1482)

at org.lamport.tla.toolbox.ui.navigator.ToolboxExplorer.refresh(ToolboxExplorer.java:129)

at org.lamport.tla.toolbox.ui.navigator.ToolboxExplorerResourceListener$1.run(ToolboxExplorerResourceListener.java:57)

at org.eclipse.swt.widgets.RunnableLock.run(RunnableLock.java:35)

at org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:135)

at org.eclipse.swt.widgets.Display.runAsyncMessages(Display.java:4024)

at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3700)

at org.eclipse.jface.window.Window.runEventLoop(Window.java:827)

at org.eclipse.jface.window.Window.open(Window.java:803)

at org.eclipse.jface.dialogs.MessageDialog.open(MessageDialog.java:330)

at org.eclipse.jface.dialogs.MessageDialog.open(MessageDialog.java:360)

at org.eclipse.jface.dialogs.MessageDialog.openQuestion(MessageDialog.java:455)

at org.lamport.tla.toolbox.ui.handler.ForgetSpecHandler.execute(ForgetSpecHandler.java:102)

at org.eclipse.ui.internal.handlers.HandlerProxy.execute(HandlerProxy.java:295)

at org.eclipse.ui.internal.handlers.E4HandlerProxy.execute(E4HandlerProxy.java:90)

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.e4.core.internal.di.MethodRequestor.execute(MethodRequestor.java:56)

at org.eclipse.e4.core.internal.di.InjectorImpl.invokeUsingClass(InjectorImpl.java:252)

at org.eclipse.e4.core.internal.di.InjectorImpl.invoke(InjectorImpl.java:234)

at org.eclipse.e4.core.contexts.ContextInjectionFactory.invoke(ContextInjectionFactory.java:132)

at org.eclipse.e4.core.commands.internal.HandlerServiceHandler.execute(HandlerServiceHandler.java:152)

at org.eclipse.core.commands.Command.executeWithChecks(Command.java:493)

at org.eclipse.core.commands.ParameterizedCommand.executeWithChecks(ParameterizedCommand.java:486)

at org.eclipse.e4.core.commands.internal.HandlerServiceImpl.executeHandler(HandlerServiceImpl.java:210)

at org.eclipse.e4.ui.workbench.renderers.swt.HandledContributionItem.executeItem(HandledContributionItem.java:799)

at org.eclipse.e4.ui.workbench.renderers.swt.HandledContributionItem.handleWidgetSelection(HandledContributionItem.java:675)

at org.eclipse.e4.ui.workbench.renderers.swt.HandledContributionItem.access$7(HandledContributionItem.java:659)

at org.eclipse.e4.ui.workbench.renderers.swt.HandledContributionItem$4.handleEvent(HandledContributionItem.java:592)

at org.eclipse.swt.widgets.EventTable.sendEvent(EventTable.java:84)

at org.eclipse.swt.widgets.Display.sendEvent(Display.java:4230)

at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1491)

at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1514)

at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1499)

at org.eclipse.swt.widgets.Widget.notifyListeners(Widget.java:1299)

at org.eclipse.swt.widgets.Display.runDeferredEvents(Display.java:4072)

at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3698)

at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine$4.run(PartRenderingEngine.java:1127)

at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:337)

at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine.run(PartRenderingEngine.java:1018)

at org.eclipse.e4.ui.internal.workbench.E4Workbench.createAndRunUI(E4Workbench.java:156)

at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:694)

at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:337)

at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:606)

at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:150)

at org.lamport.tla.toolbox.Application.start(Application.java:93)

at org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:196)

at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:134)

at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:104)

at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:380)

at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:235)

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:669)

at org.eclipse.equinox.launcher.Main.basicRun(Main.java:608)

at org.eclipse.equinox.launcher.Main.run(Main.java:1515)

!ENTRY org.eclipse.ui.navigator 4 0 2017-09-27 00:01:16.511

!MESSAGE An exception occurred invoking extension: toolbox.content.ModelContent for object org.lamport.tla.toolbox.spec.Spec@740b6628

!STACK 0