Re: [tlaplus] Fingerprint Collision

[Han <keepsimple@xxxxxxxxx>]

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)

On Wed, Sep 4, 2019 at 3:26 PM Hillel Wayne <hwayne@xxxxxxxxx> wrote:

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

On 9/4/19 11:29 AM, Han wrote:

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

On Fri, Jul 26, 2019 at 7:46 AM Amir Hossein Sayyad Abdi <amir.ahsa.2011@xxxxxxxxx> wrote:

Thanks for your help.

Sincerely,

AmirHossein

On Fri, Jul 26, 2019, 7:02 PM Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx> wrote:

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

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

--
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 on the web visit https://groups.google.com/d/msgid/tlaplus/CAKxfy0vS8yOGz_5dcqV%2B647_2uStSK4EnwpdB9yeOzHGyejAjw%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 on the web visit https://groups.google.com/d/msgid/tlaplus/CAEjGaqfFofphCk3ZLLMekyWzYSiTFc2xK_tzCEQVkEj_pkv51w%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 on the web visit https://groups.google.com/d/msgid/tlaplus/67a85530-5de3-8efb-0906-17e4051b36d5%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@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAEjGaqeEGLQdH6O0P0dLgHCw1kM7%2BLEh3Ln1Wp%3DtX9ASM4YsZw%40mail.gmail.com.

Attachment: Screen Shot 2019-09-05 at 12.56.32 PM.png
Description: PNG image