Check invariant preservation returns timeout

[r0ur...@gmail.com]

Hi,
Each time I try to "Check Invariant Preservation for Operations", the result would be timeout.
May i know why this is happening ? How can I solve it ?

Thank You.

[Michael Leuschel]

Hi,

can you send us the model?

Do you use ProB Tcl/Tk version and use the menu command in the Verify menu?

See

https://www3.hhu.de/stups/prob/index.php/Constraint_Based_Checking

https://www3.hhu.de/stups/prob/index.php/Tutorial_Model_Checking,_Proof_and_CBC

It could be useful to increase the TIME_OUT preference, or playing with MININT, MAXINT or in case you use deferred sets, with the default size of those sets.

But if you send us the model, we can maybe tell you more.

Kind regards,

Michael Leuschel

--
You received this message because you are subscribed to the Google Groups "ProB Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to prob-users+...@googlegroups.com.
To post to this group, send email to prob-...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/prob-users/1bc27215-ffad-47af-89a0-b60dca4ae653%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.