19864403395

/* 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.Collections;
import java.util.Comparator;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;

import net.automatalib.alphabet.Alphabet;
import net.automatalib.automaton.AutomatonCreator;
import net.automatalib.automaton.impl.CompactTransition;
import net.automatalib.automaton.mmlt.MMLTSemantics;
import net.automatalib.automaton.mmlt.MutableMMLT;
import net.automatalib.automaton.mmlt.SymbolCombiner;
import net.automatalib.automaton.mmlt.TimerInfo;
import net.automatalib.automaton.transducer.impl.CompactMealy;
import net.automatalib.common.util.Triple;
import net.automatalib.graph.Graph;
import net.automatalib.symbol.time.SymbolicInput;

/**
 * Implements a {@link MutableMMLT} by storing adjacency information in compact arrays.
 *
 * @param <I>
 *         input symbol type (of non-delaying inputs)
 * @param <O>
 *         output symbol type
 */
public class CompactMMLT<I, O> extends CompactMealy<I, O> implements MutableMMLT<Integer, I, CompactTransition<O>, O> {

    private final Map<Integer, List<TimerInfo<Integer, O>>> sortedTimers; // location -> (sorted timers)
    private final Map<Integer, Set<I>> resets; // location -> inputs (that reset all timers)

    private final O silentOutput;
    private final SymbolCombiner<O> outputCombiner;

    /**
     * Initializes a new CompactMMLT.
     *
     * @param alphabet
     *         the alphabet of non-delaying inputs
     * @param silentOutput
     *         the silent output used by this MMLT
     * @param outputCombiner
     *         the combiner function for simultaneous timeouts of periodic timers
     */
    public CompactMMLT(Alphabet<I> alphabet, O silentOutput, SymbolCombiner<O> outputCombiner) {
        this(alphabet, DEFAULT_INIT_CAPACITY, silentOutput, outputCombiner);
    }

    /**
     * Initializes a new CompactMMLT.
     *
     * @param alphabet
     *         the alphabet of non-delaying inputs
     * @param sizeHint
     *         a size hint to better allocate internal memory
     * @param silentOutput
     *         the silent output used by this MMLT
     * @param outputCombiner
     *         the combiner function for simultaneous timeouts of periodic timers
     */
    public CompactMMLT(Alphabet<I> alphabet, int sizeHint, O silentOutput, SymbolCombiner<O> outputCombiner) {
        super(alphabet, sizeHint);

        this.sortedTimers = new HashMap<>();
        this.resets = new HashMap<>();

        this.silentOutput = silentOutput;
        this.outputCombiner = outputCombiner;
    }

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

    @Override
    public SymbolCombiner<O> getOutputCombiner() {
        return this.outputCombiner;
    }

    @Override
    public boolean isLocalReset(Integer location, I input) {
        return this.resets.getOrDefault(location, Collections.emptySet()).contains(input);
    }

    @Override
    public List<TimerInfo<Integer, O>> getSortedTimers(Integer location) {
        return Collections.unmodifiableList(this.sortedTimers.getOrDefault(location, Collections.emptyList()));
    }

    @Override
    public MMLTSemantics<Integer, I, ?, O> getSemantics() {
        return new DefaultMMLTSemantics<>(this);
    }

    private void ensureThatCanAddTimer(List<TimerInfo<Integer, O>> timers,
                                       String name,
                                       long initial,
                                       List<O> outputs,
                                       boolean periodic) {
        if (outputs.isEmpty() || outputs.contains(silentOutput)) {
            throw new IllegalArgumentException(String.format("Timer '%s': outputs are empty or contain silent output.",
                                                             name));
        }

        for (O output : outputs) {
            if (getOutputCombiner().isCombinedSymbol(output)) {
                throw new IllegalArgumentException(String.format(
                        "Timer '%s': output '%s' is a combined symbol. You must only provide atomic outputs.",
                        name,
                        output));
            }
        }

        // Verify that the timer name is unique:
        for (TimerInfo<Integer, O> integerOTimerInfo : timers) {
            if (integerOTimerInfo.name().equals(name)) {
                throw new IllegalArgumentException(String.format("Location already has a timer of the name '%s'.",
                                                                 name));
            }
        }

        // Ensure that our new timer can time out AND that its timeouts do not coincide with that of an existing one-shot timer:
        for (TimerInfo<Integer, O> t : timers) {
            if (!t.periodic()) {
                if (initial > t.initial()) {
                    throw new IllegalArgumentException(String.format(
                            "The initial value %d of '%s' exceeds that of a one-shot timer; will never time out.",
                            initial,
                            name));
                }
                if (periodic && t.initial() % initial == 0) {
                    // Our new periodic timer will time out at the same time as the existing one-shot timer.
                    // This makes the model non-deterministic and is not allowed:
                    throw new IllegalArgumentException(String.format(
                            "The timer '%s' times out at the same time as a one-shot timer (%d).",
                            name,
                            initial));
                }
            }
        }
        if (!periodic) {
            // Our new one-shot timer is the one-shot timer with the highest initial value (or the only one).
            // Check that no timer with a lower initial value will time out at the same time:
            for (TimerInfo<Integer, O> timer : timers) {
                if (timer.initial() <= initial && initial % timer.initial() == 0) {
                    throw new IllegalArgumentException(String.format(
                            "The existing timer '%s' times out at the same time as the new one-shot timer (%d).",
                            timer.name(),
                            initial));
                }
            }
        }
    }

