6433387082

Committed 06 Oct 2023 03:10PM UTC coverage: 92.296% (-0.007%) from 92.303%

Build # 6433387082

Build Type

push

github

Committed by

mtf90

Commit Message

update Falk's developer id

Run Details

11573 of 12539 relevant lines covered (92.3%)

1.67 hits per line

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

98.08

/algorithms/passive/ostia/src/main/java/de/learnlib/algorithms/ostia/OSTIA.java

/* Copyright (C) 2013-2023 TU Dortmund
 * This file is part of LearnLib, http://www.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.algorithms.ostia;

import java.util.ArrayDeque;
import java.util.ArrayList;
import java.util.Collection;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.LinkedHashSet;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;
import java.util.Objects;
import java.util.Optional;
import java.util.Queue;
import java.util.Set;

import de.learnlib.api.algorithm.PassiveLearningAlgorithm;
import de.learnlib.api.query.DefaultQuery;
import net.automatalib.automata.transducers.SubsequentialTransducer;
import net.automatalib.commons.smartcollections.IntSeq;
import net.automatalib.commons.util.Pair;
import net.automatalib.words.Alphabet;
import net.automatalib.words.GrowingAlphabet;
import net.automatalib.words.Word;
import net.automatalib.words.impl.GrowingMapAlphabet;
import org.checkerframework.checker.nullness.qual.NonNull;
import org.checkerframework.checker.nullness.qual.Nullable;

/**
 * Implementation of the "onward subsequential transducer inference algorithm" (OSTIA) from the paper <a
 * href="https://doi.org/10.1109/34.211465">Learning Subsequential Transducers for Pattern Recognition Interpretation
 * Tasks</a> by Oncina, García and Vidal.
 */
public class OSTIA<I, O> implements PassiveLearningAlgorithm<SubsequentialTransducer<?, I, ?, O>, I, Word<O>> {

    private final Alphabet<I> inputAlphabet;
    private final GrowingAlphabet<O> outputAlphabet;
    private final State root;
    private boolean hasBeenComputed;

    public OSTIA(Alphabet<I> inputAlphabet) {
        this.inputAlphabet = inputAlphabet;
        this.outputAlphabet = new GrowingMapAlphabet<>();
        this.root = new State(inputAlphabet.size());
        this.hasBeenComputed = false;
    }

    @Override
    public void addSamples(Collection<? extends DefaultQuery<I, Word<O>>> samples) {
        for (DefaultQuery<I, Word<O>> sample : samples) {
            final Word<O> output = sample.getOutput();
            this.outputAlphabet.addAll(output.asList());
            buildPttOnward(root,
                           sample.getInput().asIntSeq(inputAlphabet),
                           IntQueue.asQueue(output.asIntSeq(outputAlphabet)));
        }
    }

    @Override
    public SubsequentialTransducer<?, I, ?, O> computeModel() {
        if (!hasBeenComputed) {
            hasBeenComputed = true;
            ostia(root);
        }
        return new OSSTWrapper<>(root, inputAlphabet, outputAlphabet);
    }

    public static State buildPtt(int alphabetSize, Iterator<Pair<IntSeq, IntSeq>> informant) {
        final State root = new State(alphabetSize);
        while (informant.hasNext()) {
            Pair<IntSeq, IntSeq> inout = informant.next();
            buildPttOnward(root, inout.getFirst(), IntQueue.asQueue(inout.getSecond()));
        }
        return root;
    }

