28013097648

Committed 23 Jun 2026 08:30AM UTC coverage: 92.876% (-0.1%) from 93.007%

Build # 28013097648

Build Type

Pull #103

github

Committed by

web-flow

Commit Message

Merge 1553bac46 into 87b9d660b

Pull Request Pull Request #103: Distinguish between structural and semantic interpretations of automata

Coverage Stats

268 of 313 new or added lines in 46 files covered. (85.62%)

5 existing lines in 2 files now uncovered.

17560 of 18907 relevant lines covered (92.88%)

1.72 hits per line

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

75.0

/api/src/main/java/net/automatalib/automaton/abstraction/DeterministicAbstractions.java

/* Copyright (C) 2013-2026 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.abstraction;

import java.util.function.IntFunction;

import net.automatalib.automaton.DeterministicAutomaton;
import org.checkerframework.checker.nullness.qual.Nullable;

/**
 * Abstractions for {@link DeterministicAutomaton}s.
 */
public interface DeterministicAbstractions {

    /**
     * Base interface for {@link SimpleDeterministicAbstractions.IntAbstraction integer abstractions} of a
     * {@link DeterministicAutomaton}.
     *
     * @param <T>
     *         transition type
     */
    interface IntAbstraction<T> extends SimpleDeterministicAbstractions.IntAbstraction {

        /**
         * Retrieves the (abstracted) successor of a transition object.
         *
         * @param transition
         *         the transition object
         *
         * @return the integer representing the successor of the given transition
         */
        int getIntSuccessor(T transition);
    }

    /**
     * Interface for {@link SimpleDeterministicAbstractions.StateIntAbstraction state integer abstractions} of a
     * {@link DeterministicAutomaton}.
     *
     * @param <I>
     *         input symbol type
     * @param <T>
     *         transition type
     */
    interface StateIntAbstraction<I, T>
            extends IntAbstraction<T>, SimpleDeterministicAbstractions.StateIntAbstraction<I> {

        @Override
        default int getSuccessor(int state, I input) {
            T trans = getTransition(state, input);
            if (trans == null) {
                return INVALID_STATE;
            }
            return getIntSuccessor(trans);
        }

        /**
         * Retrieves the outgoing transition for an (abstracted) source state and input symbol, or returns {@code null}
         * if the automaton has no transition for this state and input.
         *
         * @param state
         *         the integer representing the source state
         * @param input
         *         the input symbol
         *
         * @return the outgoing transition, or {@code null}
         */
        @Nullable
        T getTransition(int state, I input);

    }

    /**
     * Interface for {@link SimpleDeterministicAbstractions.FullIntAbstraction full integer abstractions} of a
     * {@link DeterministicAutomaton}.
     *
     * @param <T>
     *         transition type
     */
    interface FullIntAbstraction<T> extends IntAbstraction<T>, SimpleDeterministicAbstractions.FullIntAbstraction {

        @Override
        default int getSuccessor(int state, int input) {
            T trans = getTransition(state, input);
            if (trans == null) {
                return INVALID_STATE;
            }
            return getIntSuccessor(trans);
        }

        /**
         * Retrieves the outgoing transition for an (abstracted) source state and (abstracted) input symbol, or returns
         * {@code null} if the automaton has no transition for this state and input.
         *
         * @param state
         *         the integer representing the source state
         * @param input
         *         the integer representing the input symbol
         *
         * @return the outgoing transition, or {@code null}
         */
        @Nullable
        T getTransition(int state, int input);

    }

    class StateIntAbstractionImpl<S, I, T, A extends DeterministicAutomaton<S, I, T>>
            extends SimpleDeterministicAbstractions.StateIntAbstractionImpl<S, I, A>
            implements StateIntAbstraction<I, T> {

        public StateIntAbstractionImpl(A automaton) {
            super(automaton);
        }

        @Override
        public int getIntSuccessor(T transition) {
            return stateToInt(automaton.getSuccessor(transition));
        }

        @Override
        public @Nullable T getTransition(int state, I input) {
            return automaton.getTransition(intToState(state), input);
        }
    }

    class FullIntAbstractionImpl<I, T, A extends StateIntAbstraction<I, T>>
            extends SimpleDeterministicAbstractions.FullIntAbstractionImpl<I, A> implements FullIntAbstraction<T> {

        public FullIntAbstractionImpl(A stateAbstraction, int numInputs, IntFunction<? extends I> symMapping) {
            super(stateAbstraction, numInputs, symMapping);
        }

        @Override
        public @Nullable T getTransition(int state, int input) {
            return stateAbstraction.getTransition(state, intToSym(input));
        }

        @Override
        public int getIntSuccessor(T transition) {
            return stateAbstraction.getIntSuccessor(transition);
        }
    }
}

