model: document ModelChecker::mo_graph

model: document ModelChecker::mo_graph

The modification order graph is a complex data structure, and there are a few
pieces of high-level information that should be noted. For example, the edges
are actually directed from most recent to oldest, which is somewhat in reverse
of the usage in the literature, where

  a --mo--> b

means that a comes *before* b in the modification order. This convention can be
changed in the future, but it should be documented here.