I am working on TLA in order to analyze the filters in Dynamic networks, how can I see the states and the results of TLC models checking if there no error trace>
Sometimes I deliberately introduce an error in a spec, like a type invariant violation, to let Toolbox display the sequence of states that leads to the error.
Regards,
Yuri