29161451305

Committed 11 Jul 2026 03:18PM UTC coverage: 93.029% (+0.02%) from 93.007%

Build # 29161451305

Build Type

push

github

Committed by

mtf90

Commit Message

generify some nomenclature

Coverage Stats

6 of 6 new or added lines in 1 file covered. (100.0%)

10 existing lines in 3 files now uncovered.

17562 of 18878 relevant lines covered (93.03%)

1.73 hits per line

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

93.42

/util/src/main/java/net/automatalib/util/automaton/procedural/SBAs.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.util.automaton.procedural;

import java.util.Collection;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Map;
import java.util.Map.Entry;
import java.util.Objects;
import java.util.Set;
import java.util.function.Function;

import net.automatalib.alphabet.Alphabet;
import net.automatalib.alphabet.ProceduralInputAlphabet;
import net.automatalib.automaton.fsa.DFA;
import net.automatalib.automaton.fsa.MutableDFA;
import net.automatalib.automaton.fsa.impl.CompactDFA;
import net.automatalib.automaton.procedural.SBA;
import net.automatalib.automaton.procedural.SPA;
import net.automatalib.automaton.procedural.SPMM;
import net.automatalib.automaton.procedural.impl.StackSPA;
import net.automatalib.common.util.HashUtil;
import net.automatalib.graph.ContextFreeModalProcessSystem;
import net.automatalib.modelchecking.ModelChecker;
import net.automatalib.ts.TransitionPredicate;
import net.automatalib.util.automaton.copy.AutomatonCopyMethod;
import net.automatalib.util.automaton.copy.AutomatonLowLevelCopy;
import net.automatalib.util.automaton.fsa.DFAs;
import net.automatalib.util.automaton.fsa.MutableDFAs;
import net.automatalib.util.automaton.predicate.TransitionPredicates;
import net.automatalib.word.Word;
import org.checkerframework.checker.nullness.qual.Nullable;

/**
 * Operations on {@link SBA}s.
 */
public final class SBAs {

    private SBAs() {
        // prevent instantiation
    }

    /**
     * Computes a set of access sequences and terminating sequences for a given {@link SBA}. This is a convenience
     * method for {@link #computeATSequences(SBA, ProceduralInputAlphabet)} that automatically uses the
     * {@link SBA#getInputAlphabet() input alphabet} of the given {@code sba}.
     *
     * @param sba
     *         the {@link SBA} for which the sequences should be computed
     * @param <I>
     *         input symbol type
     *
     * @return an {@link ATSequences} object which contains the respective sequences.
     *
     * @see #computeATSequences(SBA, ProceduralInputAlphabet)
     */
    public static <I> ATSequences<I> computeATSequences(SBA<?, I> sba) {
        return computeATSequences(sba, sba.getInputAlphabet());
    }

    /**
     * Computes a set of access sequences and terminating sequences for a given {@link SBA} limited to the symbols of
     * the given {@link ProceduralInputAlphabet}.
     *
     * @param sba
     *         the {@link SBA} for which the sequences should be computed
     * @param alphabet
     *         the {@link ProceduralInputAlphabet} whose symbols should be used for computing the respective sequences
     * @param <I>
     *         input symbol type
     *
     * @return an {@link ATSequences} object which contains the respective sequences.
     *
     * @see #computeAccessSequences(SBA, ProceduralInputAlphabet, Map)
     * @see #computeTerminatingSequences(SBA, ProceduralInputAlphabet)
     */
    public static <I> ATSequences<I> computeATSequences(SBA<?, I> sba, ProceduralInputAlphabet<I> alphabet) {

        assert isValid(sba, alphabet);

        final Map<I, Word<I>> terminatingSequences = computeTerminatingSequences(sba, alphabet);
        final Map<I, Word<I>> accessSequences = computeAccessSequences(sba, alphabet, terminatingSequences);

        return new ATSequences<>(accessSequences, terminatingSequences);
    }

