Error Tracing VIS produces a debug trace to help the designer understand the cause of the failure. Common corrective actions are the correction of an error in the original system description or addition of fairness constraints. If model checking or language emptiness checks fail, VIS reports the failure with a counterexample, i.e., an error trace of sample ``bad'' behavior (behavior seen in the system that does not satisfy the property - for model checking, or invalid behavior seen in the system - for language emptiness). This is called the ``debug'' trace. Debug traces list a set of states that are on a path to a fair cycle and fail the CTL formula.

Contact 

©2002-2018 U.C. Regents