19967145117

Committed 05 Dec 2025 03:09PM UTC coverage: 92.796% (+0.03%) from 92.771%

Build # 19967145117

Build Type

push

github

Committed by

mtf90

Commit Message

lassos: cleanup type information

Run Details

5 of 5 new or added lines in 1 file covered. (100.0%)

1 existing line in 1 file now uncovered.

17210 of 18546 relevant lines covered (92.8%)

1.72 hits per line

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

84.21

/core/src/main/java/net/automatalib/modelchecking/impl/AbstractLasso.java

/* Copyright (C) 2013-2025 TU Dortmund University
 * This file is part of AutomataLib <https://automatalib.net>.
 *
 * 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 net.automatalib.modelchecking.impl;

import java.util.Collection;
import java.util.HashMap;
import java.util.Map;
import java.util.Objects;
import java.util.SortedSet;
import java.util.TreeSet;

import net.automatalib.alphabet.Alphabet;
import net.automatalib.alphabet.impl.Alphabets;
import net.automatalib.automaton.concept.DetOutputAutomaton;
import net.automatalib.common.util.collection.CollectionUtil;
import net.automatalib.modelchecking.Lasso;
import net.automatalib.ts.simple.SimpleDTS;
import net.automatalib.word.Word;
import net.automatalib.word.WordBuilder;
import org.checkerframework.checker.nullness.qual.Nullable;

public abstract class AbstractLasso<I, D> implements Lasso<I, D> {

    public static final String NO_LASSO = "Automaton is not lasso shaped";

    private final Word<I> word;
    private final Word<I> loop;
    private final Word<I> prefix;
    private final D output;
    private final Alphabet<I> inputAlphabet;
    private final int unfolds;
    private final SortedSet<Integer> loopBeginIndices = new TreeSet<>();
    private final DetOutputAutomaton<?, I, ?, D> automaton;

    /**
     * Constructs a finite representation of a given automaton (that contains a lasso), by unrolling the loop
     * {@code unfoldTimes}.
     *
     * @param automaton
     *         the automaton containing the lasso.
     * @param inputs
     *         the input alphabet.
     * @param unfoldTimes
     *         the number of times the loop needs to be unrolled, must be {@code > 0}.
     * @param <S>
     *         the state type
     */
    public <S> AbstractLasso(DetOutputAutomaton<S, I, ?, D> automaton,
                             Collection<? extends I> inputs,
                             int unfoldTimes) {
        this(automaton, validateLassoShape(automaton, inputs, unfoldTimes), inputs, unfoldTimes);
    }

    // utility constructor to prevent finalizer attacks, see SEI CERT Rule OBJ-11
    private <S> AbstractLasso(DetOutputAutomaton<S, I, ?, D> automaton,
                              S init,
                              Collection<? extends I> inputs,
                              int unfoldTimes) {
        // save the original automaton
        this.automaton = automaton;

        this.unfolds = unfoldTimes;

        // construct the input alphabet
        inputAlphabet = Alphabets.fromCollection(inputs);

        // create a map for the visited states
        final Map<S, Integer> states = new HashMap<>();

        // create a WordBuilder, for the finite representation of the lasso
        final WordBuilder<I> wb = new WordBuilder<>();

        // start visiting the initial state
        S current = init;

        // index for the current state
        int i = 0;
        do {
            // create a mapping from the current state to the state index
            states.put(current, i++);

            // find the input that leads to the next state
            for (I in : inputAlphabet) {
                final S succ = automaton.getSuccessor(current, in);
                if (succ != null) {
                    // append the input to the finite representation
                    wb.append(in);

                    // continue with the next state.
                    current = succ;
                    break;
                }
            }
        } while (!states.containsKey(current));

        // save the state index at which the loop begins
        final int loopBegin = states.get(current);

        // determine the loop of the lasso
        loop = wb.toWord(loopBegin, wb.size());

        // determine the prefix of the lasso
        prefix = wb.toWord(0, loopBegin);

        // append the loop several times to the finite representation
        for (int u = 1; u < unfoldTimes; u++) {
            wb.append(loop);
        }

        // store the entire finite representation of the lasso
        word = wb.toWord();

        // store the finite representation of output of the lasso
        output = automaton.computeOutput(word);

        // store all the symbol indices after which the beginning of the loop is visited.
        for (int l = prefix.length(); l <= word.length(); l += loop.length()) {
            loopBeginIndices.add(l);
        }
    }

    @Override
    public DetOutputAutomaton<?, I, ?, D> getAutomaton() {
        return automaton;
    }

    @Override
    public int getUnfolds() {
        return unfolds;
    }

    @Override
    public Word<I> getWord() {
        return word;
    }

    @Override
    public Word<I> getLoop() {
        return loop;
    }

    @Override
    public Word<I> getPrefix() {
        return prefix;
    }

    @Override
    public D getOutput() {
        return output;
    }

    @Override
    public SortedSet<Integer> getLoopBeginIndices() {
        return loopBeginIndices;
    }

    @Override
    public Integer getInitialState() {
        return 0;
    }

    /**
     * Get the successor state of a given state, or {@code null} when no such successor exists.
     *
     * @see SimpleDTS#getSuccessor(Object, Object)
     */
    @Override
    public @Nullable Integer getSuccessor(Integer state, I input) {
        final Integer result;
        if (state < word.length() && Objects.equals(input, word.getSymbol(state))) {
            result = state + 1;
        } else {
            result = null;
        }

        return result;
    }

    @Override
    public Collection<Integer> getStates() {
        return CollectionUtil.intRange(0, word.length());
    }

    /**
     * Gets the input alphabet of this automaton.
     *
     * @return the Alphabet.
     */
    @Override
    public Alphabet<I> getInputAlphabet() {
        return inputAlphabet;
    }

    @Override
    public @Nullable Integer getTransition(Integer state, I input) {
        return getSuccessor(state, input);
    }

    private static <S, I, D> S validateLassoShape(DetOutputAutomaton<S, I, ?, D> automaton,
                                                  Collection<? extends I> inputs,
                                                  int unfoldTimes) {
        if (unfoldTimes <= 0) {
            throw new AssertionError();
        }

        final S init = automaton.getInitialState();
        if (init == null) {
            throw new IllegalArgumentException(NO_LASSO);
        }

        states:
        for (S s : automaton) {
            for (I i : inputs) {
                if (automaton.getSuccessor(s, i) != null) {
                    continue states;
                }
            }
            throw new IllegalArgumentException(NO_LASSO);
        }

        return init;
    }
}