    /**
     * Computes for a given {@link SBA} a set of terminating sequences using the given
     * {@link ProceduralInputAlphabet alphabet}. Terminating sequences transfer a procedure from its initial state to a
     * returnable state. This method furthermore checks that the hierarchy of calls is well-defined, i.e. it only
     * includes procedural invocations <i>p</i> for determining a terminating sequence if <i>p</i> has a valid
     * terminating sequence itself.
     *
     * @param sba
     *         the {@link SBA} to analyze
     * @param alphabet
     *         the {@link ProceduralInputAlphabet} whose symbols should be used for determining the terminating
     *         sequences
     * @param <I>
     *         input symbol type
     *
     * @return A map from procedures (restricted to the call symbols of the given alphabet) to the terminating
     * sequences. This map may be partial as some procedures may not have a well-defined terminating sequence for the
     * given alphabet.
     */
    public static <I> Map<I, Word<I>> computeTerminatingSequences(SBA<?, I> sba, ProceduralInputAlphabet<I> alphabet) {
        final Word<I> returnWord = Word.fromLetter(alphabet.getReturnSymbol());
        return ProceduralUtil.computeTerminatingSequences(sba.getProcedures(),
                                                          alphabet,
                                                          (dfa, trace) -> dfa.computeSuffixOutput(trace, returnWord));
    }

    /**
     * Computes for a given {@link SBA} a set of access sequences using the given
     * {@link ProceduralInputAlphabet alphabet}. An access sequence (for procedure <i>p</i>) transfers an {@link SBA}
     * from its initial state to a state that is able to successfully execute a run of <i>p</i>. This method furthermore
     * checks that potentially nested calls are well-defined, i.e. it only includes procedural invocations <i>p</i> for
     * determining access sequences if <i>p</i> has a valid terminating sequence and therefore can be expanded
     * correctly.
     *
     * @param sba
     *         the {@link SBA} to analyze
     * @param alphabet
     *         the {@link ProceduralInputAlphabet} whose symbols should be used for determining the access and return
     *         sequences
     * @param terminatingSequences
     *         a {@link Map} of call symbols to terminating sequences used to expand nested invocations in access
     *         sequences
     * @param <I>
     *         input symbol type
     *
     * @return A pair of maps from procedures (restricted to the call symbols of the given alphabet) to the
     * access/return sequences. These maps may be partial as some procedures may not have well-defined
     * access/terminating sequences for the given alphabet.
     */
    public static <I> Map<I, Word<I>> computeAccessSequences(SBA<?, I> sba,
                                                             ProceduralInputAlphabet<I> alphabet,
                                                             Map<I, Word<I>> terminatingSequences) {

        return ProceduralUtil.computeAccessSequences(sba.getProcedures(),
                                                     alphabet,
                                                     sba.getProceduralInputs(alphabet),
                                                     sba.getInitialProcedure(),
                                                     terminatingSequences,
                                                     DFA::accepts);
    }

    /**
     * Checks whether the given {@link SBA} is valid, This is a convenience method for
     * {@link #isValid(SBA, ProceduralInputAlphabet)} that uses the {@link SBA#getInputAlphabet() input alphabet} of the
     * given {@link SBA}.
     *
     * @param sba
     *         the {@link SBA} to analyze
     * @param <I>
     *         input symbol type
     *
     * @return {@code true} if {@code sba} is valid, {@code false} otherwise.
     *
     * @see #isValid(SBA, ProceduralInputAlphabet)
     */
    public static <I> boolean isValid(SBA<?, I> sba) {
        return isValid(sba, sba.getInputAlphabet());
    }

    /**
     * Checks whether the given {@link SBA} is valid with respect to the given {@link ProceduralInputAlphabet}, i.e.,
     * whether its {@link SBA#getProcedures() procedures} are prefix-closed, return-closed, and call-closed.
     * <p>
     * A procedure is considered prefix-closed iff any continuation of a rejected word is rejected as well.
     * <p>
     * A procedure is considered return-closed iff any continuation beyond the
     * {@link ProceduralInputAlphabet#getReturnSymbol() return symbol} is rejected.
     * <p>
     * A procedure is considered call-closed iff any continuation beyond a non-terminating
     * {@link ProceduralInputAlphabet#getCallAlphabet() call symbol} is rejected.
     *
     * @param sba
     *         the {@link SBA} to analyze
     * @param alphabet
     *         the {@link ProceduralInputAlphabet} whose symbols should be used for checking validity
     * @param <I>
     *         input symbol type
     *
     * @return {@code true} if {@code sba} is valid, {@code false} otherwise.
     */
    public static <I> boolean isValid(SBA<?, I> sba, ProceduralInputAlphabet<I> alphabet) {

        final Map<I, Word<I>> ts = computeTerminatingSequences(sba, alphabet);
        final Collection<I> proceduralInputs = sba.getProceduralInputs(alphabet);
        final Set<I> nonContinuableSymbols = new HashSet<>(alphabet.getCallAlphabet());
        nonContinuableSymbols.removeAll(ts.keySet());
        nonContinuableSymbols.retainAll(proceduralInputs);
        nonContinuableSymbols.add(alphabet.getReturnSymbol());

        for (DFA<?, I> p : sba.getProcedures().values()) {
            if (!DFAs.isPrefixClosed(p, proceduralInputs) ||
                !isCallAndReturnClosed(p, proceduralInputs, nonContinuableSymbols)) {
                return false;
            }
        }

        return true;
    }