    @Override
    public void addPeriodicTimer(Integer location, String name, long initial, List<O> outputs) {
        final List<TimerInfo<Integer, O>> localTimers =
                this.sortedTimers.computeIfAbsent(location, k -> new ArrayList<>());

        ensureThatCanAddTimer(localTimers, name, initial, outputs, true);
        localTimers.add(new TimerInfo<>(name, initial, outputs, location, true));
        localTimers.sort(Comparator.comparingLong(TimerInfo::initial));
    }

    @Override
    public void addOneShotTimer(Integer location, String name, long initial, List<O> outputs, Integer target) {
        final List<TimerInfo<Integer, O>> localTimers =
                this.sortedTimers.computeIfAbsent(location, k -> new ArrayList<>());

        ensureThatCanAddTimer(localTimers, name, initial, outputs, false);
        localTimers.add(new TimerInfo<>(name, initial, outputs, target, false));
        localTimers.sort(Comparator.comparingLong(TimerInfo::initial));

        // Remove all timers with higher initial value, as these can no longer time out:
        localTimers.removeIf(t -> t.initial() > initial);
    }

    @Override
    public void removeTimer(Integer location, String timerName) {
        final List<TimerInfo<Integer, O>> localTimers = this.sortedTimers.get(location);
        if (localTimers != null) {
            localTimers.removeIf(t -> t.name().equals(timerName));
        }
    }

    @Override
    public void addLocalReset(Integer location, I input) {
        // Ensure that input causes self-loop:
        final Integer target = this.getSuccessor(location, input);
        if (target == null || !target.equals(location)) {
            throw new IllegalArgumentException("Provided input is not defined or does not trigger a self-loop.");
        }

        resets.computeIfAbsent(location, k -> new HashSet<>()).add(input);
    }

    @Override
    public void removeLocalReset(Integer location, I input) {
        final Set<I> localResets = resets.get(location);
        if (localResets != null) {
            localResets.remove(input);
        }
    }

    @Override
    public void clear() {
        super.clear();
        this.sortedTimers.clear();
        this.resets.clear();
    }

    @Override
    public Graph<Integer, Triple<SymbolicInput<I>, O, Integer>> graphView() {
        return MutableMMLT.super.graphView();
    }

    public static class Creator<I, O> implements AutomatonCreator<CompactMMLT<I, O>, I> {

        private final O silentOutput;
        private final SymbolCombiner<O> outputCombiner;

        public Creator(O silentOutput, SymbolCombiner<O> outputCombiner) {
            this.silentOutput = silentOutput;
            this.outputCombiner = outputCombiner;
        }

        @Override
        public CompactMMLT<I, O> createAutomaton(Alphabet<I> alphabet, int numStatesHint) {
            return new CompactMMLT<>(alphabet, numStatesHint, silentOutput, outputCombiner);
        }

