Re: [tlaplus] Fingerprint collision

My question is more about the output part, I had no errors and no output except the fingerprint. Does TLC prints the output every single time after the state exploration or I can interpret the fingerprint notification as a result and move forward ?

On Saturday, April 19, 2025, Felipe Oliveira Carvalho <felipekde@xxxxxxxxx> wrote:

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

On Sat, Apr 19, 2025 at 8:48 PM naveen reddy <pnreddy1245@xxxxxxxxx> wrote:
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@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/39774466-334f-4273-9edf-921a123fd481n%40googlegroups.com.

--
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@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CAOC8YXaLp%2BSuZjWJZDTeb8LvEWbXsOfb-wMnoVon35BV7s3fPw%40mail.gmail.com.

--
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/CAC2D9h5Bwou857waTyb6%2BaB%3DpHmFhnS8X_EkEATOv4MOfGhbwg%40mail.gmail.com.