1	/* Copyright (C) 2013-2026 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.abstraction;
17
18	import java.util.function.IntFunction;
19
20	import net.automatalib.automaton.DeterministicAutomaton;
21	import org.checkerframework.checker.nullness.qual.Nullable;
22
23	/**
24	* Abstractions for {@link DeterministicAutomaton}s.
25	*/
26	public interface DeterministicAbstractions {
27
28	/**
29	* Base interface for {@link SimpleDeterministicAbstractions.IntAbstraction integer abstractions} of a
30	* {@link DeterministicAutomaton}.
31	*
32	* @param <T>
33	* transition type
34	*/
35	interface IntAbstraction<T> extends SimpleDeterministicAbstractions.IntAbstraction {
36
37	/**
38	* Retrieves the (abstracted) successor of a transition object.
39	*
40	* @param transition
41	* the transition object
42	*
43	* @return the integer representing the successor of the given transition
44	*/
45	int getIntSuccessor(T transition);
46	}
47
48	/**
49	* Interface for {@link SimpleDeterministicAbstractions.StateIntAbstraction state integer abstractions} of a
50	* {@link DeterministicAutomaton}.
51	*
52	* @param <I>
53	* input symbol type
54	* @param <T>
55	* transition type
56	*/
57	interface StateIntAbstraction<I, T>
58	extends IntAbstraction<T>, SimpleDeterministicAbstractions.StateIntAbstraction<I> {
59
60	@Override
61	default int getSuccessor(int state, I input) {
NEW 62	T trans = getTransition(state, input);	×
NEW 63	if (trans == null) {	×
NEW 64	return INVALID_STATE;	×
65	}
NEW 66	return getIntSuccessor(trans);	×
67	}
68
69	/**
70	* Retrieves the outgoing transition for an (abstracted) source state and input symbol, or returns {@code null}
71	* if the automaton has no transition for this state and input.
72	*
73	* @param state
74	* the integer representing the source state
75	* @param input
76	* the input symbol
77	*
78	* @return the outgoing transition, or {@code null}
79	*/
80	@Nullable
81	T getTransition(int state, I input);
82
83	}
84
85	/**
86	* Interface for {@link SimpleDeterministicAbstractions.FullIntAbstraction full integer abstractions} of a
87	* {@link DeterministicAutomaton}.
88	*
89	* @param <T>
90	* transition type
91	*/
92	interface FullIntAbstraction<T> extends IntAbstraction<T>, SimpleDeterministicAbstractions.FullIntAbstraction {
93
94	@Override
95	default int getSuccessor(int state, int input) {
96	T trans = getTransition(state, input);	1✔
97	if (trans == null) {	1✔
98	return INVALID_STATE;	1✔
99	}
100	return getIntSuccessor(trans);	1✔
101	}
102
103	/**
104	* Retrieves the outgoing transition for an (abstracted) source state and (abstracted) input symbol, or returns
105	* {@code null} if the automaton has no transition for this state and input.
106	*
107	* @param state
108	* the integer representing the source state
109	* @param input
110	* the integer representing the input symbol
111	*
112	* @return the outgoing transition, or {@code null}
113	*/
114	@Nullable
115	T getTransition(int state, int input);
116
117	}
118
119	class StateIntAbstractionImpl<S, I, T, A extends DeterministicAutomaton<S, I, T>>
120	extends SimpleDeterministicAbstractions.StateIntAbstractionImpl<S, I, A>
121	implements StateIntAbstraction<I, T> {
122
123	public StateIntAbstractionImpl(A automaton) {
124	super(automaton);	1✔
125	}	1✔
126
127	@Override
128	public int getIntSuccessor(T transition) {
129	return stateToInt(automaton.getSuccessor(transition));	1✔
130	}
131
132	@Override
133	public @Nullable T getTransition(int state, I input) {
134	return automaton.getTransition(intToState(state), input);	1✔
135	}
136	}
137
138	class FullIntAbstractionImpl<I, T, A extends StateIntAbstraction<I, T>>
139	extends SimpleDeterministicAbstractions.FullIntAbstractionImpl<I, A> implements FullIntAbstraction<T> {
140
141	public FullIntAbstractionImpl(A stateAbstraction, int numInputs, IntFunction<? extends I> symMapping) {
142	super(stateAbstraction, numInputs, symMapping);	1✔
143	}	1✔
144
145	@Override
146	public @Nullable T getTransition(int state, int input) {
147	return stateAbstraction.getTransition(state, intToSym(input));	1✔
148	}
149
150	@Override
151	public int getIntSuccessor(T transition) {
152	return stateAbstraction.getIntSuccessor(transition);	1✔
153	}
154	}
155	}

LearnLib / automatalib / 28013097648

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