| Limitations |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| | Cant
model all of TCAS |
|||||||||||||
| | Pushing
limits of SMV (more than 200 bit |
|||||||||||||
| variables
is problematic) |
||||||||||||||
| | Need
some non-linear arithmetic to model parts |
|||||||||||||
| of Other_Aircraft |
||||||||||||||
| | New
result that represents constraints as BDD |
|||||||||||||
| variables
and uses a constraint solver |
||||||||||||||
| | How
to pick appropriate formulae to check? |
|||||||||||||
