CounterexampleAnalysis::computeIndex can incorrectly judge that a CE leads to a guard refinement

[pfg666]

The problem seems to be in how we determine when guard refinement happens. We say that:

        boolean sulHasMoreRegs = !pivHyp.keySet().containsAll(pivSul.keySet());                

        boolean hypRefinesTransition = 
                hypRefinesTransitions(location, act, resSul.getSdt(), pivSul);
        ...
        return (sulHasMoreRegs || !hypRefinesTransition) ? 
                IndexResult.HAS_CE_AND_REFINES : IndexResult.HAS_CE_NO_REFINE; `

hypRefinesTransitions returns true if and only if each transition guard in the Hypothesis at the location of the CE prefix, for the first action symbol following the prefix (act), refines (i.e. is equivalent or implies) an initial action guard in the SUL SDT generated for CE prefix/suffix split (resSul).

Unfortunately, this method returning false is not always indicative of refinement. There may be transition guards that do not refine any particular SUT guard, without there being a refinement, as is the case for the example below:

`
Hyp Transition Guards:

[((c1==p1)), ((r1==p1)), (((c1!=p1) && (r1!=p1)))]

SUL SDT Initial Guards:

[((c1==p1)), ((c1!=p1))]
`

No guard refinement should be determined for this case, yet it is, since, the transition guard ((r1==p1)) does not refine any individual SUL guard.

I think the proper way of determining refinement is by checking if for each initial action guard in the SUT SDT there is a refining transition guard in the Hyp. If so, we do not need guard refinement. Otherwise, we do.

[fhowar]

The assumption in the implementation is that guards are mutually exclusive. I will leave this open for now and first figure out how/why/if guards should be overlapping.