    private static <S, I> boolean isCallAndReturnClosed(DFA<S, I> procedure,
                                                        Collection<I> inputs,
                                                        Collection<I> nonContinuableInputs) {

        for (S s : procedure) {
            for (I i : nonContinuableInputs) {
                final S succ = procedure.getSuccessor(s, i);
                final S toAnalyze;

                if (succ != null && procedure.isAccepting(succ)) {
                    toAnalyze = procedure.getSuccessor(succ, i);

                    // ensure that toAnalyze is effectively a "success sink"
                    for (I i2 : inputs) {
                        if (!Objects.equals(procedure.getSuccessor(succ, i2), toAnalyze)) {
                            return false;
                        }
                    }
                } else {
                    toAnalyze = succ;
                }

                if (toAnalyze != null && !isSink(procedure, inputs, toAnalyze)) {
                    return false;
                }
            }
        }

        return true;
    }

    private static <S, I> boolean isSink(DFA<S, I> dfa, Collection<I> inputs, S state) {

        if (dfa.isAccepting(state)) {
            return false;
        }

        for (I i : inputs) {
            final S succ = dfa.getSuccessor(state, i);
            if (succ != null && !Objects.equals(succ, state)) {
                return false;
            }
        }

        return true;
    }

    /**
     * Checks if the two given {@link SBA}s are equivalent, i.e. whether there exists a
     * {@link #findSeparatingWord(SBA, SBA, ProceduralInputAlphabet) separating word} for them.
     *
     * @param sba1
     *         the first {@link SPMM}
     * @param sba2
     *         the second {@link SPMM}
     * @param alphabet
     *         the {@link ProceduralInputAlphabet} whose symbols should be used for checking equivalence
     * @param <I>
     *         input symbol type
     *
     * @return {@code true} if the two {@link SBA}s are equivalent, {@code false} otherwise.
     *
     * @see #findSeparatingWord(SBA, SBA, ProceduralInputAlphabet)
     */
    public static <I> boolean testEquivalence(SBA<?, I> sba1, SBA<?, I> sba2, ProceduralInputAlphabet<I> alphabet) {
        return findSeparatingWord(sba1, sba2, alphabet) == null;
    }

    /**
     * Computes a separating word for the two given {@link SBA}s, if existent. A separating word is a {@link Word} such
     * that one {@link SBA} {@link SBA#accepts(Iterable) behaves} different from the other.
     *
     * @param sba1
     *         the first {@link SBA}
     * @param sba2
     *         the second {@link SBA}
     * @param alphabet
     *         the {@link ProceduralInputAlphabet} whose symbols should be considered for computing the separating word
     * @param <I>
     *         input symbol type
     *
     * @return a separating word, if existent, {@code null} otherwise.
     */
    public static <I> @Nullable Word<I> findSeparatingWord(SBA<?, I> sba1,
                                                           SBA<?, I> sba2,
                                                           ProceduralInputAlphabet<I> alphabet) {

        final ATSequences<I> at1 = computeATSequences(sba1, alphabet);
        final ATSequences<I> at2 = computeATSequences(sba2, alphabet);

        return ProceduralUtil.findSeparatingWord(sba1.getProcedures(), at1, sba2.getProcedures(), at2, alphabet);
    }

    /**
     * Reduces a given {@link SBA} to its well-matched language. This is a convenience method for
     * {@link #reduce(SBA, ProceduralInputAlphabet)} that uses the {@link SBA#getInputAlphabet() input alphabet} of the
     * given {@link SBA}.
     *
     * @param sba
     *         the {@link SBA} to reduce
     * @param <I>
     *         input symbol type
     *
     * @return the reduced {@link SBA} in form of an {@link SPA}
     *
     * @see #reduce(SBA, ProceduralInputAlphabet)
     */
    public static <I> SPA<?, I> reduce(SBA<?, I> sba) {
        return reduce(sba, sba.getInputAlphabet());
    }

