[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Re: TLC didn't display statistics

From: victor.n...@xxxxxxxxx
Date: Sat, 29 Mar 2014 02:20:43 -0700 (PDT)
References: <6dd8b988-1d37-45bf-b7a2-37dfdb368285@googlegroups.com> <78edb144-d6fa-47de-b0d0-e984984ae818@googlegroups.com> <532FD7C8.9060706@lemmster.de>
Hi,

I have the same problem, on archlinux 64 bits, here is the logs that are appended to the log file after running TLC:

!ENTRY org.lamport.tla.toolbox 1 -1 2014-03-29 10:19:19.184
!MESSAGE footFileName = /home/victor/code/tla/OneBitClock.tla

!ENTRY org.lamport.tla.toolbox.tool.tlc 1 0 2014-03-29 10:19:19.288
!MESSAGE TLC ARGUMENTS: [-tool, -coverage, 3, -metadir, /home/victor/code/tla/OneBitClock.toolbox/Model_1, -fpbits, 0, MC, -workers, 2, -fp, 0, -checkpoint, 15, -config, MC.cfg]

!ENTRY org.lamport.tla.toolbox.tool.tlc 1 0 2014-03-29 10:19:19.288
!MESSAGE JAVA VM ARGUMENTS: [-Dtlc2.tool.fp.FPSet.impl=tlc2.tool.fp.MSBDiskFPSet, -Xmx884m]

!ENTRY org.lamport.tla.toolbox.tool.tlc 1 0 2014-03-29 10:19:19.289
!MESSAGE Nested JVM used for model checker is: /usr/lib/jvm/java-7-openjdk/jre

!ENTRY org.lamport.tla.toolbox.tool.tlc.ui 1 -1 2014-03-29 10:19:19.294
!MESSAGE TLCOutputSourceRegistry for model checking maintains 1 sources.

!ENTRY org.lamport.tla.toolbox.tool.tlc.ui 1 -1 2014-03-29 10:19:19.294
!MESSAGE The source OneBitClock___Model_1.launch has 4 prio and 1 listeners

!ENTRY org.lamport.tla.toolbox 1 -1 2014-03-29 10:19:19.403
!MESSAGE Spec build invoked on OneBitClock ...

!ENTRY org.lamport.tla.toolbox 1 -1 2014-03-29 10:19:19.421
!MESSAGE Resulting status is:  parsed 
... build invocation finished.

!ENTRY org.lamport.tla.toolbox.tool.tlc.ui 4 0 2014-03-29 10:19:19.918
!MESSAGE Error reading progress information
!STACK 0
java.lang.NumberFormatException: For input string: "6 857"
	at java.lang.NumberFormatException.forInputString(NumberFormatException.java:65)
	at java.lang.Long.parseLong(Long.java:441)
	at java.lang.Long.parseLong(Long.java:483)
	at org.lamport.tla.toolbox.tool.tlc.output.data.StateSpaceInformationItem.parse(StateSpaceInformationItem.java:143)
	at org.lamport.tla.toolbox.tool.tlc.output.data.TLCModelLaunchDataProvider.onOutput(TLCModelLaunchDataProvider.java:375)
	at org.lamport.tla.toolbox.tool.tlc.output.source.CachingTLCOutputSource.onOutput(CachingTLCOutputSource.java:89)
	at org.lamport.tla.toolbox.tool.tlc.output.source.CachingTLCOutputSource.onOutput(CachingTLCOutputSource.java:57)
	at org.lamport.tla.toolbox.tool.tlc.output.source.TagBasedTLCOutputIncrementalParser$TLCOutputPartitionChangeListener.documentPartitioningChanged(TagBasedTLCOutputIncrementalParser.java:226)
	at org.eclipse.jface.text.AbstractDocument.fireDocumentPartitioningChanged(AbstractDocument.java:611)
	at org.eclipse.jface.text.AbstractDocument.doFireDocumentChanged2(AbstractDocument.java:755)
	at org.eclipse.jface.text.AbstractDocument.doFireDocumentChanged(AbstractDocument.java:736)
	at org.eclipse.jface.text.AbstractDocument.doFireDocumentChanged(AbstractDocument.java:721)
	at org.eclipse.jface.text.AbstractDocument.fireDocumentChanged(AbstractDocument.java:796)
	at org.eclipse.jface.text.AbstractDocument.replace(AbstractDocument.java:1191)
	at org.eclipse.jface.text.AbstractDocument.replace(AbstractDocument.java:1210)
	at org.lamport.tla.toolbox.tool.tlc.output.source.TagBasedTLCOutputIncrementalParser.addIncrement(TagBasedTLCOutputIncrementalParser.java:324)
	at org.lamport.tla.toolbox.tool.tlc.output.ParsingTLCOutputSink.addIncrement(ParsingTLCOutputSink.java:47)
	at org.lamport.tla.toolbox.tool.tlc.output.ParsingTLCOutputSink.appendText(ParsingTLCOutputSink.java:39)
	at org.lamport.tla.toolbox.tool.tlc.output.internal.BroadcastStreamListener.streamAppended(BroadcastStreamListener.java:44)
	at org.eclipse.debug.internal.core.OutputStreamMonitor$ContentNotifier.run(OutputStreamMonitor.java:257)
	at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:42)
	at org.eclipse.debug.internal.core.OutputStreamMonitor$ContentNotifier.notifyAppend(OutputStreamMonitor.java:267)
	at org.eclipse.debug.internal.core.OutputStreamMonitor.fireStreamAppended(OutputStreamMonitor.java:116)
	at org.eclipse.debug.internal.core.OutputStreamMonitor.read(OutputStreamMonitor.java:156)
	at org.eclipse.debug.internal.core.OutputStreamMonitor.access$1(OutputStreamMonitor.java:134)
	at org.eclipse.debug.internal.core.OutputStreamMonitor$1.run(OutputStreamMonitor.java:207)
	at java.lang.Thread.run(Thread.java:744)

