Discussion
What are the limits?
- Specification size
- We produce around 200 boolean variables, about the edge of what SMV can handle
- Numerical issues (multiply, divide, etc.)
- Needed to refine Other_Aircraft
- Desirable properties to check?
Domain expertise is critical