    /**
     * Reduces a given {@link SBA} to its well-matched language restricted to the symbols of the given
     * {@link ProceduralInputAlphabet}. The reduced {@link SBA} only accepts a {@link Word} iff it is (minimally)
     * well-matched and accepted by the original {@link SBA} as well.
     *
     * @param sba
     *         the {@link SBA} to reduce
     * @param alphabet
     *         the {@link ProceduralInputAlphabet} whose symbols should be considered for reduction
     * @param <I>
     *         input symbol type
     *
     * @return the reduced {@link SBA} in form of an {@link SPA}
     */
    public static <I> SPA<?, I> reduce(SBA<?, I> sba, ProceduralInputAlphabet<I> alphabet) {
        final Map<I, DFA<?, I>> procedures = sba.getProcedures();
        final Map<I, DFA<?, I>> spaProcedures = new HashMap<>(HashUtil.capacity(procedures.size()));
        final Collection<I> proceduralInputs = sba.getProceduralInputs(alphabet);
        proceduralInputs.remove(alphabet.getReturnSymbol());

        for (Entry<I, DFA<?, I>> e : procedures.entrySet()) {
            spaProcedures.put(e.getKey(), reduce(e.getValue(), alphabet, proceduralInputs));
        }

        return new StackSPA<>(alphabet, sba.getInitialProcedure(), spaProcedures);
    }

    private static <S, I> DFA<?, I> reduce(DFA<S, I> dfa,
                                           ProceduralInputAlphabet<I> alphabet,
                                           Collection<I> sourceInputs) {

        final I returnSymbol = alphabet.getReturnSymbol();
        final Alphabet<I> proceduralAlphabet = alphabet.getProceduralAlphabet();

        final Function<S, Boolean> spMapping = s -> {
            final S succ = dfa.getSuccessor(s, returnSymbol);
            return succ != null && dfa.isAccepting(succ);
        };
        final TransitionPredicate<S, I, S> transFilter = TransitionPredicates.inputIsNot(returnSymbol);

        final MutableDFA<Integer, I> result = new CompactDFA<>(proceduralAlphabet);
        AutomatonLowLevelCopy.rawCopy(AutomatonCopyMethod.BFS,
                                      dfa,
                                      sourceInputs,
                                      result,
                                      spMapping,
                                      o -> null,
                                      o -> true,
                                      transFilter);

        MutableDFAs.complete(result, proceduralAlphabet, true);
        return result;
    }

    /**
     * Returns a {@link ContextFreeModalProcessSystem}-based view on the language of a given {@link SBA} such that there
     * exists a {@code w}-labeled path in the returned CFMPS if and only if {@code w} is accepted by the given
     * {@link SBA}. This allows one to model-check language properties of {@link SBA}s with tools such as M3C.
     *
     * @param sba
     *         the {@link SBA} to convert
     * @param <I>
     *         input symbol type
     *
     * @return the {@link ContextFreeModalProcessSystem}-based view on the given {@code sba}.
     */
    public static <I> ContextFreeModalProcessSystem<I, Void> toCFMPS(SBA<?, I> sba) {
        assert SBAs.isValid(sba);
        return new CFMPSViewSBA<>(sba);
    }

