[Verifpal] 0.7.5 combinatorial explosion?

Loup Vaillant David loup at loup-vaillant.fr
Sat Oct 19 22:10:36 CEST 2019


(Sorry for the long silence, life happened.)

I have tested version 0.7.5 on my Monokex X pattern (attached). It's
been running for several hours now, with no end in sight. I've stopped
it. The last line said:

    Stage 2, Analysis 12847...

(It did about one analysis per second.)

I don't know if this is expected, but such explosion is why I gave up
on Tamarin in the first place. Verifpal was always pretty fast on this
particular analysis, so I guess this is a bug? Any idea what could have
caused this?


-------------- next part --------------
A non-text attachment was scrubbed...
Name: x-active.vp
Type: text/x-csrc
Size: 2213 bytes
Desc: not available
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20191019/fbffeab8/attachment.c>

More information about the Verifpal mailing list