Fingerprint Collision

[Amir Hossein Sayyad Abdi]

Hi everyone,

I have updated the toolbox to the latest version 1.6.0 of 10 July, and after running TLC on my spec I am getting a red box saying "Fingerprint collision probability: calculated 3.8E-7 observed: 3.9E-8".

What does this mean? The spec that I checked had no errors previously!

Sincerely,

AmirHossein

[Markus Kuppe]

On 26.07.19 02:25, Amir Hossein Sayyad Abdi wrote:
> I have updated the toolbox to the latest version 1.6.0 of 10 July, and
> after running TLC on my spec I am getting a red box saying "Fingerprint
> collision probability: calculated 3.8E-7 observed: 3.9E-8".
>
> What does this mean? The spec that I checked had no errors previously!

Hi AmirHossein,

previous Toolbox versions have always shown the 'Fingerprint collision
probability'. With the UI remake as part of the 1.6 Toolbox release,
the 'Fingerprint collision probability' moved to the notification area
on the 'Model Checking Results' tab. 'Fingerprint collision
probability' itself is discussed at [1].

Hope this helps,
Markus

[1] http://discuss.tlapl.us/msg02600.html

[Amir Hossein Sayyad Abdi]

Thanks for your help.

Sincerely,

AmirHossein

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/98f4860d-a8d4-a2fa-175d-c9a612de7b1c%40lemmster.de.

[Han]

Hi,

I've read this thread and the referenced older thread, including this description:  "Deciding if the hash collision probability is sufficiently low requires

engineering judgment."  

however I still was wondering: 

When should we try to judge about the notification of Fingerprint collision probability ? Is there any case where it indicates a problem with our TLA+ Spec? 

Currently, my spec running TLC model checker shows: "Fingerprint collision probability: calculated: 7.0E-14" , I don't know if it's something I should fix with my spec. 

Thanks,

Han

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAKxfy0vS8yOGz_5dcqV%2B647_2uStSK4EnwpdB9yeOzHGyejAjw%40mail.gmail.com.

[Hillel Wayne]

Hi Han,

A fingerprint collision probability of 7.0E-14 is a 0.000000000007% chance your spec had a hash collision. I'd say you're safe :)

H

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAEjGaqfFofphCk3ZLLMekyWzYSiTFc2xK_tzCEQVkEj_pkv51w%40mail.gmail.com.

[Han]

Thanks Hillel.  It's just that I think the current UI coloring (yellow-red-ish) for the fingerprint collision is confusing to average users, even if they understand the definition of the probability.  The way it displays the message is a bit unsettling. :-)

attaching a screenshot for the "DieHard" example run (based on the spec from the Video Course)

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/67a85530-5de3-8efb-0906-17e4051b36d5%40gmail.com.