formulate property

[Diep Chi Pham]

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

[Stephan Merz]

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

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/0806983f-3991-4cbe-8278-b0ca5e3e8dd3n%40googlegroups.com.

[Diep Chi Pham]

Dear Stephen,

Thank you very much for your very helpful answer. 

Best regards,

TA

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/24AE7BBB-038E-423D-9537-85281D4B45C9%40gmail.com.