- Let
`xi`and`psi`be two objects.- Representation by variables $x$ and $y$.
- How to model concurrent changes to
`xi`and`psi`? - Simultaneous change to $x$ and $y$?
- Separate changes to $x$ and $y$ in some order?

- Interleaving representations
- Simultaneous changes to $x,y$ are disallowed.
- $x,y$ may be output variables of different processes.
- System with $n$ components in which $v$
_{i}is tuple of output variables of component $i$. - Interleaving represented by TLA formula

$Disjoint$($v$_{1}, ..., $v$_{n}) $<=>$*and*$$_{i notequal j}`always`[($v$_{i}' = $v$_{i})*or*($v$_{j}' = $v$_{j})]$$_{<vi, vj>}

- TLA uses interleaving representation.
- Adequate for
*any*system that is modeled at sufficiently fine grain of atomicity.

- Adequate for

Wolfgang.Schreiner@risc.uni-linz.ac.at

$$Id: spec1.tex,v 1.1 1996/05/13 09:04:04 schreine Exp schreine $$