--Please re-read all the answers in this thread. There is no need for reviewing the spec.--On Tue, Apr 22, 2025 at 12:56 AM naveen reddy <pnreddy1245@xxxxxxxxx> wrote:Can someone review the specification that I have an provide me the feedback, please..
On Sunday, April 20, 2025, Stephan Merz <stephan.merz@xxxxxxxxx> wrote:----In case of a hash collision, TLC may fail to explore part of the state space because it believes that it has already seen the state whose hash value equals that of a previously explored state. If TLC reports the same number of reachable states with a different seed you can be practically sure that no state was missed.StephanOn 20 Apr 2025, at 17:14, naveen reddy <pnreddy1245@xxxxxxxxx> wrote:I did run it with the different seed value and there isn't any change in the fingerprint, I think this is a positive output of the model to move forward ?On Sun, Apr 20, 2025 at 1:07 AM Stephan Merz <stephan.merz@xxxxxxxxx> wrote:Yes, TLC always prints an estimate of the probability of hash collisions. If that estimate is high and you want to go an extra mile, you can relaunch TLC with a different hash seed.StephanOn 20 Apr 2025, at 06:19, naveen reddy <pnreddy1245@xxxxxxxxx> wrote: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/
--
FelipeOn 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.ThanksNaveen--
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@googlegroups.com .
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/ .CAC2D9h5Bwou857waTyb6%2BaB% 3DpHmFhnS8X_EkEATOv4MOfGhbwg% 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@googlegroups.com .
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/53A35542-AE87- .4D2D-B3E7-2C425EF8FC1C% 40gmail.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/CAC2D9h5eBHE_ .WmooJxUJJB-pbGdJRERYqg_ KRjmj2TXKMNyYDQ%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@googlegroups.com .
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/81BC091B-84AC- .4CCF-8B41-5CC6AA0475CD% 40gmail.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/ .CAC2D9h6cpbBa5bXavHhtMHjgs% 2B3Pv_wQfNx%3DW8ng-cEUrN0yPQ% 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@googlegroups.com .
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/ .CAOC8YXZq96LUXcpeDhUZ9qfWcQs_ D2DFqh6_vE0t_b%2B%3DfAgBHg% 40mail.gmail.com