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

96.77

/core/src/main/java/net/automatalib/automaton/mmlt/impl/ReducedMMLTSemantics.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.HashMap;
import java.util.List;
import java.util.Map;
import java.util.Map.Entry;
import java.util.Objects;

import net.automatalib.alphabet.Alphabet;
import net.automatalib.automaton.mmlt.MMLT;
import net.automatalib.automaton.mmlt.MMLTSemantics;
import net.automatalib.automaton.mmlt.State;
import net.automatalib.automaton.transducer.impl.CompactMealy;
import net.automatalib.symbol.time.TimedInput;
import net.automatalib.symbol.time.TimedOutput;
import net.automatalib.symbol.time.TimeoutSymbol;

/**
 * Provides a reduced version of the semantics automaton of an MMLT. This reduced version retains all configurations
 * that can be reached by timeouts and non-delaying inputs. It omits configurations that can only be reached by at least
 * two subsequent time steps.
 * <p>
 * The resulting automaton suffices to check the equivalence of two MMLTs. However, as the timeStep-transition is
 * undefined in some configurations, the automaton cannot execute any sequence of inputs that can be executed on an
 * MMLT.
 *
 * @param <S>
 *         location type of the original MMLT
 * @param <I>
 *         input symbol of the original MMLT
 * @param <O>
 *         output symbol type of the original MMLT
 */
public final class ReducedMMLTSemantics<S, I, O> extends CompactMealy<TimedInput<I>, TimedOutput<O>> {

    private final Map<State<S, O>, Integer> stateMap;

    private ReducedMMLTSemantics(Alphabet<TimedInput<I>> alphabet) {
        super(alphabet);
        this.stateMap = new HashMap<>();
    }

    /**
     * Constructs a reduced semantics view for the given MMLT.
     *
     * @param mmlt
     *         the MMLT
     * @param <S>
     *         location type of the original MMLT
     * @param <I>
     *         input symbol of the original MMLT
     * @param <O>
     *         output symbol type of the original MMLT
     *
     * @return the reduced semantics view
     */
    public static <S, I, O> ReducedMMLTSemantics<S, I, O> forMMLT(MMLT<S, I, ?, O> mmlt) {
        return forMMLT(mmlt, mmlt.getSemantics());
    }

    private static <S, I, T, O> ReducedMMLTSemantics<S, I, O> forMMLT(MMLT<S, I, ?, O> automaton,
                                                                      MMLTSemantics<S, I, T, O> semantics) {
        // Create alphabet for expanded form:
        Alphabet<TimedInput<I>> alphabet = semantics.getInputAlphabet();

        ReducedMMLTSemantics<S, I, O> mealy = new ReducedMMLTSemantics<>(alphabet);

        // 1a: Add all configurations that can be reached via timeouts/non-delaying inputs, or are at least one time
        // step away from these configurations:
        for (S loc : automaton) {
            getRelevantConfigurations(loc, automaton, semantics).forEach(c -> mealy.stateMap.put(c, mealy.addState()));
        }

        // 1b: Mark initial state:
        State<S, O> initialConfig = semantics.getInitialState();
        mealy.setInitialState(mealy.stateMap.get(initialConfig));

        // 2. Add transitions:
        for (State<S, O> config : mealy.stateMap.keySet()) {
            Integer sourceState = mealy.stateMap.get(config);

            for (TimedInput<I> sym : alphabet) {
                T trans = semantics.getTransition(config, sym);
                if (trans != null) {
                    TimedOutput<O> output = semantics.getTransitionOutput(trans);

                    // Try to find matching state. If not found, leave undefined:
                    int targetId = mealy.stateMap.getOrDefault(semantics.getSuccessor(trans), -1);
                    if (targetId != -1) {
                        mealy.addTransition(sourceState, sym, targetId, output);
                    }
                }
            }
        }

        return mealy;
    }

