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;

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

import org.checkerframework.checker.nullness.qual.Nullable;

/**
 * A state configuration of an MMLT. A configuration is a tuple of an active location and the valuation of its timers.
 *
 * @param <S>
 *         location type
 * @param <O>
 *         output symbol type
 */
public final class State<S, O> {

    private final S location;

    private final List<TimerInfo<S, O>> sortedTimers;
    private final long[] timerValues;
    private final long[] initialValues;
    private final long minimumTimerValue;

    private final long entryDistance;

    /**
     * Initializes the entry configuration for the provided location, where all timers have their initial value.
     *
     * @param location
     *         the location
     * @param sortedTimers
     *         the timers of the location, sorted by initial value
     */
    public State(S location, List<TimerInfo<S, O>> sortedTimers) {
        this.location = location;

        this.sortedTimers = sortedTimers;

        this.initialValues = new long[sortedTimers.size()];
        this.timerValues = new long[sortedTimers.size()];
        this.minimumTimerValue = sortedTimers.isEmpty() ? 0 : sortedTimers.get(0).initial();

        for (int i = 0; i < sortedTimers.size(); i++) {
            final long initial = sortedTimers.get(i).initial();
            initialValues[i] = initial;
            timerValues[i] = initial; // reset
        }

        this.entryDistance = 0;
    }

    private State(S location,
                  List<TimerInfo<S, O>> sortedTimers,
                  long[] timerValues,
                  long[] initialValues,
                  long entryDistance,
                  long minimumTimerValue) {
        this.location = location;
        this.sortedTimers = sortedTimers;

        this.initialValues = initialValues;
        this.minimumTimerValue = minimumTimerValue;
        this.timerValues = timerValues;
        this.entryDistance = entryDistance;
    }

    /**
     * Returns the MMLT location of this state.
     *
     * @return the location
     */
    public S getLocation() {
        return location;
    }

    /**
     * Returns the entry distance. This is the minimal number of time steps required to reach this configuration from
     * the entry configuration.
     *
     * @return the entry distance
     */
    public long getEntryDistance() {
        return entryDistance;
    }

    /**
     * Indicates if this is the entry configuration of the location. A configuration is the entry configuration if all
     * timers have their initial value.
     *
     * @return {@code true} if this is the entry configuration, {@code false} otherwise
     */
    public boolean isEntryConfig() {
        return this.entryDistance == 0;
    }

    /**
     * Indicates if this configuration is stable. A configuration is stable if its entry distance is less than the
     * initial value of the timer with the lowest initial value of the location. If the location has no timers, its only
     * configuration is its entry configuration, which is always stable.
     *
     * @return {@code true} if stable, {@code false} otherwise
     */
    public boolean isStableConfig() {
        return this.entryDistance == 0 || this.entryDistance < minimumTimerValue;
    }

    /**
     * Returns a copy of {@code this} state with all timers reset to their initial values.
     *
     * @return the new state with all its timers reset
     */
    public State<S, O> resetTimers() {
        return new State<>(location, sortedTimers, initialValues.clone(), initialValues, 0, minimumTimerValue);
    }

    /**
     * Returns all timers that time out in the least number of time steps.
     *
     * @return the timed out timers
     */
    public @Nullable TimeoutPair<S, O> getNextExpiringTimers() {
        if (sortedTimers.isEmpty()) {
            return null;
        } else if (this.sortedTimers.size() == 1) {
            // No need to collect timeouts - there is only one timer that can expire.
            // The time to its timeout is its remaining value:
            return new TimeoutPair<>(this.timerValues[0], Collections.singletonList(this.sortedTimers.get(0)));

        } else {
            // Multiple timers may time out at the same time.
            // Get minimum distance to next timeout:
            long minValue = Long.MAX_VALUE;
            for (int i = 0; i < sortedTimers.size(); i++) {
                if (timerValues[i] < minValue) {
                    minValue = timerValues[i];
                }
            }

            assert minValue != Long.MAX_VALUE;

            // Collect info of all timers that time out then:
            List<TimerInfo<S, O>> expiringTimers = new ArrayList<>();
            for (int i = 0; i < sortedTimers.size(); i++) {
                if (timerValues[i] == minValue) {
                    expiringTimers.add(this.sortedTimers.get(i));
                }
            }

            // Return timed-out timers:
            return new TimeoutPair<>(minValue, expiringTimers);
        }
    }

