Fingerprint Collision

71 views
Skip to first unread message

Amir Hossein Sayyad Abdi

unread,
Jul 26, 2019, 5:25:41 AM7/26/19
to tla...@googlegroups.com
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

unread,
Jul 26, 2019, 10:32:13 AM7/26/19
to tla...@googlegroups.com
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

unread,
Jul 26, 2019, 10:46:57 AM7/26/19
to tla...@googlegroups.com
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

unread,
Sep 4, 2019, 12:29:32 PM9/4/19
to tla...@googlegroups.com
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



Hillel Wayne

unread,
Sep 4, 2019, 6:25:45 PM9/4/19
to tla...@googlegroups.com

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

Han

unread,
Sep 5, 2019, 4:00:37 PM9/5/19
to tla...@googlegroups.com
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)


Screen Shot 2019-09-05 at 12.56.32 PM.png
Reply all
Reply to author
Forward
0 new messages