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

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

import java.util.ArrayList;
import java.util.List;
import java.util.Objects;

import net.automatalib.alphabet.Alphabet;
import net.automatalib.alphabet.impl.MapAlphabet;
import net.automatalib.automaton.mmlt.MMLT;
import net.automatalib.automaton.mmlt.MMLTSemantics;
import net.automatalib.automaton.mmlt.State;
import net.automatalib.automaton.mmlt.TimeoutPair;
import net.automatalib.automaton.mmlt.TimerInfo;
import net.automatalib.automaton.transducer.impl.MealyTransition;
import net.automatalib.symbol.time.InputSymbol;
import net.automatalib.symbol.time.TimeStepSequence;
import net.automatalib.symbol.time.TimedInput;
import net.automatalib.symbol.time.TimedOutput;
import net.automatalib.symbol.time.TimeoutSymbol;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

/**
 * Default implementation for an {@link MMLTSemantics} that wraps arbitrary {@link MMLT}s.
 *
 * @param <S>
 *         location type of the original MMLT
 * @param <I>
 *         input symbol of the original MMLT
 * @param <T>
 *         transition type of the original MMLT
 * @param <O>
 *         output symbol type of the original MMLT
 */
public class DefaultMMLTSemantics<S, I, T, O>
        implements MMLTSemantics<S, I, MealyTransition<State<S, O>, TimedOutput<O>>, O> {

    private static final Logger LOGGER = LoggerFactory.getLogger(DefaultMMLTSemantics.class);

    private final MMLT<S, I, T, O> model;
    private final @Nullable State<S, O> initialConfiguration;
    private final Alphabet<TimedInput<I>> alphabet;
    private final TimedOutput<O> silentOutput;

    public DefaultMMLTSemantics(MMLT<S, I, T, O> model) {
        this.model = model;

        final S initialLocation = model.getInitialState();
        if (initialLocation == null) {
            this.initialConfiguration = null;
        } else {
            this.initialConfiguration = new State<>(initialLocation, model.getSortedTimers(initialLocation));
        }

        final Alphabet<I> inputs = model.getInputAlphabet();
        final List<TimedInput<I>> timedInputs = new ArrayList<>(inputs.size() + 2);
        for (I i : inputs) {
            timedInputs.add(TimedInput.input(i));
        }
        timedInputs.add(TimedInput.timeout());
        timedInputs.add(TimedInput.step());

        this.alphabet = new MapAlphabet<>(timedInputs);
        this.silentOutput = new TimedOutput<>(model.getSilentOutput());
    }

    @Override
    public Alphabet<TimedInput<I>> getInputAlphabet() {
        return alphabet;
    }

    @Override
    public TimedOutput<O> getSilentOutput() {
        return this.silentOutput;
    }

    @Override
    public @Nullable State<S, O> getInitialState() {
        return this.initialConfiguration;
    }

    @Override
    public MealyTransition<State<S, O>, TimedOutput<O>> getTransition(State<S, O> source, TimedInput<I> input) {
        return getTransition(source, input, Long.MAX_VALUE);
    }

    @Override
    public MealyTransition<State<S, O>, TimedOutput<O>> getTransition(State<S, O> source,
                                                                      TimedInput<I> input,
                                                                      long maxWaitingTime) {
        if (input instanceof InputSymbol<I> ndi) {
            return getTransition(source, ndi);
        } else if (input instanceof TimeoutSymbol<I>) {
            return getTimeoutTransition(source, maxWaitingTime);
        } else if (input instanceof TimeStepSequence<I> ts) {
            // Per step, we can advance at most by the time to the next timeout:
            State<S, O> currentConfig = source;
            O lastOutput = null;
            long remainingTime = ts.timeSteps();

            if (remainingTime > 1) {
                LOGGER.warn(
                        "The transition output of a time step sequence with more than one symbol only contains the output for the sequence");
            }

            while (remainingTime > 0) {
                MealyTransition<State<S, O>, TimedOutput<O>> nextTimeoutTrans =
                        getTimeoutTransition(currentConfig, remainingTime);
                currentConfig = nextTimeoutTrans.getSuccessor();
                lastOutput = nextTimeoutTrans.getOutput().symbol();
                if (Objects.equals(lastOutput, this.getSilentOutput().symbol())) {
                    // No timer will expire during remaining waiting time:
                    break;
                } else {
                    remainingTime -= nextTimeoutTrans.getOutput().delay();
                }
            }

            assert lastOutput != null;
            return new MealyTransition<>(currentConfig, new TimedOutput<>(lastOutput));
        } else {
            throw new IllegalArgumentException("Unknown input symbol type");
        }
    }

    private MealyTransition<State<S, O>, TimedOutput<O>> getTransition(State<S, O> source, InputSymbol<I> input) {
        State<S, O> target;
        TimedOutput<O> output;

        T trans = model.getTransition(source.getLocation(), input.symbol());
        if (trans == null) { // silent self-loop
            target = source;
            output = this.getSilentOutput();
        } else {
            // Identify successor configuration:
            S succ = model.getSuccessor(trans);
            if (!Objects.equals(succ, source.getLocation())) {
                // Change to a different location resets all timers in target:
                target = new State<>(succ, model.getSortedTimers(succ));
            } else if (model.isLocalReset(source.getLocation(), input.symbol())) {
                target = source.resetTimers();
            } else {
                target = source;
            }
            output = new TimedOutput<>(model.getTransitionProperty(trans));
        }

        // Return output:
        return new MealyTransition<>(target, output);
    }

    @Override
    public TimedOutput<O> getTransitionOutput(MealyTransition<State<S, O>, TimedOutput<O>> transition) {
        return transition.getOutput();
    }

    @Override
    public State<S, O> getSuccessor(MealyTransition<State<S, O>, TimedOutput<O>> transition) {
        return transition.getSuccessor();
    }

    private MealyTransition<State<S, O>, TimedOutput<O>> getTimeoutTransition(State<S, O> source, long maxWaitingTime) {
        State<S, O> target;
        TimedOutput<O> output;

        TimeoutPair<S, O> nextTimeouts = source.getNextExpiringTimers();
        if (nextTimeouts == null) {
            // no timers:
            output = this.getSilentOutput();
            target = source;
        } else if (nextTimeouts.delay() > maxWaitingTime) {
            // timers, but too far away:
            target = source.decrement(maxWaitingTime);
            output = this.getSilentOutput();
        } else {
            if (nextTimeouts.allPeriodic()) {
                target = source.decrement(nextTimeouts.delay());
            } else {
                // query target + update configuration:
                assert nextTimeouts.timers().size() == 1;
                TimerInfo<S, O> timer = nextTimeouts.timers().get(0);
                S successor = timer.target();

                target = new State<>(successor, model.getSortedTimers(successor));
            }

            // Combine all outputs at the next timeout:
            List<O> outputs;
            if (nextTimeouts.timers().size() == 1) {
                outputs = nextTimeouts.timers().get(0).outputs();
            } else {
                outputs = new ArrayList<>();
                for (TimerInfo<S, O> timer : nextTimeouts.timers()) {
                    outputs.addAll(timer.outputs());
                }
            }
            O combinedOutput = model.getOutputCombiner().combineSymbols(outputs);
            output = new TimedOutput<>(combinedOutput, nextTimeouts.delay());
        }

        return new MealyTransition<>(target, output);
    }
}

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.mmlt.impl;
17
18	import java.util.ArrayList;
19	import java.util.List;
20	import java.util.Objects;
21
22	import net.automatalib.alphabet.Alphabet;
23	import net.automatalib.alphabet.impl.MapAlphabet;
24	import net.automatalib.automaton.mmlt.MMLT;
25	import net.automatalib.automaton.mmlt.MMLTSemantics;
26	import net.automatalib.automaton.mmlt.State;
27	import net.automatalib.automaton.mmlt.TimeoutPair;
28	import net.automatalib.automaton.mmlt.TimerInfo;
29	import net.automatalib.automaton.transducer.impl.MealyTransition;
30	import net.automatalib.symbol.time.InputSymbol;
31	import net.automatalib.symbol.time.TimeStepSequence;
32	import net.automatalib.symbol.time.TimedInput;
33	import net.automatalib.symbol.time.TimedOutput;
34	import net.automatalib.symbol.time.TimeoutSymbol;
35	import org.checkerframework.checker.nullness.qual.Nullable;
36	import org.slf4j.Logger;
37	import org.slf4j.LoggerFactory;
38
39	/**
40	* Default implementation for an {@link MMLTSemantics} that wraps arbitrary {@link MMLT}s.
41	*
42	* @param <S>
43	* location type of the original MMLT
44	* @param <I>
45	* input symbol of the original MMLT
46	* @param <T>
47	* transition type of the original MMLT
48	* @param <O>
49	* output symbol type of the original MMLT
50	*/
51	public class DefaultMMLTSemantics<S, I, T, O>
52	implements MMLTSemantics<S, I, MealyTransition<State<S, O>, TimedOutput<O>>, O> {
53
54	private static final Logger LOGGER = LoggerFactory.getLogger(DefaultMMLTSemantics.class);	2✔
55
56	private final MMLT<S, I, T, O> model;
57	private final @Nullable State<S, O> initialConfiguration;
58	private final Alphabet<TimedInput<I>> alphabet;
59	private final TimedOutput<O> silentOutput;
60
61	public DefaultMMLTSemantics(MMLT<S, I, T, O> model) {	2✔
62	this.model = model;	2✔
63
64	final S initialLocation = model.getInitialState();	2✔
65	if (initialLocation == null) {	2✔
66	this.initialConfiguration = null;	1✔
67	} else {
68	this.initialConfiguration = new State<>(initialLocation, model.getSortedTimers(initialLocation));	2✔
69	}
70
71	final Alphabet<I> inputs = model.getInputAlphabet();	2✔
72	final List<TimedInput<I>> timedInputs = new ArrayList<>(inputs.size() + 2);	2✔
73	for (I i : inputs) {	2✔
74	timedInputs.add(TimedInput.input(i));	2✔
75	}	2✔
76	timedInputs.add(TimedInput.timeout());	2✔
77	timedInputs.add(TimedInput.step());	2✔
78
79	this.alphabet = new MapAlphabet<>(timedInputs);	2✔
80	this.silentOutput = new TimedOutput<>(model.getSilentOutput());	2✔
81	}	2✔
82
83	@Override
84	public Alphabet<TimedInput<I>> getInputAlphabet() {
85	return alphabet;	2✔
86	}
87
88	@Override
89	public TimedOutput<O> getSilentOutput() {
90	return this.silentOutput;	2✔
91	}
92
93	@Override
94	public @Nullable State<S, O> getInitialState() {
95	return this.initialConfiguration;	2✔
96	}
97
98	@Override
99	public MealyTransition<State<S, O>, TimedOutput<O>> getTransition(State<S, O> source, TimedInput<I> input) {
100	return getTransition(source, input, Long.MAX_VALUE);	2✔
101	}
102
103	@Override
104	public MealyTransition<State<S, O>, TimedOutput<O>> getTransition(State<S, O> source,
105	TimedInput<I> input,
106	long maxWaitingTime) {
107	if (input instanceof InputSymbol<I> ndi) {	2✔
108	return getTransition(source, ndi);	2✔
109	} else if (input instanceof TimeoutSymbol<I>) {	2✔
110	return getTimeoutTransition(source, maxWaitingTime);	2✔
111	} else if (input instanceof TimeStepSequence<I> ts) {	2✔
112	// Per step, we can advance at most by the time to the next timeout:
113	State<S, O> currentConfig = source;	2✔
114	O lastOutput = null;	2✔
115	long remainingTime = ts.timeSteps();	2✔
116
117	if (remainingTime > 1) {	2✔
118	LOGGER.warn(	2✔
119	"The transition output of a time step sequence with more than one symbol only contains the output for the sequence");
120	}
121
122	while (remainingTime > 0) {	2✔
123	MealyTransition<State<S, O>, TimedOutput<O>> nextTimeoutTrans =	2✔
124	getTimeoutTransition(currentConfig, remainingTime);	2✔
125	currentConfig = nextTimeoutTrans.getSuccessor();	2✔
126	lastOutput = nextTimeoutTrans.getOutput().symbol();	2✔
127	if (Objects.equals(lastOutput, this.getSilentOutput().symbol())) {	2✔
128	// No timer will expire during remaining waiting time:
129	break;	2✔
130	} else {
131	remainingTime -= nextTimeoutTrans.getOutput().delay();	2✔
132	}
133	}	2✔
134
135	assert lastOutput != null;	2✔
136	return new MealyTransition<>(currentConfig, new TimedOutput<>(lastOutput));	2✔
137	} else {
UNCOV 138	throw new IllegalArgumentException("Unknown input symbol type");	×
139	}
140	}
141
142	private MealyTransition<State<S, O>, TimedOutput<O>> getTransition(State<S, O> source, InputSymbol<I> input) {
143	State<S, O> target;
144	TimedOutput<O> output;
145
146	T trans = model.getTransition(source.getLocation(), input.symbol());	2✔
147	if (trans == null) { // silent self-loop	2✔
148	target = source;	2✔
149	output = this.getSilentOutput();	2✔
150	} else {
151	// Identify successor configuration:
152	S succ = model.getSuccessor(trans);	2✔
153	if (!Objects.equals(succ, source.getLocation())) {	2✔
154	// Change to a different location resets all timers in target:
155	target = new State<>(succ, model.getSortedTimers(succ));	2✔
156	} else if (model.isLocalReset(source.getLocation(), input.symbol())) {	2✔
157	target = source.resetTimers();	2✔
158	} else {
159	target = source;	1✔
160	}
161	output = new TimedOutput<>(model.getTransitionProperty(trans));	2✔
162	}
163
164	// Return output:
165	return new MealyTransition<>(target, output);	2✔
166	}
167
168	@Override
169	public TimedOutput<O> getTransitionOutput(MealyTransition<State<S, O>, TimedOutput<O>> transition) {
170	return transition.getOutput();	2✔
171	}
172
173	@Override
174	public State<S, O> getSuccessor(MealyTransition<State<S, O>, TimedOutput<O>> transition) {
175	return transition.getSuccessor();	2✔
176	}
177
178	private MealyTransition<State<S, O>, TimedOutput<O>> getTimeoutTransition(State<S, O> source, long maxWaitingTime) {
179	State<S, O> target;
180	TimedOutput<O> output;
181
182	TimeoutPair<S, O> nextTimeouts = source.getNextExpiringTimers();	2✔
183	if (nextTimeouts == null) {	2✔
184	// no timers:
185	output = this.getSilentOutput();	2✔
186	target = source;	2✔
187	} else if (nextTimeouts.delay() > maxWaitingTime) {	2✔
188	// timers, but too far away:
189	target = source.decrement(maxWaitingTime);	2✔
190	output = this.getSilentOutput();	2✔
191	} else {
192	if (nextTimeouts.allPeriodic()) {	2✔
193	target = source.decrement(nextTimeouts.delay());	2✔
194	} else {
195	// query target + update configuration:
196	assert nextTimeouts.timers().size() == 1;	2✔
197	TimerInfo<S, O> timer = nextTimeouts.timers().get(0);	2✔
198	S successor = timer.target();	2✔
199
200	target = new State<>(successor, model.getSortedTimers(successor));	2✔
201	}
202
203	// Combine all outputs at the next timeout:
204	List<O> outputs;
205	if (nextTimeouts.timers().size() == 1) {	2✔
206	outputs = nextTimeouts.timers().get(0).outputs();	2✔
207	} else {
208	outputs = new ArrayList<>();	2✔
209	for (TimerInfo<S, O> timer : nextTimeouts.timers()) {	2✔
210	outputs.addAll(timer.outputs());	2✔
211	}	2✔
212	}
213	O combinedOutput = model.getOutputCombiner().combineSymbols(outputs);	2✔
214	output = new TimedOutput<>(combinedOutput, nextTimeouts.delay());	2✔
215	}
216
217	return new MealyTransition<>(target, output);	2✔
218	}
219	}

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