Re: [tlaplus] Fingerprint Collision

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.