Put state invariants in TransitionLabelMap

[GoogleCodeExporter]

Currently, we use PartitionInvWrapper to hold invariants on each outgoing edge 
of a partition. This way, we cannot reuse the GraphExporter code because 
GraphExporter only works with IGraph (e.g., PartitionGraph).

To reuse GraphExporter, we need to be able to access state invariants via 
PartitionGraph. One way is to maintain state invariants in TransitionLabelMap, 
which is maintained by Transition. (We don't want to maintain state invariants 
in Transition directly, because Transitions must apply to both Partitions and 
EventNodes but invariants only make sense for Partitions.) We need to add a new 
kind of TransitionLabelType e.g. DAIKON_INVARIANTS that maps to a list of 
invariants.

Transitions are constructed every time PartitionGraph is traversed (e.g., when 
Partition.getAllTransitions() is called). So, to avoid generating invariants 
every time PartitionGraph is traversed, we need to make a new method for 
Partition that generates Transitions as well as their corresponding invariants.

Original issue reported on code.google.com by ssukkerd on 21 Feb 2013 at 12:50

• Blocking: #286

[GoogleCodeExporter]

Original comment by ssukkerd on 21 Feb 2013 at 12:53

• Now blocking: #286

[GoogleCodeExporter]

Solution in revision c2191dce52f5, please review.

Original comment by ssukkerd on 22 Feb 2013 at 9:50

[GoogleCodeExporter]

The change to runSynoptic always computes Daikon invariants on the
final Synoptic graph. This breaks integration tests in
synoptic.tests.integration.EndToEndMainTests, as well as a test in
InvariMint, and maybe elsewhere. The code hardcodes Daikon support,
but if we merge this into default then we'll have a non-working
version of Synoptic. So, this needs to get fixed somehow -- either by
resolving the TODO that's there (it's another issue), or adding a
special flag to run Synoptic in this mode, or in some other way.

The changes in Partition look fine, except that Partition now caches
transitions, which it didn't do before. Since you intend to generate
these at the very end of the Synoptic process, when Partitions are no
longer created/destroyed, this is okay. But, this needs to be well
documented. I suggest adding a "NOTE: .." in the comment above the
definition of transitionsWithInvs var and also in the method comment
of getTransitionsWithDaikonInvariants.

And, the above brings up a question -- why have Partition cache the
invariant-based transitions in the first place? Can't you simply
return the set of generated partitions, as Partition currently does
with e.g., getTransitionsWithExactRelations?

The method addCorrectStateToDaikonizer needs a better name. I don't
understand what you mean by "CorrectState" here.

The name of Partition.createTransition method is similarly
obscure. Maybe rename it to createInvTransition, instead?

You need to update the TransitionLabelsMap.compareTo with the call
to/comparison of getDaikonInvariants() that you've added.

Finally, it would be nice to see some tests that exercise the new
code, particularly the new methods in Partition.

Original comment by bestchai on 9 Mar 2013 at 5:21

[GoogleCodeExporter]

I addressed most of your comments, except for adding condition to run Daikon 
support and tests. However, since I remove transitionsWithInvs caching, now 
runSynoptic doesn't call anything with Daikon support, so all the integration 
tests pass. Please review this revision 372e55e0282c. For adding condition to 
run Daikon support, I'll work on it in another issue. For tests, it will also 
be in another issue because it would need significantly more work.

Original comment by ssukkerd on 22 Mar 2013 at 6:29

[GoogleCodeExporter]

Merged into default with revision f5404c6b55ae

Original comment by bestchai on 23 Mar 2013 at 5:42

• Changed state: Fixed