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

Re: [tlaplus] Invariance under transition order

Thanks! This is exactly my problem, and I see that you have a good definition of the property I'm looking for: 

    "We will then establish a reduction theorem that shows that for every fine-grained run there exists an equivalent round-based (“coarse-grained”) run in the sense that the two runs exhibit the same sequences of local states of all processes, modulo stuttering"

The question is, then, suppose I have a set of such local state variables, how do I specify in TLA+ "this variable always obtains the same sequence of values modulo stuttering"?