13138848026

Committed 04 Feb 2025 02:53PM UTC coverage: 92.108% (+2.2%) from 89.877%

Build # 13138848026

Build Type

push

github

Committed by

mtf90

Commit Message

[maven-release-plugin] prepare release automatalib-0.12.0

Run Details

16609 of 18032 relevant lines covered (92.11%)

1.7 hits per line

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

93.33

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

}

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

LearnLib / automatalib / 13138848026

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