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

72.79

/datastructures/pta/src/main/java/de/learnlib/datastructure/pta/pta/BasePTA.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.datastructure.pta.pta;

import java.util.ArrayDeque;
import java.util.ArrayList;
import java.util.Collection;
import java.util.Deque;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Objects;
import java.util.Queue;
import java.util.Set;
import java.util.function.Function;
import java.util.stream.Collectors;
import java.util.stream.IntStream;

import com.google.common.collect.AbstractIterator;
import com.google.common.collect.Iterators;
import net.automatalib.automata.MutableDeterministic;
import net.automatalib.automata.UniversalDeterministicAutomaton;
import net.automatalib.commons.smartcollections.IntSeq;
import net.automatalib.commons.util.Pair;
import net.automatalib.graphs.Graph;
import net.automatalib.util.automata.Automata;
import net.automatalib.visualization.DefaultVisualizationHelper;
import net.automatalib.visualization.VisualizationHelper;
import net.automatalib.words.Alphabet;
import org.checkerframework.checker.index.qual.NonNegative;
import org.checkerframework.checker.nullness.qual.Nullable;

/**
 * Base class for prefix tree acceptors.
 *
 * @param <SP>
 *         state property type
 * @param <TP>
 *         transition property type
 * @param <S>
 *         state type
 */
