Toolbox running under Java 1.8

[tkki...@aol.com]

Hi folks. After reading Viewpoint in the Communications of the ACM I was motivated to try TLA+. I can get the command line tools to work but the toolbox refuses to run the model checker but it does parse specs ok. I have tried both the current version and the release candidate. I am using windows 7 with Java 1.8.0_25 and the only conclusion I can come to is that the version of Eclipse that the toolbox uses won't run correctly with Java 1.8. Is this a known issue or am I simply doing something stupid?

Regards

Tony

[Markus Alexander Kuppe]

Hi Tony,

is there some sort of output like an exception shown in the Toolbox's
"TLC Console" when you try to launch the model checker? If not, can you
send me the .log file in workspace/.metadata relative to the Toolbox's
installation directory.

I haven't checked Win7 explicitly, but the release candidate is working
fine on Win8.1 and Java8 here.

Cheers
Markus

[tkki...@aol.com]

Hi Marcus

The TLC console doesn't seem to appear. When I select it under Menu: TLC Model Checker I get a docked window displaying the text "No consoles to display at this time". I have a progress window open as well at it shows some output when I do a parse but nothing at all for Run Model.


The log is:


!SESSION 2015-05-11 16:58:33.723 -----------------------------------------------
eclipse.buildId=1.5.0
java.version=1.8.0_25
java.vendor=Oracle Corporation
BootLoader constants: OS=win32, ARCH=x86_64, WS=win32, NL=en_GB
Command-line arguments: -os win32 -ws win32 -arch x86_64

!ENTRY org.lamport.tla.toolbox.product.standalone 1 -1 2015-05-11 16:58:37.732
!MESSAGE TLA+ Toolbox started without arguments.

!ENTRY org.lamport.tla.toolbox 1 -1 2015-05-11 16:58:37.826
!MESSAGE footFileName = C:\Users\owner\Documents\Tkwork\Development\TLA\AsynchronousInterface\AsynchInterface.tla

!ENTRY org.lamport.tla.toolbox 1 -1 2015-05-11 16:58:37.841
!MESSAGE footFileName = C:\Users\owner\Documents\Tkwork\Development\TLA\AsynchronousInterface\Channel.tla

!ENTRY org.lamport.tla.toolbox 1 -1 2015-05-11 16:58:37.841
!MESSAGE footFileName = C:\Users\owner\Documents\Tkwork\Development\TLA\HourClock\HourClock.tla

!ENTRY org.lamport.tla.toolbox 1 -1 2015-05-11 16:58:37.857
!MESSAGE footFileName = C:\Users\owner\Documents\Tkwork\Development\TLA\HourClock\HourClock2.tla

!ENTRY org.lamport.tla.toolbox 1 -1 2015-05-11 16:58:38.075
!MESSAGE Spec build invoked on Channel ...

!ENTRY org.lamport.tla.toolbox 1 -1 2015-05-11 16:58:38.559
!MESSAGE Resulting status is: parsed
... build invocation finished.

!ENTRY org.lamport.tla.toolbox 1 -1 2015-05-11 16:58:44.430
!MESSAGE Added a parse result listener.There are now 1 listeners.

Thanks for looking at this.

Regards

Tony