|
|
|
| Use
of non-determinism: |
||
| needed to reduce size of the BDDs |
||
|
|
|
|
|
|
|
|
|
|
|
|
|
| • | Inputs
from environment |
|||||||||||
| – | Altitude
:= {1000…8000} |
|||||||||||
| • | Simplification
of functions |
|||||||||||
| – | Alt_Rate
:= |
|||||||||||
| 0.25*(Alt_Baro-ZP)/Delta_t |
||||||||||||
| – | Alt_Rate
:= {-2000…2000} |
|||||||||||
| • | Unmodelled
parts of specification |
|||||||||||
| – | States
of Other_Aircraft treated as non- |
|||||||||||
| deterministic
input variables |
||||||||||||
