2727import java .util .Map ;
2828import java .util .Objects ;
2929import java .util .Queue ;
30+ import java .util .Set ;
3031
3132import javax .annotation .Nonnull ;
3233
3940import net .automatalib .words .Word ;
4041
4142import com .google .common .collect .AbstractIterator ;
43+ import com .google .common .collect .Sets ;
4244
4345import de .learnlib .algorithms .ttt .base .TTTHypothesis .TTTEdge ;
4446import de .learnlib .api .AccessSequenceTransformer ;
@@ -71,6 +73,8 @@ public static class BuilderDefaults {
7173 protected final DiscriminationTree <I ,D > dtree ;
7274 // private final SuffixTrie<I> suffixTrie = new SuffixTrie<>();
7375
76+ private final Set <Word <I >> finalDiscriminators = Sets .newHashSet (Word .epsilon ());
77+
7478 private final Collection <WeakReference <TTTEventListener <I , D >>> eventListeners = new UnorderedCollection <>();
7579
7680 /**
@@ -145,10 +149,10 @@ public boolean refineHypothesis(DefaultQuery<I, D> ceQuery) {
145149
146150 DefaultQuery <I , D > currCe = ceQuery ;
147151
148- while (currCe != null ) {
152+ // while(currCe != null) {
149153 while (refineHypothesisSingle (currCe ));
150- currCe = checkHypothesisConsistency ();
151- }
154+ // currCe = checkHypothesisConsistency();
155+ // }
152156
153157 return true ;
154158 }
@@ -425,6 +429,10 @@ private GlobalSplitter<I,D> findSplitterGlobal() {
425429 Iterator <DTNode <I ,D >> blocksIt = blockList .iterator ();
426430 while (blocksIt .hasNext ()) {
427431 DTNode <I ,D > blockRoot = blocksIt .next ();
432+ if (finalDiscriminators .contains (blockRoot .getDiscriminator ().subWord (1 ))) {
433+ declareFinal (blockRoot );
434+ continue ;
435+ }
428436 Splitter <I ,D > splitter = findSplitter (blockRoot );
429437 if (splitter != null ) {
430438 if (bestSplitter == null || splitter .discriminator .length ()
@@ -521,38 +529,38 @@ private Splitter<I,D> findSplitter(DTNode<I,D> blockRoot) {
521529 return new Splitter <>(state1 , state2 , bestI , bestLCA );
522530 }
523531
524- /**
525- * Checks whether the hypothesis is consistent with the discrimination tree.
526- * If an inconsistency is discovered, it is returned in the form of a counterexample.
527- *
528- * @return a counterexample uncovering an inconsistency, or {@code null}
529- * if the hypothesis is consistent with the discrimination tree
530- */
531- // TODO can be removed
532- private DefaultQuery <I , D > checkHypothesisConsistency () {
533- for (DTNode <I ,D > leaf : dtree .getRoot ().subtreeLeaves ()) {
534- TTTState <I ,D > state = leaf .state ;
535- if (state == null ) {
536- continue ;
537- }
538-
539- DTNode <I ,D > curr = state .dtLeaf ;
540- DTNode <I ,D > next = curr .getParent ();
541-
542- while (next != null ) {
543- Word <I > discr = next .getDiscriminator ();
544- D expected = curr .getParentEdgeLabel ();
545-
546- if (!Objects .equals (computeHypothesisOutput (state , discr ), expected )) {
547- return new DefaultQuery <>(state .getAccessSequence (), discr , expected );
548- }
549- curr = next ;
550- next = curr .getParent ();
551- }
552- }
553-
554- return null ;
555- }
532+ // /**
533+ // * Checks whether the hypothesis is consistent with the discrimination tree.
534+ // * If an inconsistency is discovered, it is returned in the form of a counterexample.
535+ // *
536+ // * @return a counterexample uncovering an inconsistency, or {@code null}
537+ // * if the hypothesis is consistent with the discrimination tree
538+ // */
539+ // // TODO can be removed
540+ // private DefaultQuery<I, D> checkHypothesisConsistency() {
541+ // for(DTNode<I,D> leaf : dtree.getRoot().subtreeLeaves()) {
542+ // TTTState<I,D> state = leaf.state;
543+ // if(state == null) {
544+ // continue;
545+ // }
546+ //
547+ // DTNode<I,D> curr = state.dtLeaf;
548+ // DTNode<I,D> next = curr.getParent();
549+ //
550+ // while(next != null) {
551+ // Word<I> discr = next.getDiscriminator();
552+ // D expected = curr.getParentEdgeLabel();
553+ //
554+ // if(!Objects.equals(computeHypothesisOutput(state, discr), expected)) {
555+ // return new DefaultQuery<>(state.getAccessSequence(), discr, expected);
556+ // }
557+ // curr = next;
558+ // next = curr.getParent();
559+ // }
560+ // }
561+ //
562+ // return null;
563+ // }
556564
557565 /**
558566 * Creates a state in the hypothesis. This method cannot be used for the initial
@@ -581,8 +589,7 @@ protected TTTState<I,D> getTarget(TTTTransition<I,D> trans) {
581589 if (trans .isTree ()) {
582590 return trans .getTreeTarget ();
583591 }
584- DTNode <I ,D > dtTarget = updateDTTarget (trans );
585- return dtTarget .state ;
592+ return updateTarget (trans );
586593 }
587594
588595 /**
@@ -628,15 +635,15 @@ private void finalizeDiscriminator(DTNode<I,D> blockRoot, Splitter<I,D> splitter
628635 notifyPreFinalizeDiscriminator (blockRoot , splitter );
629636
630637 Word <I > finalDiscriminator = prepareSplit (blockRoot , splitter );
631-
632638 Map <D ,DTNode <I ,D >> repChildren = createMap ();
633-
639+
634640 for (D label : blockRoot .splitData .getLabels ()) {
635641 repChildren .put (label , extractSubtree (blockRoot , label ));
636642 }
637643 blockRoot .replaceChildren (repChildren );
638-
644+
639645 blockRoot .setDiscriminator (finalDiscriminator );
646+
640647 declareFinal (blockRoot );
641648
642649 notifyPostFinalizeDiscriminator (blockRoot , splitter );
@@ -647,6 +654,7 @@ protected void declareFinal(DTNode<I,D> blockRoot) {
647654 blockRoot .splitData = null ;
648655
649656 blockRoot .removeFromBlockList ();
657+ finalDiscriminators .add (blockRoot .getDiscriminator ());
650658
651659 for (DTNode <I ,D > subtree : blockRoot .getChildren ()) {
652660 assert subtree .splitData == null ;
@@ -668,13 +676,14 @@ protected void declareFinal(DTNode<I,D> blockRoot) {
668676 * @return the discriminator to use for splitting
669677 */
670678 private Word <I > prepareSplit (DTNode <I ,D > node , Splitter <I ,D > splitter ) {
679+ int symbolIdx = splitter .symbolIdx ;
680+ I symbol = alphabet .getSymbol (symbolIdx );
681+ Word <I > discriminator = splitter .discriminator .prepend (symbol );
682+
671683 Deque <DTNode <I ,D >> dfsStack = new ArrayDeque <>();
672684
673685 DTNode <I ,D > succSeparator = splitter .succSeparator ;
674- int symbolIdx = splitter .symbolIdx ;
675- I symbol = alphabet .getSymbol (symbolIdx );
676686
677- Word <I > discriminator = splitter .discriminator .prepend (symbol );
678687
679688 dfsStack .push (node );
680689 assert node .splitData == null ;
@@ -1027,13 +1036,7 @@ private void closeTransition(TTTTransition<I,D> trans) {
10271036 return ;
10281037 }
10291038
1030- DTNode <I ,D > dtTarget = updateDTTarget (trans );
1031-
1032- if (dtTarget .state == null ) {
1033- TTTState <I ,D > state = createState (trans );
1034- link (dtTarget , state );
1035- initializeState (state );
1036- }
1039+ updateTarget (trans );
10371040 }
10381041
10391042 /**
@@ -1047,6 +1050,19 @@ private DTNode<I,D> updateDTTarget(TTTTransition<I,D> transition) {
10471050 return updateDTTarget (transition , true );
10481051 }
10491052
1053+ private TTTState <I , D > updateTarget (TTTTransition <I , D > trans ) {
1054+ DTNode <I ,D > node = updateDTTarget (trans );
1055+
1056+ TTTState <I ,D > state = node .state ;
1057+ if (state == null ) {
1058+ state = createState (trans );
1059+ link (node , state );
1060+ initializeState (state );
1061+ }
1062+
1063+ return state ;
1064+ }
1065+
10501066 /**
10511067 * Updates the transition to point to either a leaf in the discrimination tree,
10521068 * or---if the {@code hard} parameter is set to {@code false}---to a block
0 commit comments