Dvlab Open Wiki
Invariants are not in normal form
- Submitted by: Luca
- Date: Dec 12, 2005
- Assigned to: Marco
- Fixed on Dec 20, 2005. Mildly tested.
When we build a symbolic representation, we don't strengthen the invariants to put them in normal form, as required by Definition 8 of the FROCOS paper. Many things break if we don't do this, including the fact that simulation can behave in inappropriate ways. We should play the safety games for I and O to strengthen the I and O invariants and put them into normal form, when building the symbolic representation.