        @Override
        public CompactMMLT<I, O> createAutomaton(Alphabet<I> alphabet) {
            return new CompactMMLT<>(alphabet, silentOutput, outputCombiner);
        }
    }
}

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.Collections;
20	import java.util.Comparator;
21	import java.util.HashMap;
22	import java.util.HashSet;
23	import java.util.List;
24	import java.util.Map;
25	import java.util.Set;
26
27	import net.automatalib.alphabet.Alphabet;
28	import net.automatalib.automaton.AutomatonCreator;
29	import net.automatalib.automaton.impl.CompactTransition;
30	import net.automatalib.automaton.mmlt.MMLTSemantics;
31	import net.automatalib.automaton.mmlt.MutableMMLT;
32	import net.automatalib.automaton.mmlt.SymbolCombiner;
33	import net.automatalib.automaton.mmlt.TimerInfo;
34	import net.automatalib.automaton.transducer.impl.CompactMealy;
35	import net.automatalib.common.util.Triple;
36	import net.automatalib.graph.Graph;
37	import net.automatalib.symbol.time.SymbolicInput;
38
39	/**
40	* Implements a {@link MutableMMLT} by storing adjacency information in compact arrays.
41	*
42	* @param <I>
43	* input symbol type (of non-delaying inputs)
44	* @param <O>
45	* output symbol type
46	*/
47	public class CompactMMLT<I, O> extends CompactMealy<I, O> implements MutableMMLT<Integer, I, CompactTransition<O>, O> {
48
49	private final Map<Integer, List<TimerInfo<Integer, O>>> sortedTimers; // location -> (sorted timers)
50	private final Map<Integer, Set<I>> resets; // location -> inputs (that reset all timers)
51
52	private final O silentOutput;
53	private final SymbolCombiner<O> outputCombiner;
54
55	/**
56	* Initializes a new CompactMMLT.
57	*
58	* @param alphabet
59	* the alphabet of non-delaying inputs
60	* @param silentOutput
61	* the silent output used by this MMLT
62	* @param outputCombiner
63	* the combiner function for simultaneous timeouts of periodic timers
64	*/
65	public CompactMMLT(Alphabet<I> alphabet, O silentOutput, SymbolCombiner<O> outputCombiner) {
66	this(alphabet, DEFAULT_INIT_CAPACITY, silentOutput, outputCombiner);	2✔
67	}	2✔
68
69	/**
70	* Initializes a new CompactMMLT.
71	*
72	* @param alphabet
73	* the alphabet of non-delaying inputs
74	* @param sizeHint
75	* a size hint to better allocate internal memory
76	* @param silentOutput
77	* the silent output used by this MMLT
78	* @param outputCombiner
79	* the combiner function for simultaneous timeouts of periodic timers
80	*/
81	public CompactMMLT(Alphabet<I> alphabet, int sizeHint, O silentOutput, SymbolCombiner<O> outputCombiner) {
82	super(alphabet, sizeHint);	2✔
83
84	this.sortedTimers = new HashMap<>();	2✔
85	this.resets = new HashMap<>();	2✔
86
87	this.silentOutput = silentOutput;	2✔
88	this.outputCombiner = outputCombiner;	2✔
89	}	2✔
90
91	@Override
92	public O getSilentOutput() {
93	return this.silentOutput;	2✔
94	}
95
96	@Override
97	public SymbolCombiner<O> getOutputCombiner() {
98	return this.outputCombiner;	2✔
99	}
100
101	@Override
102	public boolean isLocalReset(Integer location, I input) {
103	return this.resets.getOrDefault(location, Collections.emptySet()).contains(input);	2✔
104	}
105
106	@Override
107	public List<TimerInfo<Integer, O>> getSortedTimers(Integer location) {
108	return Collections.unmodifiableList(this.sortedTimers.getOrDefault(location, Collections.emptyList()));	2✔
109	}
110
111	@Override
112	public MMLTSemantics<Integer, I, ?, O> getSemantics() {
113	return new DefaultMMLTSemantics<>(this);	2✔
114	}
115
116	private void ensureThatCanAddTimer(List<TimerInfo<Integer, O>> timers,
117	String name,
118	long initial,
119	List<O> outputs,
120	boolean periodic) {
121	if (outputs.isEmpty() \|\| outputs.contains(silentOutput)) {	2✔
122	throw new IllegalArgumentException(String.format("Timer '%s': outputs are empty or contain silent output.",	2✔
123	name));
124	}
125
126	for (O output : outputs) {	2✔
127	if (getOutputCombiner().isCombinedSymbol(output)) {	2✔
128	throw new IllegalArgumentException(String.format(	2✔
129	"Timer '%s': output '%s' is a combined symbol. You must only provide atomic outputs.",
130	name,
131	output));
132	}
133	}	2✔
134
135	// Verify that the timer name is unique:
136	for (TimerInfo<Integer, O> integerOTimerInfo : timers) {	2✔
137	if (integerOTimerInfo.name().equals(name)) {	2✔
138	throw new IllegalArgumentException(String.format("Location already has a timer of the name '%s'.",	2✔
139	name));
140	}
141	}	2✔
142
143	// Ensure that our new timer can time out AND that its timeouts do not coincide with that of an existing one-shot timer:
144	for (TimerInfo<Integer, O> t : timers) {	2✔
145	if (!t.periodic()) {	2✔
146	if (initial > t.initial()) {	2✔
147	throw new IllegalArgumentException(String.format(	2✔
148	"The initial value %d of '%s' exceeds that of a one-shot timer; will never time out.",
149	initial,	2✔
150	name));
151	}
152	if (periodic && t.initial() % initial == 0) {	2✔
153	// Our new periodic timer will time out at the same time as the existing one-shot timer.
154	// This makes the model non-deterministic and is not allowed:
155	throw new IllegalArgumentException(String.format(	2✔
156	"The timer '%s' times out at the same time as a one-shot timer (%d).",
157	name,
158	initial));	2✔
159	}
160	}
161	}	2✔
162	if (!periodic) {	2✔
163	// Our new one-shot timer is the one-shot timer with the highest initial value (or the only one).
164	// Check that no timer with a lower initial value will time out at the same time:
165	for (TimerInfo<Integer, O> timer : timers) {	2✔
166	if (timer.initial() <= initial && initial % timer.initial() == 0) {	2✔
167	throw new IllegalArgumentException(String.format(	2✔
168	"The existing timer '%s' times out at the same time as the new one-shot timer (%d).",
169	timer.name(),	2✔
170	initial));	2✔
171	}
172	}	2✔
173	}
174	}	2✔
175
176	@Override
177	public void addPeriodicTimer(Integer location, String name, long initial, List<O> outputs) {
178	final List<TimerInfo<Integer, O>> localTimers =	2✔
179	this.sortedTimers.computeIfAbsent(location, k -> new ArrayList<>());	2✔
180
181	ensureThatCanAddTimer(localTimers, name, initial, outputs, true);	2✔
182	localTimers.add(new TimerInfo<>(name, initial, outputs, location, true));	2✔
183	localTimers.sort(Comparator.comparingLong(TimerInfo::initial));	2✔
184	}	2✔
185
186	@Override
187	public void addOneShotTimer(Integer location, String name, long initial, List<O> outputs, Integer target) {
188	final List<TimerInfo<Integer, O>> localTimers =	2✔
189	this.sortedTimers.computeIfAbsent(location, k -> new ArrayList<>());	2✔
190
191	ensureThatCanAddTimer(localTimers, name, initial, outputs, false);	2✔
192	localTimers.add(new TimerInfo<>(name, initial, outputs, target, false));	2✔
193	localTimers.sort(Comparator.comparingLong(TimerInfo::initial));	2✔
194
195	// Remove all timers with higher initial value, as these can no longer time out:
196	localTimers.removeIf(t -> t.initial() > initial);	2✔
197	}	2✔
198
199	@Override
200	public void removeTimer(Integer location, String timerName) {
201	final List<TimerInfo<Integer, O>> localTimers = this.sortedTimers.get(location);	1✔
202	if (localTimers != null) {	1✔
203	localTimers.removeIf(t -> t.name().equals(timerName));	1✔
204	}
205	}	1✔
206
207	@Override
208	public void addLocalReset(Integer location, I input) {
209	// Ensure that input causes self-loop:
210	final Integer target = this.getSuccessor(location, input);	2✔
211	if (target == null \|\| !target.equals(location)) {	2✔
NEW 212	throw new IllegalArgumentException("Provided input is not defined or does not trigger a self-loop.");	×
213	}
214
215	resets.computeIfAbsent(location, k -> new HashSet<>()).add(input);	2✔
216	}	2✔
217
218	@Override
219	public void removeLocalReset(Integer location, I input) {
220	final Set<I> localResets = resets.get(location);	1✔
221	if (localResets != null) {	1✔
222	localResets.remove(input);	1✔
223	}
224	}	1✔
225
226	@Override
227	public void clear() {
228	super.clear();	2✔
229	this.sortedTimers.clear();	2✔
230	this.resets.clear();	2✔
231	}	2✔
232
233	@Override
234	public Graph<Integer, Triple<SymbolicInput<I>, O, Integer>> graphView() {
235	return MutableMMLT.super.graphView();	1✔
236	}
237
238	public static class Creator<I, O> implements AutomatonCreator<CompactMMLT<I, O>, I> {
239
240	private final O silentOutput;
241	private final SymbolCombiner<O> outputCombiner;
242
243	public Creator(O silentOutput, SymbolCombiner<O> outputCombiner) {	2✔
244	this.silentOutput = silentOutput;	2✔
245	this.outputCombiner = outputCombiner;	2✔
246	}	2✔
247
248	@Override
249	public CompactMMLT<I, O> createAutomaton(Alphabet<I> alphabet, int numStatesHint) {
250	return new CompactMMLT<>(alphabet, numStatesHint, silentOutput, outputCombiner);	2✔
251	}
252
253	@Override
254	public CompactMMLT<I, O> createAutomaton(Alphabet<I> alphabet) {
NEW 255	return new CompactMMLT<>(alphabet, silentOutput, outputCombiner);	×
256	}
257	}
258	}

LearnLib / automatalib / 19864403395

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