• Home
  • Features
  • Pricing
  • Docs
  • Announcements
  • Sign In

LearnLib / learnlib / 29938144974

22 Jul 2026 04:28PM UTC coverage: 95.321% (-0.004%) from 95.325%
29938144974

push

github

mtf90
adjust to AutomataLib refacotrings

33 of 35 new or added lines in 13 files covered. (94.29%)

14912 of 15644 relevant lines covered (95.32%)

1.74 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

88.51
/algorithms/active/ttt-vpa/src/main/java/de/learnlib/algorithm/ttt/vpa/TTTLearnerVPA.java
1
/* Copyright (C) 2013-2026 TU Dortmund University
2
 * This file is part of LearnLib <https://learnlib.de>.
3
 *
4
 * Licensed under the Apache License, Version 2.0 (the "License");
5
 * you may not use this file except in compliance with the License.
6
 * You may obtain a copy of the License at
7
 *
8
 *     http://www.apache.org/licenses/LICENSE-2.0
9
 *
10
 * Unless required by applicable law or agreed to in writing, software
11
 * distributed under the License is distributed on an "AS IS" BASIS,
12
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13
 * See the License for the specific language governing permissions and
14
 * limitations under the License.
15
 */
16
package de.learnlib.algorithm.ttt.vpa;
17

18
import java.util.ArrayDeque;
19
import java.util.ArrayList;
20
import java.util.Collections;
21
import java.util.Deque;
22
import java.util.HashMap;
23
import java.util.HashSet;
24
import java.util.List;
25
import java.util.Map;
26
import java.util.Objects;
27
import java.util.Set;
28

29
import de.learnlib.acex.AcexAnalyzer;
30
import de.learnlib.algorithm.observationpack.vpa.OPLearnerVPA;
31
import de.learnlib.algorithm.observationpack.vpa.hypothesis.AbstractHypTrans;
32
import de.learnlib.algorithm.observationpack.vpa.hypothesis.ContextPair;
33
import de.learnlib.algorithm.observationpack.vpa.hypothesis.DTNode;
34
import de.learnlib.algorithm.observationpack.vpa.hypothesis.HypLoc;
35
import de.learnlib.algorithm.observationpack.vpa.hypothesis.TransList;
36
import de.learnlib.datastructure.discriminationtree.SplitData;
37
import de.learnlib.datastructure.list.IntrusiveList;
38
import de.learnlib.oracle.MembershipOracle;
39
import de.learnlib.query.DefaultQuery;
40
import de.learnlib.query.Query;
41
import de.learnlib.tooling.annotation.builder.GenerateBuilder;
42
import net.automatalib.alphabet.VPAlphabet;
43
import net.automatalib.automaton.vpa.SEVPA;
44
import net.automatalib.automaton.vpa.StackContents;
45
import net.automatalib.automaton.vpa.State;
46
import net.automatalib.common.util.collection.CollectionUtil;
47
import net.automatalib.ts.acceptor.DeterministicAcceptorTS;
48
import net.automatalib.word.Word;
49
import org.checkerframework.checker.nullness.qual.Nullable;
50

51
/**
52
 * A {@link SEVPA}-based adoption of the "TTT" algorithm.
53
 *
54
 * @param <I>
55
 *         input symbol type
56
 */
