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,

our continuous build [1] has a fix [2] for an issue that is likely the
root cause. Please let me know when it doesn't fix your problem. It does
fix the "Already on disk"-RuntimeException for a different spec/model
that has been shared with me off-list.

The bug causes false-negatives for a tiny fraction of fingerprint
lookups, resulting in repeated exploration of identical states. It
doesn't invalidate the model checking result though, if TLC finished
successfully.

Thanks
Markus

[1] http://tla.msr-inria.inria.fr/tlatoolbox/ci/
[2]
http://tlaplus.codeplex.com/SourceControl/changeset/d15068f4a559ca3d0101ebee258719192f8af377