!ENTRY org.eclipse.ui 4 0 2014-03-29 10:19:19.924
!MESSAGE Unhandled event loop exception
!STACK 0
org.eclipse.swt.SWTException: Failed to execute runnable (org.eclipse.core.runtime.AssertionFailedException: null argument:)
	at org.eclipse.swt.SWT.error(SWT.java:4282)
	at org.eclipse.swt.SWT.error(SWT.java:4197)
	at org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:138)
	at org.eclipse.swt.widgets.Display.runAsyncMessages(Display.java:3563)
	at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3212)
	at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2696)
	at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2660)
	at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2494)
	at org.eclipse.ui.internal.Workbench$7.run(Workbench.java:674)
	at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)
	at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:667)
	at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
	at org.lamport.tla.toolbox.Application.start(Application.java:41)
	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:57)
	at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.lang.reflect.Method.invoke(Method.java:606)
	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)
	at org.eclipse.equinox.launcher.Main.main(Main.java:1386)
Caused by: org.eclipse.core.runtime.AssertionFailedException: null argument:
	at org.eclipse.core.runtime.Assert.isNotNull(Assert.java:85)
	at org.eclipse.core.runtime.Assert.isNotNull(Assert.java:73)
	at org.eclipse.jface.viewers.StructuredViewer.assertElementsNotNull(StructuredViewer.java:599)
	at org.eclipse.jface.viewers.StructuredViewer.getRawChildren(StructuredViewer.java:1011)
	at org.eclipse.jface.viewers.ColumnViewer.getRawChildren(ColumnViewer.java:703)
	at org.eclipse.jface.viewers.AbstractTableViewer.getRawChildren(AbstractTableViewer.java:1087)
	at org.eclipse.jface.viewers.StructuredViewer.getFilteredChildren(StructuredViewer.java:917)
	at org.eclipse.jface.viewers.StructuredViewer.getSortedChildren(StructuredViewer.java:1067)
	at org.eclipse.jface.viewers.AbstractTableViewer.internalRefreshAll(AbstractTableViewer.java:701)
	at org.eclipse.jface.viewers.AbstractTableViewer.internalRefresh(AbstractTableViewer.java:649)
	at org.eclipse.jface.viewers.AbstractTableViewer.internalRefresh(AbstractTableViewer.java:636)
	at org.eclipse.jface.viewers.AbstractTableViewer$2.run(AbstractTableViewer.java:592)
	at org.eclipse.jface.viewers.StructuredViewer.preservingSelection(StructuredViewer.java:1443)
	at org.eclipse.jface.viewers.StructuredViewer.preservingSelection(StructuredViewer.java:1404)
	at org.eclipse.jface.viewers.AbstractTableViewer.inputChanged(AbstractTableViewer.java:590)
	at org.eclipse.jface.viewers.ContentViewer.setInput(ContentViewer.java:280)
	at org.eclipse.jface.viewers.StructuredViewer.setInput(StructuredViewer.java:1690)
	at org.lamport.tla.toolbox.tool.tlc.ui.editor.page.ResultPage$2.run(ResultPage.java:185)
	at org.eclipse.swt.widgets.RunnableLock.run(RunnableLock.java:35)
	at org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:135)
	... 23 more

