final Queue<StatePair> currentExplorationBoundary = new LinkedList<StatePair>();// FIFO queue
final Map<StatePair,CmpVertex> pairsToGraphStates = new HashMap<StatePair,CmpVertex>();
LearnerGraph result = new LearnerGraph(config);result.initEmpty();
// Two sets are constructed so that I do not have to think about vertices which are shared between the two graphs regardless whether such a case is possible or not.
final Set<CmpVertex> encounteredGraph = new HashSet<CmpVertex>();
StatePair statePair = new StatePair(graph.getInit(),from.getInit());
encounteredGraph.add(statePair.firstElem);
result.setInit(AbstractLearnerGraph.cloneCmpVertex(graph.getInit(), config));
result.transitionMatrix.put(result.getInit(), result.createNewRow());
pairsToGraphStates.put(statePair, result.getInit());
boolean graphModified = false;
if (statePair.firstElem.isAccept() && !statePair.secondElem.isAccept())
{// initial states are incompatible because the tentative automaton is accept and
// the max automaton is reject, hence either override if possible and requested or throw.
if (override)
{
result.getInit().setAccept(false);graphModified = true;
}
else
throw new IllegalArgumentException("incompatible labelling: maximal automaton is all-reject and tentative one is not");
}
if (statePair.firstElem.isAccept() == statePair.secondElem.isAccept())
currentExplorationBoundary.add(statePair);
Map<Label,CmpVertex> emptyTargets = result.createNewRow();
while(!currentExplorationBoundary.isEmpty())
{
statePair = currentExplorationBoundary.remove();
assert graph.transitionMatrix.containsKey(statePair.firstElem) : "state "+statePair.firstElem+" is not known to the first graph";
assert statePair.secondElem == null || from.transitionMatrix.containsKey(statePair.secondElem) : "state "+statePair.secondElem+" is not known to the second graph";
assert statePair.secondElem == null || statePair.firstElem.isAccept() == statePair.secondElem.isAccept() : "incompatible labelling of "+statePair;
Map<Label,CmpVertex> graphTargets = graph.transitionMatrix.get(statePair.firstElem),
maxTargets = statePair.secondElem == null? emptyTargets:from.transitionMatrix.get(statePair.secondElem);
CmpVertex currentRepresentative = pairsToGraphStates.get(statePair);assert currentRepresentative != null;
for(Entry<Label,CmpVertex> labelstate:graphTargets.entrySet())
{
Label label = labelstate.getKey();
CmpVertex graphState = labelstate.getValue();// the original one
CmpVertex maxState = maxTargets.get(label);
if (maxState == null)
{// this is the case where a transition in a tentative graph is not matched by any in a maximal automaton
if (!maxIsPartial)
throw new IllegalArgumentException("In state pair "+statePair+" transition labelled by "+label+" is not matched in a maximal automaton");
}
StatePair nextPair = new StatePair(graphState,maxState);
// Now that we're making a step to a state pair where (graphState,maxState) pair has not been seen before,
// it is quite possible that we have to clone the corresponding state in a tentative graph so as to ensure
// that each state from a tentative graph is paired with no more than a single state in a maximal automaton
// (this corresponds to a construction of a cross-product of states).
// A state of a tentative state can be unpaired if the maximal automaton is partial,
// i.e. it contains a number of counter-examples rather than all possible sequences. This is another
// thing to check for in this method - if taking of an LTL-derived graph this should be deemed an error.
boolean shouldDescend = true;
CmpVertex nextGraphVertex = pairsToGraphStates.get(nextPair);// get a state representing the next pair of states
if (nextGraphVertex == null)
{// not seen this pair already hence might have to clone.
if (!encounteredGraph.contains(graphState))
{// since we did not see this pair before, the first encountered
// vertex (graphState) is now a representative of the pair nextPair
nextGraphVertex = AbstractLearnerGraph.cloneCmpVertex(graphState, config);encounteredGraph.add(graphState);
pairsToGraphStates.put(nextPair,nextGraphVertex);
result.transitionMatrix.put(nextGraphVertex, result.createNewRow());
shouldDescend = nextGraphVertex.isAccept();
}
else
{// graphState already paired with one of the states in maximal automaton hence clone the state
boolean accept = graphState.isAccept() && (maxState == null || maxState.isAccept());// do not descend if the next state is reject or the next state in a maximal automaton is reject
if (graphState.isAccept() != accept)
{// tentative automaton reaches an accept state but the maximal automaton gets into reject-state
if (!override)
throw new IllegalArgumentException("incompatible labelling: maximal automaton chops off some paths in a tentative automaton");
graphModified=true;
}
nextGraphVertex = AbstractLearnerGraph.generateNewCmpVertex(result.nextID(accept), config);
if (GlobalConfiguration.getConfiguration().isAssertEnabled() && result.findVertex(nextGraphVertex) != null) throw new IllegalArgumentException("duplicate vertex with ID "+nextGraphVertex.getStringId()+" in graph "+result);
DeterministicDirectedSparseGraph.copyVertexData(graphState, nextGraphVertex);nextGraphVertex.setAccept(accept);
result.transitionMatrix.put(nextGraphVertex,result.createNewRow());
pairsToGraphStates.put(nextPair, nextGraphVertex);
if (!accept) shouldDescend = false;
}
}
else // already seen the next pair hence no need to descend
shouldDescend = false;
result.transitionMatrix.get(currentRepresentative).put(label,nextGraphVertex);
if (shouldDescend)
// need to explore all transitions from the new state pair.
currentExplorationBoundary.offer(nextPair);
}
for(Entry<Label,CmpVertex> labelstate:maxTargets.entrySet())
{
Label label = labelstate.getKey();
if (!graphTargets.containsKey(label) && !labelstate.getValue().isAccept())
{// a transition in a maximal automaton is not matched but leads to a reject-state hence direct to a reject-state adding it if necessary
CmpVertex newVert = pairsToGraphStates.get(new StatePair(null,labelstate.getValue()));
if (newVert == null)
{
newVert = result.copyVertexUnderDifferentName(labelstate.getValue());
pairsToGraphStates.put(new StatePair(null,labelstate.getValue()), newVert);
}
result.transitionMatrix.get(currentRepresentative).put(label, newVert);graphModified=true;
}
}
}