TLC fingerprint value already on disk

[Dominik Hansen]

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?

Thanks

Dominik

[Markus Alexander Kuppe]

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

[Markus Alexander Kuppe]

On 20.05.2015 14:32, Dominik Hansen wrote:

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

[dohan]

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.

Thank you Markus. It also fixes my problem.