    private static void buildPttOnward(State ptt, IntSeq input, @Nullable IntQueue output) {
        State pttIter = ptt;
        @Nullable IntQueue outputIter = output;

        for (int i = 0; i < input.size(); i++) {//input index
            final int symbol = input.get(i);
            final Edge edge;
            if (pttIter.transitions[symbol] == null) {
                edge = new Edge();
                edge.out = outputIter;
                edge.target = new State(pttIter.transitions.length);
                pttIter.transitions[symbol] = edge;
                outputIter = null;
            } else {
                edge = pttIter.transitions[symbol];
                IntQueue commonPrefixEdge = edge.out;
                IntQueue commonPrefixEdgePrev = null;
                IntQueue commonPrefixInformant = outputIter;
                while (commonPrefixEdge != null && commonPrefixInformant != null &&
                       commonPrefixEdge.value == commonPrefixInformant.value) {
                    commonPrefixInformant = commonPrefixInformant.next;
                    commonPrefixEdgePrev = commonPrefixEdge;
                    commonPrefixEdge = commonPrefixEdge.next;
                }
                /*
                informant=x
                edge.out=y
                ->
                informant=lcp(x,y)^-1 x
                edge=lcp(x,y)
                pushback=lcp(x,y)^-1 y
                */
                if (commonPrefixEdgePrev == null) {
                    edge.out = null;
                } else {
                    commonPrefixEdgePrev.next = null;
                }
                edge.target.prependButIgnoreMissingStateOutput(commonPrefixEdge);
                outputIter = commonPrefixInformant;
            }
            pttIter = edge.target;
        }
        if (pttIter.out != null && !IntQueue.eq(pttIter.out.str, outputIter)) {
            throw new IllegalArgumentException("For input '" + input + "' the state output is '" + pttIter.out +
                                               "' but training sample has remaining suffix '" + outputIter + '\'');
        }
        pttIter.out = new Out(outputIter);
    }

    private static void addBlueStates(State parent, Queue<Blue> blue) {
        for (int i = 0; i < parent.transitions.length; i++) {
            final Edge transition = parent.transitions[i];
            if (transition != null) {
                assert !contains(blue, transition.target);
                assert transition.target != parent;
                blue.add(new Blue(parent, i));
            }
        }
    }

    public static void ostia(State transducer) {
        final Queue<Blue> blue = new LinkedList<>();
        final Set<State> red = new LinkedHashSet<>();
        assert isTree(transducer, new HashSet<>());
        red.add(transducer);
        addBlueStates(transducer, blue);
        assert uniqueItems(blue);
        assert disjoint(blue, red);
        assert validateBlueAndRed(transducer, red, blue);
        blue:
        while (!blue.isEmpty()) {
            @SuppressWarnings("nullness") // false positive https://github.com/typetools/checker-framework/issues/399
            final @NonNull Blue next = blue.poll();
            final @Nullable State blueState = next.state();
            assert blueState != null;
            assert isTree(blueState, new HashSet<>());
            assert uniqueItems(blue);
            assert !contains(blue, blueState);
            assert disjoint(blue, red);
            for (State redState : red) {
                if (ostiaMerge(next, redState, blue, red)) {
                    assert disjoint(blue, red);
                    assert uniqueItems(blue);
                    continue blue;
                }
            }
            assert isTree(blueState, new HashSet<>());
            assert uniqueItems(blue);
            addBlueStates(blueState, blue);
            assert uniqueItems(blue);
            assert !contains(blue, blueState);
            assert disjoint(blue, red);
            red.add(blueState);
            assert disjoint(blue, red);
            assert validateBlueAndRed(transducer, red, blue);
        }
    }

    private static boolean ostiaMerge(Blue blue, State redState, Queue<Blue> blueToVisit, Set<State> red) {
        final Map<State, StateCopy> merged = new HashMap<>();
        final List<Blue> reachedBlueStates = new ArrayList<>();
        if (ostiaFold(redState, null, blue.parent, blue.symbol, merged, reachedBlueStates)) {
            for (Map.Entry<State, StateCopy> mergedRedState : merged.entrySet()) {
                assert mergedRedState.getKey() == mergedRedState.getValue().original;
                mergedRedState.getValue().assign();
            }
            for (Blue reachedBlueCandidate : reachedBlueStates) {
                if (red.contains(reachedBlueCandidate.parent)) {
                    assert !contains(blueToVisit, reachedBlueCandidate.state());
                    blueToVisit.add(reachedBlueCandidate);
                }
            }
            return true;
        }
        return false;
    }