    /**
     * Returns a new state in which all timer values have been decreased by the specified amount. This amount must be at
     * most the time to the next timeout. If this sets a timer to zero, this timer is immediately reset to its initial
     * value.
     *
     * @param delay
     *         the value by which to decrement the current timers
     *
     * @return the new state with updated timers
     */
    public State<S, O> decrement(long delay) {
        int timerResets = 0;
        int oneShotResets = 0;

        final long[] newTimerValues = this.timerValues.clone();

        for (int i = 0; i < this.sortedTimers.size(); i++) {
            long newValue = newTimerValues[i] - delay;

            if (newValue < 0) {
                throw new IllegalArgumentException("Can only advance to next timeout.");
            } else if (newValue == 0) {
                if (!sortedTimers.get(i).periodic()) {
                    oneShotResets += 1;
                }

                newValue = initialValues[i];
                timerResets += 1;
            }
            newTimerValues[i] = newValue;
        }

        assert oneShotResets <= 1;
        final long newEntryDistance;

        if (timerResets == this.sortedTimers.size() || oneShotResets == 1) {
            // reset all timers -> back at entry config:
            newEntryDistance = 0;
        } else {
            newEntryDistance = this.entryDistance + delay;
        }

        return new State<>(location, sortedTimers, newTimerValues, initialValues, newEntryDistance, minimumTimerValue);
    }

    @Override
    public boolean equals(@Nullable Object o) {
        return this == o || o instanceof State<?, ?> that && this.minimumTimerValue == that.minimumTimerValue &&
                            entryDistance == that.entryDistance && Objects.equals(location, that.location) &&
                            Objects.equals(sortedTimers, that.sortedTimers) &&
                            Arrays.equals(timerValues, that.timerValues) &&
                            Arrays.equals(initialValues, that.initialValues);
    }

    @Override
    public int hashCode() {
        return Objects.hash(location,
                            sortedTimers,
                            Arrays.hashCode(timerValues),
                            Arrays.hashCode(initialValues),
                            minimumTimerValue,
                            entryDistance);
    }

