[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Verification of Temporal Property
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.