- ($P$, $L$) is machine-closed
`A`($P$*and*$L$) $<=>$ $P$.- $L$ constrains only infinite behaviors.

- Fairness properties used to write machine-closed specfications:
- Action
`A`is subaction of safety property $P$ iff for every finite behavior`rho`= <$r$_{0}, ..., $r$_{n}> the following holds: - If
`rho`satisfies $P$ and`A`is enabled in $r$_{n}, then there exists some $r$_{n}such that <$r$_{0}, ..., $r$_{n+1}> satsfies $P$ and <$r$_{n}, $r$_{n+1}> is an`A`step. - If
`A`$=>$`A`, then`A`is subaction of $Init$*and*`always`[`A`]$$_{v}.

- Action
- Proposition 1:
- If $P$ is safety property and $L$ is conjunction of formulas
WF$$
_{w}(`A`) and/or SF$$_{w}(`A`) such that`A`*and*($w\text{'}$*notequal*$w$) is a subaction of $P$, then $(P,L)$ is machine-closed. `A`($Init$*and*`always`[`A`]$$_{v}*and*$L$) = $Init$*and*`always`[`A`]$$_{v}.

- If $P$ is safety property and $L$ is conjunction of formulas
WF$$

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

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