    @Override
    public String toString() {
        return String.format("[%s,%d]", this.location, this.entryDistance);
    }
}

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;
17
18	import java.util.ArrayList;
19	import java.util.Arrays;
20	import java.util.Collections;
21	import java.util.List;
22	import java.util.Objects;
23
24	import org.checkerframework.checker.nullness.qual.Nullable;
25
26	/**
27	* A state configuration of an MMLT. A configuration is a tuple of an active location and the valuation of its timers.
28	*
29	* @param <S>
30	* location type
31	* @param <O>
32	* output symbol type
33	*/
34	public final class State<S, O> {	1✔
35
36	private final S location;
37
38	private final List<TimerInfo<S, O>> sortedTimers;
39	private final long[] timerValues;
40	private final long[] initialValues;
41	private final long minimumTimerValue;
42
43	private final long entryDistance;
44
45	/**
46	* Initializes the entry configuration for the provided location, where all timers have their initial value.
47	*
48	* @param location
49	* the location
50	* @param sortedTimers
51	* the timers of the location, sorted by initial value
52	*/
53	public State(S location, List<TimerInfo<S, O>> sortedTimers) {	1✔
54	this.location = location;	1✔
55
56	this.sortedTimers = sortedTimers;	1✔
57
58	this.initialValues = new long[sortedTimers.size()];	1✔
59	this.timerValues = new long[sortedTimers.size()];	1✔
60	this.minimumTimerValue = sortedTimers.isEmpty() ? 0 : sortedTimers.get(0).initial();	1✔
61
62	for (int i = 0; i < sortedTimers.size(); i++) {	1✔
63	final long initial = sortedTimers.get(i).initial();	1✔
64	initialValues[i] = initial;	1✔
65	timerValues[i] = initial; // reset	1✔
66	}
67
68	this.entryDistance = 0;	1✔
69	}	1✔
70
71	private State(S location,
72	List<TimerInfo<S, O>> sortedTimers,
73	long[] timerValues,
74	long[] initialValues,
75	long entryDistance,
76	long minimumTimerValue) {	1✔
77	this.location = location;	1✔
78	this.sortedTimers = sortedTimers;	1✔
79
80	this.initialValues = initialValues;	1✔
81	this.minimumTimerValue = minimumTimerValue;	1✔
82	this.timerValues = timerValues;	1✔
83	this.entryDistance = entryDistance;	1✔
84	}	1✔
85
86	/**
87	* Returns the MMLT location of this state.
88	*
89	* @return the location
90	*/
91	public S getLocation() {
92	return location;	1✔
93	}
94
95	/**
96	* Returns the entry distance. This is the minimal number of time steps required to reach this configuration from
97	* the entry configuration.
98	*
99	* @return the entry distance
100	*/
101	public long getEntryDistance() {
102	return entryDistance;	1✔
103	}
104
105	/**
106	* Indicates if this is the entry configuration of the location. A configuration is the entry configuration if all
107	* timers have their initial value.
108	*
109	* @return {@code true} if this is the entry configuration, {@code false} otherwise
110	*/
111	public boolean isEntryConfig() {
112	return this.entryDistance == 0;	1✔
113	}
114
115	/**
116	* Indicates if this configuration is stable. A configuration is stable if its entry distance is less than the
117	* initial value of the timer with the lowest initial value of the location. If the location has no timers, its only
118	* configuration is its entry configuration, which is always stable.
119	*
120	* @return {@code true} if stable, {@code false} otherwise
121	*/
122	public boolean isStableConfig() {
123	return this.entryDistance == 0 \|\| this.entryDistance < minimumTimerValue;	1✔
124	}
125
126	/**
127	* Returns a copy of {@code this} state with all timers reset to their initial values.
128	*
129	* @return the new state with all its timers reset
130	*/
131	public State<S, O> resetTimers() {
132	return new State<>(location, sortedTimers, initialValues.clone(), initialValues, 0, minimumTimerValue);	1✔
133	}
134
135	/**
136	* Returns all timers that time out in the least number of time steps.
137	*
138	* @return the timed out timers
139	*/
140	public @Nullable TimeoutPair<S, O> getNextExpiringTimers() {
141	if (sortedTimers.isEmpty()) {	1✔
142	return null;	1✔
143	} else if (this.sortedTimers.size() == 1) {	1✔
144	// No need to collect timeouts - there is only one timer that can expire.
145	// The time to its timeout is its remaining value:
146	return new TimeoutPair<>(this.timerValues[0], Collections.singletonList(this.sortedTimers.get(0)));	1✔
147
148	} else {
149	// Multiple timers may time out at the same time.
150	// Get minimum distance to next timeout:
151	long minValue = Long.MAX_VALUE;	1✔
152	for (int i = 0; i < sortedTimers.size(); i++) {	1✔
153	if (timerValues[i] < minValue) {	1✔
154	minValue = timerValues[i];	1✔
155	}
156	}
157
158	assert minValue != Long.MAX_VALUE;	1✔
159
160	// Collect info of all timers that time out then:
161	List<TimerInfo<S, O>> expiringTimers = new ArrayList<>();	1✔
162	for (int i = 0; i < sortedTimers.size(); i++) {	1✔
163	if (timerValues[i] == minValue) {	1✔
164	expiringTimers.add(this.sortedTimers.get(i));	1✔
165	}
166	}
167
168	// Return timed-out timers:
169	return new TimeoutPair<>(minValue, expiringTimers);	1✔
170	}
171	}
172
173	/**
174	* Returns a new state in which all timer values have been decreased by the specified amount. This amount must be at
175	* most the time to the next timeout. If this sets a timer to zero, this timer is immediately reset to its initial
176	* value.
177	*
178	* @param delay
179	* the value by which to decrement the current timers
180	*
181	* @return the new state with updated timers
182	*/
183	public State<S, O> decrement(long delay) {
184	int timerResets = 0;	1✔
185	int oneShotResets = 0;	1✔
186
187	final long[] newTimerValues = this.timerValues.clone();	1✔
188
189	for (int i = 0; i < this.sortedTimers.size(); i++) {	1✔
190	long newValue = newTimerValues[i] - delay;	1✔
191
192	if (newValue < 0) {	1✔
NEW 193	throw new IllegalArgumentException("Can only advance to next timeout.");	×
194	} else if (newValue == 0) {	1✔
195	if (!sortedTimers.get(i).periodic()) {	1✔
NEW 196	oneShotResets += 1;	×
197	}
198
199	newValue = initialValues[i];	1✔
200	timerResets += 1;	1✔
201	}
202	newTimerValues[i] = newValue;	1✔
203	}
204
205	assert oneShotResets <= 1;	1✔
206	final long newEntryDistance;
207
208	if (timerResets == this.sortedTimers.size() \|\| oneShotResets == 1) {	1✔
209	// reset all timers -> back at entry config:
210	newEntryDistance = 0;	1✔
211	} else {
212	newEntryDistance = this.entryDistance + delay;	1✔
213	}
214
215	return new State<>(location, sortedTimers, newTimerValues, initialValues, newEntryDistance, minimumTimerValue);	1✔
216	}
217
218	@Override
219	public boolean equals(@Nullable Object o) {
220	return this == o \|\| o instanceof State<?, ?> that && this.minimumTimerValue == that.minimumTimerValue &&	1✔
221	entryDistance == that.entryDistance && Objects.equals(location, that.location) &&	1✔
222	Objects.equals(sortedTimers, that.sortedTimers) &&	1✔
223	Arrays.equals(timerValues, that.timerValues) &&	1✔
224	Arrays.equals(initialValues, that.initialValues);	1✔
225	}
226
227	@Override
228	public int hashCode() {
229	return Objects.hash(location,	1✔
230	sortedTimers,
231	Arrays.hashCode(timerValues),	1✔
232	Arrays.hashCode(initialValues),	1✔
233	minimumTimerValue,	1✔
234	entryDistance);	1✔
235	}
236
237	@Override
238	public String toString() {
NEW 239	return String.format("[%s,%d]", this.location, this.entryDistance);	×
240	}
241	}

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