19995144613

Committed 06 Dec 2025 10:24PM UTC coverage: 92.834% (+0.04%) from 92.796%

Build # 19995144613

Build Type

push

github

Committed by

mtf90

Commit Message

simplify procedural implementations

since the output semantics now better handle partial systems, get rid of explicit sink management

Run Details

42 of 45 new or added lines in 5 files covered. (93.33%)

4 existing lines in 4 files now uncovered.

17191 of 18518 relevant lines covered (92.83%)

1.72 hits per line

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

97.73

/core/src/main/java/net/automatalib/automaton/procedural/impl/StackSPA.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.automaton.procedural.impl;

import java.util.Collections;
import java.util.Map;
import java.util.Objects;

import net.automatalib.alphabet.ProceduralInputAlphabet;
import net.automatalib.automaton.fsa.DFA;
import net.automatalib.automaton.procedural.SPA;
import net.automatalib.ts.simple.SimpleDTS;
import org.checkerframework.checker.nullness.qual.Nullable;

/**
 * A stack-based implementation for the (instrumented) language of an {@link SPA}.
 *
 * @param <S>
 *         procedural state type
 * @param <I>
 *         input symbol type
 */
public class StackSPA<S, I> implements SPA<StackState<S, I, DFA<S, I>>, I>, SimpleDTS<StackState<S, I, DFA<S, I>>, I> {

    private final ProceduralInputAlphabet<I> alphabet;
    private final @Nullable I initialCall;
    private final Map<I, DFA<S, I>> procedures;

    // cast is fine, because we make sure to only query states belonging to the respective procedures
    @SuppressWarnings("unchecked")
    public StackSPA(ProceduralInputAlphabet<I> alphabet,
                    @Nullable I initialCall,
                    Map<I, ? extends DFA<? extends S, I>> procedures) {
        this.alphabet = alphabet;
        this.initialCall = initialCall;
        this.procedures = (Map<I, DFA<S, I>>) procedures;
    }

    @Override
    public StackState<S, I, DFA<S, I>> getTransition(StackState<S, I, DFA<S, I>> state, I input) {
        if (state.isTerm()) {
            return null;
        } else if (alphabet.isInternalSymbol(input)) {
            if (state.isInit()) {
                return null;
            }

            final DFA<S, I> model = state.getProcedure();
            final S next = model.getTransition(state.getCurrentState(), input);

            // undefined internal transition
            if (next == null) {
                return null;
            }

            return state.updateState(next);
        } else if (alphabet.isCallSymbol(input)) {
            if (state.isInit() && !Objects.equals(this.initialCall, input)) {
                return null;
            }

            final DFA<S, I> model = this.procedures.get(input);

            if (model == null) {
                return null;
            }

            final S next = model.getInitialState();

            if (next == null) {
                return null;
            }

            // store the procedural successor in the stack so that we don't need to look it up on return symbols
            final StackState<S, I, DFA<S, I>> returnState;
            if (state.isInit()) {
                returnState = StackState.term();
            } else {
                final S succ = state.getProcedure().getSuccessor(state.getCurrentState(), input);
                if (succ == null) {
                    return null;
                }
                returnState = state.updateState(succ);
            }

            return returnState.push(model, next);
        } else if (alphabet.isReturnSymbol(input)) {
            if (state.isInit()) {
                return null;
            }

            // if we returned the state before, we checked that a procedure is available
            final DFA<S, I> model = state.getProcedure();

            // cannot return, reject word
            if (!model.isAccepting(state.getCurrentState())) {
                return null;
            }

            return state.pop();
        } else {
            return null;
        }
    }

    @Override
    public boolean isAccepting(StackState<S, I, DFA<S, I>> state) {
        return state.isTerm();
    }

    @Override
    public StackState<S, I, DFA<S, I>> getInitialState() {
        return StackState.init();
    }

    @Override
    public @Nullable I getInitialProcedure() {
        return initialCall;
    }

    @Override
    public ProceduralInputAlphabet<I> getInputAlphabet() {
        return this.alphabet;
    }

