Invariant Printing

This treatment minimizes the invariants used in the proof of the valid properties, and shows them in the output without logging them on disk. Unlike Invariant Logging, this post-analysis does not try to express the invariants as a contract but in terms of streams used in original model. Thus, it is more likely to succeed (see Failures section in Invariant Logging).