mgijsberti / synoptic

Automatically exported from code.google.com/p/synoptic
0 stars 0 forks source link

Implement a version of the kTails algorithm that works on ChainsTraceGraph instances #232

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago
We need a complete/generic kTails version that we can use to evaluate the 
InvariMint kTails formulation/approach. The current kTails used by Synoptic 
during coarsening is tightly integrated with invariant checking logic, so we 
need to create a separate complete and generic kTails implementation.

The kTails driver in the coarsening code is 
synoptic.algorithms.bisim.Bisimulation.mergePartitions. kTails equivalence used 
by this code is implemented by synoptic.algorithms.bisim.KTails.kEquals.

Add the complete kTails algorithm to the KTails class.

Original issue reported on code.google.com by bestchai on 8 Mar 2012 at 6:59

GoogleCodeExporter commented 9 years ago
A generic version of the kTails algorithm is not going to be possible without 
significant changes to the IGraph/INode interfaces and code that depends on 
these.

Instead, the focus of this issue should be on implementing a version of kTails 
that works specifically on trace graphs (i.e., ChainsTraceGraph instances). 
This will help us compare the original kTails algorithm against the InvariMint 
approach. For example, we would be able to evaluate their relative performance.

Original comment by bestchai on 29 Mar 2012 at 12:47

GoogleCodeExporter commented 9 years ago

Original comment by jenny.abrahamson on 2 Apr 2012 at 8:21

GoogleCodeExporter commented 9 years ago
Addressed in revision 5994c5589dca, please review.

Original comment by jenny.abrahamson on 13 Apr 2012 at 8:47

GoogleCodeExporter commented 9 years ago
A few outstanding issues:

- There is only one test that calls the new performKTails() method. This test 
is an integration test in the InvariMint project -- 
EndToEndKTailsTest.simpleLogTest. You need at least a few more tests of this 
method. These should be added to synoptic.tests.units.KTailsTests.

- The EndToEndKTailsTest.simpleLogTest fails. The problem seems to be in the 
transition iterator of ITransition<Partition> instances. This is probably 
un-related to the new kTails code. But, it would help to have a small unit test 
that triggers this.

- You've added the performKTails method to synoptic.algorithms.graph.KTails. 
However, there is already a synoptic.algorithms.bisim.KTails. We should have 
just one class for all KTails-related method. I suggest keeping the 
graph.KTails class, since KTails will now be used outside of the bisim 
algorithm.

- The code in performKTails often checks for partition size of 0 (e.g., if 
(p.size() == 0)). This is not necessary since a PartitionMerge will remove one 
of the partitions being merged in commit (on graph.apply).

- The first half of performKTails() is a kind of PartitionGraph constructor -- 
it trivially translates a ChainsTraceGraph into a partition graph by mapping 
one event node to a unique partition. But, the code for this already exists -- 
the PartitionGraph.partitionSeparately() method does this. You should re-use 
this code by calling the PartitionGraph constructor with partitionByLabel=false.

I think that after the above two changes are implemented the performKTails() 
will be much simpler. You should probably start with these (before writing 
tests and isolating the bug mentioned at the top).

Original comment by bestchai on 13 Apr 2012 at 10:25

GoogleCodeExporter commented 9 years ago
Addressed in revision 11599f0939b6, please review

Original comment by jenny.abrahamson on 18 Apr 2012 at 7:33