13791485380

Committed 11 Mar 2025 02:53PM UTC coverage: 92.059% (-0.05%) from 92.108%

Build # 13791485380

Build Type

push

github

Committed by

mtf90

Commit Message

update changelog

Run Details

16601 of 18033 relevant lines covered (92.06%)

1.7 hits per line

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

98.4

/serialization/aut/src/main/java/net/automatalib/serialization/aut/InternalAUTParser.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.serialization.aut;

import java.io.BufferedReader;
import java.io.IOException;
import java.io.InputStream;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Map;
import java.util.Set;
import java.util.function.Function;

import net.automatalib.alphabet.Alphabet;
import net.automatalib.alphabet.impl.Alphabets;
import net.automatalib.automaton.AutomatonCreator;
import net.automatalib.automaton.MutableAutomaton;
import net.automatalib.common.util.HashUtil;
import net.automatalib.common.util.IOUtil;
import net.automatalib.exception.FormatException;
import net.automatalib.serialization.InputModelData;
import net.automatalib.serialization.InputModelDeserializer;
import org.checkerframework.checker.nullness.qual.Nullable;

class InternalAUTParser<I, T, @Nullable TP, A extends MutableAutomaton<Integer, I, T, ?, TP>>
        implements InputModelDeserializer<I, A> {

    private final Function<String, I> inputTransformer;
    private final AutomatonCreator<A, I> creator;
    private final Set<String> alphabetSymbols;
    private final Map<Integer, Map<String, Set<Integer>>> transitionMap;

    private int initialState;
    private int numStates;
    private int currentLine;
    private int currentPos;

    InternalAUTParser(Function<String, I> inputTransformer, AutomatonCreator<A, I> creator) {
        this.inputTransformer = inputTransformer;
        this.creator = creator;
        this.alphabetSymbols = new HashSet<>();
        this.transitionMap = new HashMap<>();
    }

    @Override
    public InputModelData<I, A> readModel(InputStream is) throws IOException, FormatException {

        try (BufferedReader br = new BufferedReader(IOUtil.asNonClosingUTF8Reader(is))) {
            // parsing
            parseHeader(br);
            while (parseTransition(br)) {
                // consume transitions
            }

            // automaton construction
            final Map<String, I> inputMap = new HashMap<>(HashUtil.capacity(this.alphabetSymbols.size()));
            for (String s : this.alphabetSymbols) {
                inputMap.put(s, inputTransformer.apply(s));
            }
            final Alphabet<I> alphabet = Alphabets.fromCollection(inputMap.values());

            final A result = creator.createAutomaton(alphabet, numStates);

            for (int i = 0; i < numStates; i++) {
                result.addState();
            }

            for (Map.Entry<Integer, Map<String, Set<Integer>>> outgoing : transitionMap.entrySet()) {
                final Integer src = outgoing.getKey();
                for (Map.Entry<String, Set<Integer>> targets : outgoing.getValue().entrySet()) {
                    final String input = targets.getKey();
                    final Set<Integer> tgts = targets.getValue();
                    for (Integer tgt : tgts) {
                        result.addTransition(src, inputMap.get(input), tgt, null);
                    }
                }
            }
            result.setInitial(initialState, true);

            return new InputModelData<>(result, alphabet);
        } finally {
            // cleanup
            initialState = 0;
            numStates = 0;
            currentLine = 0;
            currentPos = 0;
            alphabetSymbols.clear();
            transitionMap.clear();
        }
    }

    private void parseHeader(BufferedReader reader) throws IOException, FormatException {
        final String line = reader.readLine();

        if (line == null) {
            throw new FormatException(buildErrorMessage("Missing description"));
        }

        char[] currentLineContent = line.toCharArray();
        currentPos = 0;

        shiftToNextNonWhitespace(currentLineContent);
        verifyDesAndShift(currentLineContent);
        verifyLBracketAndShift(currentLineContent);
        initialState = parseNumberAndShift(currentLineContent);
        verifyCommaAndShift(currentLineContent);
        parseNumberAndShift(currentLineContent); // ignore number of transitions
        verifyCommaAndShift(currentLineContent);
        numStates = parseNumberAndShift(currentLineContent); // store number of states
        if (numStates < 1) {
            throw new FormatException("Number of states must be >= 1");
        }
        verifyRBracketAndShift(currentLineContent);
    }

    private boolean parseTransition(BufferedReader reader) throws IOException, FormatException {
        final String line = reader.readLine();

        if (line == null) {
            return false;
        }

        char[] currentLineContent = line.toCharArray();
        currentLine++;
        currentPos = 0;

        final int start;
        final String label;
        final int dest;

        shiftToNextNonWhitespace(currentLineContent);
        verifyLBracketAndShift(currentLineContent);
        start = parseNumberAndShift(currentLineContent);
        verifyCommaAndShift(currentLineContent);
        label = parseLabelAndShift(currentLineContent);
        verifyCommaAndShift(currentLineContent);
        dest = parseNumberAndShift(currentLineContent);
        verifyRBracketAndShift(currentLineContent);

        alphabetSymbols.add(label);
        transitionMap.computeIfAbsent(start, k -> new HashMap<>())
                     .computeIfAbsent(label, k -> new HashSet<>())
                     .add(dest);

        return true;
    }

    private void verifyDesAndShift(char[] currentLineContent) throws FormatException {

        if (currentLineContent[currentPos] != 'd' || currentLineContent[currentPos + 1] != 'e' ||
            currentLineContent[currentPos + 2] != 's') {
            throw new FormatException(buildErrorMessage("Missing 'des' keyword"));
        }

        currentPos += 3;
        shiftToNextNonWhitespace(currentLineContent);
    }

    private void verifyLBracketAndShift(char[] currentLineContent) throws FormatException {
        verifySymbolAndShift(currentLineContent, '(');
    }

    private void verifyRBracketAndShift(char[] currentLineContent) throws FormatException {
        verifySymbolAndShift(currentLineContent, ')');
    }

    private void verifyCommaAndShift(char[] currentLineContent) throws FormatException {
        verifySymbolAndShift(currentLineContent, ',');
    }

    private void verifySymbolAndShift(char[] currentLineContent, char symbol) throws FormatException {

        if (currentLineContent[currentPos] != symbol) {
            throw new FormatException(buildErrorMessage("Expected: " + symbol));
        }

        currentPos++;
        shiftToNextNonWhitespace(currentLineContent);
    }

    private void shiftToNextNonWhitespace(char[] currentLineContent) {
        while (currentPos < currentLineContent.length && Character.isWhitespace(currentLineContent[currentPos])) {
            currentPos++;
        }
    }

    private int parseNumberAndShift(char[] currentLineContent) throws FormatException {

        final StringBuilder sb = new StringBuilder();

        char sym = currentLineContent[currentPos];

        while (Character.isDigit(sym)) {
            sb.append(sym);
            currentPos++;
            sym = currentLineContent[currentPos];
        }

        if (sb.length() == 0) {
            throw new FormatException(buildErrorMessage("Expected a positive number"));
        }

        // forward pointer
        shiftToNextNonWhitespace(currentLineContent);
        return Integer.parseInt(sb.toString());
    }

    private String parseLabelAndShift(char[] currentLineContent) throws FormatException {

        if (currentLineContent[currentPos] == '"') {
            return parseQuotedLabelAndShift(currentLineContent);
        } else {
            return parseNormalLabelAndShift(currentLineContent);
        }
    }

    private String parseQuotedLabelAndShift(char[] currentLineContent) {
        int openingIndex = currentPos;
        int closingIndex = currentLineContent.length - 1;

        // find terminating "
        while (currentLineContent[closingIndex--] != '"') {
            // consume characters
        }

        // skip terminating " as well
        currentPos = closingIndex + 2;
        shiftToNextNonWhitespace(currentLineContent);

        return new String(currentLineContent, openingIndex + 1, closingIndex - openingIndex);
    }

    private String parseNormalLabelAndShift(char[] currentLineContent) throws FormatException {

        final char firstChar = currentLineContent[currentPos];

        if (currentLineContent[currentPos] == '*') {
            currentPos++;
            shiftToNextNonWhitespace(currentLineContent);
            return "*";
        } else if (Character.isLetter(firstChar)) {
            int startIdx = currentPos;

            while (isValidIdentifier(currentLineContent)) {
                currentPos++;
            }

            int endIdx = currentPos;

            shiftToNextNonWhitespace(currentLineContent);
            return new String(currentLineContent, startIdx, endIdx - startIdx);
        } else {
            throw new FormatException(buildErrorMessage("Invalid unquoted label"));
        }
    }

    private boolean isValidIdentifier(char[] currentLineContent) {
        final char currentChar = currentLineContent[currentPos];
        return Character.isLetterOrDigit(currentChar) || currentChar == '_';
    }

    private String buildErrorMessage(String desc) {
        return "In line " + currentLine + ", col " + currentPos + ": " + desc;
    }
}

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.serialization.aut;
17
18	import java.io.BufferedReader;
19	import java.io.IOException;
20	import java.io.InputStream;
21	import java.util.HashMap;
22	import java.util.HashSet;
23	import java.util.Map;
24	import java.util.Set;
25	import java.util.function.Function;
26
27	import net.automatalib.alphabet.Alphabet;
28	import net.automatalib.alphabet.impl.Alphabets;
29	import net.automatalib.automaton.AutomatonCreator;
30	import net.automatalib.automaton.MutableAutomaton;
31	import net.automatalib.common.util.HashUtil;
32	import net.automatalib.common.util.IOUtil;
33	import net.automatalib.exception.FormatException;
34	import net.automatalib.serialization.InputModelData;
35	import net.automatalib.serialization.InputModelDeserializer;
36	import org.checkerframework.checker.nullness.qual.Nullable;
37
38	class InternalAUTParser<I, T, @Nullable TP, A extends MutableAutomaton<Integer, I, T, ?, TP>>
39	implements InputModelDeserializer<I, A> {
40
41	private final Function<String, I> inputTransformer;
42	private final AutomatonCreator<A, I> creator;
43	private final Set<String> alphabetSymbols;
44	private final Map<Integer, Map<String, Set<Integer>>> transitionMap;
45
46	private int initialState;
47	private int numStates;
48	private int currentLine;
49	private int currentPos;
50
51	InternalAUTParser(Function<String, I> inputTransformer, AutomatonCreator<A, I> creator) {	2✔
52	this.inputTransformer = inputTransformer;	2✔
53	this.creator = creator;	2✔
54	this.alphabetSymbols = new HashSet<>();	2✔
55	this.transitionMap = new HashMap<>();	2✔
56	}	2✔
57
58	@Override
59	public InputModelData<I, A> readModel(InputStream is) throws IOException, FormatException {
60
61	try (BufferedReader br = new BufferedReader(IOUtil.asNonClosingUTF8Reader(is))) {	2✔
62	// parsing
63	parseHeader(br);	2✔
64	while (parseTransition(br)) {	2✔
65	// consume transitions
66	}
67
68	// automaton construction
69	final Map<String, I> inputMap = new HashMap<>(HashUtil.capacity(this.alphabetSymbols.size()));	2✔
70	for (String s : this.alphabetSymbols) {	2✔
71	inputMap.put(s, inputTransformer.apply(s));	2✔
72	}	2✔
73	final Alphabet<I> alphabet = Alphabets.fromCollection(inputMap.values());	2✔
74
75	final A result = creator.createAutomaton(alphabet, numStates);	2✔
76
77	for (int i = 0; i < numStates; i++) {	2✔
78	result.addState();	2✔
79	}
80
81	for (Map.Entry<Integer, Map<String, Set<Integer>>> outgoing : transitionMap.entrySet()) {	2✔
82	final Integer src = outgoing.getKey();	2✔
83	for (Map.Entry<String, Set<Integer>> targets : outgoing.getValue().entrySet()) {	2✔
84	final String input = targets.getKey();	2✔
85	final Set<Integer> tgts = targets.getValue();	2✔
86	for (Integer tgt : tgts) {	2✔
87	result.addTransition(src, inputMap.get(input), tgt, null);	2✔
88	}	2✔
89	}	2✔
90	}	2✔
91	result.setInitial(initialState, true);	2✔
92
93	return new InputModelData<>(result, alphabet);	2✔
94	} finally {
95	// cleanup
96	initialState = 0;	2✔
97	numStates = 0;	2✔
98	currentLine = 0;	2✔
99	currentPos = 0;	2✔
100	alphabetSymbols.clear();	2✔
101	transitionMap.clear();	2✔
102	}
103	}
104
105	private void parseHeader(BufferedReader reader) throws IOException, FormatException {
106	final String line = reader.readLine();	2✔
107
108	if (line == null) {	2✔
109	throw new FormatException(buildErrorMessage("Missing description"));	×
110	}
111
112	char[] currentLineContent = line.toCharArray();	2✔
113	currentPos = 0;	2✔
114
115	shiftToNextNonWhitespace(currentLineContent);	2✔
116	verifyDesAndShift(currentLineContent);	2✔
117	verifyLBracketAndShift(currentLineContent);	2✔
118	initialState = parseNumberAndShift(currentLineContent);	2✔
119	verifyCommaAndShift(currentLineContent);	2✔
120	parseNumberAndShift(currentLineContent); // ignore number of transitions	2✔
121	verifyCommaAndShift(currentLineContent);	2✔
122	numStates = parseNumberAndShift(currentLineContent); // store number of states	2✔
123	if (numStates < 1) {	2✔
124	throw new FormatException("Number of states must be >= 1");	2✔
125	}
126	verifyRBracketAndShift(currentLineContent);	2✔
127	}	2✔
128
129	private boolean parseTransition(BufferedReader reader) throws IOException, FormatException {
130	final String line = reader.readLine();	2✔
131
132	if (line == null) {	2✔
133	return false;	2✔
134	}
135
136	char[] currentLineContent = line.toCharArray();	2✔
137	currentLine++;	2✔
138	currentPos = 0;	2✔
139
140	final int start;
141	final String label;
142	final int dest;
143
144	shiftToNextNonWhitespace(currentLineContent);	2✔
145	verifyLBracketAndShift(currentLineContent);	2✔
146	start = parseNumberAndShift(currentLineContent);	2✔
147	verifyCommaAndShift(currentLineContent);	2✔
148	label = parseLabelAndShift(currentLineContent);	2✔
149	verifyCommaAndShift(currentLineContent);	2✔
150	dest = parseNumberAndShift(currentLineContent);	2✔
151	verifyRBracketAndShift(currentLineContent);	2✔
152
153	alphabetSymbols.add(label);	2✔
154	transitionMap.computeIfAbsent(start, k -> new HashMap<>())	2✔
155	.computeIfAbsent(label, k -> new HashSet<>())	2✔
156	.add(dest);	2✔
157
158	return true;	2✔
159	}
160
161	private void verifyDesAndShift(char[] currentLineContent) throws FormatException {
162
163	if (currentLineContent[currentPos] != 'd' \|\| currentLineContent[currentPos + 1] != 'e' \|\|	2✔
164	currentLineContent[currentPos + 2] != 's') {
165	throw new FormatException(buildErrorMessage("Missing 'des' keyword"));	2✔
166	}
167
168	currentPos += 3;	2✔
169	shiftToNextNonWhitespace(currentLineContent);	2✔
170	}	2✔
171
172	private void verifyLBracketAndShift(char[] currentLineContent) throws FormatException {
173	verifySymbolAndShift(currentLineContent, '(');	2✔
174	}	2✔
175
176	private void verifyRBracketAndShift(char[] currentLineContent) throws FormatException {
177	verifySymbolAndShift(currentLineContent, ')');	2✔
178	}	2✔
179
180	private void verifyCommaAndShift(char[] currentLineContent) throws FormatException {
181	verifySymbolAndShift(currentLineContent, ',');	2✔
182	}	2✔
183
184	private void verifySymbolAndShift(char[] currentLineContent, char symbol) throws FormatException {
185
186	if (currentLineContent[currentPos] != symbol) {	2✔
187	throw new FormatException(buildErrorMessage("Expected: " + symbol));	2✔
188	}
189
190	currentPos++;	2✔
191	shiftToNextNonWhitespace(currentLineContent);	2✔
192	}	2✔
193
194	private void shiftToNextNonWhitespace(char[] currentLineContent) {
195	while (currentPos < currentLineContent.length && Character.isWhitespace(currentLineContent[currentPos])) {	2✔
196	currentPos++;	2✔
197	}
198	}	2✔
199
200	private int parseNumberAndShift(char[] currentLineContent) throws FormatException {
201
202	final StringBuilder sb = new StringBuilder();	2✔
203
204	char sym = currentLineContent[currentPos];	2✔
205
206	while (Character.isDigit(sym)) {	2✔
207	sb.append(sym);	2✔
208	currentPos++;	2✔
209	sym = currentLineContent[currentPos];	2✔
210	}
211
212	if (sb.length() == 0) {	2✔
213	throw new FormatException(buildErrorMessage("Expected a positive number"));	2✔
214	}
215
216	// forward pointer
217	shiftToNextNonWhitespace(currentLineContent);	2✔
218	return Integer.parseInt(sb.toString());	2✔
219	}
220
221	private String parseLabelAndShift(char[] currentLineContent) throws FormatException {
222
223	if (currentLineContent[currentPos] == '"') {	2✔
224	return parseQuotedLabelAndShift(currentLineContent);	2✔
225	} else {
226	return parseNormalLabelAndShift(currentLineContent);	2✔
227	}
228	}
229
230	private String parseQuotedLabelAndShift(char[] currentLineContent) {
231	int openingIndex = currentPos;	2✔
232	int closingIndex = currentLineContent.length - 1;	2✔
233
234	// find terminating "
235	while (currentLineContent[closingIndex--] != '"') {	2✔
236	// consume characters
237	}
238
239	// skip terminating " as well
240	currentPos = closingIndex + 2;	2✔
241	shiftToNextNonWhitespace(currentLineContent);	2✔
242
243	return new String(currentLineContent, openingIndex + 1, closingIndex - openingIndex);	2✔
244	}
245
246	private String parseNormalLabelAndShift(char[] currentLineContent) throws FormatException {
247
248	final char firstChar = currentLineContent[currentPos];	2✔
249
250	if (currentLineContent[currentPos] == '*') {	2✔
251	currentPos++;	2✔
252	shiftToNextNonWhitespace(currentLineContent);	2✔
253	return "*";	2✔
254	} else if (Character.isLetter(firstChar)) {	2✔
255	int startIdx = currentPos;	2✔
256
257	while (isValidIdentifier(currentLineContent)) {	2✔
258	currentPos++;	2✔
259	}
260
261	int endIdx = currentPos;	2✔
262
263	shiftToNextNonWhitespace(currentLineContent);	2✔
264	return new String(currentLineContent, startIdx, endIdx - startIdx);	2✔
265	} else {
266	throw new FormatException(buildErrorMessage("Invalid unquoted label"));	×
267	}
268	}
269
270	private boolean isValidIdentifier(char[] currentLineContent) {
271	final char currentChar = currentLineContent[currentPos];	2✔
272	return Character.isLetterOrDigit(currentChar) \|\| currentChar == '_';	2✔
273	}
274
275	private String buildErrorMessage(String desc) {
276	return "In line " + currentLine + ", col " + currentPos + ": " + desc;	2✔
277	}
278	}

LearnLib / automatalib / 13791485380

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