19556545386

Committed 21 Nov 2025 01:10AM UTC coverage: 94.471%. First build

Build # 19556545386

Build Type

Pull #155

github

Committed by

web-flow

Commit Message

Merge d1e6e0721 into 7c236fec9

Pull Request Pull Request #155: Bump Java Version to 17/25

Run Details

59 of 83 new or added lines in 25 files covered. (71.08%)

12611 of 13349 relevant lines covered (94.47%)

1.73 hits per line

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

75.76

/algorithms/active/ttt-vpa/src/main/java/de/learnlib/algorithm/ttt/vpa/Splitter.java

/* Copyright (C) 2013-2025 TU Dortmund University
 * This file is part of LearnLib <https://learnlib.de>.
 *
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 *     http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 */
package de.learnlib.algorithm.ttt.vpa;

import de.learnlib.algorithm.observationpack.vpa.hypothesis.ContextPair;
import de.learnlib.algorithm.observationpack.vpa.hypothesis.DTNode;
import de.learnlib.algorithm.observationpack.vpa.hypothesis.HypLoc;
import net.automatalib.word.Word;

/**
 * Data structure for representing a splitter.
 * <p>
 * A splitter is represented by an input symbol, and a DT node that separates the successors (wrt. the input symbol) of
 * the original states. From this, a discriminator can be obtained by prepending the input symbol to the discriminator
 * that labels the separating successor.
 * <p>
 * <b>Note:</b> as the discriminator finalization is applied to the root of a block and affects all nodes, there is no
 * need to store references to the source states from which this splitter was obtained.
 *
 * @param <I>
 *         input symbol type
 */
public final class Splitter<I> {

    public final I symbol;
    public final HypLoc<I> location;
    public final I otherSymbol;
    public final SplitType type;
    public final DTNode<I> succSeparator;

    public Splitter(I symbol, DTNode<I> succSeparator) {
        this.symbol = symbol;
        this.location = null;
        this.otherSymbol = null;
        this.type = SplitType.INTERNAL;
        this.succSeparator = succSeparator;
    }

    public Splitter(I symbol, HypLoc<I> location, I otherSymbol, boolean call, DTNode<I> succSeparator) {
        this.symbol = symbol;
        this.location = location;
        this.otherSymbol = otherSymbol;
        this.type = call ? SplitType.CALL : SplitType.RETURN;
        this.succSeparator = succSeparator;
    }

    public ContextPair<I> getDiscriminator() {
        return succSeparator.getDiscriminator();
    }

    public ContextPair<I> getNewDiscriminator() {
        Word<I> prefix = succSeparator.getDiscriminator().getPrefix();
        Word<I> suffix = succSeparator.getDiscriminator().getSuffix();

        return switch (type) {
            case INTERNAL -> new ContextPair<>(prefix, suffix.prepend(symbol));
            case RETURN -> new ContextPair<>(prefix.concat(location.getAccessSequence()).append(otherSymbol),
                                             suffix.prepend(symbol));
            case CALL -> new ContextPair<>(prefix,
                                           location.getAccessSequence()
                                                   .prepend(symbol)
                                                   .append(otherSymbol)
                                                   .concat(suffix));
        };
    }

    public int getNewDiscriminatorLength() {
        if (type == SplitType.INTERNAL) {
            return succSeparator.getDiscriminator().getLength() + 1;
        }
        return succSeparator.getDiscriminator().getLength() + location.getAccessSequence().length() + 2;
    }

    public enum SplitType {
        INTERNAL,
        CALL,
        RETURN
    }
}

1	/* Copyright (C) 2013-2025 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 de.learnlib.algorithm.observationpack.vpa.hypothesis.ContextPair;
19	import de.learnlib.algorithm.observationpack.vpa.hypothesis.DTNode;
20	import de.learnlib.algorithm.observationpack.vpa.hypothesis.HypLoc;
21	import net.automatalib.word.Word;
22
23	/**
24	* Data structure for representing a splitter.
25	* <p>
26	* A splitter is represented by an input symbol, and a DT node that separates the successors (wrt. the input symbol) of
27	* the original states. From this, a discriminator can be obtained by prepending the input symbol to the discriminator
28	* that labels the separating successor.
29	* <p>
30	* <b>Note:</b> as the discriminator finalization is applied to the root of a block and affects all nodes, there is no
31	* need to store references to the source states from which this splitter was obtained.
32	*
33	* @param <I>
34	* input symbol type
35	*/
36	public final class Splitter<I> {
37
38	public final I symbol;
39	public final HypLoc<I> location;
40	public final I otherSymbol;
41	public final SplitType type;
42	public final DTNode<I> succSeparator;
43
44	public Splitter(I symbol, DTNode<I> succSeparator) {	2✔
45	this.symbol = symbol;	2✔
46	this.location = null;	2✔
47	this.otherSymbol = null;	2✔
48	this.type = SplitType.INTERNAL;	2✔
49	this.succSeparator = succSeparator;	2✔
50	}	2✔
51
52	public Splitter(I symbol, HypLoc<I> location, I otherSymbol, boolean call, DTNode<I> succSeparator) {	2✔
53	this.symbol = symbol;	2✔
54	this.location = location;	2✔
55	this.otherSymbol = otherSymbol;	2✔
56	this.type = call ? SplitType.CALL : SplitType.RETURN;	2✔
57	this.succSeparator = succSeparator;	2✔
58	}	2✔
59
60	public ContextPair<I> getDiscriminator() {
61	return succSeparator.getDiscriminator();	×
62	}
63
64	public ContextPair<I> getNewDiscriminator() {
65	Word<I> prefix = succSeparator.getDiscriminator().getPrefix();	2✔
66	Word<I> suffix = succSeparator.getDiscriminator().getSuffix();	2✔
67
68	return switch (type) {	2✔
69	case INTERNAL -> new ContextPair<>(prefix, suffix.prepend(symbol));	2✔
NEW 70	case RETURN -> new ContextPair<>(prefix.concat(location.getAccessSequence()).append(otherSymbol),	×
NEW 71	suffix.prepend(symbol));	×
NEW 72	case CALL -> new ContextPair<>(prefix,	×
NEW 73	location.getAccessSequence()	×
NEW 74	.prepend(symbol)	×
NEW 75	.append(otherSymbol)	×
NEW 76	.concat(suffix));	×
77	};
78	}
79
80	public int getNewDiscriminatorLength() {
81	if (type == SplitType.INTERNAL) {	2✔
82	return succSeparator.getDiscriminator().getLength() + 1;	2✔
83	}
84	return succSeparator.getDiscriminator().getLength() + location.getAccessSequence().length() + 2;	2✔
85	}
86
87	public enum SplitType {	2✔
88	INTERNAL,	2✔
89	CALL,	2✔
90	RETURN	2✔
91	}
92	}

LearnLib / learnlib / 19556545386

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

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