[tlaplus] formulate property

[Diep Chi Pham <diepchi.pham2011@xxxxxxxxx>]

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.