57
public class TTTLearnerVPA<I> extends OPLearnerVPA<I> {
2✔
58

59
    private final IntrusiveList<DTNode<I>> blockList = new IntrusiveList<>();
2✔
60

61
    @GenerateBuilder(defaults = BuilderDefaults.class)
62
    public TTTLearnerVPA(VPAlphabet<I> alphabet, MembershipOracle<I, Boolean> oracle, AcexAnalyzer analyzer) {
63
        super(alphabet, oracle, analyzer);
2✔
64
    }
2✔
65

66
    @Override
67
    protected State<HypLoc<I>> getDefinitiveSuccessor(State<HypLoc<I>> baseState, Word<I> suffix) {
68
        NonDetState<HypLoc<I>> curr = NonDetState.fromDet(baseState);
2✔
69
        int lastDet = 0;
2✔
70
        NonDetState<HypLoc<I>> lastDetState = curr;
2✔
71
        int i = 0;
2✔
72
        for (I sym : suffix) {
2✔
73
            if (alphabet.isCallSymbol(sym)) {
2✔
74
                Set<Integer> stackSyms = new HashSet<>();
2✔
75
                for (HypLoc<I> loc : curr.getLocations()) {
2✔
76
                    int stackSym = hypothesis.encodeStackSym(loc, sym);
2✔
77
                    stackSyms.add(stackSym);
2✔
78
                }
2✔
79
                NonDetStackContents nsc = NonDetStackContents.push(stackSyms, curr.getStack());
2✔
80
                curr = new NonDetState<>(Collections.singleton(hypothesis.getInitialState()), nsc);
2✔
81
            } else if (alphabet.isReturnSymbol(sym)) {
2✔
82
                Set<HypLoc<I>> succs = new HashSet<>();
2✔
83
                for (HypLoc<I> loc : curr.getLocations()) {
2✔
84
                    for (int stackSym : curr.getStack().peek()) {
2✔
85
                        AbstractHypTrans<I> trans = hypothesis.getReturnTransition(loc, sym, stackSym);
2✔
86
                        if (trans.isTree()) {
2✔
87
                            succs.add(trans.getTreeTarget());
×
88
                        } else {
89
                            CollectionUtil.add(succs, trans.getNonTreeTarget().subtreeLocsIterator());
2✔
90
                        }
91
                    }
2✔
92
                }
2✔
93
                curr = new NonDetState<>(succs, curr.getStack().pop());
2✔
94
            } else {
2✔
95
                Set<HypLoc<I>> succs = new HashSet<>();
2✔
96
                for (HypLoc<I> loc : curr.getLocations()) {
2✔
97
                    AbstractHypTrans<I> trans = hypothesis.getInternalTransition(loc, sym);
2✔
98
                    if (trans.isTree()) {
2✔
99
                        succs.add(trans.getTreeTarget());
2✔
100
                    } else {
101
                        CollectionUtil.add(succs, trans.getNonTreeTarget().subtreeLocsIterator());
2✔
102
                    }
103
                }
2✔
104
                curr = new NonDetState<>(succs, curr.getStack());
2✔
105
            }
106
            i++;
2✔
107
            if (!curr.isNonDet()) {
2✔
108
                lastDet = i;
2✔
109
                lastDetState = curr;
2✔
110
            }
111
        }
2✔
112

113
        if (lastDet < suffix.length()) {
2✔
114
            determinize(lastDetState.determinize(), suffix.subWord(lastDet));
×
115
        }
116
        DeterministicAcceptorTS<State<HypLoc<I>>, I> semantics = hypothesis.getSemantics();
2✔
117
        return semantics.getSuccessor(baseState, suffix);
2✔
118
    }
119

120
    @Override
121
    protected boolean refineHypothesisSingle(DefaultQuery<I, Boolean> ceQuery) {
122
        Word<I> ceWord = ceQuery.getInput();
2✔
123

124
        Boolean out = computeHypothesisOutput(ceWord);
2✔
125

126
        if (Objects.equals(out, ceQuery.getOutput())) {
2✔
127
            return false;
2✔
128
        }
129

130
        OutputInconsistency<I> outIncons = new OutputInconsistency<>(hypothesis.getInitialState(),
2✔
131
                                                                     new ContextPair<>(Word.epsilon(), ceWord),
2✔
132
                                                                     ceQuery.getOutput());
2✔
133

134
        do {
135
            splitState(outIncons);
2✔
136
            do {
137
                closeTransitions();
2✔
138
            } while (finalizeAny());
2✔
139

140
            outIncons = findOutputInconsistency();
2✔
141
        } while (outIncons != null);
2✔
142

143
        return true;
2✔
144
    }
145

146
    protected boolean computeHypothesisOutput(Word<I> word) {
147
        DeterministicAcceptorTS<State<HypLoc<I>>, I> semantics = hypothesis.getSemantics();
2✔
148
        State<HypLoc<I>> curr = semantics.getInitialState();
2✔
149
        for (I sym : word) {
2✔
150
            curr = getAnySuccessor(curr, sym);
2✔
151
        }
2✔
152
        return semantics.isAccepting(curr);
2✔
153
    }
154

155
    private void splitState(OutputInconsistency<I> outIncons) {
156
        PrefixTransformAcex acex = deriveAcex(outIncons);
2✔
157
        int breakpoint = analyzer.analyzeAbstractCounterexample(acex);
2✔
158

159
        Word<I> acexSuffix = acex.getSuffix();
2✔
160
        Word<I> prefix = acexSuffix.prefix(breakpoint);
2✔
161
        I act = acexSuffix.getSymbol(breakpoint);
2✔
162
        Word<I> suffix = acexSuffix.subWord(breakpoint + 1);
2✔
163

164
        DeterministicAcceptorTS<State<HypLoc<I>>, I> semantics = hypothesis.getSemantics();
2✔
165
        State<HypLoc<I>> state = semantics.getSuccessor(acex.getBaseState(), prefix);
2✔
166
        assert state != null;
2✔
167
        State<HypLoc<I>> succState = semantics.getSuccessor(state, act);
2✔
168
        assert succState != null;
2✔
169

170
        ContextPair<I> context = new ContextPair<>(transformAccessSequence(succState.getStackContents()), suffix);
2✔
171

172
        AbstractHypTrans<I> trans = hypothesis.getInternalTransition(state, act);
2✔
173
        assert trans != null;
2✔
174

175
        HypLoc<I> newLoc = makeTree(trans);
2✔
176
        DTNode<I> oldDtNode = succState.getLocation().getLeaf();
2✔
177
        openTransitions.concat(oldDtNode.getIncoming());
2✔
178
        DTNode<I>.SplitResult children = oldDtNode.split(context, acex.effect(breakpoint), acex.effect(breakpoint + 1));
2✔
179
        oldDtNode.setTemp(true);
2✔
180
        if (!oldDtNode.getParent().isTemp()) {
2✔
181
            blockList.add(oldDtNode);
2✔
182
        }
183
        link(children.nodeOld, newLoc);
2✔
184
        link(children.nodeNew, succState.getLocation());
2✔
185
        initializeLocation(newLoc);
2✔
186
    }
2✔
187

188
    protected boolean finalizeAny() {
189
        assert openTransitions.isEmpty();
2✔
190

191
        GlobalSplitter<I> splitter = findSplitterGlobal();
2✔
192
        if (splitter != null) {
2✔
193
            finalizeDiscriminator(splitter.blockRoot, splitter.localSplitter);
2✔
194
            return true;
2✔
195
        }
196
        return false;
2✔
197
    }
198

199
    private @Nullable OutputInconsistency<I> findOutputInconsistency() {
200
        OutputInconsistency<I> best = null;
2✔
201

202
        for (HypLoc<I> loc : hypothesis.getStates()) {
2✔
203
            int locAsLen = loc.getAccessSequence().length();
2✔
204
            DTNode<I> node = loc.getLeaf();
2✔
205
            while (!node.isRoot()) {
2✔
206
                boolean expectedOut = node.getParentOutcome();
2✔
207
                node = node.getParent();
2✔
208
                ContextPair<I> discr = node.getDiscriminator();
2✔
209
                if (best == null || discr.getLength() + locAsLen < best.totalLength()) {
2✔
210
                    boolean hypOut = computeHypothesisOutput(discr.getPrefix()
2✔
211
                                                                  .concat(loc.getAccessSequence(), discr.getSuffix()));
2✔
212
                    if (hypOut != expectedOut) {
2✔
213
                        best = new OutputInconsistency<>(loc, discr, expectedOut);
2✔
214
                    }
215
                }
216
            }
2✔
217
        }
2✔
218
        return best;
2✔
219
    }
220

221
    protected State<HypLoc<I>> getAnySuccessor(State<HypLoc<I>> state, I sym) {
222
        final VPAlphabet.SymbolType type = alphabet.getSymbolType(sym);
2✔
223
        final StackContents stackContents = state.getStackContents();
2✔
224

225
        return switch (type) {
2✔
226
            case INTERNAL: {
227
                AbstractHypTrans<I> trans = hypothesis.getInternalTransition(state.getLocation(), sym);
2✔
228
                HypLoc<I> succLoc;
229
                if (trans.isTree()) {
2✔
230
                    succLoc = trans.getTreeTarget();
2✔
231
                } else {
232
                    succLoc = trans.getNonTreeTarget().subtreeLocsIterator().next();
2✔
233
                }
234
                yield new State<>(succLoc, stackContents);
2✔
235
            }
236
            case CALL: {
237
                int stackSym = hypothesis.encodeStackSym(state.getLocation(), sym);
2✔
238
                yield new State<>(hypothesis.getInitialState(), StackContents.push(stackSym, stackContents));
2✔
239
            }
240
            case RETURN: {
241
                assert stackContents != null;
2✔
242
                AbstractHypTrans<I> trans =
2✔
243
                        hypothesis.getReturnTransition(state.getLocation(), sym, stackContents.peek());
2✔
244
                HypLoc<I> succLoc;
245
                if (trans.isTree()) {
2✔
246
                    succLoc = trans.getTreeTarget();
2✔
247
                } else {
248
                    succLoc = trans.getNonTreeTarget().subtreeLocsIterator().next();
2✔
249
                }
250
                yield new State<>(succLoc, stackContents.pop());
2✔
251
            }
252
        };
253
    }
254

255
    private PrefixTransformAcex deriveAcex(OutputInconsistency<I> outIncons) {
256
        PrefixTransformAcex acex =
2✔
257
                new PrefixTransformAcex(outIncons.location.getAccessSequence(), outIncons.discriminator);
2✔
258
        acex.setEffect(0, outIncons.expectedOut);
2✔
259
        acex.setEffect(acex.getLength() - 1, !outIncons.expectedOut);
2✔
260

261
        return acex;
2✔
262
    }
263

264
    /**
265
     * Determines a global splitter, i.e., a splitter for any block. This method may (but is not required to) employ
266
     * heuristics to obtain a splitter with a relatively short suffix length.
267
     *
268
     * @return a splitter for any of the blocks
269
     */
270
    private @Nullable GlobalSplitter<I> findSplitterGlobal() {
271
        DTNode<I> bestBlockRoot = null;
2✔
272
        Splitter<I> bestSplitter = null;
2✔
273

274
        for (DTNode<I> blockRoot : blockList) {
2✔
275
            Splitter<I> splitter = findSplitter(blockRoot);
2✔
276

277
            if (splitter != null && (bestSplitter == null ||
2✔
278
                                     splitter.getNewDiscriminatorLength() < bestSplitter.getNewDiscriminatorLength())) {
×
279
                bestSplitter = splitter;
2✔
280
                bestBlockRoot = blockRoot;
2✔
281
            }
282
        }
2✔
283

284
        if (bestSplitter == null) {
2✔
285
            return null;
2✔
286
        }
287

288
        return new GlobalSplitter<>(bestBlockRoot, bestSplitter);
2✔
289
    }
290

291
    /**
292
     * Finalize a discriminator. Given a block root and a {@link Splitter}, replace the discriminator at the block root
293
     * by the one derived from the splitter, and update the discrimination tree accordingly.
294
     *
295
     * @param blockRoot
296
     *         the block root whose discriminator to finalize
297
     * @param splitter
298
     *         the splitter to use for finalization
299
     */
300
    private void finalizeDiscriminator(DTNode<I> blockRoot, Splitter<I> splitter) {
301
        assert blockRoot.isBlockRoot();
2✔
302

303
        ContextPair<I> newDiscr = splitter.getNewDiscriminator();
2✔
304

305
        assert !blockRoot.getDiscriminator().equals(newDiscr);
2✔
306

307
        ContextPair<I> finalDiscriminator = prepareSplit(blockRoot, splitter);
2✔
308
        Map<Boolean, DTNode<I>> repChildren = new HashMap<>();
2✔
309
        for (Boolean label : blockRoot.getSplitData().getLabels()) {
2✔
310
            repChildren.put(label, extractSubtree(blockRoot, label));
2✔
311
        }
2✔
312
        blockRoot.replaceChildren(repChildren);
2✔
313

314
        blockRoot.setDiscriminator(finalDiscriminator);
2✔
315

316
        declareFinal(blockRoot);
2✔
317
    }
2✔
318

319
    /**
320
     * Determines a (local) splitter for a given block. This method may (but is not required to) employ heuristics to
321
     * obtain a splitter with a relatively short suffix.
322
     *
323
     * @param blockRoot
324
     *         the root of the block
325
     *
326
     * @return a splitter for this block, or {@code null} if no such splitter could be found.
327
     */
328
    private @Nullable Splitter<I> findSplitter(DTNode<I> blockRoot) {
329
        int alphabetSize =
2✔
330
                alphabet.getNumInternals() + alphabet.getNumCalls() * alphabet.getNumReturns() * hypothesis.size() * 2;
2✔
331

332
        @SuppressWarnings("unchecked")
333
        DTNode<I>[] lcas = new DTNode[alphabetSize];
2✔
334

335
        for (HypLoc<I> loc : blockRoot.subtreeLocations()) {
2✔
336
            int i = 0;
2✔
337
            for (I intSym : alphabet.getInternalAlphabet()) {
2✔
338
                DTNode<I> currLca = lcas[i];
2✔
339
                AbstractHypTrans<I> trans = hypothesis.getInternalTransition(loc, intSym);
2✔
340
                assert trans.getTargetNode() != null;
2✔
341
                if (currLca == null) {
2✔
342
                    lcas[i] = trans.getTargetNode();
2✔
343
                } else {
344
                    lcas[i] = dtree.leastCommonAncestor(currLca, trans.getTargetNode());
2✔
345
                }
346
                i++;
2✔
347
            }
2✔
348
            for (I retSym : alphabet.getReturnAlphabet()) {
2✔
349
                for (I callSym : alphabet.getCallAlphabet()) {
2✔
350
                    for (HypLoc<I> stackLoc : hypothesis.getStates()) {
2✔
351
                        AbstractHypTrans<I> trans = hypothesis.getReturnTransition(loc, retSym, stackLoc, callSym);
2✔
352
                        DTNode<I> currLca = lcas[i];
2✔
353
                        assert trans.getTargetNode() != null;
2✔
354
                        if (currLca == null) {
2✔
355
                            lcas[i] = trans.getTargetNode();
2✔
356
                        } else {
357
                            lcas[i] = dtree.leastCommonAncestor(currLca, trans.getTargetNode());
2✔
358
                        }
359
                        i++;
2✔
360

361
                        trans = hypothesis.getReturnTransition(stackLoc, retSym, loc, callSym);
2✔
362
                        currLca = lcas[i];
2✔
363
                        if (currLca == null) {
2✔
364
                            lcas[i] = trans.getTargetNode();
2✔
365
                        } else {
366
                            lcas[i] = dtree.leastCommonAncestor(currLca, trans.getTargetNode());
2✔
367
                        }
368
                        i++;
2✔
369
                    }
2✔
370
                }
2✔
371
            }
2✔
372
        }
2✔
373

374
        int shortestLen = Integer.MAX_VALUE;
2✔
375
        Splitter<I> shortestSplitter = null;
2✔
376

377
        int i = 0;
2✔
378
        for (I intSym : alphabet.getInternalAlphabet()) {
2✔
379
            DTNode<I> currLca = lcas[i];
2✔
380
            if (!currLca.isLeaf() && !currLca.isTemp()) {
2✔
381
                Splitter<I> splitter = new Splitter<>(intSym, currLca);
2✔
382
                int newLen = splitter.getNewDiscriminatorLength();
2✔
383
                if (shortestSplitter == null || shortestLen > newLen) {
2✔
384
                    shortestSplitter = splitter;
2✔
385
                    shortestLen = newLen;
2✔
386
                }
387
            }
388
            i++;
2✔
389
        }
2✔
390
        for (I retSym : alphabet.getReturnAlphabet()) {
2✔
391
            for (I callSym : alphabet.getCallAlphabet()) {
2✔
392
                for (HypLoc<I> stackLoc : hypothesis.getStates()) {
2✔
393
                    DTNode<I> currLca = lcas[i];
2✔
394
                    assert currLca != null;
2✔
395
                    if (!currLca.isLeaf() && !currLca.isTemp()) {
2✔
396
                        Splitter<I> splitter = new Splitter<>(retSym, stackLoc, callSym, false, currLca);
2✔
397
                        int newLen = splitter.getNewDiscriminatorLength();
2✔
398
                        if (shortestSplitter == null || shortestLen > newLen) {
2✔
399
                            shortestSplitter = splitter;
×
400
                            shortestLen = newLen;
×
401
                        }
402
                    }
403
                    i++;
2✔
404

405
                    currLca = lcas[i];
2✔
406
                    assert currLca != null;
2✔
407
                    if (!currLca.isLeaf() && !currLca.isTemp()) {
2✔
408
                        Splitter<I> splitter = new Splitter<>(callSym, stackLoc, retSym, true, currLca);
2✔
409
                        int newLen = splitter.getNewDiscriminatorLength();
2✔
410
                        if (shortestSplitter == null || shortestLen > newLen) {
2✔
411
                            shortestSplitter = splitter;
×
412
                            shortestLen = newLen;
×
413
                        }
414
                    }
415
                    i++;
2✔
416
                }
2✔
417
            }
2✔
418
        }
2✔
419

420
        return shortestSplitter;
2✔
421
    }
422

423
    /**
424
     * Prepare a split operation on a block, by marking all the nodes and transitions in the subtree (and annotating
425
     * them with {@link SplitData} objects).
426
     *
427
     * @param node
428
     *         the block root to be split
429
     * @param splitter
430
     *         the splitter to use for splitting the block
431
     *
432
     * @return the discriminator to use for splitting
433
     */
434
    private ContextPair<I> prepareSplit(DTNode<I> node, Splitter<I> splitter) {
435
        ContextPair<I> discriminator = splitter.getNewDiscriminator();
2✔
436

437
        Deque<DTNode<I>> dfsStack = new ArrayDeque<>();
2✔
438
        List<SplitQuery<I>> queries = new ArrayList<>();
2✔
439

440
        DTNode<I> succSeparator = splitter.succSeparator;
2✔
441

442
        dfsStack.push(node);
2✔
443
        assert node.getSplitData() == null;
2✔
444

445
        while (!dfsStack.isEmpty()) {
2✔
446
            DTNode<I> curr = dfsStack.pop();
2✔
447
            assert curr.getSplitData() == null;
2✔
448

449
            curr.setSplitData(new SplitData<>(TransList::new));
2✔
450

451
            for (AbstractHypTrans<I> trans : curr.getIncoming()) {
2✔
452
                queries.add(new SplitQuery<>(trans, discriminator));
2✔
453
            }
2✔
454

455
            if (!queries.isEmpty()) {
2✔
456
                oracle.processQueries(queries);
2✔
457

458
                for (SplitQuery<I> query : queries) {
2✔
459
                    curr.getSplitData().getIncoming(query.output).add(query.transition);
2✔
460
                    markAndPropagate(curr, query.output);
2✔
461
                }
2✔
462

463
                queries.clear();
2✔
464
            }
465

466
            if (curr.isInner()) {
2✔
467
                for (DTNode<I> child : curr.getChildren()) {
2✔
468
                    dfsStack.push(child);
2✔
469
                }
2✔
470
            } else {
471
                HypLoc<I> loc = curr.getData();
2✔
472
                assert loc != null;
2✔
473

474
                // Try to deduct the outcome from the DT target of
475
                // the respective transition
476
                AbstractHypTrans<I> trans = getSplitterTrans(loc, splitter);
2✔
477
                Boolean outcome = succSeparator.subtreeLabel(trans.getTargetNode());
2✔
478
                assert outcome != null;
2✔
479
                curr.getSplitData().setStateLabel(outcome);
2✔
480
                markAndPropagate(curr, outcome);
2✔
481
            }
482

483
        }
2✔
484

485
        return discriminator;
2✔
486
    }
487

488
    /**
489
     * Extract a (reduced) subtree containing all nodes with the given label from the subtree given by its root.
490
     * "Reduced" here refers to the fact that the resulting subtree will contain no inner nodes with only one child. The
491
     * tree returned by this method (represented by its root) will have as a parent node the root that was passed to
492
     * this method.
493
     *
494
     * @param root
495
     *         the root of the subtree from which to extract
496
     * @param label
497
     *         the label of the nodes to extract
498
     *
499
     * @return the extracted subtree
500
     */
501
    private DTNode<I> extractSubtree(DTNode<I> root, Boolean label) {
502
        assert root.getSplitData() != null;
2✔
503
        assert root.getSplitData().isMarked(label);
2✔
504

505
        Deque<ExtractRecord<I>> stack = new ArrayDeque<>();
2✔
506

507
        DTNode<I> firstExtracted = new DTNode<>(root, label);
2✔
508

509
        stack.push(new ExtractRecord<>(root, firstExtracted));
2✔
510
        while (!stack.isEmpty()) {
2✔
511
            ExtractRecord<I> curr = stack.pop();
2✔
512

513
            DTNode<I> original = curr.original;
2✔
514
            DTNode<I> extracted = curr.extracted;
2✔
515

516
            moveIncoming(extracted, original, label);
2✔
517

518
            if (original.isLeaf()) {
2✔
519
                if (Objects.equals(original.getSplitData().getStateLabel(), label)) {
2✔
520
                    link(extracted, original.getData());
2✔
521
                } else {
522
                    createNewState(extracted);
×
523
                }
524
                extracted.updateIncoming();
2✔
525
            } else {
526
                List<DTNode<I>> markedChildren = new ArrayList<>();
2✔
527

528
                for (DTNode<I> child : original.getChildren()) {
2✔
529
                    if (child.getSplitData().isMarked(label)) {
2✔
530
                        markedChildren.add(child);
2✔
531
                    }
532
                }
2✔
533

534
                if (markedChildren.size() > 1) {
2✔
535
                    Map<Boolean, DTNode<I>> childMap = new HashMap<>();
×
536
                    for (DTNode<I> c : markedChildren) {
×
537
                        Boolean childLabel = c.getParentOutcome();
×
538
                        DTNode<I> extractedChild = new DTNode<>(extracted, childLabel);
×
539
                        childMap.put(childLabel, extractedChild);
×
540
                        stack.push(new ExtractRecord<>(c, extractedChild));
×
541
                    }
×
542
                    extracted.split(original.getDiscriminator(), childMap);
×
543
                    extracted.updateIncoming();
×
544
                    extracted.setTemp(true);
×
545
                } else if (markedChildren.size() == 1) {
2✔
546
                    stack.push(new ExtractRecord<>(markedChildren.get(0), extracted));
2✔
547
                } else { // markedChildren.isEmppty()
548
                    createNewState(extracted);
×
549
                    extracted.updateIncoming();
×
550
                }
551
            }
552

553
            assert extracted.getSplitData() == null;
2✔
554
        }
2✔
555

556
        return firstExtracted;
2✔
557
    }
558

559
    protected void declareFinal(DTNode<I> blockRoot) {
560
        blockRoot.setTemp(false);
2✔
561
        blockRoot.setSplitData(null);
2✔
562

563
        blockRoot.removeFromList();
2✔
564

565
        for (DTNode<I> subtree : blockRoot.getChildren()) {
2✔
566
            assert subtree.getSplitData() == null;
2✔
567
            //blockRoot.setChild(subtree.getParentLabel(), subtree);
568
            // Register as blocks, if they are non-trivial subtrees
569
            if (subtree.isInner()) {
2✔
570
                blockList.add(subtree);
×
571
            }
572
        }
2✔
573

574
        openTransitions.concat(blockRoot.getIncoming());
2✔
575
    }
2✔
576

577
    /**
578
     * Marks a node, and propagates the label up to all nodes on the path from the block root to this node.
579
     *
580
     * @param node
581
     *         the node to mark
582
     * @param label
583
     *         the label to mark the node with
584
     */
585
    private static <I> void markAndPropagate(DTNode<I> node, Boolean label) {
586
        DTNode<I> curr = node;
2✔
587

588
        while (curr != null && curr.getSplitData() != null) {
2✔
589
            if (!curr.getSplitData().mark(label)) {
2✔
590
                return;
2✔
591
            }
592
            curr = curr.getParent();
2✔
593
        }
594
    }
2✔
595

596
    public AbstractHypTrans<I> getSplitterTrans(HypLoc<I> loc, Splitter<I> splitter) {
597
        return switch (splitter.type) {
2✔
598
            case INTERNAL -> hypothesis.getInternalTransition(loc, splitter.symbol);
2✔
599
            case RETURN -> hypothesis.getReturnTransition(loc, splitter.symbol, splitter.location, splitter.otherSymbol);
×
600
            case CALL -> hypothesis.getReturnTransition(splitter.location, splitter.otherSymbol, loc, splitter.symbol);
×
601
        };
602
    }
603

604
    private static <I> void moveIncoming(DTNode<I> newNode, DTNode<I> oldNode, Boolean label) {
605
        newNode.getIncoming().concat(oldNode.getSplitData().getIncoming(label));
2✔
606
    }
2✔
607

608
    /**
609
     * Create a new state during extraction on-the-fly. This is required if a node in the DT has an incoming transition
610
     * with a certain label, but in its subtree there are no leaves with this label as their state label.
611
     *
612
     * @param newNode
613
     *         the extracted node
614
     */
615
    private void createNewState(DTNode<I> newNode) {
616
        AbstractHypTrans<I> newTreeTrans = newNode.getIncoming().chooseMinimal();
×
617
        assert newTreeTrans != null;
×
618

619
        HypLoc<I> newLoc = makeTree(newTreeTrans);
×
620
        link(newNode, newLoc);
×
621
        initializeLocation(newLoc);
×
622
    }
×
623

624
    protected void determinize(State<HypLoc<I>> state, Word<I> suffix) {
NEW
625
        DeterministicAcceptorTS<State<HypLoc<I>>, I> semantics = hypothesis.getSemantics();
×
626
        State<HypLoc<I>> curr = state;
×
627
        for (I sym : suffix) {
×
628
            if (!alphabet.isCallSymbol(sym)) {
×
629
                AbstractHypTrans<I> trans = hypothesis.getInternalTransition(curr, sym);
×
630
                assert trans != null;
×
631
                if (!trans.isTree() && !trans.getNonTreeTarget().isLeaf()) {
×
632
                    updateDTTargets(Collections.singletonList(trans), true);
×
633
                }
634
            }
NEW
635
            curr = semantics.getSuccessor(curr, sym);
×
636
        }
×
637
    }
×
638

639
    private static final class SplitQuery<I> extends Query<I, Boolean> {
640

641
        private final AbstractHypTrans<I> transition;
642
        private final ContextPair<I> discriminator;
643
        private Boolean output;
644

645
        SplitQuery(AbstractHypTrans<I> transition, ContextPair<I> discriminator) {
2✔
646
            this.transition = transition;
2✔
647
            this.discriminator = discriminator;
2✔
648
        }
2✔
649

650
        @Override
651
        public void answer(Boolean output) {
652
            this.output = output;
2✔
653
        }
2✔
654

655
        @Override
656
        public Word<I> getPrefix() {
657
            return discriminator.getPrefix().concat(transition.getAccessSequence());
2✔
658
        }
659

660
        @Override
661
        public Word<I> getSuffix() {
662
            return discriminator.getSuffix();
2✔
663
        }
664
    }
665
}
STATUS · Troubleshooting · Open an Issue · Sales · Support · CAREERS · ENTERPRISE · START FREE TRIAL · SCHEDULE DEMO
ANNOUNCEMENTS · TWITTER · TOS & SLA · Supported CI Services · What's a CI service? · Automated Testing

© 2026 Coveralls, Inc