29622048893

Committed 17 Jul 2026 11:59PM UTC coverage: 92.904% (-0.1%) from 93.039%

Build # 29622048893

Build Type

Pull #103

github

Committed by

web-flow

Commit Message

Merge 8e66953a6 into edbbaaaa4

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

Coverage Stats

283 of 329 new or added lines in 48 files covered. (86.02%)

5 existing lines in 2 files now uncovered.

17595 of 18939 relevant lines covered (92.9%)

1.72 hits per line

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

11.76

/api/src/main/java/net/automatalib/automaton/vpa/SEVPA.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 java.util.ArrayList;
import java.util.Collection;
import java.util.Collections;
import java.util.List;

import net.automatalib.alphabet.VPAlphabet;
import net.automatalib.automaton.UniversalAutomaton;
import net.automatalib.automaton.concept.InitialState;
import net.automatalib.automaton.concept.InputAlphabetHolder;
import net.automatalib.automaton.concept.SuffixOutput;
import net.automatalib.automaton.vpa.SEVPAGraphView.SevpaViewEdge;
import net.automatalib.graph.Graph;
import net.automatalib.graph.concept.GraphViewable;
import net.automatalib.semantic.DeterministicSemantics;
import net.automatalib.ts.acceptor.DeterministicAcceptorTS;
import org.checkerframework.checker.nullness.qual.Nullable;

/**
 * Interface for k-SEVPAs (k-module single entry visibly push-down automata), a visibly push-down automaton of specific
 * structure and semantics. Additionally -- unless specified other by an implementation -- this interface only accepts
 * well-matched words.
 * <p>
 * For more information on the semantics of VPAs see e.g. <a href="https://doi.org/10.1007/11523468_89">Congruences for
 * Visibly Pushdown Languages</a> by Alur, Kumar, Madhusudan and Viswanathan.
 * <p>
 * Note that this formalism integrates into the hierarchy of a non-deterministic {@link UniversalAutomaton} because a
 * single return symbol may identify multiple transitions depending on the current top-of-stack symbol. Via
 * {@link #getInternalSuccessor(Object, Object)} and {@link #getReturnSuccessor(Object, Object, int)}, these information
 * can be accessed deterministically. As a result, its <em>states</em> act more like locations than actual states. A
 * (deterministic, infinite-state) semantics view can be obtained via the {@link #getSemantics()} method.
 * <p>
 * For convenience, this type also implements {@link SuffixOutput} which delegates computation directly to its
 * {@link DeterministicSemantics semantics}.
 *
 * @param <L>
 *         location type
 * @param <I>
 *         input symbol type
 */
