Re: [tlaplus] formulate property

On Fri, Dec 18, 2020 at 8:36 AM Stephan Merz <stephan.merz@xxxxxxxxx> wrote:

Hello,

I suggest adding an auxiliary variable, let's call it `progress', initialized to "none" and that gets updated to "A" by action A etc. Then verify the invariant

progress = "C" => ~ ENABLED Next

Stephan

On 16 Dec 2020, at 15:15, Diep Chi Pham <diepchi.pham2011@xxxxxxxxx> wrote:

Dear all,

I have a spec and want to check a property as follows:
If action A is fired and then action B is fired and then action C is fired then there is a deadlock.
Could you tell me how can I formulate that property to verify it in the TLC model checker?

Thank you very much,
Best regards,
DC

--
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/0806983f-3991-4cbe-8278-b0ca5e3e8dd3n%40googlegroups.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/24AE7BBB-038E-423D-9537-85281D4B45C9%40gmail.com.