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)).