12650654883

Committed 07 Jan 2025 11:26AM UTC coverage: 91.569%. First build

Build # 12650654883

Build Type

Pull #85

github

Committed by

web-flow

Commit Message

Merge 2499df5ae into d156e0830

Pull Request Pull Request #85: Update dependencies

Run Details

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

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 / 12650654883

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