    private static boolean ostiaFold(State red,
                                     @Nullable IntQueue pushedBack,
                                     State blueParent,
                                     int symbolIncomingToBlue,
                                     Map<State, StateCopy> mergedStates,
                                     List<Blue> reachedBlueStates) {
        final Edge incomingTransition = blueParent.transitions[symbolIncomingToBlue];
        assert incomingTransition != null;
        final State blueState = incomingTransition.target;
        assert red != blueState;
        assert !mergedStates.containsKey(blueState);

        final StateCopy mergedRedState = mergedStates.computeIfAbsent(red, StateCopy::new);
        final StateCopy mergedBlueState = new StateCopy(blueState);
        final Edge mergedIncomingTransition =
                mergedStates.computeIfAbsent(blueParent, StateCopy::new).transitions[symbolIncomingToBlue];
        assert mergedIncomingTransition != null;
        mergedIncomingTransition.target = red;

        final StateCopy prevBlue = mergedStates.put(blueState, mergedBlueState);
        assert prevBlue == null;

        mergedBlueState.prepend(pushedBack);
        if (mergedBlueState.out != null) {
            if (mergedRedState.out == null) {
                mergedRedState.out = mergedBlueState.out;
            } else if (!IntQueue.eq(mergedRedState.out.str, mergedBlueState.out.str)) {
                return false;
            }
        }
        for (int i = 0; i < mergedRedState.transitions.length; i++) {
            final Edge transitionBlue = mergedBlueState.transitions[i];
            if (transitionBlue != null) {
                final Edge transitionRed = mergedRedState.transitions[i];
                if (transitionRed == null) {
                    mergedRedState.transitions[i] = new Edge(transitionBlue);
                    reachedBlueStates.add(new Blue(red, i));
                } else {
                    IntQueue commonPrefixRed = transitionRed.out;
                    IntQueue commonPrefixBlue = transitionBlue.out;
                    IntQueue commonPrefixBluePrev = null;
                    while (commonPrefixBlue != null && commonPrefixRed != null &&
                           commonPrefixBlue.value == commonPrefixRed.value) {
                        commonPrefixBluePrev = commonPrefixBlue;
                        commonPrefixBlue = commonPrefixBlue.next;
                        commonPrefixRed = commonPrefixRed.next;
                    }
                    assert commonPrefixBluePrev == null || commonPrefixBluePrev.next == commonPrefixBlue;
                    if (commonPrefixRed == null) {
                        if (commonPrefixBluePrev == null) {
                            transitionBlue.out = null;
                        } else {
                            commonPrefixBluePrev.next = null;
                        }
                        assert Objects.equals(Optional.ofNullable(mergedBlueState.transitions[i]).map(e -> e.target),
                                              Optional.ofNullable(blueState.transitions[i]).map(e -> e.target));
                        if (!ostiaFold(transitionRed.target,
                                       commonPrefixBlue,
                                       blueState,
                                       i,
                                       mergedStates,
                                       reachedBlueStates)) {
                            return false;
                        }
                    } else {
                        return false;
                    }
                }
            }
        }
        return true;
    }

    public static @Nullable IntSeq run(State init, IntSeq input) {
        final List<Integer> output = new ArrayList<>();
        State iter = init;
        for (int i = 0; i < input.size(); i++) {
            final Edge edge = iter.transitions[input.get(i)];
            if (edge == null) {
                return null;
            }
            iter = edge.target;
            IntQueue q = edge.out;
            while (q != null) {
                output.add(q.value);
                q = q.next;
            }
        }
        if (iter.out == null) {
            return null;
        }
        IntQueue q = iter.out.str;
        while (q != null) {
            output.add(q.value);
            q = q.next;
        }
        return IntSeq.of(output);
    }

    // Assertion methods

    private static boolean disjoint(Queue<Blue> blue, Set<State> red) {
        for (Blue b : blue) {
            if (red.contains(b.state())) {
                return false;
            }
        }
        return true;
    }

    private static boolean contains(Queue<Blue> blue, @Nullable State state) {
        for (Blue b : blue) {
            if (Objects.equals(state, b.state())) {
                return true;
            }
        }
        return false;
    }

    private static boolean uniqueItems(Queue<Blue> blue) {
        final Set<@Nullable State> unique = new HashSet<>();
        for (Blue b : blue) {
            if (!unique.add(b.state())) {
                return false;
            }
        }
        return true;
    }

    private static boolean validateBlueAndRed(State root, Set<State> red, Queue<Blue> blue) {
        final Set<State> reachable = new HashSet<>();
        isTree(root, reachable);
        for (State r : red) {
            for (Edge edge : r.transitions) {
                assert edge == null || contains(blue, edge.target) ^ red.contains(edge.target);
            }
            assert reachable.contains(r);
        }
        for (Blue b : blue) {
            assert red.contains(b.parent);
            assert reachable.contains(b.state());
        }
        return true;
    }

