Re: [tlaplus] formulate property

[Stephan Merz <stephan.merz@xxxxxxxxx>]

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.