Re: [tlaplus] TLC: NoSuchElementException on checkpoint restore

[Markus Alexander Kuppe <tlaplus-go...@xxxxxxxxxxx>]

On 09.12.2015 13:13, Jaak Ristioja wrote:
> 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?

Hi Jaak,

what number of distributed fingerprint sets have you been using? Zero
for the built-in set or >0 distributed sets.

You are leaving the beaten path when you try to recovery from
checkpoints created by a different TLC mode. Why do want to do this anyway?

Markus