[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] TLC footprint value already on disk

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


[1] http://tla.msr-inria.inria.fr/tlatoolbox/ci/