Missing error trace on invariant violation

68 views

Skip to first unread message

Lorin Hochstein

unread,

Sep 26, 2017, 10:31:27 PM9/26/17

to tlaplus

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

Spec:

------------------------- MODULE ConcurrentUpdates -------------------------

EXTENDS Naturals

CONSTANT N

ASSUME N \in Nat /\ N > 1

--algorithm Increment

variable count=0;

process P \in 1..N

variables temp=0,

i=0;

begin

set: i := i+1;

temp := count;

inc: count := temp+1;

if i < N then goto set end if;

end process

end algorithm

\* BEGIN TRANSLATION

VARIABLES count, pc, temp, i

vars == << count, pc, temp, i >>

ProcSet == (1..N)

Init == (* Global variables *)

/\ count = 0

(* Process P *)

/\ temp = [self \in 1..N |-> 0]

/\ i = [self \in 1..N |-> 0]

/\ pc = [self \in ProcSet |-> "set"]

set(self) == /\ pc[self] = "set"

/\ i' = [i EXCEPT ![self] = i[self]+1]

/\ temp' = [temp EXCEPT ![self] = count]

/\ pc' = [pc EXCEPT ![self] = "inc"]

/\ count' = count

inc(self) == /\ pc[self] = "inc"

/\ count' = temp[self]+1

/\ IF i[self] < N

THEN /\ pc' = [pc EXCEPT ![self] = "set"]

ELSE /\ pc' = [pc EXCEPT ![self] = "Done"]

/\ UNCHANGED << temp, i >>

P(self) == set(self) \/ inc(self)

Next == (\E self \in 1..N: P(self))

\/ (* Disjunct to prevent deadlock on termination *)

((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)

Spec == Init /\ [][Next]_vars

Termination == <>(\A self \in ProcSet: pc[self] = "Done")

\* END TRANSLATION

UpperBound == (\A self \in ProcSet: pc[self] = "Done") => count \leq N*N

TypeOK == /\ count \in Nat

/\ i \in [ProcSet -> Nat]

/\ pc \in [ProcSet -> {"set", "inc", "Done"}]

/\ temp \in [ProcSet -> Nat]

Inv == /\ TypeOK

/\ UpperBound

=============================================================================

Model:

(I'm using this to assist me in finding an inductive invariant)

Init: Inv

Next: Next

Values:

N <- 3

State constraint:

/\ temp \in [ProcSet -> 0..4]

/\ count < 5

Definition override:

Nat <- 0..5

Lorin

Markus Alexander Kuppe

unread,

Sep 27, 2017, 2:52:50 AM9/27/17

to tla...@googlegroups.com

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

lor...@gmail.com

unread,

Sep 27, 2017, 3:10:01 AM9/27/17

to tla...@googlegroups.com

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