public interface SEVPA<L, I> extends UniversalAutomaton<L, I, L, Boolean, Void>,
                                     InitialState<L>,
                                     DeterministicSemantics,
                                     SuffixOutput<I, Boolean>,
                                     GraphViewable,
                                     InputAlphabetHolder<I> {

    @Override
    VPAlphabet<I> getInputAlphabet();

    L getModuleEntry(I callSym);

    int getNumStackSymbols();

    int encodeStackSym(L srcLoc, I callSym);

    @Nullable L getInternalSuccessor(L loc, I intSym);

    @Nullable L getReturnSuccessor(L loc, I retSym, int stackSym);

    @Override // do not allow a nullable initial state
    L getInitialState();

    @Override
    default Void getTransitionProperty(L transition) {
        return null;
    }

    @Override
    default Collection<L> getTransitions(L state, I input) {
        final VPAlphabet<I> alphabet = getInputAlphabet();
        return switch (alphabet.getSymbolType(input)) {
            case CALL:
                yield Collections.singleton(getModuleEntry(input));
            case INTERNAL:
                final L iSucc = getInternalSuccessor(state, input);
                yield iSucc == null ? Collections.emptyList() : Collections.singleton(iSucc);
            case RETURN:
                final int symbols = getNumStackSymbols();
                final List<L> result = new ArrayList<>(symbols);
                for (int i = 0; i < symbols; i++) {
                    final L rSucc = getReturnSuccessor(state, input, i);
                    if (rSucc != null) {
                        result.add(rSucc);
                    }
                }
                yield result;
        };
    }

    @Override
    default L getSuccessor(L transition) {
        return transition;
    }

    @Override
    default DeterministicAcceptorTS<State<L>, I> getSemantics() {
        return new SEVPASemantics<>(this);
    }

    @Override
    default Boolean computeSuffixOutput(Iterable<? extends I> prefix, Iterable<? extends I> suffix) {
        return getSemantics().computeSuffixOutput(prefix, suffix);
    }

    @Override
    default Graph<L, SevpaViewEdge<L, I>> graphView() {
        return new SEVPAGraphView<>(this);
    }
}

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 java.util.ArrayList;
19	import java.util.Collection;
20	import java.util.Collections;
21	import java.util.List;
22
23	import net.automatalib.alphabet.VPAlphabet;
24	import net.automatalib.automaton.UniversalAutomaton;
25	import net.automatalib.automaton.concept.InitialState;
26	import net.automatalib.automaton.concept.InputAlphabetHolder;
27	import net.automatalib.automaton.concept.SuffixOutput;
28	import net.automatalib.automaton.vpa.SEVPAGraphView.SevpaViewEdge;
29	import net.automatalib.graph.Graph;
30	import net.automatalib.graph.concept.GraphViewable;
31	import net.automatalib.semantic.DeterministicSemantics;
32	import net.automatalib.ts.acceptor.DeterministicAcceptorTS;
33	import org.checkerframework.checker.nullness.qual.Nullable;
34
35	/**
36	* Interface for k-SEVPAs (k-module single entry visibly push-down automata), a visibly push-down automaton of specific
37	* structure and semantics. Additionally -- unless specified other by an implementation -- this interface only accepts
38	* well-matched words.
39	* <p>
40	* For more information on the semantics of VPAs see e.g. <a href="https://doi.org/10.1007/11523468_89">Congruences for
41	* Visibly Pushdown Languages</a> by Alur, Kumar, Madhusudan and Viswanathan.
42	* <p>
43	* Note that this formalism integrates into the hierarchy of a non-deterministic {@link UniversalAutomaton} because a
44	* single return symbol may identify multiple transitions depending on the current top-of-stack symbol. Via
45	* {@link #getInternalSuccessor(Object, Object)} and {@link #getReturnSuccessor(Object, Object, int)}, these information
46	* can be accessed deterministically. As a result, its <em>states</em> act more like locations than actual states. A
47	* (deterministic, infinite-state) semantics view can be obtained via the {@link #getSemantics()} method.
48	* <p>
49	* For convenience, this type also implements {@link SuffixOutput} which delegates computation directly to its
50	* {@link DeterministicSemantics semantics}.
51	*
52	* @param <L>
53	* location type
54	* @param <I>
55	* input symbol type
56	*/
57	public interface SEVPA<L, I> extends UniversalAutomaton<L, I, L, Boolean, Void>,
58	InitialState<L>,
59	DeterministicSemantics,
60	SuffixOutput<I, Boolean>,
61	GraphViewable,
62	InputAlphabetHolder<I> {
63
64	@Override
65	VPAlphabet<I> getInputAlphabet();
66
67	L getModuleEntry(I callSym);
68
69	int getNumStackSymbols();
70
71	int encodeStackSym(L srcLoc, I callSym);
72
73	@Nullable L getInternalSuccessor(L loc, I intSym);
74
75	@Nullable L getReturnSuccessor(L loc, I retSym, int stackSym);
76
77	@Override // do not allow a nullable initial state
78	L getInitialState();
79
80	@Override
81	default Void getTransitionProperty(L transition) {
NEW 82	return null;	×
83	}
84
85	@Override
86	default Collection<L> getTransitions(L state, I input) {
NEW 87	final VPAlphabet<I> alphabet = getInputAlphabet();	×
NEW 88	return switch (alphabet.getSymbolType(input)) {	×
89	case CALL:
NEW 90	yield Collections.singleton(getModuleEntry(input));	×
91	case INTERNAL:
NEW 92	final L iSucc = getInternalSuccessor(state, input);	×
NEW 93	yield iSucc == null ? Collections.emptyList() : Collections.singleton(iSucc);	×
94	case RETURN:
NEW 95	final int symbols = getNumStackSymbols();	×
NEW 96	final List<L> result = new ArrayList<>(symbols);	×
NEW 97	for (int i = 0; i < symbols; i++) {	×
NEW 98	final L rSucc = getReturnSuccessor(state, input, i);	×
NEW 99	if (rSucc != null) {	×
NEW 100	result.add(rSucc);	×
101	}
102	}
NEW 103	yield result;	×
104	};
105	}
106
107	@Override
108	default L getSuccessor(L transition) {
NEW 109	return transition;	×
110	}
111
112	@Override
113	default DeterministicAcceptorTS<State<L>, I> getSemantics() {
114	return new SEVPASemantics<>(this);	1✔
115	}
116
117	@Override
118	default Boolean computeSuffixOutput(Iterable<? extends I> prefix, Iterable<? extends I> suffix) {
NEW 119	return getSemantics().computeSuffixOutput(prefix, suffix);	×
120	}
121
122	@Override
123	default Graph<L, SevpaViewEdge<L, I>> graphView() {
124	return new SEVPAGraphView<>(this);	1✔
125	}
126	}

LearnLib / automatalib / 29622048893

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