Go backward to TLA
Go up to Top
Go forward to The Queue Example
- Let xi and psi be two objects.
- Representation by variables and .
- How to model concurrent changes to xi and psi?
- Simultaneous change to and ?
- Separate changes to and in some order?
- Interleaving representations
- Simultaneous changes to are disallowed.
- may be output variables of different processes.
- System with components in which is tuple of output variables
of component .
- Interleaving represented by TLA formula
(, ..., )
always [(' = ) or (' = )]
- TLA uses interleaving representation.
- Adequate for any system that
is modeled at sufficiently fine grain of atomicity.
Id: spec1.tex,v 1.1 1996/05/13 09:04:04 schreine Exp schreine