Go up to Top
Go forward to Component Specification
Decomposing a Complete Specification
- Specifying a Component
- Output variables
- Input variables
- exists : Init and always [A] and .
- State function
- Initial condition Init
- Initial values of and .
- Next-state action A
- Component steps A ( )
- Environment steps.
- A A or (<, >'
= <, >)
- Fairness conditions
- Conjunction of formulas
WF and/or
SF
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: spec2.tex,v 1.1 1996/05/24 15:01:43 schreine Exp schreine