[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:
> 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?
our continuous build  has a fix  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