28013097648

Committed 23 Jun 2026 08:30AM UTC coverage: 92.876% (-0.1%) from 93.007%

Build # 28013097648

Build Type

Pull #103

github

Committed by

web-flow

Commit Message

Merge 1553bac46 into 87b9d660b

Pull Request Pull Request #103: Distinguish between structural and semantic interpretations of automata

Coverage Stats

268 of 313 new or added lines in 46 files covered. (85.62%)

5 existing lines in 2 files now uncovered.

17560 of 18907 relevant lines covered (92.88%)

1.72 hits per line

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

95.65

/api/src/main/java/net/automatalib/automaton/vpa/SEVPASemantics.java

/* Copyright (C) 2013-2026 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.automaton.vpa;

import net.automatalib.alphabet.VPAlphabet;
import net.automatalib.ts.acceptor.DeterministicAcceptorTS;
import org.checkerframework.checker.nullness.qual.Nullable;

public class SEVPASemantics<L, I> implements DeterministicAcceptorTS<State<L>, I> {

    private final SEVPA<L, I> sevpa;
    private final VPAlphabet<I> alphabet;

    public SEVPASemantics(SEVPA<L, I> sevpa) {
        this.sevpa = sevpa;
        this.alphabet = sevpa.getInputAlphabet();
    }

    @Override
    public @Nullable State<L> getTransition(State<L> state, I input) {
        final L loc = state.getLocation();
        return switch (alphabet.getSymbolType(input)) {
            case CALL:
                final int newStackElem = sevpa.encodeStackSym(loc, input);
                yield new State<>(sevpa.getModuleEntry(input),
                                  StackContents.push(newStackElem, state.getStackContents()));
            case RETURN: {
                final StackContents contents = state.getStackContents();
                if (contents == null) {
                    yield null;
                }
                final int stackElem = contents.peek();
                final L succ = sevpa.getReturnSuccessor(loc, input, stackElem);
                if (succ == null) {
                    yield null;
                }
                yield new State<>(succ, contents.pop());
            }
            case INTERNAL: {
                final L succ = sevpa.getInternalSuccessor(loc, input);
                if (succ == null) {
                    yield null;
                }
                yield new State<>(succ, state.getStackContents());
            }
        };
    }

    @Override
    public boolean isAccepting(State<L> state) {
        return sevpa.getStateProperty(state.getLocation()) && state.getStackContents() == null;
    }

    @Override
    public State<L> getInitialState() {
        return new State<>(sevpa.getInitialState(), null);
    }
}

1	/* Copyright (C) 2013-2026 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.automaton.vpa;
17
18	import net.automatalib.alphabet.VPAlphabet;
19	import net.automatalib.ts.acceptor.DeterministicAcceptorTS;
20	import org.checkerframework.checker.nullness.qual.Nullable;
21
22	public class SEVPASemantics<L, I> implements DeterministicAcceptorTS<State<L>, I> {
23
24	private final SEVPA<L, I> sevpa;
25	private final VPAlphabet<I> alphabet;
26
27	public SEVPASemantics(SEVPA<L, I> sevpa) {	1✔
28	this.sevpa = sevpa;	1✔
29	this.alphabet = sevpa.getInputAlphabet();	1✔
30	}	1✔
31
32	@Override
33	public @Nullable State<L> getTransition(State<L> state, I input) {
34	final L loc = state.getLocation();	1✔
35	return switch (alphabet.getSymbolType(input)) {	1✔
36	case CALL:
37	final int newStackElem = sevpa.encodeStackSym(loc, input);	1✔
38	yield new State<>(sevpa.getModuleEntry(input),	1✔
39	StackContents.push(newStackElem, state.getStackContents()));	1✔
40	case RETURN: {
41	final StackContents contents = state.getStackContents();	1✔
42	if (contents == null) {	1✔
43	yield null;	1✔
44	}
45	final int stackElem = contents.peek();	1✔
46	final L succ = sevpa.getReturnSuccessor(loc, input, stackElem);	1✔
47	if (succ == null) {	1✔
48	yield null;	1✔
49	}
50	yield new State<>(succ, contents.pop());	1✔
51	}
52	case INTERNAL: {
53	final L succ = sevpa.getInternalSuccessor(loc, input);	1✔
54	if (succ == null) {	1✔
NEW 55	yield null;	×
56	}
57	yield new State<>(succ, state.getStackContents());	1✔
58	}
59	};
60	}
61
62	@Override
63	public boolean isAccepting(State<L> state) {
64	return sevpa.getStateProperty(state.getLocation()) && state.getStackContents() == null;	1✔
65	}
66
67	@Override
68	public State<L> getInitialState() {
69	return new State<>(sevpa.getInitialState(), null);	1✔
70	}
71	}

LearnLib / automatalib / 28013097648

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