    /**
     * Transforms a model checker for {@link ContextFreeModalProcessSystem}s to a model checker for {@link SBA}s by
     * transforming the {@link SBA} via {@link #toCFMPS(SBA)}.
     *
     * @param modelChecker
     *         the original model checker
     * @param <I>
     *         input symbol type
     * @param <P>
     *         property type
     * @param <R>
     *         counterexample type
     *
     * @return the transformed model checker
     */
    public static <I, P, R> ModelChecker<I, SBA<?, I>, P, R> transformModelChecker(ModelChecker<I, ContextFreeModalProcessSystem<I, Void>, P, R> modelChecker) {
        return (automaton, inputs, property) -> modelChecker.findCounterExample(toCFMPS(automaton), inputs, property);
    }

}

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.util.automaton.procedural;
17
18	import java.util.Collection;
19	import java.util.HashMap;
20	import java.util.HashSet;
21	import java.util.Map;
22	import java.util.Map.Entry;
23	import java.util.Objects;
24	import java.util.Set;
25	import java.util.function.Function;
26
27	import net.automatalib.alphabet.Alphabet;
28	import net.automatalib.alphabet.ProceduralInputAlphabet;
29	import net.automatalib.automaton.fsa.DFA;
30	import net.automatalib.automaton.fsa.MutableDFA;
31	import net.automatalib.automaton.fsa.impl.CompactDFA;
32	import net.automatalib.automaton.procedural.SBA;
33	import net.automatalib.automaton.procedural.SPA;
34	import net.automatalib.automaton.procedural.SPMM;
35	import net.automatalib.automaton.procedural.impl.StackSPA;
36	import net.automatalib.common.util.HashUtil;
37	import net.automatalib.graph.ContextFreeModalProcessSystem;
38	import net.automatalib.modelchecking.ModelChecker;
39	import net.automatalib.ts.TransitionPredicate;
40	import net.automatalib.util.automaton.copy.AutomatonCopyMethod;
41	import net.automatalib.util.automaton.copy.AutomatonLowLevelCopy;
42	import net.automatalib.util.automaton.fsa.DFAs;
43	import net.automatalib.util.automaton.fsa.MutableDFAs;
44	import net.automatalib.util.automaton.predicate.TransitionPredicates;
45	import net.automatalib.word.Word;
46	import org.checkerframework.checker.nullness.qual.Nullable;
47
48	/**
49	* Operations on {@link SBA}s.
50	*/
51	public final class SBAs {	2✔
52
53	private SBAs() {
54	// prevent instantiation
55	}
56
57	/**
58	* Computes a set of access sequences and terminating sequences for a given {@link SBA}. This is a convenience
59	* method for {@link #computeATSequences(SBA, ProceduralInputAlphabet)} that automatically uses the
60	* {@link SBA#getInputAlphabet() input alphabet} of the given {@code sba}.
61	*
62	* @param sba
63	* the {@link SBA} for which the sequences should be computed
64	* @param <I>
65	* input symbol type
66	*
67	* @return an {@link ATSequences} object which contains the respective sequences.
68	*
69	* @see #computeATSequences(SBA, ProceduralInputAlphabet)
70	*/
71	public static <I> ATSequences<I> computeATSequences(SBA<?, I> sba) {
72	return computeATSequences(sba, sba.getInputAlphabet());	2✔
73	}
74
75	/**
76	* Computes a set of access sequences and terminating sequences for a given {@link SBA} limited to the symbols of
77	* the given {@link ProceduralInputAlphabet}.
78	*
79	* @param sba
80	* the {@link SBA} for which the sequences should be computed
81	* @param alphabet
82	* the {@link ProceduralInputAlphabet} whose symbols should be used for computing the respective sequences
83	* @param <I>
84	* input symbol type
85	*
86	* @return an {@link ATSequences} object which contains the respective sequences.
87	*
88	* @see #computeAccessSequences(SBA, ProceduralInputAlphabet, Map)
89	* @see #computeTerminatingSequences(SBA, ProceduralInputAlphabet)
90	*/
91	public static <I> ATSequences<I> computeATSequences(SBA<?, I> sba, ProceduralInputAlphabet<I> alphabet) {
92
93	assert isValid(sba, alphabet);	2✔
94
95	final Map<I, Word<I>> terminatingSequences = computeTerminatingSequences(sba, alphabet);	2✔
96	final Map<I, Word<I>> accessSequences = computeAccessSequences(sba, alphabet, terminatingSequences);	2✔
97
98	return new ATSequences<>(accessSequences, terminatingSequences);	2✔
99	}
100
101	/**
102	* Computes for a given {@link SBA} a set of terminating sequences using the given
103	* {@link ProceduralInputAlphabet alphabet}. Terminating sequences transfer a procedure from its initial state to a
104	* returnable state. This method furthermore checks that the hierarchy of calls is well-defined, i.e. it only
105	* includes procedural invocations <i>p</i> for determining a terminating sequence if <i>p</i> has a valid
106	* terminating sequence itself.
107	*
108	* @param sba
109	* the {@link SBA} to analyze
110	* @param alphabet
111	* the {@link ProceduralInputAlphabet} whose symbols should be used for determining the terminating
112	* sequences
113	* @param <I>
114	* input symbol type
115	*
116	* @return A map from procedures (restricted to the call symbols of the given alphabet) to the terminating
117	* sequences. This map may be partial as some procedures may not have a well-defined terminating sequence for the
118	* given alphabet.
119	*/
120	public static <I> Map<I, Word<I>> computeTerminatingSequences(SBA<?, I> sba, ProceduralInputAlphabet<I> alphabet) {
121	final Word<I> returnWord = Word.fromLetter(alphabet.getReturnSymbol());	2✔
122	return ProceduralUtil.computeTerminatingSequences(sba.getProcedures(),	2✔
123	alphabet,
124	(dfa, trace) -> dfa.computeSuffixOutput(trace, returnWord));	2✔
125	}
126
127	/**
128	* Computes for a given {@link SBA} a set of access sequences using the given
129	* {@link ProceduralInputAlphabet alphabet}. An access sequence (for procedure <i>p</i>) transfers an {@link SBA}
130	* from its initial state to a state that is able to successfully execute a run of <i>p</i>. This method furthermore
131	* checks that potentially nested calls are well-defined, i.e. it only includes procedural invocations <i>p</i> for
132	* determining access sequences if <i>p</i> has a valid terminating sequence and therefore can be expanded
133	* correctly.
134	*
135	* @param sba
136	* the {@link SBA} to analyze
137	* @param alphabet
138	* the {@link ProceduralInputAlphabet} whose symbols should be used for determining the access and return
139	* sequences
140	* @param terminatingSequences
141	* a {@link Map} of call symbols to terminating sequences used to expand nested invocations in access
142	* sequences
143	* @param <I>
144	* input symbol type
145	*
146	* @return A pair of maps from procedures (restricted to the call symbols of the given alphabet) to the
147	* access/return sequences. These maps may be partial as some procedures may not have well-defined
148	* access/terminating sequences for the given alphabet.
149	*/
150	public static <I> Map<I, Word<I>> computeAccessSequences(SBA<?, I> sba,
151	ProceduralInputAlphabet<I> alphabet,
152	Map<I, Word<I>> terminatingSequences) {
153
154	return ProceduralUtil.computeAccessSequences(sba.getProcedures(),	2✔
155	alphabet,
156	sba.getProceduralInputs(alphabet),	2✔
157	sba.getInitialProcedure(),	2✔
158	terminatingSequences,
159	DFA::accepts);
160	}
161
162	/**
163	* Checks whether the given {@link SBA} is valid, This is a convenience method for
164	* {@link #isValid(SBA, ProceduralInputAlphabet)} that uses the {@link SBA#getInputAlphabet() input alphabet} of the
165	* given {@link SBA}.
166	*
167	* @param sba
168	* the {@link SBA} to analyze
169	* @param <I>
170	* input symbol type
171	*
172	* @return {@code true} if {@code sba} is valid, {@code false} otherwise.
173	*
174	* @see #isValid(SBA, ProceduralInputAlphabet)
175	*/
176	public static <I> boolean isValid(SBA<?, I> sba) {
177	return isValid(sba, sba.getInputAlphabet());	2✔
178	}
179
180	/**
181	* Checks whether the given {@link SBA} is valid with respect to the given {@link ProceduralInputAlphabet}, i.e.,
182	* whether its {@link SBA#getProcedures() procedures} are prefix-closed, return-closed, and call-closed.
183	* <p>
184	* A procedure is considered prefix-closed iff any continuation of a rejected word is rejected as well.
185	* <p>
186	* A procedure is considered return-closed iff any continuation beyond the
187	* {@link ProceduralInputAlphabet#getReturnSymbol() return symbol} is rejected.
188	* <p>
189	* A procedure is considered call-closed iff any continuation beyond a non-terminating
190	* {@link ProceduralInputAlphabet#getCallAlphabet() call symbol} is rejected.
191	*
192	* @param sba
193	* the {@link SBA} to analyze
194	* @param alphabet
195	* the {@link ProceduralInputAlphabet} whose symbols should be used for checking validity
196	* @param <I>
197	* input symbol type
198	*
199	* @return {@code true} if {@code sba} is valid, {@code false} otherwise.
200	*/
201	public static <I> boolean isValid(SBA<?, I> sba, ProceduralInputAlphabet<I> alphabet) {
202
203	final Map<I, Word<I>> ts = computeTerminatingSequences(sba, alphabet);	2✔
204	final Collection<I> proceduralInputs = sba.getProceduralInputs(alphabet);	2✔
205	final Set<I> nonContinuableSymbols = new HashSet<>(alphabet.getCallAlphabet());	2✔
206	nonContinuableSymbols.removeAll(ts.keySet());	2✔
207	nonContinuableSymbols.retainAll(proceduralInputs);	2✔
208	nonContinuableSymbols.add(alphabet.getReturnSymbol());	2✔
209
210	for (DFA<?, I> p : sba.getProcedures().values()) {	2✔
211	if (!DFAs.isPrefixClosed(p, proceduralInputs) \|\|	2✔
212	!isCallAndReturnClosed(p, proceduralInputs, nonContinuableSymbols)) {	2✔
UNCOV 213	return false;	×
214	}
215	}	2✔
216
217	return true;	2✔
218	}
219
220	private static <S, I> boolean isCallAndReturnClosed(DFA<S, I> procedure,
221	Collection<I> inputs,
222	Collection<I> nonContinuableInputs) {
223
224	for (S s : procedure) {	2✔
225	for (I i : nonContinuableInputs) {	2✔
226	final S succ = procedure.getSuccessor(s, i);	2✔
227	final S toAnalyze;
228
229	if (succ != null && procedure.isAccepting(succ)) {	2✔
230	toAnalyze = procedure.getSuccessor(succ, i);	2✔
231
232	// ensure that toAnalyze is effectively a "success sink"
233	for (I i2 : inputs) {	2✔
234	if (!Objects.equals(procedure.getSuccessor(succ, i2), toAnalyze)) {	2✔
UNCOV 235	return false;	×
236	}
237	}	2✔
238	} else {
239	toAnalyze = succ;	2✔
240	}
241
242	if (toAnalyze != null && !isSink(procedure, inputs, toAnalyze)) {	2✔
UNCOV 243	return false;	×
244	}
245	}	2✔
246	}	2✔
247
248	return true;	2✔
249	}
250
251	private static <S, I> boolean isSink(DFA<S, I> dfa, Collection<I> inputs, S state) {
252
253	if (dfa.isAccepting(state)) {	2✔
UNCOV 254	return false;	×
255	}
256
257	for (I i : inputs) {	2✔
258	final S succ = dfa.getSuccessor(state, i);	2✔
259	if (succ != null && !Objects.equals(succ, state)) {	2✔
UNCOV 260	return false;	×
261	}
262	}	2✔
263
264	return true;	2✔
265	}
266
267	/**
268	* Checks if the two given {@link SBA}s are equivalent, i.e. whether there exists a
269	* {@link #findSeparatingWord(SBA, SBA, ProceduralInputAlphabet) separating word} for them.
270	*
271	* @param sba1
272	* the first {@link SPMM}
273	* @param sba2
274	* the second {@link SPMM}
275	* @param alphabet
276	* the {@link ProceduralInputAlphabet} whose symbols should be used for checking equivalence
277	* @param <I>
278	* input symbol type
279	*
280	* @return {@code true} if the two {@link SBA}s are equivalent, {@code false} otherwise.
281	*
282	* @see #findSeparatingWord(SBA, SBA, ProceduralInputAlphabet)
283	*/
284	public static <I> boolean testEquivalence(SBA<?, I> sba1, SBA<?, I> sba2, ProceduralInputAlphabet<I> alphabet) {
285	return findSeparatingWord(sba1, sba2, alphabet) == null;	2✔
286	}
287
288	/**
289	* Computes a separating word for the two given {@link SBA}s, if existent. A separating word is a {@link Word} such
290	* that one {@link SBA} {@link SBA#accepts(Iterable) behaves} different from the other.
291	*
292	* @param sba1
293	* the first {@link SBA}
294	* @param sba2
295	* the second {@link SBA}
296	* @param alphabet
297	* the {@link ProceduralInputAlphabet} whose symbols should be considered for computing the separating word
298	* @param <I>
299	* input symbol type
300	*
301	* @return a separating word, if existent, {@code null} otherwise.
302	*/
303	public static <I> @Nullable Word<I> findSeparatingWord(SBA<?, I> sba1,
304	SBA<?, I> sba2,
305	ProceduralInputAlphabet<I> alphabet) {
306
307	final ATSequences<I> at1 = computeATSequences(sba1, alphabet);	2✔
308	final ATSequences<I> at2 = computeATSequences(sba2, alphabet);	2✔
309
310	return ProceduralUtil.findSeparatingWord(sba1.getProcedures(), at1, sba2.getProcedures(), at2, alphabet);	2✔
311	}
312
313	/**
314	* Reduces a given {@link SBA} to its well-matched language. This is a convenience method for
315	* {@link #reduce(SBA, ProceduralInputAlphabet)} that uses the {@link SBA#getInputAlphabet() input alphabet} of the
316	* given {@link SBA}.
317	*
318	* @param sba
319	* the {@link SBA} to reduce
320	* @param <I>
321	* input symbol type
322	*
323	* @return the reduced {@link SBA} in form of an {@link SPA}
324	*
325	* @see #reduce(SBA, ProceduralInputAlphabet)
326	*/
327	public static <I> SPA<?, I> reduce(SBA<?, I> sba) {
328	return reduce(sba, sba.getInputAlphabet());	2✔
329	}
330
331	/**
332	* Reduces a given {@link SBA} to its well-matched language restricted to the symbols of the given
333	* {@link ProceduralInputAlphabet}. The reduced {@link SBA} only accepts a {@link Word} iff it is (minimally)
334	* well-matched and accepted by the original {@link SBA} as well.
335	*
336	* @param sba
337	* the {@link SBA} to reduce
338	* @param alphabet
339	* the {@link ProceduralInputAlphabet} whose symbols should be considered for reduction
340	* @param <I>
341	* input symbol type
342	*
343	* @return the reduced {@link SBA} in form of an {@link SPA}
344	*/
345	public static <I> SPA<?, I> reduce(SBA<?, I> sba, ProceduralInputAlphabet<I> alphabet) {
346	final Map<I, DFA<?, I>> procedures = sba.getProcedures();	2✔
347	final Map<I, DFA<?, I>> spaProcedures = new HashMap<>(HashUtil.capacity(procedures.size()));	2✔
348	final Collection<I> proceduralInputs = sba.getProceduralInputs(alphabet);	2✔
349	proceduralInputs.remove(alphabet.getReturnSymbol());	2✔
350
351	for (Entry<I, DFA<?, I>> e : procedures.entrySet()) {	2✔
352	spaProcedures.put(e.getKey(), reduce(e.getValue(), alphabet, proceduralInputs));	2✔
353	}	2✔
354
355	return new StackSPA<>(alphabet, sba.getInitialProcedure(), spaProcedures);	2✔
356	}
357
358	private static <S, I> DFA<?, I> reduce(DFA<S, I> dfa,
359	ProceduralInputAlphabet<I> alphabet,
360	Collection<I> sourceInputs) {
361
362	final I returnSymbol = alphabet.getReturnSymbol();	2✔
363	final Alphabet<I> proceduralAlphabet = alphabet.getProceduralAlphabet();	2✔
364
365	final Function<S, Boolean> spMapping = s -> {	2✔
366	final S succ = dfa.getSuccessor(s, returnSymbol);	2✔
367	return succ != null && dfa.isAccepting(succ);	2✔
368	};
369	final TransitionPredicate<S, I, S> transFilter = TransitionPredicates.inputIsNot(returnSymbol);	2✔
370
371	final MutableDFA<Integer, I> result = new CompactDFA<>(proceduralAlphabet);	2✔
372	AutomatonLowLevelCopy.rawCopy(AutomatonCopyMethod.BFS,	2✔
373	dfa,
374	sourceInputs,
375	result,
376	spMapping,
377	o -> null,	2✔
378	o -> true,	2✔
379	transFilter);
380
381	MutableDFAs.complete(result, proceduralAlphabet, true);	2✔
382	return result;	2✔
383	}
384
385	/**
386	* Returns a {@link ContextFreeModalProcessSystem}-based view on the language of a given {@link SBA} such that there
387	* exists a {@code w}-labeled path in the returned CFMPS if and only if {@code w} is accepted by the given
388	* {@link SBA}. This allows one to model-check language properties of {@link SBA}s with tools such as M3C.
389	*
390	* @param sba
391	* the {@link SBA} to convert
392	* @param <I>
393	* input symbol type
394	*
395	* @return the {@link ContextFreeModalProcessSystem}-based view on the given {@code sba}.
396	*/
397	public static <I> ContextFreeModalProcessSystem<I, Void> toCFMPS(SBA<?, I> sba) {
398	assert SBAs.isValid(sba);	2✔
399	return new CFMPSViewSBA<>(sba);	2✔
400	}
401
402	/**
403	* Transforms a model checker for {@link ContextFreeModalProcessSystem}s to a model checker for {@link SBA}s by
404	* transforming the {@link SBA} via {@link #toCFMPS(SBA)}.
405	*
406	* @param modelChecker
407	* the original model checker
408	* @param <I>
409	* input symbol type
410	* @param <P>
411	* property type
412	* @param <R>
413	* counterexample type
414	*
415	* @return the transformed model checker
416	*/
417	public static <I, P, R> ModelChecker<I, SBA<?, I>, P, R> transformModelChecker(ModelChecker<I, ContextFreeModalProcessSystem<I, Void>, P, R> modelChecker) {
418	return (automaton, inputs, property) -> modelChecker.findCounterExample(toCFMPS(automaton), inputs, property);	2✔
419	}
420
421	}

LearnLib / automatalib / 29161451305

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