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

*From*: Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx>*Date*: Mon, 1 Feb 2016 13:12:34 -0800 (PST)*References*: <7d43683c-769a-428d-87d6-3d198ffc220f@googlegroups.com> <F0F3D161-847D-4BC9-A6F2-586986BE7619@gmail.com>

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"?

Ron

**Follow-Ups**:**Re: [tlaplus] Invariance under transition order***From:*Stephan Merz

**References**:**Invariance under transition order***From:*Ron Pressler

**Re: [tlaplus] Invariance under transition order***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Invariance under transition order** - Next by Date:
**Re: [tlaplus] Choose and TLC** - Previous by thread:
**Re: [tlaplus] Invariance under transition order** - Next by thread:
**Re: [tlaplus] Invariance under transition order** - Index(es):