!ENTRY org.lamport.tla.toolbox 1 -1 2014-03-29 10:19:20.458
!MESSAGE Spec build invoked on OneBitClock ...

!ENTRY org.lamport.tla.toolbox 1 -1 2014-03-29 10:19:20.477
!MESSAGE Resulting status is:  parsed 
... build invocation finished.

!ENTRY org.eclipse.ui 4 0 2014-03-29 10:19:20.541
!MESSAGE Unhandled event loop exception
!STACK 0
org.eclipse.swt.SWTException: Failed to execute runnable (org.eclipse.core.runtime.AssertionFailedException: null argument:)
	at org.eclipse.swt.SWT.error(SWT.java:4282)
	at org.eclipse.swt.SWT.error(SWT.java:4197)
	at org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:138)
	at org.eclipse.swt.widgets.Display.runAsyncMessages(Display.java:3563)
	at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3212)
	at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2696)
	at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2660)
	at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2494)
	at org.eclipse.ui.internal.Workbench$7.run(Workbench.java:674)
	at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)
	at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:667)
	at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
	at org.lamport.tla.toolbox.Application.start(Application.java:41)
	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:57)
	at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.lang.reflect.Method.invoke(Method.java:606)
	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)
	at org.eclipse.equinox.launcher.Main.main(Main.java:1386)
Caused by: org.eclipse.core.runtime.AssertionFailedException: null argument:
	at org.eclipse.core.runtime.Assert.isNotNull(Assert.java:85)
	at org.eclipse.core.runtime.Assert.isNotNull(Assert.java:73)
	at org.eclipse.jface.viewers.StructuredViewer.assertElementsNotNull(StructuredViewer.java:599)
	at org.eclipse.jface.viewers.StructuredViewer.getRawChildren(StructuredViewer.java:1011)
	at org.eclipse.jface.viewers.ColumnViewer.getRawChildren(ColumnViewer.java:703)
	at org.eclipse.jface.viewers.AbstractTableViewer.getRawChildren(AbstractTableViewer.java:1087)
	at org.eclipse.jface.viewers.StructuredViewer.getFilteredChildren(StructuredViewer.java:917)
	at org.eclipse.jface.viewers.StructuredViewer.getSortedChildren(StructuredViewer.java:1067)
	at org.eclipse.jface.viewers.AbstractTableViewer.internalRefreshAll(AbstractTableViewer.java:701)
	at org.eclipse.jface.viewers.AbstractTableViewer.internalRefresh(AbstractTableViewer.java:649)
	at org.eclipse.jface.viewers.AbstractTableViewer.internalRefresh(AbstractTableViewer.java:636)
	at org.eclipse.jface.viewers.AbstractTableViewer$2.run(AbstractTableViewer.java:592)
	at org.eclipse.jface.viewers.StructuredViewer.preservingSelection(StructuredViewer.java:1443)
	at org.eclipse.jface.viewers.StructuredViewer.preservingSelection(StructuredViewer.java:1404)
	at org.eclipse.jface.viewers.AbstractTableViewer.inputChanged(AbstractTableViewer.java:590)
	at org.eclipse.jface.viewers.ContentViewer.setInput(ContentViewer.java:280)
	at org.eclipse.jface.viewers.StructuredViewer.setInput(StructuredViewer.java:1690)
	at org.lamport.tla.toolbox.tool.tlc.ui.editor.page.ResultPage$2.run(ResultPage.java:185)
	at org.eclipse.swt.widgets.RunnableLock.run(RunnableLock.java:35)
	at org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:135)
	... 23 more
References:
- TLC didn't display statistics
  - From: Amira Methni
- Re: TLC didn't display statistics
  - From: Amira Methni
- Re: [tlaplus] Re: TLC didn't display statistics
  - From: Markus Alexander Kuppe
Prev by Date: Re: [tlaplus] New release of the Toolbox and TLAPS
Next by Date: Re: [tlaplus] Re: TLC didn't display statistics
Previous by thread: Re: [tlaplus] Re: TLC didn't display statistics
Next by thread: Re: [tlaplus] Re: TLC didn't display statistics
Index(es):
- Date
- Thread