This is a very low probability: 0.000000000000012. Many words and numbers to say "impossible".
The checker creates a fingerprint of every state that it visits so that it can answer the question "have I seen this state before?" by comparing the fingerprints instead of the entire state. That's much faster and doesn't require remembering all the states, only the fingerprints, so it doesn't consume a lot of RAM. There is a very remote possibility that two different states explored by the checker when it checks your model share the same fingerprint, but it's so remote it's irrelevant.
Good post on the subject of hash collisions:
https://preshing.com/20110504/hash-collision-probabilities/--
Felipe
Hello Team,
I have a specification and when I run the TLC the model stops with the notification of
"Fingerprint collision probability: calculated 1.2E-14.
How should I interpret this, does this mean my model is good to go or am I missing something. I did the research and read the home page where this was mentioned but wanted to seek clarity from the community.
Thanks
Naveen
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/39774466-334f-4273-9edf-921a123fd481n%40googlegroups.com.