1	/* Copyright (C) 2013-2025 TU Dortmund University
2	* This file is part of AutomataLib <https://automatalib.net>.
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 net.automatalib.modelchecking.impl;
17
18	import java.util.Collection;
19	import java.util.HashMap;
20	import java.util.Map;
21	import java.util.Objects;
22	import java.util.SortedSet;
23	import java.util.TreeSet;
24
25	import net.automatalib.alphabet.Alphabet;
26	import net.automatalib.alphabet.impl.Alphabets;
27	import net.automatalib.automaton.concept.DetOutputAutomaton;
28	import net.automatalib.common.util.collection.CollectionUtil;
29	import net.automatalib.modelchecking.Lasso;
30	import net.automatalib.ts.simple.SimpleDTS;
31	import net.automatalib.word.Word;
32	import net.automatalib.word.WordBuilder;
33	import org.checkerframework.checker.nullness.qual.Nullable;
34
35	public abstract class AbstractLasso<I, D> implements Lasso<I, D> {
36
37	public static final String NO_LASSO = "Automaton is not lasso shaped";
38
39	private final Word<I> word;
40	private final Word<I> loop;
41	private final Word<I> prefix;
42	private final D output;
43	private final Alphabet<I> inputAlphabet;
44	private final int unfolds;
45	private final SortedSet<Integer> loopBeginIndices = new TreeSet<>();	2✔
46	private final DetOutputAutomaton<?, I, ?, D> automaton;
47
48	/**
49	* Constructs a finite representation of a given automaton (that contains a lasso), by unrolling the loop
50	* {@code unfoldTimes}.
51	*
52	* @param automaton
53	* the automaton containing the lasso.
54	* @param inputs
55	* the input alphabet.
56	* @param unfoldTimes
57	* the number of times the loop needs to be unrolled, must be {@code > 0}.
58	* @param <S>
59	* the state type
60	*/
61	public <S> AbstractLasso(DetOutputAutomaton<S, I, ?, D> automaton,
62	Collection<? extends I> inputs,
63	int unfoldTimes) {
64	this(automaton, validateLassoShape(automaton, inputs, unfoldTimes), inputs, unfoldTimes);	2✔
65	}	2✔
66
67	// utility constructor to prevent finalizer attacks, see SEI CERT Rule OBJ-11
68	private <S> AbstractLasso(DetOutputAutomaton<S, I, ?, D> automaton,
69	S init,
70	Collection<? extends I> inputs,
71	int unfoldTimes) {	2✔
72	// save the original automaton
73	this.automaton = automaton;	2✔
74
75	this.unfolds = unfoldTimes;	2✔
76
77	// construct the input alphabet
78	inputAlphabet = Alphabets.fromCollection(inputs);	2✔
79
80	// create a map for the visited states
81	final Map<S, Integer> states = new HashMap<>();	2✔
82
83	// create a WordBuilder, for the finite representation of the lasso
84	final WordBuilder<I> wb = new WordBuilder<>();	2✔
85
86	// start visiting the initial state
87	S current = init;	2✔
88
89	// index for the current state
90	int i = 0;	2✔
91	do {
92	// create a mapping from the current state to the state index
93	states.put(current, i++);	2✔
94
95	// find the input that leads to the next state
96	for (I in : inputAlphabet) {	2✔
97	final S succ = automaton.getSuccessor(current, in);	2✔
98	if (succ != null) {	2✔
99	// append the input to the finite representation
100	wb.append(in);	2✔
101
102	// continue with the next state.
103	current = succ;	2✔
104	break;	2✔
105	}
106	}	1✔
107	} while (!states.containsKey(current));	2✔
108
109	// save the state index at which the loop begins
110	final int loopBegin = states.get(current);	2✔
111
112	// determine the loop of the lasso
113	loop = wb.toWord(loopBegin, wb.size());	2✔
114
115	// determine the prefix of the lasso
116	prefix = wb.toWord(0, loopBegin);	2✔
117
118	// append the loop several times to the finite representation
119	for (int u = 1; u < unfoldTimes; u++) {	2✔
120	wb.append(loop);	1✔
121	}
122
123	// store the entire finite representation of the lasso
124	word = wb.toWord();	2✔
125
126	// store the finite representation of output of the lasso
127	output = automaton.computeOutput(word);	2✔
128
129	// store all the symbol indices after which the beginning of the loop is visited.
130	for (int l = prefix.length(); l <= word.length(); l += loop.length()) {	2✔
131	loopBeginIndices.add(l);	2✔
132	}
133	}	2✔
134
135	@Override
136	public DetOutputAutomaton<?, I, ?, D> getAutomaton() {
137	return automaton;	×
138	}
139
140	@Override
141	public int getUnfolds() {
142	return unfolds;	×
143	}
144
145	@Override
146	public Word<I> getWord() {
147	return word;	2✔
148	}
149
150	@Override
151	public Word<I> getLoop() {
152	return loop;	2✔
153	}
154
155	@Override
156	public Word<I> getPrefix() {
157	return prefix;	2✔
158	}
159
160	@Override
161	public D getOutput() {
162	return output;	2✔
163	}
164
165	@Override
166	public SortedSet<Integer> getLoopBeginIndices() {
167	return loopBeginIndices;	2✔
168	}
169
170	@Override
171	public Integer getInitialState() {
172	return 0;	1✔
173	}
174
175	/**
176	* Get the successor state of a given state, or {@code null} when no such successor exists.
177	*
178	* @see SimpleDTS#getSuccessor(Object, Object)
179	*/
180	@Override
181	public @Nullable Integer getSuccessor(Integer state, I input) {
182	final Integer result;
183	if (state < word.length() && Objects.equals(input, word.getSymbol(state))) {	1✔
184	result = state + 1;	1✔
185	} else {
186	result = null;	×
187	}
188
189	return result;	1✔
190	}
191
192	@Override
193	public Collection<Integer> getStates() {
194	return CollectionUtil.intRange(0, word.length());	×
195	}
196
197	/**
198	* Gets the input alphabet of this automaton.
199	*
200	* @return the Alphabet.
201	*/
202	@Override
203	public Alphabet<I> getInputAlphabet() {
204	return inputAlphabet;	×
205	}
206
207	@Override
208	public @Nullable Integer getTransition(Integer state, I input) {
209	return getSuccessor(state, input);	×
210	}
211
212	private static <S, I, D> S validateLassoShape(DetOutputAutomaton<S, I, ?, D> automaton,
213	Collection<? extends I> inputs,
214	int unfoldTimes) {
215	if (unfoldTimes <= 0) {	2✔
216	throw new AssertionError();	×
217	}
218
219	final S init = automaton.getInitialState();	2✔
220	if (init == null) {	2✔
UNCOV 221	throw new IllegalArgumentException(NO_LASSO);	×
222	}
223
224	states:
225	for (S s : automaton) {	2✔
226	for (I i : inputs) {	2✔
227	if (automaton.getSuccessor(s, i) != null) {	2✔
228	continue states;	2✔
229	}
230	}	1✔
231	throw new IllegalArgumentException(NO_LASSO);	×
232	}
233
234	return init;	2✔
235	}
236	}

LearnLib / automatalib / 19967145117

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