    private static boolean isTree(State root, Set<State> nodes) {
        final Queue<State> toVisit = new ArrayDeque<>();
        toVisit.add(root);
        boolean isTree = true;
        while (!toVisit.isEmpty()) {
            @SuppressWarnings("nullness") // false positive https://github.com/typetools/checker-framework/issues/399
            final @NonNull State s = toVisit.poll();
            if (nodes.add(s)) {
                for (Edge edge : s.transitions) {
                    if (edge != null) {
                        toVisit.add(edge.target);
                    }
                }
            } else {
                isTree = false;
            }

        }
        return isTree;
    }

}


1	/* Copyright (C) 2013-2023 TU Dortmund
2	* This file is part of LearnLib, http://www.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.algorithms.ostia;
17
18	import java.util.ArrayDeque;
19	import java.util.ArrayList;
20	import java.util.Collection;
21	import java.util.HashMap;
22	import java.util.HashSet;
23	import java.util.Iterator;
24	import java.util.LinkedHashSet;
25	import java.util.LinkedList;
26	import java.util.List;
27	import java.util.Map;
28	import java.util.Objects;
29	import java.util.Optional;
30	import java.util.Queue;
31	import java.util.Set;
32
33	import de.learnlib.api.algorithm.PassiveLearningAlgorithm;
34	import de.learnlib.api.query.DefaultQuery;
35	import net.automatalib.automata.transducers.SubsequentialTransducer;
36	import net.automatalib.commons.smartcollections.IntSeq;
37	import net.automatalib.commons.util.Pair;
38	import net.automatalib.words.Alphabet;
39	import net.automatalib.words.GrowingAlphabet;
40	import net.automatalib.words.Word;
41	import net.automatalib.words.impl.GrowingMapAlphabet;
42	import org.checkerframework.checker.nullness.qual.NonNull;
43	import org.checkerframework.checker.nullness.qual.Nullable;
44
45	/**
46	* Implementation of the "onward subsequential transducer inference algorithm" (OSTIA) from the paper <a
47	* href="https://doi.org/10.1109/34.211465">Learning Subsequential Transducers for Pattern Recognition Interpretation
48	* Tasks</a> by Oncina, García and Vidal.
49	*/
50	public class OSTIA<I, O> implements PassiveLearningAlgorithm<SubsequentialTransducer<?, I, ?, O>, I, Word<O>> {	2✔
51
52	private final Alphabet<I> inputAlphabet;
53	private final GrowingAlphabet<O> outputAlphabet;
54	private final State root;
55	private boolean hasBeenComputed;
56
57	public OSTIA(Alphabet<I> inputAlphabet) {	2✔
58	this.inputAlphabet = inputAlphabet;	2✔
59	this.outputAlphabet = new GrowingMapAlphabet<>();	2✔
60	this.root = new State(inputAlphabet.size());	2✔
61	this.hasBeenComputed = false;	2✔
62	}	2✔
63
64	@Override
65	public void addSamples(Collection<? extends DefaultQuery<I, Word<O>>> samples) {
66	for (DefaultQuery<I, Word<O>> sample : samples) {	2✔
67	final Word<O> output = sample.getOutput();	2✔
68	this.outputAlphabet.addAll(output.asList());	2✔
69	buildPttOnward(root,	2✔
70	sample.getInput().asIntSeq(inputAlphabet),	2✔
71	IntQueue.asQueue(output.asIntSeq(outputAlphabet)));	2✔
72	}	2✔
73	}	2✔
74
75	@Override
76	public SubsequentialTransducer<?, I, ?, O> computeModel() {
77	if (!hasBeenComputed) {	2✔
78	hasBeenComputed = true;	2✔
79	ostia(root);	2✔
80	}
81	return new OSSTWrapper<>(root, inputAlphabet, outputAlphabet);	2✔
82	}
83
84	public static State buildPtt(int alphabetSize, Iterator<Pair<IntSeq, IntSeq>> informant) {
85	final State root = new State(alphabetSize);	2✔
86	while (informant.hasNext()) {	2✔
87	Pair<IntSeq, IntSeq> inout = informant.next();	2✔
88	buildPttOnward(root, inout.getFirst(), IntQueue.asQueue(inout.getSecond()));	2✔
89	}	2✔
90	return root;	2✔
91	}
92
93	private static void buildPttOnward(State ptt, IntSeq input, @Nullable IntQueue output) {
94	State pttIter = ptt;	2✔
95	@Nullable IntQueue outputIter = output;	2✔
96
97	for (int i = 0; i < input.size(); i++) {//input index	2✔
98	final int symbol = input.get(i);	2✔
99	final Edge edge;
100	if (pttIter.transitions[symbol] == null) {	2✔
101	edge = new Edge();	2✔
102	edge.out = outputIter;	2✔
103	edge.target = new State(pttIter.transitions.length);	2✔
104	pttIter.transitions[symbol] = edge;	2✔
105	outputIter = null;	2✔
106	} else {
107	edge = pttIter.transitions[symbol];	2✔
108	IntQueue commonPrefixEdge = edge.out;	2✔
109	IntQueue commonPrefixEdgePrev = null;	2✔
110	IntQueue commonPrefixInformant = outputIter;	2✔
111	while (commonPrefixEdge != null && commonPrefixInformant != null &&	2✔
112	commonPrefixEdge.value == commonPrefixInformant.value) {
113	commonPrefixInformant = commonPrefixInformant.next;	2✔
114	commonPrefixEdgePrev = commonPrefixEdge;	2✔
115	commonPrefixEdge = commonPrefixEdge.next;	2✔
116	}
117	/*
118	informant=x
119	edge.out=y
120	->
121	informant=lcp(x,y)^-1 x
122	edge=lcp(x,y)
123	pushback=lcp(x,y)^-1 y
124	*/
125	if (commonPrefixEdgePrev == null) {	2✔
126	edge.out = null;	2✔
127	} else {
128	commonPrefixEdgePrev.next = null;	2✔
129	}
130	edge.target.prependButIgnoreMissingStateOutput(commonPrefixEdge);	2✔
131	outputIter = commonPrefixInformant;	2✔
132	}
133	pttIter = edge.target;	2✔
134	}
135	if (pttIter.out != null && !IntQueue.eq(pttIter.out.str, outputIter)) {	2✔
136	throw new IllegalArgumentException("For input '" + input + "' the state output is '" + pttIter.out +	2✔
137	"' but training sample has remaining suffix '" + outputIter + '\'');
138	}
139	pttIter.out = new Out(outputIter);	2✔
140	}	2✔
141
142	private static void addBlueStates(State parent, Queue<Blue> blue) {
143	for (int i = 0; i < parent.transitions.length; i++) {	2✔
144	final Edge transition = parent.transitions[i];	2✔
145	if (transition != null) {	2✔
146	assert !contains(blue, transition.target);	2✔
147	assert transition.target != parent;	2✔
148	blue.add(new Blue(parent, i));	2✔
149	}
150	}
151	}	2✔
152
153	public static void ostia(State transducer) {
154	final Queue<Blue> blue = new LinkedList<>();	2✔
155	final Set<State> red = new LinkedHashSet<>();	2✔
156	assert isTree(transducer, new HashSet<>());	2✔
157	red.add(transducer);	2✔
158	addBlueStates(transducer, blue);	2✔
159	assert uniqueItems(blue);	2✔
160	assert disjoint(blue, red);	2✔
161	assert validateBlueAndRed(transducer, red, blue);	2✔
162	blue:
163	while (!blue.isEmpty()) {	2✔
164	@SuppressWarnings("nullness") // false positive https://github.com/typetools/checker-framework/issues/399
165	final @NonNull Blue next = blue.poll();	2✔
166	final @Nullable State blueState = next.state();	2✔
167	assert blueState != null;	2✔
168	assert isTree(blueState, new HashSet<>());	2✔
169	assert uniqueItems(blue);	2✔
170	assert !contains(blue, blueState);	2✔
171	assert disjoint(blue, red);	2✔
172	for (State redState : red) {	2✔
173	if (ostiaMerge(next, redState, blue, red)) {	2✔
174	assert disjoint(blue, red);	2✔
175	assert uniqueItems(blue);	2✔
176	continue blue;
177	}
178	}	2✔
179	assert isTree(blueState, new HashSet<>());	2✔
180	assert uniqueItems(blue);	2✔
181	addBlueStates(blueState, blue);	2✔
182	assert uniqueItems(blue);	2✔
183	assert !contains(blue, blueState);	2✔
184	assert disjoint(blue, red);	2✔
185	red.add(blueState);	2✔
186	assert disjoint(blue, red);	2✔
187	assert validateBlueAndRed(transducer, red, blue);	2✔
188	}	2✔
189	}	2✔
190
191	private static boolean ostiaMerge(Blue blue, State redState, Queue<Blue> blueToVisit, Set<State> red) {
192	final Map<State, StateCopy> merged = new HashMap<>();	2✔
193	final List<Blue> reachedBlueStates = new ArrayList<>();	2✔
194	if (ostiaFold(redState, null, blue.parent, blue.symbol, merged, reachedBlueStates)) {	2✔
195	for (Map.Entry<State, StateCopy> mergedRedState : merged.entrySet()) {	2✔
196	assert mergedRedState.getKey() == mergedRedState.getValue().original;	2✔
197	mergedRedState.getValue().assign();	2✔
198	}	2✔
199	for (Blue reachedBlueCandidate : reachedBlueStates) {	2✔
200	if (red.contains(reachedBlueCandidate.parent)) {	2✔
201	assert !contains(blueToVisit, reachedBlueCandidate.state());	2✔
202	blueToVisit.add(reachedBlueCandidate);	2✔
203	}
204	}	2✔
205	return true;	2✔
206	}
207	return false;	2✔
208	}
209
210	private static boolean ostiaFold(State red,
211	@Nullable IntQueue pushedBack,
212	State blueParent,
213	int symbolIncomingToBlue,
214	Map<State, StateCopy> mergedStates,
215	List<Blue> reachedBlueStates) {
216	final Edge incomingTransition = blueParent.transitions[symbolIncomingToBlue];	2✔
217	assert incomingTransition != null;	2✔
218	final State blueState = incomingTransition.target;	2✔
219	assert red != blueState;	2✔
220	assert !mergedStates.containsKey(blueState);	2✔
221
222	final StateCopy mergedRedState = mergedStates.computeIfAbsent(red, StateCopy::new);	2✔
223	final StateCopy mergedBlueState = new StateCopy(blueState);	2✔
224	final Edge mergedIncomingTransition =	2✔
225	mergedStates.computeIfAbsent(blueParent, StateCopy::new).transitions[symbolIncomingToBlue];	2✔
226	assert mergedIncomingTransition != null;	2✔
227	mergedIncomingTransition.target = red;	2✔
228
229	final StateCopy prevBlue = mergedStates.put(blueState, mergedBlueState);	2✔
230	assert prevBlue == null;	2✔
231
232	mergedBlueState.prepend(pushedBack);	2✔
233	if (mergedBlueState.out != null) {	2✔
234	if (mergedRedState.out == null) {	2✔
235	mergedRedState.out = mergedBlueState.out;	2✔
236	} else if (!IntQueue.eq(mergedRedState.out.str, mergedBlueState.out.str)) {	2✔
237	return false;	2✔
238	}
239	}
240	for (int i = 0; i < mergedRedState.transitions.length; i++) {	2✔
241	final Edge transitionBlue = mergedBlueState.transitions[i];	2✔
242	if (transitionBlue != null) {	2✔
243	final Edge transitionRed = mergedRedState.transitions[i];	2✔
244	if (transitionRed == null) {	2✔
245	mergedRedState.transitions[i] = new Edge(transitionBlue);	2✔
246	reachedBlueStates.add(new Blue(red, i));	2✔
247	} else {
248	IntQueue commonPrefixRed = transitionRed.out;	2✔
249	IntQueue commonPrefixBlue = transitionBlue.out;	2✔
250	IntQueue commonPrefixBluePrev = null;	2✔
251	while (commonPrefixBlue != null && commonPrefixRed != null &&	2✔
252	commonPrefixBlue.value == commonPrefixRed.value) {
253	commonPrefixBluePrev = commonPrefixBlue;	2✔
254	commonPrefixBlue = commonPrefixBlue.next;	2✔
255	commonPrefixRed = commonPrefixRed.next;	2✔
256	}
257	assert commonPrefixBluePrev == null \|\| commonPrefixBluePrev.next == commonPrefixBlue;	2✔
258	if (commonPrefixRed == null) {	2✔
259	if (commonPrefixBluePrev == null) {	2✔
260	transitionBlue.out = null;	2✔
261	} else {
262	commonPrefixBluePrev.next = null;	2✔
263	}
264	assert Objects.equals(Optional.ofNullable(mergedBlueState.transitions[i]).map(e -> e.target),	2✔
265	Optional.ofNullable(blueState.transitions[i]).map(e -> e.target));	2✔
266	if (!ostiaFold(transitionRed.target,	2✔
267	commonPrefixBlue,
268	blueState,
269	i,
270	mergedStates,
271	reachedBlueStates)) {
272	return false;	2✔
273	}
274	} else {
275	return false;	2✔
276	}
277	}
278	}
279	}
280	return true;	2✔
281	}
282
283	public static @Nullable IntSeq run(State init, IntSeq input) {
284	final List<Integer> output = new ArrayList<>();	2✔
285	State iter = init;	2✔
286	for (int i = 0; i < input.size(); i++) {	2✔
287	final Edge edge = iter.transitions[input.get(i)];	2✔
288	if (edge == null) {	2✔
289	return null;	×
290	}
291	iter = edge.target;	2✔
292	IntQueue q = edge.out;	2✔
293	while (q != null) {	2✔
294	output.add(q.value);	2✔
295	q = q.next;	2✔
296	}
297	}
298	if (iter.out == null) {	2✔
299	return null;	×
300	}
301	IntQueue q = iter.out.str;	2✔
302	while (q != null) {	2✔
303	output.add(q.value);	2✔
304	q = q.next;	2✔
305	}
306	return IntSeq.of(output);	2✔
307	}
308
309	// Assertion methods
310
311	private static boolean disjoint(Queue<Blue> blue, Set<State> red) {
312	for (Blue b : blue) {	2✔
313	if (red.contains(b.state())) {	2✔
314	return false;	×
315	}
316	}	2✔
317	return true;	2✔
318	}
319
320	private static boolean contains(Queue<Blue> blue, @Nullable State state) {
321	for (Blue b : blue) {	2✔
322	if (Objects.equals(state, b.state())) {	2✔
323	return true;	2✔
324	}
325	}	2✔
326	return false;	2✔
327	}
328
329	private static boolean uniqueItems(Queue<Blue> blue) {
330	final Set<@Nullable State> unique = new HashSet<>();	2✔
331	for (Blue b : blue) {	2✔
332	if (!unique.add(b.state())) {	2✔
333	return false;	×
334	}
335	}	2✔
336	return true;	2✔
337	}
338
339	private static boolean validateBlueAndRed(State root, Set<State> red, Queue<Blue> blue) {
340	final Set<State> reachable = new HashSet<>();	2✔
341	isTree(root, reachable);	2✔
342	for (State r : red) {	2✔
343	for (Edge edge : r.transitions) {	2✔
344	assert edge == null \|\| contains(blue, edge.target) ^ red.contains(edge.target);	2✔
345	}
346	assert reachable.contains(r);	2✔
347	}	2✔
348	for (Blue b : blue) {	2✔
349	assert red.contains(b.parent);	2✔
350	assert reachable.contains(b.state());	2✔
351	}	2✔
352	return true;	2✔
353	}
354
355	private static boolean isTree(State root, Set<State> nodes) {
356	final Queue<State> toVisit = new ArrayDeque<>();	2✔
357	toVisit.add(root);	2✔
358	boolean isTree = true;	2✔
359	while (!toVisit.isEmpty()) {	2✔
360	@SuppressWarnings("nullness") // false positive https://github.com/typetools/checker-framework/issues/399
361	final @NonNull State s = toVisit.poll();	2✔
362	if (nodes.add(s)) {	2✔
363	for (Edge edge : s.transitions) {	2✔
364	if (edge != null) {	2✔
365	toVisit.add(edge.target);	2✔
366	}
367	}
368	} else {
369	isTree = false;	2✔
370	}
371
372	}	2✔
373	return isTree;	2✔
374	}
375
376	}
377

LearnLib / learnlib / 6433387082

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