Improving IntrBy comments and surfacing differences between TO invariant miners

Code review comments focusing on comments in the IntrBy code added in Issue351.

In CountingInvariantMiner:

- method-level comment of extractPathInvariantsFromWalkCounts : needs
details of how IntrBy are mined. This is the most important method to
change, probably.

-  protected boolean interrupts : to someone who hears "interrupts"
for the first time it's not clear what it means. Unlike "never
followed by". I would add something here to explain when this returns
true/false. Also, maybe changing this to "interruptedBy" would be
better -- fits the current code style.

In ChainWalkingTOInvMiner:

- computeInvariants : lists all invariants and details how they are
mined across traces, except the interruptedBy. Needs that paragraph.

- class-level comment : would be nice to list invariants it mines
here, and _emphasize_ that unlike the transitive closure miner it
mines an extra invariant.

In ConstrainedInvMiner:

- computeInvariants X 2 (two methods with same name): seem to
constrain IntrBy as well, no? Update comments.

- class-level : same -- "The only two invariants that can be
constrained are AlwaysFollowedInvariant and AlwaysPrecedesInvariant."
= inaccurate.

- computeConstraints : I really don't like the look of "TODO: document
me!". This seems like an important method that is central to
constraint mining and I have no idea what it does.

In TransitiveClosureInvMiner:

- class-level : I would add a comment to say that it does _not_ mine
the interrupted by invariant and say that the ChainWalkingTOInvMiner
does mine this invariant.

SynopticMain.mineTOInvariants : in the "useTransitiveClosureMining"
condition there needs to be a "WARNING: " print out that says that the
interrupted by invariant is not mined by the
TransitiveClosureInvMiner. Probably nice to also list all of the
invariant types mined by the particular miner in both branches of the
conditional there. So it is extra clear what is/isn't mined.

I think that the "useTransitiveClosureMining" option in
SynopticOptions can also be expanded to include the explanation.
Someone somewhere will hate us for not having sufficient
documentation. At least we can change the @Option print-out to state
what the ChainWalkingTOInvMiner and the TransitiveClosureInvMiner mine
and what they do not mine.

Original issue reported on code.google.com by bestchai on 21 Jan 2014 at 3:06

mgijsberti / synoptic

Improving IntrBy comments and surfacing differences between TO invariant miners #353