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

# Re: [tlaplus] Invariance under transition order

 On 01 Feb 2016, at 22:12, Ron Pressler wrote: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"?Here's one suggestion on how to do that. Specify the two semantics, say, by formulas CoarseSpec and FineSpec. Then define a mapping that computes the "coarse" state from the "fine" state, by restricting to rounds that all processes have already executed, and prove that for any fine-grained execution the result of the mapping is a coarse-grained execution. To be a little more concrete, let's assume your coarse-grained spec looks something like this.--- MODULE Coarse ---CONSTANT Proc  \* the processes of the algorithmVARIABLE x     \* the local states of each processInit == x = [p \in Proc |-> init(p)]   \* initialize every processNext == x' = [p \in Proc |-> f(x,p)]   \* all processes execute in lock-stepSpec == Init /\ [][Next]_x             \* ignoring liveness for simplicity=====Fine-grained executions are specified by interleaving the processes. In order to simplify the statement of the relation between the two semantics, let's record for every process the history of its past states. (In practice, you probably want to introduce a history variable separate from the "real" specification.)--- MODULE Fine ---CONSTANT ProcVARIABLE yInit == y = [p \in Proc |-> << ... >>]  \* singleton sequence containing initial stateNext == \E p \in Proc :   y' = [y EXCEPT ![p] = Append(@, ...)] \* process p moves and records its new stateSpec == Init /\ [][Next]_y(* Now recover the abstract state for the last round that all processes executed.   Note that the state of the fine-grained spec may need to be more detailed: the   operator g (not defined here) retrieves the abstract state of process p. *)Min(S) == CHOOSE n \in S : \A m \in S : n <= mabs == LET n == Min( {Len[y][p] : p \in Proc} )       IN  [p \in Proc |-> g(y[p][n], p)]C == INSTANCE Coarse WITH x <- absTHEOREM Spec => C!Spec=====Does this make sense?Stephan