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

98.08

/core/src/main/java/net/automatalib/automaton/procedural/impl/StackSPMM.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.procedural.SPMM;
import net.automatalib.automaton.transducer.MealyMachine;
import net.automatalib.automaton.transducer.impl.MealyTransition;
import org.checkerframework.checker.nullness.qual.Nullable;

/**
 * A stack-based implementation for the (instrumented) transductions of an {@link SPMM}.
 *
 * @param <S>
 *         procedural state type
 * @param <I>
 *         input symbol type
 * @param <T>
 *         transition type
 * @param <O>
 *         output symbol type
 */
public class StackSPMM<S, I, T, O>
        implements SPMM<StackState<S, I, MealyMachine<S, I, T, O>>, I, MealyTransition<StackState<S, I, MealyMachine<S, I, T, O>>, O>, O> {

    private final ProceduralInputAlphabet<I> alphabet;
    private final O errorOutput;

    private final @Nullable I initialCall;
    private final O initialOutput;
    private final Map<I, MealyMachine<S, I, T, O>> procedures;

    @SuppressWarnings("unchecked")
    public StackSPMM(ProceduralInputAlphabet<I> alphabet,
                     @Nullable I initialCall,
                     O initialOutput,
                     O errorOutput,
                     Map<I, ? extends MealyMachine<? extends S, I, ? extends T, O>> procedures) {
        this.alphabet = alphabet;
        this.errorOutput = errorOutput;
        this.initialCall = initialCall;
        this.initialOutput = initialOutput;
        this.procedures = (Map<I, MealyMachine<S, I, T, O>>) procedures;
    }

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

            final MealyMachine<S, I, T, O> model = state.getProcedure();
            final T t = model.getTransition(state.getCurrentState(), input);

            // undefined internal transition
            if (t == null || isErrorOutput(model.getTransitionOutput(t))) {
                return null;
            }

            return new MealyTransition<>(state.updateState(model.getSuccessor(t)), model.getTransitionOutput(t));
        } else if (alphabet.isCallSymbol(input)) {
            if (state.isInit() && !Objects.equals(this.initialCall, input)) {
                return null;
            }

            final MealyMachine<S, I, T, O> 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, MealyMachine<S, I, T, O>> returnState;
            final O output;
            if (state.isInit()) {
                returnState = StackState.term();
                output = initialOutput;
            } else {
                final MealyMachine<S, I, T, O> p = state.getProcedure();
                final T t = p.getTransition(state.getCurrentState(), input);

                if (t == null || isErrorOutput(p.getTransitionOutput(t))) {
                    return null;
                }
                returnState = state.updateState(p.getSuccessor(t));
                output = p.getTransitionOutput(t);
            }

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

            // if we returned the state before, we checked that a procedure is available
            final MealyMachine<S, I, T, O> model = state.getProcedure();
            final T t = model.getTransition(state.getCurrentState(), input);

            if (t == null || isErrorOutput(model.getTransitionOutput(t))) {
                return null;
            }

            return new MealyTransition<>(state.pop(), model.getTransitionOutput(t));
        } else {
            return null;
        }
    }

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

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

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

    @Override
    public O getErrorOutput() {
        return this.errorOutput;
    }

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

    @Override
    public O getTransitionOutput(MealyTransition<StackState<S, I, MealyMachine<S, I, T, O>>, O> transition) {
        return transition.getOutput();
    }

    @Override
    public StackState<S, I, MealyMachine<S, I, T, O>> getSuccessor(MealyTransition<StackState<S, I, MealyMachine<S, I, T, O>>, O> transition) {
        return transition.getSuccessor();
    }

}

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.procedural.SPMM;
24	import net.automatalib.automaton.transducer.MealyMachine;
25	import net.automatalib.automaton.transducer.impl.MealyTransition;
26	import org.checkerframework.checker.nullness.qual.Nullable;
27
28	/**
29	* A stack-based implementation for the (instrumented) transductions of an {@link SPMM}.
30	*
31	* @param <S>
32	* procedural state type
33	* @param <I>
34	* input symbol type
35	* @param <T>
36	* transition type
37	* @param <O>
38	* output symbol type
39	*/
40	public class StackSPMM<S, I, T, O>
41	implements SPMM<StackState<S, I, MealyMachine<S, I, T, O>>, I, MealyTransition<StackState<S, I, MealyMachine<S, I, T, O>>, O>, O> {
42
43	private final ProceduralInputAlphabet<I> alphabet;
44	private final O errorOutput;
45
46	private final @Nullable I initialCall;
47	private final O initialOutput;
48	private final Map<I, MealyMachine<S, I, T, O>> procedures;
49
50	@SuppressWarnings("unchecked")
51	public StackSPMM(ProceduralInputAlphabet<I> alphabet,
52	@Nullable I initialCall,
53	O initialOutput,
54	O errorOutput,
55	Map<I, ? extends MealyMachine<? extends S, I, ? extends T, O>> procedures) {	2✔
56	this.alphabet = alphabet;	2✔
57	this.errorOutput = errorOutput;	2✔
58	this.initialCall = initialCall;	2✔
59	this.initialOutput = initialOutput;	2✔
60	this.procedures = (Map<I, MealyMachine<S, I, T, O>>) procedures;	2✔
61	}	2✔
62
63	@Override
64	public @Nullable MealyTransition<StackState<S, I, MealyMachine<S, I, T, O>>, O> getTransition(StackState<S, I, MealyMachine<S, I, T, O>> state,
65	I input) {
66	if (state.isTerm()) {	2✔
NEW 67	return null;	×
68	} else if (alphabet.isInternalSymbol(input)) {	2✔
69	if (state.isInit()) {	2✔
70	return null;	2✔
71	}
72
73	final MealyMachine<S, I, T, O> model = state.getProcedure();	2✔
74	final T t = model.getTransition(state.getCurrentState(), input);	2✔
75
76	// undefined internal transition
77	if (t == null \|\| isErrorOutput(model.getTransitionOutput(t))) {	2✔
78	return null;	2✔
79	}
80
81	return new MealyTransition<>(state.updateState(model.getSuccessor(t)), model.getTransitionOutput(t));	2✔
82	} else if (alphabet.isCallSymbol(input)) {	2✔
83	if (state.isInit() && !Objects.equals(this.initialCall, input)) {	2✔
84	return null;	2✔
85	}
86
87	final MealyMachine<S, I, T, O> model = this.procedures.get(input);	2✔
88
89	if (model == null) {	2✔
90	return null;	2✔
91	}
92
93	final S next = model.getInitialState();	2✔
94
95	if (next == null) {	2✔
96	return null;	1✔
97	}
98
99	// store the procedural successor in the stack so that we don't need to look it up on return symbols
100	final StackState<S, I, MealyMachine<S, I, T, O>> returnState;
101	final O output;
102	if (state.isInit()) {	2✔
103	returnState = StackState.term();	2✔
104	output = initialOutput;	2✔
105	} else {
106	final MealyMachine<S, I, T, O> p = state.getProcedure();	2✔
107	final T t = p.getTransition(state.getCurrentState(), input);	2✔
108
109	if (t == null \|\| isErrorOutput(p.getTransitionOutput(t))) {	2✔
110	return null;	2✔
111	}
112	returnState = state.updateState(p.getSuccessor(t));	2✔
113	output = p.getTransitionOutput(t);	2✔
114	}
115
116	return new MealyTransition<>(returnState.push(model, next), output);	2✔
117	} else if (alphabet.isReturnSymbol(input)) {	2✔
118	if (state.isInit()) {	2✔
119	return null;	2✔
120	}
121
122	// if we returned the state before, we checked that a procedure is available
123	final MealyMachine<S, I, T, O> model = state.getProcedure();	2✔
124	final T t = model.getTransition(state.getCurrentState(), input);	2✔
125
126	if (t == null \|\| isErrorOutput(model.getTransitionOutput(t))) {	2✔
127	return null;	2✔
128	}
129
130	return new MealyTransition<>(state.pop(), model.getTransitionOutput(t));	2✔
131	} else {
132	return null;	2✔
133	}
134	}
135
136	@Override
137	public StackState<S, I, MealyMachine<S, I, T, O>> getInitialState() {
138	return StackState.init();	2✔
139	}
140
141	@Override
142	public @Nullable I getInitialProcedure() {
143	return initialCall;	1✔
144	}
145
146	@Override
147	public ProceduralInputAlphabet<I> getInputAlphabet() {
148	return this.alphabet;	1✔
149	}
150
151	@Override
152	public O getErrorOutput() {
153	return this.errorOutput;	2✔
154	}
155
156	@Override
157	public Map<I, MealyMachine<?, I, ?, O>> getProcedures() {
158	return Collections.unmodifiableMap(procedures);	1✔
159	}
160
161	@Override
162	public O getTransitionOutput(MealyTransition<StackState<S, I, MealyMachine<S, I, T, O>>, O> transition) {
163	return transition.getOutput();	2✔
164	}
165
166	@Override
167	public StackState<S, I, MealyMachine<S, I, T, O>> getSuccessor(MealyTransition<StackState<S, I, MealyMachine<S, I, T, O>>, O> transition) {
168	return transition.getSuccessor();	2✔
169	}
170
171	}

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