Language Emptiness The language of a design is given by sequences over the set of reachable states that do not violate the fairness constraint. If the language is empty, we know that the system does not exhibit any legal behavior. VIS supports the command lang_empty as an alias for model checking the formula EG  true. This is relevant when verification is done by adding a component which monitors the design and has fair runs precisely when the observed behavior does not satisfy the specification. Before invoking model checking, lang_empty can also be used to ensure that the system is non-trivial. This is pertinent because the fairness constraints specified may make the entire system ``unfair'', and an empty system passes all universal properties.

Contact 

©2002-2018 U.C. Regents