* Record/Replay: the MC can display a textual representation of a path in the
execution graph. It can then be replayed outside of the model checker.
* Record/Replay: the MC can display a textual representation of a path in the
execution graph. It can then be replayed outside of the model checker.