    /**
     * Retrieves a list of configurations of the provided location that can be reached via timeouts and those that are
     * at most one time step away from these.
     *
     * @param <S>
     *         location type of the original MMLT
     * @param <I>
     *         input symbol of the original MMLT
     * @param <T>
     *         transition type of the MMLTSemantics
     * @param <O>
     *         output symbol type of the original MMLT
     * @param location
     *         the considered location
     * @param mmlt
     *         the MMLT
     * @param semantics
     *         the semantics automaton of {@code mmlt}
     *
     * @return the list of the relevant configurations of the location
     */
    private static <S, I, T, O> List<State<S, O>> getRelevantConfigurations(S location,
                                                                            MMLT<S, I, ?, O> mmlt,
                                                                            MMLTSemantics<S, I, T, O> semantics) {

        List<State<S, O>> configurations = new ArrayList<>();

        State<S, O> currentConfiguration = new State<>(location, mmlt.getSortedTimers(location));
        configurations.add(currentConfiguration);

        // Enumerate all timeouts, until we change to a different location or re-enter the entry configuration
        // of this location:
        while (true) {
            // Wait for next timeout:
            T trans = semantics.getTransition(currentConfiguration, new TimeoutSymbol<>());
            if (trans != null) {
                TimedOutput<O> output = semantics.getTransitionOutput(trans);
                State<S, O> target = semantics.getSuccessor(trans);
                if (output.equals(semantics.getSilentOutput())) {
                    break; // no timeout
                }

                if (output.delay() > 1) {
                    // More than one time unit away -> add 1-step successor config.
                    // If one time unit away, the successor is already in our list.
                    State<S, O> newGapConfig = currentConfiguration.decrement(1);
                    configurations.add(newGapConfig);
                }

                if (target.isEntryConfig()) {
                    break; // location change OR repeating behavior
                }
                configurations.add(target);
                currentConfiguration = target;
            } else {
                return configurations;
            }
        }
        return configurations;
    }

    /**
     * Returns the state that represents the provided configuration. If the configuration is not included and
     * allowApproximate is set, the closest configuration of the same location (with a smaller entry distance) will be
     * returned. If {@code allowApproximate} is not set, an error is thrown.
     *
     * @param configuration
     *         the provided configuration
     * @param allowApproximate
     *         a flag to indicate whether the closest matching state is returned if the configuration is not part of the
     *         reduced automaton
     *
     * @return the corresponding state in the reduced automaton
     */
    public Integer getStateForConfiguration(State<S, O> configuration, boolean allowApproximate) {

        Entry<State<S, O>, Integer> closestMatch = null;

        for (Entry<State<S, O>, Integer> e : stateMap.entrySet()) {
            State<S, O> cfg = e.getKey();
            if (!Objects.equals(cfg.getLocation(), configuration.getLocation()) ||
                cfg.getEntryDistance() > configuration.getEntryDistance()) {
                continue;
            }

            if (cfg.getEntryDistance() == configuration.getEntryDistance()) {
                // Perfect match:
                return e.getValue();
            }

            if (closestMatch == null || cfg.getEntryDistance() > closestMatch.getKey().getEntryDistance()) {
                // Closer than previous candidate:
                closestMatch = e;
            }
        }

        if (closestMatch == null || !allowApproximate) {
            throw new IllegalStateException("Could not find corresponding configuration in expanded form");
        }

        return closestMatch.getValue();
    }

