Re: [tlaplus] TLC footprint value already on disk

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

On 20.05.2015 14:32, Dominik Hansen wrote:
> Hi,
> 
> TLC reports the following error message when I run it on my model with a
> large state space:
> 
>     Progress(45) at 2015-05-20 13:52:02: 16033373 states generated
>     (2.015.370 s/min), 11993254 distinct states found (1.995.379
>     ds/min), 1277839 states left on queue.
> 
>     Error: 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.lang.RuntimeException:
>     DiskFPSet.mergeNewEntries: 9223335424116589377 is already on disk.
> 
> Does it mean there is a (detected) hash collision?
> Is there a workaround to avoid this error?


Hi Dominik,

no, it does not indicate a hash collision. It rather shows that TLC
explored the same state twice. It shouldn't, because it's obviously
inefficient, but doesn't invalidate the model checking result.

Technically this exception is thrown when the in-memory fingerprint set
gets merged into a previously written set on disk and both sets contain
an identical fingerprint.

Can you privately share the spec with which this bug has happened? How
long - on what machine - did it take to run into the exception?

Thanks
Markus