For debugging complicated errors, DESpot provides the feature of generating a counter example. This is a short sequence of events inducing a traversal of the system's synchronous product from the initial state to the error state. This provides a mechanism to pinpoint the state where the error occurred. An incremental approach is adopted wherein the very first error generated is used for debugging. Its removal allows the users to move to the next error, assuming it is still relevant. Based on the project type, choose the appropriate topic for a step-by-step procedure to generate a counter example.