TLC didn't display statistics

[Amira Methni]

Hi,

After installing the latest updates of TLAToolbox, when I tried to execute a model, the toolbox didn't display state space progress in "Statistics" panel.

It's possible to get these informations from TLC console but it's no more displayed in "Model Checking Result" section.

Is it a bug from latest updates?

Thanks

 

[Stephan Merz]

Hello Amira,

I'm running the Toolbox version 1.4.8 of 25 February 2014 on Mac OS X 10.9.2, and I don't see any change of behavior, see attached screenshot.

Could you describe your problem in a bit more detail (what Toolbox version, what OS, under which circumstances the error appears)?

Thanks,

Stephan

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Amira Methni]

My Toolbox version is 1.4.8 of 25 February 2014. And I'm running it into Ubuntu 12.04 (64-bit version).

I tried to remove the toolbox and reinstall a new version (also the 1.4.8) and the problem persists (see the screenshot attached).

[Markus Alexander Kuppe]

On 03/17/2014 06:00 PM, Amira Methni wrote:
> My Toolbox version is 1.4.8 of 25 February 2014. And I'm running it into
> Ubuntu 12.04 (64-bit version).
> I tried to remove the toolbox and reinstall a new version (also the
> 1.4.8) and the problem persists (see the screenshot attached).

Hi Amira,

can you post the content of the toolbox's log file? It is located in
"workspace/.metadata/.log" inside the toolbox's installation folder. It
might tell us why the toolbox doesn't show the state space progress.

Btw. on Ubuntu 12.10 64bit, the toolbox 1.4.8 shows states just fine.

Thanks
Markus

[victor.n...@gmail.com]

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

[victor.n...@gmail.com]

And I may add that running the toolbox with "LANG=en_GB.UTF-8" do solve the problem (the exception gave me a clue ;)

[victor.n...@gmail.com]

But still the graph does not appear when clicking on one of the header of the state space table.
Well a window appears, but it is empty.

(Sorry, I keep discovering things after sending messages, but I think I am done now :)

[Leslie Lamport]

   But still the graph does not appear when clicking on one of the header of the state space table.
   Well a window appears, but it is empty.

Are you aware that it requires at least two point to form a graph, so the window should appear empty unless there are at least 2 lines of statistics? 

[victor.n...@gmail.com]

No I was not, I was trying the tutorial and didn't think it through, thanks for the clarification :)