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.83

/core/src/main/java/net/automatalib/automaton/procedural/impl/StackSBA.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.SBA;
import net.automatalib.ts.simple.SimpleDTS;
import org.checkerframework.checker.nullness.qual.Nullable;

/**
 * A stack-based implementation for the (instrumented) language of an {@link SBA}.
 *
 * @param <S>
 *         procedural state type
 * @param <I>
 *         input symbol type
 */
public class StackSBA<S, I> implements SBA<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 StackSBA(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 @Nullable 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 || !model.isAccepting(next)) {
                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 DFA<S, I> p = state.getProcedure();
                final S succ = p.getSuccessor(state.getCurrentState(), input);
                if (succ == null || !p.isAccepting(succ)) {
                    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();
            final S succ = model.getSuccessor(state.getCurrentState(), input);

            // cannot return, reject word
            if (succ == null || !model.isAccepting(succ)) {
                return null;
            }

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

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

    @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.SBA;
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 SBA}.
30	*
31	* @param <S>
32	* procedural state type
33	* @param <I>
34	* input symbol type
35	*/
36	public class StackSBA<S, I> implements SBA<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 StackSBA(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 @Nullable StackState<S, I, DFA<S, I>> getTransition(StackState<S, I, DFA<S, I>> state, I input) {
54	if (state.isTerm()) {	2✔
NEW 55	return null;	×
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 \|\| !model.isAccepting(next)) {	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;	2✔
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✔
84	return null;	1✔
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 DFA<S, I> p = state.getProcedure();	2✔
93	final S succ = p.getSuccessor(state.getCurrentState(), input);	2✔
94	if (succ == null \|\| !p.isAccepting(succ)) {	2✔
95	return null;	2✔
96	}
97	returnState = state.updateState(succ);	2✔
98	}
99
100	return returnState.push(model, next);	2✔
101	} else if (alphabet.isReturnSymbol(input)) {	2✔
102	if (state.isInit()) {	2✔
103	return null;	2✔
104	}
105
106	// if we returned the state before, we checked that a procedure is available
107	final DFA<S, I> model = state.getProcedure();	2✔
108	final S succ = model.getSuccessor(state.getCurrentState(), input);	2✔
109
110	// cannot return, reject word
111	if (succ == null \|\| !model.isAccepting(succ)) {	2✔
112	return null;	2✔
113	}
114
115	return state.pop();	2✔
116	} else {
117	return null;	2✔
118	}
119	}
120
121	@Override
122	public boolean isAccepting(StackState<S, I, DFA<S, I>> state) {
123	return state.isInit() \|\| state.isTerm() \|\| state.getProcedure().isAccepting(state.getCurrentState());	2✔
124	}
125
126	@Override
127	public StackState<S, I, DFA<S, I>> getInitialState() {
128	return StackState.init();	2✔
129	}
130
131	@Override
132	public @Nullable I getInitialProcedure() {
133	return initialCall;	1✔
134	}
135
136	@Override
137	public ProceduralInputAlphabet<I> getInputAlphabet() {
138	return this.alphabet;	1✔
139	}
140
141	@Override
142	public Map<I, DFA<?, I>> getProcedures() {
143	return Collections.unmodifiableMap(procedures);	1✔
144	}
145	}

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