Re: TLC: NoSuchElementException on checkpoint restore

Hello, I was able to recover my checkpoint using the latest integration build.

http://tla.msr-inria.inria.fr/tlatoolbox/ci/tladist/

Giuliano

On Sunday, April 10, 2016 at 10:30:50 AM UTC-4, Giuliano wrote:

I forgot to mention that I am using the TLA+ command-line tools.
TLC reports:
TLC2 Version 2.08 of 21 December 2015

On Sunday, April 10, 2016 at 10:04:17 AM UTC-4, Giuliano wrote:
Hello, I am encountering the same error, but I did not run TLC in distributed mode.
I started TLC on the command line as follows.
java -cp ../tla/ -Xmx70g -Xms10g tlc2.TLC -workers 16 -maxSetSize 10000000 -deadlock -coverage 15 MC.tla
After stopping TLC accidentally (after several days unfortunately), I tried recovering the last checkpoint as follows.
java -cp ../tla/ -Xmx70g -Xms10g tlc2.TLC -workers 16 -maxSetSize 10000000 -deadlock -recover states/16-04-07-07-52-44 -coverage 15 MC.tla
This resulted in :
java.util.NoSuchElementException
at tlc2.tool.fp.MSBDiskFPSet$TLCIterator.getLast(MSBDiskFPSet.java:321)
at tlc2.tool.fp.MSBDiskFPSet$MSBFlusher.mergeNewEntries(MSBDiskFPSet.java:108)
at tlc2.tool.fp.DiskFPSet$Flusher.mergeNewEntries(DiskFPSet.java:1298)
at tlc2.tool.fp.DiskFPSet.recoverFP(DiskFPSet.java:896)
at tlc2.tool.fp.DiskFPSet.recover(DiskFPSet.java:939)
at tlc2.tool.ModelChecker.recover(ModelChecker.java:782)
at tlc2.tool.ModelChecker.modelCheck(ModelChecker.java:114)
at tlc2.TLC.process(TLC.java:773)
at tlc2.TLC.main(TLC.java:195)

Any idea that would help me recover the last checkpoint would be appreciated.
Thanks,
Giuliano

On Wednesday, December 9, 2015 at 7:13:54 AM UTC-5, Jaak Ristioja wrote:
Hello!

After switching from distributed ad-hoc mode to non-distributed mode and
recovering from checkpoint, I get the following exception:

@!@!@STARTMSG 2197:0 @!@!@
Starting recovery from checkpoint 15-12-02-13-53-09/
@!@!@ENDMSG 2197 @!@!@
@!@!@STARTMSG 1000:1 @!@!@
TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.util.NoSuchElementException
java.util.NoSuchElementException
at
tlc2.tool.fp.MSBDiskFPSet$TLCIterator.getLast(MSBDiskFPSet.java:321)
at
tlc2.tool.fp.MSBDiskFPSet$MSBFlusher.mergeNewEntries(MSBDiskFPSet.java:108)
at
tlc2.tool.fp.DiskFPSet$Flusher.mergeNewEntries(DiskFPSet.java:1298)
at tlc2.tool.fp.DiskFPSet.recoverFP(DiskFPSet.java:896)
at tlc2.tool.fp.DiskFPSet.recover(DiskFPSet.java:939)
at tlc2.tool.ModelChecker.recover(ModelChecker.java:778)
at tlc2.tool.ModelChecker.modelCheck(ModelChecker.java:114)
at tlc2.TLC.process(TLC.java:773)
at tlc2.TLC.main(TLC.java:195)

@!@!@ENDMSG 1000 @!@!@
@!@!@STARTMSG 2186:0 @!@!@
Finished in 04s at (2015-12-09 14:06:40)
@!@!@ENDMSG 2186 @!@!@

Recovering from the same checkpoint when switching back to distributed
ad-hoc mode works. Looks like this might be caused by the FPSet not
being present? Is there a workaround or an easy fix for this?

Best regards,
Jaak