stateActual = actual.getInit();stateExpected = expected.getInit();
}
Queue<StatePair> currentExplorationBoundary = new LinkedList<StatePair>();// FIFO queue
CollectionOfPairs statesAddedToBoundary = new CollectionOfPairs(expected,actual);
currentExplorationBoundary.add(new StatePair(stateExpected,stateActual));statesAddedToBoundary.addAndCheck(new StatePair(stateExpected,stateActual));
switch(compareVertices)
{
case DEEP:
if (!DeterministicDirectedSparseGraph.deepEquals(stateExpected,stateActual))
return new DifferentFSMException("vertices "+stateExpected+" and "+stateActual+" have different values of attributes");
if (stateActual.getOrigState() == null)
{
if (stateExpected.getOrigState() != null)
return new DifferentFSMException("vertices "+stateExpected+" and "+stateActual+" have different names");
}
else
if (!stateActual.getOrigState().equals(stateExpected.getOrigState()))
return new DifferentFSMException("vertices "+stateExpected+" and "+stateActual+" have different names");
break;
case NAMES:
if (!stateActual.getOrigState().equals(stateExpected.getOrigState()))
return new DifferentFSMException("vertices "+stateExpected+" and "+stateActual+" have different names");
break;
case NONE:// nothing needs doing
break;
}
CmpVertex sink = generateSinkState(expected);
boolean prefixClosed = expected.config.isPrefixClosed() && actual.config.isPrefixClosed();
Map<Label, CmpVertex> sinkRow = expected.createNewRow();
while(!currentExplorationBoundary.isEmpty())
{
StatePair statePair = currentExplorationBoundary.remove();
assert statePair.firstElem == sink || expected.transitionMatrix.containsKey(statePair.firstElem) : "state "+statePair.firstElem+" is not known to the expected graph";
assert statePair.secondElem == sink || actual.transitionMatrix.containsKey(statePair.secondElem) : "state "+statePair.secondElem+" is not known to the actual graph";
if (statePair.firstElem.isAccept() != statePair.secondElem.isAccept())
return new DifferentFSMException("states "+statePair.firstElem+" and " + statePair.secondElem+" have a different acceptance labelling between the machines");
Map<Label,CmpVertex> expectedTargets = statePair.firstElem == sink?sinkRow:expected.transitionMatrix.get(statePair.firstElem);
Map<Label,CmpVertex> actualTargets = statePair.secondElem == sink?sinkRow:actual.transitionMatrix.get(statePair.secondElem);
//if (prefixClosed && expectedTargets.size() != actualTargets.size())// each of them is equal to the keyset size from determinism
// return new DifferentFSMException("different number of transitions from states "+statePair);
Set<Label> outgoing = new TreeSet<Label>();outgoing.addAll(expectedTargets.keySet());outgoing.addAll(actualTargets.keySet());
for(Label label:outgoing)
{
CmpVertex nextExpectedState = null;
if (!expectedTargets.containsKey(label))
{
if (prefixClosed)
return new DifferentFSMException("no transition with expected label \""+label+"\" from a state \""+statePair.secondElem+"\" corresponding to \""+statePair.firstElem+"\"");
nextExpectedState = sink;
}
else
nextExpectedState = expectedTargets.get(label);
CmpVertex nextActualState = null;
if (!actualTargets.containsKey(label))
{
if (prefixClosed)
return new DifferentFSMException("no transition with actual label \""+label+"\" from a state \""+statePair.firstElem+"\" corresponding to \""+statePair.secondElem+"\"");
nextActualState = sink;
}
else
nextActualState = actualTargets.get(label);
StatePair nextPair = new StatePair(nextExpectedState,nextActualState);
//System.out.println("outgoing: "+statePair.getR()+","+statePair.getQ()+"-"+label+"->"+nextPair.getR()+","+nextPair.getQ());// elements of the pairs are in reverse order
if (statesAddedToBoundary.addAndCheck(nextPair))
{
switch(compareVertices)
{