19853794526

Committed 02 Dec 2025 09:32AM UTC coverage: 92.771% (+0.2%) from 92.565%

Build # 19853794526

Build Type

Pull #96

github

Committed by

web-flow

Commit Message

Merge cbacc09aa into f5349326b

Pull Request Pull Request #96: Code for Mealy machines with local timers.

Coverage Stats

649 of 661 new or added lines in 21 files covered. (98.18%)

17146 of 18482 relevant lines covered (92.77%)

1.72 hits per line

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

95.65

/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.concept.Output;
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 net.automatalib.word.Word;
import net.automatalib.word.WordBuilder;
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 Word<TimedOutput<O>> computeSuffixOutput(Iterable<? extends TimedInput<I>> prefix,
                                                    Iterable<? extends TimedInput<I>> suffix) {
        WordBuilder<TimedOutput<O>> wb = Output.getBuilderFor(suffix);
        State<S, O> currentConfiguration = getState(prefix);

        if (currentConfiguration == null) {
            return Word.epsilon();
        }

        for (TimedInput<I> sym : suffix) {
            MealyTransition<State<S, O>, TimedOutput<O>> trans = getTransition(currentConfiguration, sym);

            if (trans == null) {
                break;
            }

            final TimedOutput<O> output = trans.getOutput();
            if (sym instanceof TimeStepSequence<?> ts && ts.timeSteps() > 1) {
                LOGGER.warn("Computing output of time step sequence with more than one symbol." +
                            "The computed output only contains the output for the sequence.");
            }

            wb.append(output);
            currentConfiguration = trans.getSuccessor();
        }

        return wb.toWord();
    }

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

LearnLib / automatalib / 19853794526

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