[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Verification of Temporal Property

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.