public class BasePTA<SP, TP, S extends AbstractBasePTAState<SP, TP, S>>
        implements UniversalDeterministicAutomaton<S, Integer, PTATransition<S>, SP, TP> {

    protected final @NonNegative int alphabetSize;
    protected final S root;

    /**
     * Constructor.
     *
     * @param alphabetSize
     *         the size of the input alphabet
     * @param root
     *         the root state
     */
    public BasePTA(@NonNegative int alphabetSize, S root) {
        this.alphabetSize = alphabetSize;
        this.root = Objects.requireNonNull(root);
    }

    /**
     * Retrieves the state reached by the given word (represented as an {@code int} array). If there is no path for the
     * given word in the PTA, {@code null} is returned.
     *
     * @param word
     *         the word
     *
     * @return the state reached by this word, or {@code null} if there is no path for the given word in the PTA
     */
    public @Nullable S getState(int[] word) {
        S curr = root;
        int len = word.length;
        for (int i = 0; i < len && curr != null; i++) {
            curr = curr.getSuccessor(word[i]);
        }
        return curr;
    }

    /**
     * Adds a sample to the PTA, and sets the property of the last reached (or inserted) state accordingly.
     *
     * @param sample
     *         the word to add to the PTA
     * @param lastProperty
     *         the property of the last state to set
     */
    public void addSample(IntSeq sample, SP lastProperty) {
        S target = getOrCreateState(sample);
        if (!target.tryMergeStateProperty(lastProperty)) {
            throw new IllegalStateException();
        }
    }

    /**
     * Retrieves the state reached by the given word (represented as an {@code int} array). If there is no path for the
     * word in the PTA, it will be added to the PTA on-the-fly.
     *
     * @param word
     *         the word
     *
     * @return the state reached by this word, which might have been newly created (along with all required predecessor
     * states)
     */
    public S getOrCreateState(IntSeq word) {
        S curr = root;
        for (int sym : word) {
            curr = curr.getOrCreateSuccessor(sym, alphabetSize);
        }

        return curr;
    }

    public void addSampleWithStateProperties(int[] sample, List<? extends SP> lastStateProperties) {
        int sampleLen = sample.length;
        int skip = sampleLen + 1 - lastStateProperties.size();
        if (skip < 0) {
            throw new IllegalArgumentException();
        }

        S curr = getRoot();
        int i = 0;
        while (i < skip) {
            int sym = sample[i++];
            curr = curr.getOrCreateSuccessor(sym, alphabetSize);
        }

        Iterator<? extends SP> spIt = lastStateProperties.iterator();

        while (i < sampleLen) {
            if (!curr.tryMergeStateProperty(spIt.next())) {
                throw new IllegalArgumentException();
            }
            int sym = sample[i++];
            curr = curr.getOrCreateSuccessor(sym, alphabetSize);
        }

        if (!curr.tryMergeStateProperty(spIt.next())) {
            throw new IllegalArgumentException();
        }
    }

    /**
     * Retrieves the root of the PTA.
     *
     * @return the root state
     */
    public S getRoot() {
        return root;
    }

    public void addSampleWithTransitionProperties(IntSeq sample, List<? extends TP> lastTransitionProperties) {
        int sampleLen = sample.size();
        int skip = sampleLen - lastTransitionProperties.size();
        if (skip < 0) {
            throw new IllegalArgumentException();
        }

        S curr = getRoot();
        int i = 0;
        while (i < skip) {
            int sym = sample.get(i++);
            curr = curr.getOrCreateSuccessor(sym, alphabetSize);
        }

        Iterator<? extends TP> tpIt = lastTransitionProperties.iterator();
        while (i < sampleLen) {
            int sym = sample.get(i++);
            if (!curr.tryMergeTransitionProperty(sym, alphabetSize, tpIt.next())) {
                throw new IllegalArgumentException();
            }
            curr = curr.getOrCreateSuccessor(sym, alphabetSize);
        }
    }

    public <I> void toAutomaton(MutableDeterministic<?, I, ?, ? super SP, ? super TP> automaton, Alphabet<I> alphabet) {
        toAutomaton(automaton, alphabet, sp -> sp, tp -> tp);
    }

    public <S2, I, SP2, TP2> void toAutomaton(MutableDeterministic<S2, I, ?, ? super SP2, ? super TP2> automaton,
                                              Alphabet<I> alphabet,
                                              Function<? super SP, ? extends SP2> spExtractor,
                                              Function<? super TP, ? extends TP2> tpExtractor) {

        Map<S, S2> resultStates = new HashMap<>();
        Queue<Pair<S, S2>> queue = new ArrayDeque<>();

        SP2 initProp = spExtractor.apply(root.getStateProperty());
        S2 resultInit = automaton.addInitialState(initProp);
        queue.add(Pair.of(root, resultInit));

        Pair<S, S2> curr;
        while ((curr = queue.poll()) != null) {
            S ptaState = curr.getFirst();
            S2 resultState = curr.getSecond();

            for (int i = 0; i < alphabetSize; i++) {
                S ptaSucc = ptaState.getSuccessor(i);
                if (ptaSucc != null) {
                    S2 resultSucc = resultStates.get(ptaSucc);
                    if (resultSucc == null) {
                        SP2 prop = spExtractor.apply(ptaSucc.getStateProperty());
                        resultSucc = automaton.addState(prop);
                        resultStates.put(ptaSucc, resultSucc);
                        queue.offer(Pair.of(ptaSucc, resultSucc));
                    }
                    I sym = alphabet.getSymbol(i);
                    TP2 transProp = tpExtractor.apply(ptaState.getTransProperty(i));
                    automaton.setTransition(resultState, sym, resultSucc, transProp);
                }
            }
        }

        Automata.invasiveMinimize(automaton, alphabet);
    }

    public <I> Graph<S, PTATransition<S>> graphView(Alphabet<I> alphabet) {
        return new Graph<S, PTATransition<S>>() {

            @Override
            public Collection<PTATransition<S>> getOutgoingEdges(S node) {
                return IntStream.range(0, Math.min(alphabet.size(), alphabetSize))
                                .mapToObj(i -> getTransition(node, i))
                                .filter(Objects::nonNull)
                                .collect(Collectors.toList());
            }

            @Override
            public S getTarget(PTATransition<S> edge) {
                return edge.getTarget();
            }

            @Override
            public Collection<S> getNodes() {
                return bfsStates();
            }

            @Override
            public Iterator<S> iterator() {
                return bfsIterator();
            }

            @Override
            public VisualizationHelper<S, PTATransition<S>> getVisualizationHelper() {
                return new DefaultVisualizationHelper<S, PTATransition<S>>() {

                    @Override
                    public boolean getNodeProperties(S node, Map<String, String> properties) {
                        final SP property = node.getProperty();
                        properties.put(NodeAttrs.LABEL, property == null ? "" : property.toString());
                        return super.getNodeProperties(node, properties);
                    }

                    @Override
                    public boolean getEdgeProperties(S src,
                                                     PTATransition<S> edge,
                                                     S tgt,
                                                     Map<String, String> properties) {
                        properties.put(EdgeAttrs.LABEL, String.valueOf(alphabet.getSymbol(edge.getIndex())));
                        return super.getEdgeProperties(src, edge, tgt, properties);
                    }
                };
            }
        };
    }

    /**
     * Retrieves a list of all states in this PTA that are reachable from the root state. The states will be returned in
     * breadth-first order.
     *
     * @return a breadth-first ordered list of all states in this PTA
     */
    public List<S> bfsStates() {
        List<S> stateList = new ArrayList<>();
        Set<S> visited = new HashSet<>();

        int ptr = 0;
        stateList.add(root);
        visited.add(root);
        int numStates = 1;

        while (ptr < numStates) {
            S curr = stateList.get(ptr++);
            for (int i = 0; i < alphabetSize; i++) {
                S succ = curr.getSuccessor(i);
                if (succ != null && visited.add(succ)) {
                    stateList.add(succ);
                    numStates++;
                }
            }
        }

        return stateList;
    }

    /**
     * Retrieves an iterator that can be used for iterating over all states in this PTA that are reachable from the root
     * state in a breadth-first order.
     *
     * @return an iterator for iterating over all states in this PTA
     */
    public Iterator<S> bfsIterator() {
        Set<S> visited = new HashSet<>();
        final Deque<S> bfsQueue = new ArrayDeque<>();
        bfsQueue.add(root);
        visited.add(root);

        return new AbstractIterator<S>() {

            @Override
            protected S computeNext() {
                S next = bfsQueue.poll();
                if (next == null) {
                    return endOfData();
                }
                for (int i = 0; i < alphabetSize; i++) {
                    S child = next.getSuccessor(i);
                    if (child != null && visited.add(child)) {
                        bfsQueue.offer(child);
                    }
                }
                return next;
            }
        };
    }

    @Override
    public S getSuccessor(PTATransition<S> transition) {
        return transition.getTarget();
    }

    @Override
    public @Nullable S getSuccessor(S state, Integer input) {
        return state.getSuccessor(input);
    }

    @Override
    public Iterator<S> iterator() {
        return bfsIterator();
    }

    @Override
    public Collection<S> getStates() {
        return bfsStates();
    }

    @Override
    public int size() {
        return countStates();
    }

    /**
     * Counts the number of states in this PTA. Note that this method might require a complete traversal of the PTA.
     *
     * @return the number of states in the PTA reachable from the root state
     */

    public @NonNegative int countStates() {
        return Iterators.size(bfsIterator());
    }

    @Override
    public S getInitialState() {
        return getRoot();
    }

    @Override
    public @Nullable PTATransition<S> getTransition(S state, Integer input) {
        if (input == null || state.getSuccessor(input) == null) {
            return null;
        }

        return new PTATransition<>(state, input);
    }

    @Override
    public SP getStateProperty(S state) {
        return state.getStateProperty();
    }

    @Override
    public TP getTransitionProperty(PTATransition<S> transition) {
        return transition.getSource().getTransProperty(transition.getIndex());
    }
}

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.datastructure.pta.pta;
17
18	import java.util.ArrayDeque;
19	import java.util.ArrayList;
20	import java.util.Collection;
21	import java.util.Deque;
22	import java.util.HashMap;
23	import java.util.HashSet;
24	import java.util.Iterator;
25	import java.util.List;
26	import java.util.Map;
27	import java.util.Objects;
28	import java.util.Queue;
29	import java.util.Set;
30	import java.util.function.Function;
31	import java.util.stream.Collectors;
32	import java.util.stream.IntStream;
33
34	import com.google.common.collect.AbstractIterator;
35	import com.google.common.collect.Iterators;
36	import net.automatalib.automata.MutableDeterministic;
37	import net.automatalib.automata.UniversalDeterministicAutomaton;
38	import net.automatalib.commons.smartcollections.IntSeq;
39	import net.automatalib.commons.util.Pair;
40	import net.automatalib.graphs.Graph;
41	import net.automatalib.util.automata.Automata;
42	import net.automatalib.visualization.DefaultVisualizationHelper;
43	import net.automatalib.visualization.VisualizationHelper;
44	import net.automatalib.words.Alphabet;
45	import org.checkerframework.checker.index.qual.NonNegative;
46	import org.checkerframework.checker.nullness.qual.Nullable;
47
48	/**
49	* Base class for prefix tree acceptors.
50	*
51	* @param <SP>
52	* state property type
53	* @param <TP>
54	* transition property type
55	* @param <S>
56	* state type
57	*/
58	public class BasePTA<SP, TP, S extends AbstractBasePTAState<SP, TP, S>>
59	implements UniversalDeterministicAutomaton<S, Integer, PTATransition<S>, SP, TP> {
60
61	protected final @NonNegative int alphabetSize;
62	protected final S root;
63
64	/**
65	* Constructor.
66	*
67	* @param alphabetSize
68	* the size of the input alphabet
69	* @param root
70	* the root state
71	*/
72	public BasePTA(@NonNegative int alphabetSize, S root) {	2✔
73	this.alphabetSize = alphabetSize;	2✔
74	this.root = Objects.requireNonNull(root);	2✔
75	}	2✔
76
77	/**
78	* Retrieves the state reached by the given word (represented as an {@code int} array). If there is no path for the
79	* given word in the PTA, {@code null} is returned.
80	*
81	* @param word
82	* the word
83	*
84	* @return the state reached by this word, or {@code null} if there is no path for the given word in the PTA
85	*/
86	public @Nullable S getState(int[] word) {
87	S curr = root;	×
88	int len = word.length;	×
89	for (int i = 0; i < len && curr != null; i++) {	×
90	curr = curr.getSuccessor(word[i]);	×
91	}
92	return curr;	×
93	}
94
95	/**
96	* Adds a sample to the PTA, and sets the property of the last reached (or inserted) state accordingly.
97	*
98	* @param sample
99	* the word to add to the PTA
100	* @param lastProperty
101	* the property of the last state to set
102	*/
103	public void addSample(IntSeq sample, SP lastProperty) {
104	S target = getOrCreateState(sample);	2✔
105	if (!target.tryMergeStateProperty(lastProperty)) {	2✔
106	throw new IllegalStateException();	×
107	}
108	}	2✔
109
110	/**
111	* Retrieves the state reached by the given word (represented as an {@code int} array). If there is no path for the
112	* word in the PTA, it will be added to the PTA on-the-fly.
113	*
114	* @param word
115	* the word
116	*
117	* @return the state reached by this word, which might have been newly created (along with all required predecessor
118	* states)
119	*/
120	public S getOrCreateState(IntSeq word) {
121	S curr = root;	2✔
122	for (int sym : word) {	2✔
123	curr = curr.getOrCreateSuccessor(sym, alphabetSize);	2✔
124	}	2✔
125
126	return curr;	2✔
127	}
128
129	public void addSampleWithStateProperties(int[] sample, List<? extends SP> lastStateProperties) {
130	int sampleLen = sample.length;	2✔
131	int skip = sampleLen + 1 - lastStateProperties.size();	2✔
132	if (skip < 0) {	2✔
133	throw new IllegalArgumentException();	×
134	}
135
136	S curr = getRoot();	2✔
137	int i = 0;	2✔
138	while (i < skip) {	2✔
139	int sym = sample[i++];	×
140	curr = curr.getOrCreateSuccessor(sym, alphabetSize);	×
141	}	×
142
143	Iterator<? extends SP> spIt = lastStateProperties.iterator();	2✔
144
145	while (i < sampleLen) {	2✔
146	if (!curr.tryMergeStateProperty(spIt.next())) {	2✔
147	throw new IllegalArgumentException();	×
148	}
149	int sym = sample[i++];	2✔
150	curr = curr.getOrCreateSuccessor(sym, alphabetSize);	2✔
151	}	2✔
152
153	if (!curr.tryMergeStateProperty(spIt.next())) {	2✔
154	throw new IllegalArgumentException();	×
155	}
156	}	2✔
157
158	/**
159	* Retrieves the root of the PTA.
160	*
161	* @return the root state
162	*/
163	public S getRoot() {
164	return root;	2✔
165	}
166
167	public void addSampleWithTransitionProperties(IntSeq sample, List<? extends TP> lastTransitionProperties) {
168	int sampleLen = sample.size();	1✔
169	int skip = sampleLen - lastTransitionProperties.size();	1✔
170	if (skip < 0) {	1✔
171	throw new IllegalArgumentException();	×
172	}
173
174	S curr = getRoot();	1✔
175	int i = 0;	1✔
176	while (i < skip) {	1✔
177	int sym = sample.get(i++);	×
178	curr = curr.getOrCreateSuccessor(sym, alphabetSize);	×
179	}	×
180
181	Iterator<? extends TP> tpIt = lastTransitionProperties.iterator();	1✔
182	while (i < sampleLen) {	1✔
183	int sym = sample.get(i++);	1✔
184	if (!curr.tryMergeTransitionProperty(sym, alphabetSize, tpIt.next())) {	1✔
185	throw new IllegalArgumentException();	×
186	}
187	curr = curr.getOrCreateSuccessor(sym, alphabetSize);	1✔
188	}	1✔
189	}	1✔
190
191	public <I> void toAutomaton(MutableDeterministic<?, I, ?, ? super SP, ? super TP> automaton, Alphabet<I> alphabet) {
192	toAutomaton(automaton, alphabet, sp -> sp, tp -> tp);	1✔
193	}	1✔
194
195	public <S2, I, SP2, TP2> void toAutomaton(MutableDeterministic<S2, I, ?, ? super SP2, ? super TP2> automaton,
196	Alphabet<I> alphabet,
197	Function<? super SP, ? extends SP2> spExtractor,
198	Function<? super TP, ? extends TP2> tpExtractor) {
199
200	Map<S, S2> resultStates = new HashMap<>();	1✔
201	Queue<Pair<S, S2>> queue = new ArrayDeque<>();	1✔
202
203	SP2 initProp = spExtractor.apply(root.getStateProperty());	1✔
204	S2 resultInit = automaton.addInitialState(initProp);	1✔
205	queue.add(Pair.of(root, resultInit));	1✔
206
207	Pair<S, S2> curr;
208	while ((curr = queue.poll()) != null) {	1✔
209	S ptaState = curr.getFirst();	1✔
210	S2 resultState = curr.getSecond();	1✔
211
212	for (int i = 0; i < alphabetSize; i++) {	1✔
213	S ptaSucc = ptaState.getSuccessor(i);	1✔
214	if (ptaSucc != null) {	1✔
215	S2 resultSucc = resultStates.get(ptaSucc);	1✔
216	if (resultSucc == null) {	1✔
217	SP2 prop = spExtractor.apply(ptaSucc.getStateProperty());	1✔
218	resultSucc = automaton.addState(prop);	1✔
219	resultStates.put(ptaSucc, resultSucc);	1✔
220	queue.offer(Pair.of(ptaSucc, resultSucc));	1✔
221	}
222	I sym = alphabet.getSymbol(i);	1✔
223	TP2 transProp = tpExtractor.apply(ptaState.getTransProperty(i));	1✔
224	automaton.setTransition(resultState, sym, resultSucc, transProp);	1✔
225	}
226	}
227	}	1✔
228
229	Automata.invasiveMinimize(automaton, alphabet);	1✔
230	}	1✔
231
232	public <I> Graph<S, PTATransition<S>> graphView(Alphabet<I> alphabet) {
233	return new Graph<S, PTATransition<S>>() {	2✔
234
235	@Override
236	public Collection<PTATransition<S>> getOutgoingEdges(S node) {
237	return IntStream.range(0, Math.min(alphabet.size(), alphabetSize))	2✔
238	.mapToObj(i -> getTransition(node, i))	2✔
239	.filter(Objects::nonNull)	2✔
240	.collect(Collectors.toList());	2✔
241	}
242
243	@Override
244	public S getTarget(PTATransition<S> edge) {
245	return edge.getTarget();	2✔
246	}
247
248	@Override
249	public Collection<S> getNodes() {
250	return bfsStates();	×
251	}
252
253	@Override
254	public Iterator<S> iterator() {
255	return bfsIterator();	2✔
256	}
257
258	@Override
259	public VisualizationHelper<S, PTATransition<S>> getVisualizationHelper() {
260	return new DefaultVisualizationHelper<S, PTATransition<S>>() {	2✔
261
262	@Override
263	public boolean getNodeProperties(S node, Map<String, String> properties) {
264	final SP property = node.getProperty();	2✔
265	properties.put(NodeAttrs.LABEL, property == null ? "" : property.toString());	2✔
266	return super.getNodeProperties(node, properties);	2✔
267	}
268
269	@Override
270	public boolean getEdgeProperties(S src,
271	PTATransition<S> edge,
272	S tgt,
273	Map<String, String> properties) {
274	properties.put(EdgeAttrs.LABEL, String.valueOf(alphabet.getSymbol(edge.getIndex())));	2✔
275	return super.getEdgeProperties(src, edge, tgt, properties);	2✔
276	}
277	};
278	}
279	};
280	}
281
282	/**
283	* Retrieves a list of all states in this PTA that are reachable from the root state. The states will be returned in
284	* breadth-first order.
285	*
286	* @return a breadth-first ordered list of all states in this PTA
287	*/
288	public List<S> bfsStates() {
289	List<S> stateList = new ArrayList<>();	×
290	Set<S> visited = new HashSet<>();	×
291
292	int ptr = 0;	×
293	stateList.add(root);	×
294	visited.add(root);	×
295	int numStates = 1;	×
296
297	while (ptr < numStates) {	×
298	S curr = stateList.get(ptr++);	×
299	for (int i = 0; i < alphabetSize; i++) {	×
300	S succ = curr.getSuccessor(i);	×
301	if (succ != null && visited.add(succ)) {	×
302	stateList.add(succ);	×
303	numStates++;	×
304	}
305	}
306	}	×
307
308	return stateList;	×
309	}
310
311	/**
312	* Retrieves an iterator that can be used for iterating over all states in this PTA that are reachable from the root
313	* state in a breadth-first order.
314	*
315	* @return an iterator for iterating over all states in this PTA
316	*/
317	public Iterator<S> bfsIterator() {
318	Set<S> visited = new HashSet<>();	2✔
319	final Deque<S> bfsQueue = new ArrayDeque<>();	2✔
320	bfsQueue.add(root);	2✔
321	visited.add(root);	2✔
322
323	return new AbstractIterator<S>() {	2✔
324
325	@Override
326	protected S computeNext() {
327	S next = bfsQueue.poll();	2✔
328	if (next == null) {	2✔
329	return endOfData();	2✔
330	}
331	for (int i = 0; i < alphabetSize; i++) {	2✔
332	S child = next.getSuccessor(i);	2✔
333	if (child != null && visited.add(child)) {	2✔
334	bfsQueue.offer(child);	2✔
335	}
336	}
337	return next;	2✔
338	}
339	};
340	}
341
342	@Override
343	public S getSuccessor(PTATransition<S> transition) {
344	return transition.getTarget();	×
345	}
346
347	@Override
348	public @Nullable S getSuccessor(S state, Integer input) {
349	return state.getSuccessor(input);	2✔
350	}
351
352	@Override
353	public Iterator<S> iterator() {
354	return bfsIterator();	×
355	}
356
357	@Override
358	public Collection<S> getStates() {
359	return bfsStates();	×
360	}
361
362	@Override
363	public int size() {
364	return countStates();	2✔
365	}
366
367	/**
368	* Counts the number of states in this PTA. Note that this method might require a complete traversal of the PTA.
369	*
370	* @return the number of states in the PTA reachable from the root state
371	*/
372
373	public @NonNegative int countStates() {
374	return Iterators.size(bfsIterator());	2✔
375	}
376
377	@Override
378	public S getInitialState() {
379	return getRoot();	2✔
380	}
381
382	@Override
383	public @Nullable PTATransition<S> getTransition(S state, Integer input) {
384	if (input == null \|\| state.getSuccessor(input) == null) {	2✔
385	return null;	2✔
386	}
387
388	return new PTATransition<>(state, input);	2✔
389	}
390
391	@Override
392	public SP getStateProperty(S state) {
393	return state.getStateProperty();	1✔
394	}
395
396	@Override
397	public TP getTransitionProperty(PTATransition<S> transition) {
398	return transition.getSource().getTransProperty(transition.getIndex());	×
399	}
400	}

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