12651580329

Committed 07 Jan 2025 12:29PM UTC coverage: 91.569% (+0.03%) from 91.542%

Build # 12651580329

Build Type

push

github

Committed by

web-flow

Commit Message

Update dependencies (#85)

* bump basic dependency versions

* bump checkstyle + cleanups

* bump spotbugs + cleanups

* bump pmd + cleanups

* bump checkerframework + cleanups

* some more cleanups

* ExceptionUtil: support nulls

* improve comments

* cleanup naming + formatting

* formatting

* formatting

* do not fail on javadoc warnings

completness of documentation is now checked by checkstyle and we would have to disable failing anyways when moving on to JDK 17

Run Details

192 of 217 new or added lines in 63 files covered. (88.48%)

4 existing lines in 4 files now uncovered.

16573 of 18099 relevant lines covered (91.57%)

1.69 hits per line

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

83.93

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

/* Copyright (C) 2013-2024 TU Dortmund University
 * This file is part of AutomataLib, http://www.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.NonNull;
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(validateLassoShape(automaton, inputs, unfoldTimes), automaton, inputs, unfoldTimes);
    }

    // utility constructor to prevent finalizer attacks, see SEI CERT Rule OBJ-11
    @SuppressWarnings("PMD.UnusedFormalParameter")
    private <S> AbstractLasso(boolean valid,
                              DetOutputAutomaton<S, I, ?, D> automaton,
                              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
        @SuppressWarnings("nullness") // we have checked non-nullness of the initial state
        @NonNull S current = automaton.getInitialState();

        // 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> boolean validateLassoShape(DetOutputAutomaton<S, I, ?, D> automaton,
                                                        Collection<? extends I> inputs,
                                                        int unfoldTimes) {
        if (unfoldTimes <= 0) {
            throw new AssertionError();
        }

        if (automaton.getInitialState() == 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 true;
    }
}

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

LearnLib / automatalib / 12651580329

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