TLC: NoSuchElementException on checkpoint restore

[Jaak Ristioja <jaak.r...@xxxxxxxx>]

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