|
Debug traces
Debug traces
- If the property fails on the model, then the debug trace helps to figure out the problem.
- A debug trace is a witness to the negation of the CTL formula.
- Some properties have a finite debug trace; others have an infinite debug trace.
- AG(RED) has a finite debug trace : Red, Green. It is a witness to EF(not(RED)).
- AF(GREEN) has the infinite debug trace : Red, Red, Red...... It is a witness to EG(not(GREEN)).
|