    @Override
    public Map<I, DFA<?, I>> getProcedures() {
        return Collections.unmodifiableMap(procedures);
    }
}

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.automaton.procedural.impl;
17
18	import java.util.Collections;
19	import java.util.Map;
20	import java.util.Objects;
21
22	import net.automatalib.alphabet.ProceduralInputAlphabet;
23	import net.automatalib.automaton.fsa.DFA;
24	import net.automatalib.automaton.procedural.SPA;
25	import net.automatalib.ts.simple.SimpleDTS;
26	import org.checkerframework.checker.nullness.qual.Nullable;
27
28	/**
29	* A stack-based implementation for the (instrumented) language of an {@link SPA}.
30	*
31	* @param <S>
32	* procedural state type
33	* @param <I>
34	* input symbol type
35	*/
36	public class StackSPA<S, I> implements SPA<StackState<S, I, DFA<S, I>>, I>, SimpleDTS<StackState<S, I, DFA<S, I>>, I> {
37
38	private final ProceduralInputAlphabet<I> alphabet;
39	private final @Nullable I initialCall;
40	private final Map<I, DFA<S, I>> procedures;
41
42	// cast is fine, because we make sure to only query states belonging to the respective procedures
43	@SuppressWarnings("unchecked")
44	public StackSPA(ProceduralInputAlphabet<I> alphabet,
45	@Nullable I initialCall,
46	Map<I, ? extends DFA<? extends S, I>> procedures) {	2✔
47	this.alphabet = alphabet;	2✔
48	this.initialCall = initialCall;	2✔
49	this.procedures = (Map<I, DFA<S, I>>) procedures;	2✔
50	}	2✔
51
52	@Override
53	public StackState<S, I, DFA<S, I>> getTransition(StackState<S, I, DFA<S, I>> state, I input) {
54	if (state.isTerm()) {	2✔
55	return null;	1✔
56	} else if (alphabet.isInternalSymbol(input)) {	2✔
57	if (state.isInit()) {	2✔
58	return null;	2✔
59	}
60
61	final DFA<S, I> model = state.getProcedure();	2✔
62	final S next = model.getTransition(state.getCurrentState(), input);	2✔
63
64	// undefined internal transition
65	if (next == null) {	2✔
66	return null;	2✔
67	}
68
69	return state.updateState(next);	2✔
70	} else if (alphabet.isCallSymbol(input)) {	2✔
71	if (state.isInit() && !Objects.equals(this.initialCall, input)) {	2✔
72	return null;	1✔
73	}
74
75	final DFA<S, I> model = this.procedures.get(input);	2✔
76
77	if (model == null) {	2✔
78	return null;	2✔
79	}
80
81	final S next = model.getInitialState();	2✔
82
83	if (next == null) {	2✔
NEW 84	return null;	×
85	}
86
87	// store the procedural successor in the stack so that we don't need to look it up on return symbols
88	final StackState<S, I, DFA<S, I>> returnState;
89	if (state.isInit()) {	2✔
90	returnState = StackState.term();	2✔
91	} else {
92	final S succ = state.getProcedure().getSuccessor(state.getCurrentState(), input);	2✔
93	if (succ == null) {	2✔
94	return null;	2✔
95	}
96	returnState = state.updateState(succ);	2✔
97	}
98
99	return returnState.push(model, next);	2✔
100	} else if (alphabet.isReturnSymbol(input)) {	2✔
101	if (state.isInit()) {	2✔
102	return null;	2✔
103	}
104
105	// if we returned the state before, we checked that a procedure is available
106	final DFA<S, I> model = state.getProcedure();	2✔
107
108	// cannot return, reject word
109	if (!model.isAccepting(state.getCurrentState())) {	2✔
110	return null;	1✔
111	}
112
113	return state.pop();	2✔
114	} else {
115	return null;	1✔
116	}
117	}
118
119	@Override
120	public boolean isAccepting(StackState<S, I, DFA<S, I>> state) {
121	return state.isTerm();	2✔
122	}
123
124	@Override
125	public StackState<S, I, DFA<S, I>> getInitialState() {
126	return StackState.init();	2✔
127	}
128
129	@Override
130	public @Nullable I getInitialProcedure() {
131	return initialCall;	2✔
132	}
133
134	@Override
135	public ProceduralInputAlphabet<I> getInputAlphabet() {
136	return this.alphabet;	2✔
137	}
138
139	@Override
140	public Map<I, DFA<?, I>> getProcedures() {
141	return Collections.unmodifiableMap(procedures);	2✔
142	}
143	}

LearnLib / automatalib / 19995144613

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