Re: [tlaplus] Verification of Temporal Property

[Stephen <stephen...@xxxxxxxxx>]

hi, Stephan

Sorry for replying late. The main idea of this example is learning how to define a temporal property to verify that x+y eventually eqauls specific number(i.e., 10 in my spec). I want to spec a distributed protocol with a property that must be satisfied eventually. I found tla is useful to my work, so, I start learning it.

Thanks all the guys who helped me.

regards,
Stephen