Go backward to Safety and Closure
Go up to Top
Go forward to Closure and Hiding
Machine Closure
- (, ) is machine-closed
- A( and ) .
- constrains only infinite behaviors.
- Fairness properties used to write machine-closed specfications:
- Action A is subaction of safety property iff for
every finite behavior rho = <, ..., > the
following holds:
- If rho satisfies and A is enabled in , then there
exists some such that <, ...,
> satsfies and
<, > is an A step.
- If A A, then A is subaction of
and always [A].
- Proposition 1:
- If is safety property and is conjunction of formulas
WF(A) and/or SF(A)
such that A and (notequal ) is a subaction of , then
is machine-closed.
- A( and always [A] and ) =
and always [A].
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: spec1.tex,v 1.1 1996/05/13 09:04:04 schreine Exp schreine