    /**
     * Returns the configuration that represents the provided state. Throws an error if the state is not part of the
     * reduced automaton.
     *
     * @param state
     *         considered state
     *
     * @return corresponding configuration
     */
    public State<S, O> getConfigurationForState(int state) {
        for (Entry<State<S, O>, Integer> e : this.stateMap.entrySet()) {
            if (e.getValue() == state) {
                return e.getKey();
            }
        }
        throw new IllegalStateException("Could not find corresponding configuration in expanded form");
    }
}

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.HashMap;
20	import java.util.List;
21	import java.util.Map;
22	import java.util.Map.Entry;
23	import java.util.Objects;
24
25	import net.automatalib.alphabet.Alphabet;
26	import net.automatalib.automaton.mmlt.MMLT;
27	import net.automatalib.automaton.mmlt.MMLTSemantics;
28	import net.automatalib.automaton.mmlt.State;
29	import net.automatalib.automaton.transducer.impl.CompactMealy;
30	import net.automatalib.symbol.time.TimedInput;
31	import net.automatalib.symbol.time.TimedOutput;
32	import net.automatalib.symbol.time.TimeoutSymbol;
33
34	/**
35	* Provides a reduced version of the semantics automaton of an MMLT. This reduced version retains all configurations
36	* that can be reached by timeouts and non-delaying inputs. It omits configurations that can only be reached by at least
37	* two subsequent time steps.
38	* <p>
39	* The resulting automaton suffices to check the equivalence of two MMLTs. However, as the timeStep-transition is
40	* undefined in some configurations, the automaton cannot execute any sequence of inputs that can be executed on an
41	* MMLT.
42	*
43	* @param <S>
44	* location type of the original MMLT
45	* @param <I>
46	* input symbol of the original MMLT
47	* @param <O>
48	* output symbol type of the original MMLT
49	*/
50	public final class ReducedMMLTSemantics<S, I, O> extends CompactMealy<TimedInput<I>, TimedOutput<O>> {
51
52	private final Map<State<S, O>, Integer> stateMap;
53
54	private ReducedMMLTSemantics(Alphabet<TimedInput<I>> alphabet) {
55	super(alphabet);	2✔
56	this.stateMap = new HashMap<>();	2✔
57	}	2✔
58
59	/**
60	* Constructs a reduced semantics view for the given MMLT.
61	*
62	* @param mmlt
63	* the MMLT
64	* @param <S>
65	* location type of the original MMLT
66	* @param <I>
67	* input symbol of the original MMLT
68	* @param <O>
69	* output symbol type of the original MMLT
70	*
71	* @return the reduced semantics view
72	*/
73	public static <S, I, O> ReducedMMLTSemantics<S, I, O> forMMLT(MMLT<S, I, ?, O> mmlt) {
74	return forMMLT(mmlt, mmlt.getSemantics());	2✔
75	}
76
77	private static <S, I, T, O> ReducedMMLTSemantics<S, I, O> forMMLT(MMLT<S, I, ?, O> automaton,
78	MMLTSemantics<S, I, T, O> semantics) {
79	// Create alphabet for expanded form:
80	Alphabet<TimedInput<I>> alphabet = semantics.getInputAlphabet();	2✔
81
82	ReducedMMLTSemantics<S, I, O> mealy = new ReducedMMLTSemantics<>(alphabet);	2✔
83
84	// 1a: Add all configurations that can be reached via timeouts/non-delaying inputs, or are at least one time
85	// step away from these configurations:
86	for (S loc : automaton) {	2✔
87	getRelevantConfigurations(loc, automaton, semantics).forEach(c -> mealy.stateMap.put(c, mealy.addState()));	2✔
88	}	2✔
89
90	// 1b: Mark initial state:
91	State<S, O> initialConfig = semantics.getInitialState();	2✔
92	mealy.setInitialState(mealy.stateMap.get(initialConfig));	2✔
93
94	// 2. Add transitions:
95	for (State<S, O> config : mealy.stateMap.keySet()) {	2✔
96	Integer sourceState = mealy.stateMap.get(config);	2✔
97
98	for (TimedInput<I> sym : alphabet) {	2✔
99	T trans = semantics.getTransition(config, sym);	2✔
100	if (trans != null) {	2✔
101	TimedOutput<O> output = semantics.getTransitionOutput(trans);	2✔
102
103	// Try to find matching state. If not found, leave undefined:
104	int targetId = mealy.stateMap.getOrDefault(semantics.getSuccessor(trans), -1);	2✔
105	if (targetId != -1) {	2✔
106	mealy.addTransition(sourceState, sym, targetId, output);	2✔
107	}
108	}
109	}	2✔
110	}	2✔
111
112	return mealy;	2✔
113	}
114
115	/**
116	* Retrieves a list of configurations of the provided location that can be reached via timeouts and those that are
117	* at most one time step away from these.
118	*
119	* @param <S>
120	* location type of the original MMLT
121	* @param <I>
122	* input symbol of the original MMLT
123	* @param <T>
124	* transition type of the MMLTSemantics
125	* @param <O>
126	* output symbol type of the original MMLT
127	* @param location
128	* the considered location
129	* @param mmlt
130	* the MMLT
131	* @param semantics
132	* the semantics automaton of {@code mmlt}
133	*
134	* @return the list of the relevant configurations of the location
135	*/
136	private static <S, I, T, O> List<State<S, O>> getRelevantConfigurations(S location,
137	MMLT<S, I, ?, O> mmlt,
138	MMLTSemantics<S, I, T, O> semantics) {
139
140	List<State<S, O>> configurations = new ArrayList<>();	2✔
141
142	State<S, O> currentConfiguration = new State<>(location, mmlt.getSortedTimers(location));	2✔
143	configurations.add(currentConfiguration);	2✔
144
145	// Enumerate all timeouts, until we change to a different location or re-enter the entry configuration
146	// of this location:
147	while (true) {
148	// Wait for next timeout:
149	T trans = semantics.getTransition(currentConfiguration, new TimeoutSymbol<>());	2✔
150	if (trans != null) {	2✔
151	TimedOutput<O> output = semantics.getTransitionOutput(trans);	2✔
152	State<S, O> target = semantics.getSuccessor(trans);	2✔
153	if (output.equals(semantics.getSilentOutput())) {	2✔
154	break; // no timeout	2✔
155	}
156
157	if (output.delay() > 1) {	2✔
158	// More than one time unit away -> add 1-step successor config.
159	// If one time unit away, the successor is already in our list.
160	State<S, O> newGapConfig = currentConfiguration.decrement(1);	2✔
161	configurations.add(newGapConfig);	2✔
162	}
163
164	if (target.isEntryConfig()) {	2✔
165	break; // location change OR repeating behavior	2✔
166	}
167	configurations.add(target);	2✔
168	currentConfiguration = target;	2✔
169	} else {	2✔
NEW 170	return configurations;	×
171	}
172	}	2✔
173	return configurations;	2✔
174	}
175
176	/**
177	* Returns the state that represents the provided configuration. If the configuration is not included and
178	* allowApproximate is set, the closest configuration of the same location (with a smaller entry distance) will be
179	* returned. If {@code allowApproximate} is not set, an error is thrown.
180	*
181	* @param configuration
182	* the provided configuration
183	* @param allowApproximate
184	* a flag to indicate whether the closest matching state is returned if the configuration is not part of the
185	* reduced automaton
186	*
187	* @return the corresponding state in the reduced automaton
188	*/
189	public Integer getStateForConfiguration(State<S, O> configuration, boolean allowApproximate) {
190
191	Entry<State<S, O>, Integer> closestMatch = null;	2✔
192
193	for (Entry<State<S, O>, Integer> e : stateMap.entrySet()) {	2✔
194	State<S, O> cfg = e.getKey();	2✔
195	if (!Objects.equals(cfg.getLocation(), configuration.getLocation()) \|\|	2✔
196	cfg.getEntryDistance() > configuration.getEntryDistance()) {	2✔
197	continue;	2✔
198	}
199
200	if (cfg.getEntryDistance() == configuration.getEntryDistance()) {	2✔
201	// Perfect match:
202	return e.getValue();	2✔
203	}
204
205	if (closestMatch == null \|\| cfg.getEntryDistance() > closestMatch.getKey().getEntryDistance()) {	2✔
206	// Closer than previous candidate:
207	closestMatch = e;	2✔
208	}
209	}	2✔
210
211	if (closestMatch == null \|\| !allowApproximate) {	2✔
212	throw new IllegalStateException("Could not find corresponding configuration in expanded form");	2✔
213	}
214
215	return closestMatch.getValue();	2✔
216	}
217
218	/**
219	* Returns the configuration that represents the provided state. Throws an error if the state is not part of the
220	* reduced automaton.
221	*
222	* @param state
223	* considered state
224	*
225	* @return corresponding configuration
226	*/
227	public State<S, O> getConfigurationForState(int state) {
228	for (Entry<State<S, O>, Integer> e : this.stateMap.entrySet()) {	2✔
229	if (e.getValue() == state) {	2✔
230	return e.getKey();	2✔
231	}
232	}	2✔
NEW 233	throw new IllegalStateException("Could not find corresponding configuration in expanded form");	×
234	}
235	}

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