001/* Copyright (C) 2013 TU Dortmund
002 * This file is part of AutomataLib, http://www.automatalib.net/.
003 * 
004 * AutomataLib is free software; you can redistribute it and/or
005 * modify it under the terms of the GNU Lesser General Public
006 * License version 3.0 as published by the Free Software Foundation.
007 * 
008 * AutomataLib is distributed in the hope that it will be useful,
009 * but WITHOUT ANY WARRANTY; without even the implied warranty of
010 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
011 * Lesser General Public License for more details.
012 * 
013 * You should have received a copy of the GNU Lesser General Public
014 * License along with AutomataLib; if not, see
015 * http://www.gnu.de/documents/lgpl.en.html.
016 */
017package net.automatalib.util.automata;
018
019import java.util.ArrayList;
020import java.util.Collection;
021import java.util.Collections;
022import java.util.Iterator;
023import java.util.List;
024
025import net.automatalib.automata.Automaton;
026import net.automatalib.automata.DeterministicAutomaton;
027import net.automatalib.automata.MutableDeterministic;
028import net.automatalib.automata.UniversalAutomaton;
029import net.automatalib.automata.UniversalDeterministicAutomaton;
030import net.automatalib.automata.graphs.TransitionEdge;
031import net.automatalib.graphs.Graph;
032import net.automatalib.graphs.UniversalGraph;
033import net.automatalib.util.automata.asgraph.AutomatonAsGraph;
034import net.automatalib.util.automata.asgraph.UniversalAutomatonAsGraph;
035import net.automatalib.util.automata.equivalence.CharacterizingSets;
036import net.automatalib.util.automata.equivalence.NearLinearEquivalenceTest;
037import net.automatalib.util.minimizer.Block;
038import net.automatalib.util.minimizer.BlockMap;
039import net.automatalib.util.minimizer.MinimizationResult;
040import net.automatalib.util.minimizer.Minimizer;
041import net.automatalib.util.ts.TS;
042import net.automatalib.words.Word;
043
044public class Automata extends TS {
045
046        public static <S, I, T>
047        Graph<S, TransitionEdge<I, T>> asGraph(
048                        Automaton<S, I, T> automaton, Collection<? extends I> inputs) {
049                return new AutomatonAsGraph<S, I, T,Automaton<S,I,T>>(automaton, inputs);
050        }
051        
052        public static <S,I,T,SP,TP>
053        UniversalGraph<S,TransitionEdge<I,T>,SP,TransitionEdge.Property<I,TP>> asUniversalGraph(
054                        UniversalAutomaton<S, I, T, SP, TP> automaton, Collection<? extends I> inputs) {
055                return new UniversalAutomatonAsGraph<S, I, T, SP, TP, UniversalAutomaton<S,I,T,SP,TP>>(automaton, inputs);
056        }
057        
058
059        public static <S, I, T, SP, TP, SO, TO, A extends MutableDeterministic<SO, ? super I, TO, ? super SP, ? super TP>>
060        A minimize(
061                        UniversalDeterministicAutomaton<S, I, T, SP, TP> automaton,
062                        Collection<? extends I> inputs,
063                        A output) {
064
065                UniversalGraph<S, TransitionEdge<I,T>, SP, TransitionEdge.Property<I,TP>> aag = asUniversalGraph(automaton, inputs);
066                
067                MinimizationResult<S, TransitionEdge.Property<I,TP>> mr = Minimizer.minimize(aag, Collections.singleton(automaton.getInitialState()));
068                output.clear();
069                
070                S init = automaton.getInitialState();
071                Block<S,TransitionEdge.Property<I,TP>> initBlock = mr.getBlockForState(init);
072                BlockMap<SO> bm = new BlockMap<SO>(mr);
073                
074                for(Block<S, TransitionEdge.Property<I,TP>> block : mr.getBlocks()) {
075                        S rep = mr.getRepresentative(block);
076                        SO state;
077                        SP repProp = automaton.getStateProperty(rep);
078                        if(block == initBlock)
079                                state = output.addInitialState(repProp);
080                        else
081                                state = output.addState(repProp);
082                        bm.put(block, state);
083                }
084                
085                for(Block<S,TransitionEdge.Property<I,TP>> block : mr.getBlocks()) {
086                        S rep = mr.getRepresentative(block);
087                        SO state = bm.get(block);
088                        for(I input : inputs) {
089                                T trans = automaton.getTransition(rep, input);
090                                TP prop = automaton.getTransitionProperty(trans);
091                                S oldSucc = automaton.getSuccessor(trans);
092                                Block<S,TransitionEdge.Property<I,TP>> succBlock = mr.getBlockForState(oldSucc);
093                                SO newSucc = bm.get(succBlock);
094                                output.addTransition(state, input, newSucc, prop);
095                        }
096                }
097                return output;
098        }
099        
100        private static final class ResultTransRecord<TP> {
101                public final int targetId;
102                public final TP property;
103                
104                public ResultTransRecord(int targetId, TP property) {
105                        this.targetId = targetId;
106                        this.property = property;
107                }
108        }
109        
110        private static final class ResultStateRecord<SP,TP> {
111                public final SP property;
112                public final ResultTransRecord<TP>[] transitions;
113
114                @SuppressWarnings("unchecked")
115                public ResultStateRecord(int numInputs, SP property) {
116                        this.property = property;
117                        this.transitions = new ResultTransRecord[numInputs];
118                }
119        }
120        
121        @SuppressWarnings("unchecked")
122        public static <S, I, T, SP, TP, A extends MutableDeterministic<S, I, T, SP, TP>>
123        A invasiveMinimize(A automaton, Collection<? extends I> inputs) {
124                
125                List<? extends I> inputList;
126                if(inputs instanceof List)
127                        inputList = (List<? extends I>)inputs;
128                else
129                        inputList = new ArrayList<I>(inputs);
130                
131                int numInputs = inputs.size();
132
133                UniversalGraph<S, TransitionEdge<I,T>, SP, TransitionEdge.Property<I,TP>> aag = asUniversalGraph(automaton, inputs);
134                
135                MinimizationResult<S, TransitionEdge.Property<I,TP>> mr = Minimizer.minimize(aag, automaton.getInitialStates());
136                
137                S init = automaton.getInitialState();
138                int initId = mr.getBlockForState(init).getId();
139                
140                ResultStateRecord<SP,TP>[] records = new ResultStateRecord[mr.getNumBlocks()];
141                
142                for(Block<S,TransitionEdge.Property<I,TP>> blk : mr.getBlocks()) {
143                        int id = blk.getId();
144                        S state = mr.getRepresentative(blk);
145                        SP prop = automaton.getStateProperty(state);
146                        ResultStateRecord<SP,TP> rec = new ResultStateRecord<>(numInputs, prop);
147                        records[id] = rec;
148                        for(int i = 0; i < numInputs; i++) {
149                                I input = inputList.get(i);
150                                T trans = automaton.getTransition(state, input);
151                                if(trans == null)
152                                        continue;
153                                
154                                TP transProp = automaton.getTransitionProperty(trans);
155                                S succ = automaton.getSuccessor(trans);
156                                int tgtId = mr.getBlockForState(succ).getId();
157                                rec.transitions[i] = new ResultTransRecord<TP>(tgtId, transProp);
158                        }
159                }
160                
161                automaton.clear();
162                
163                Object[] states = new Object[records.length];
164                for(int i = 0; i < records.length; i++) {
165                        ResultStateRecord<SP, TP> rec = records[i];
166                        SP prop = rec.property;
167                        S state;
168                        if(i == initId)
169                                state = automaton.addInitialState(prop);
170                        else
171                                state = automaton.addState(prop);
172                        states[i] = state;
173                }
174                
175                for(int i = 0; i < records.length; i++) {
176                        ResultStateRecord<SP, TP> rec = records[i];
177                        S state = (S)states[i];
178                        
179                        for(int j = 0; j < numInputs; j++) {
180                                ResultTransRecord<TP> transRec = rec.transitions[j];
181                                if(transRec == null)
182                                        continue;
183                                S succ = (S)states[transRec.targetId];
184                                I input = inputList.get(j);
185                                automaton.addTransition(state, input, succ, transRec.property);
186                        }
187                }
188                return automaton;
189        }
190        
191        /*
192        public static <S, I, T, SP, TP, A extends MutableDeterministic<S, I, T, SP, TP>> A minimize(
193                        A automaton, Collection<? extends I> inputs) {
194                return minimize(automaton, inputs, automaton);
195        }*/
196        
197        /**
198         * Finds a separating word for two automata. A separating word is a word that exposes
199         * a difference (differing state or transition properties, or a transition undefined in
200         * only one of the automata) between the two automata.
201         * 
202         * @param reference the one automaton to consider
203         * @param other the other automaton to consider
204         * @param inputs the input symbols to consider
205         * @return a separating word, or <tt>null</tt> if no such word could be found.
206         */
207        public static <I> Word<I> findSeparatingWord(
208                        UniversalDeterministicAutomaton<?, I, ?, ?, ?> reference,
209                        UniversalDeterministicAutomaton<?, I, ?, ?, ?> other,
210                        Collection<? extends I> inputs) {
211                return NearLinearEquivalenceTest.findSeparatingWord(reference, other, inputs);
212        }
213        
214        /**
215         * Finds a separating word for two states in an automaton. A separating word is a word
216         * that exposes a difference (differing state or transition properties, or a transition
217         * undefined in only one of the paths) between the two states.
218         * @param automaton the automaton containing the states
219         * @param state1 the one state
220         * @param state2 the other state
221         * @param inputs the input symbols to consider
222         * @return a separating word, or <tt>null</tt> if no such word could be found
223         */
224        public static <S,I> Word<I> findSeparatingWord(
225                        UniversalDeterministicAutomaton<S, I, ?, ?, ?> automaton,
226                        S state1, S state2,
227                        Collection<? extends I> inputs) {
228                return NearLinearEquivalenceTest.findSeparatingWord(automaton, state1, state2, inputs);
229        }
230        
231        /**
232         * Computes a characterizing set for the given automaton.
233         * <p>
234         * This is a convenience method acting as a shortcut to
235         * {@link CharacterizingSets#findCharacterizingSet(UniversalDeterministicAutomaton, Collection, Collection)}.
236         * 
237         * @see CharacterizingSets
238         * 
239         * @param automaton the automaton for which to determine the characterizing set
240         * @param inputs the input symbols to consider
241         * @param result the collection in which to store the characterizing words
242         */
243        public static <I> void characterizingSet(UniversalDeterministicAutomaton<?, I, ?, ?, ?> automaton,
244                        Collection<? extends I> inputs,
245                        Collection<? super Word<I>> result) {
246                CharacterizingSets.findCharacterizingSet(automaton, inputs, result);
247        }
248        
249        /**
250         * Computes a characterizing set, and returns it as a {@link List}.
251         * 
252         * @see CharacterizingSets
253         * 
254         * @param automaton the automaton for which to determine the characterizing set
255         * @param inputs the input symbols to consider
256         * @return a list containing the characterizing words
257         */
258        public static <I> List<Word<I>> characterizingSet(UniversalDeterministicAutomaton<?, I, ?, ?, ?> automaton,
259                        Collection<? extends I> inputs) {
260                List<Word<I>> result = new ArrayList<Word<I>>();
261                characterizingSet(automaton, inputs, result);
262                return result;
263        }
264        
265        /**
266         * Computes a characterizing set for a single state.
267         * <p>
268         * This is a convenience method acting as a shortcut to
269         * {@link CharacterizingSets#findCharacterizingSet(UniversalDeterministicAutomaton, Collection, Object, Collection)}.
270         * 
271         * @see CharacterizingSets
272         * 
273         * @param automaton the automaton containing the state
274         * @param inputs the input symbols to consider
275         * @param state the state for which to determine a characterizing set
276         * @param result the collection in which to store the characterizing words
277         */
278        public static <S,I> void stateCharacterizingSet(UniversalDeterministicAutomaton<S, I, ?, ?, ?> automaton,
279                        Collection<? extends I> inputs,
280                        S state,
281                        Collection<? super Word<I>> result) {
282                CharacterizingSets.findCharacterizingSet(automaton, inputs, state, result);
283        }
284        
285        /**
286         * Computes a characterizing set for a single state, and returns it as a {@link List}.
287         * 
288         * @see CharacterizingSets
289         * 
290         * @param automaton the automaton containing the state
291         * @param inputs the input symbols to consider
292         * @param state the state for which to determine a characterizing set
293         * @return a list containing the characterizing words
294         */
295        public static <S,I> List<Word<I>> stateCharacterizingSet(UniversalDeterministicAutomaton<S, I, ?, ?, ?> automaton,
296                        Collection<? extends I> inputs,
297                        S state) {
298                List<Word<I>> result = new ArrayList<Word<I>>();
299                stateCharacterizingSet(automaton, inputs, state, result);
300                return result;
301        }
302        
303        public static <I> void cover(DeterministicAutomaton<?, I, ?> automaton,
304                        Collection<? extends I> inputs, Collection<? super Word<I>> states, Collection<? super Word<I>> transitions) {
305                Covers.cover(automaton, inputs, states, transitions);
306        }
307        
308        public static <I> List<Word<I>> stateCover(DeterministicAutomaton<?, I, ?> automaton,
309                        Collection<? extends I> inputs) {
310                List<Word<I>> states = new ArrayList<Word<I>>(automaton.size());
311                cover(automaton, inputs, states, null);
312                return states;
313        }
314        
315        public static <I> List<Word<I>> transitionCover(DeterministicAutomaton<?, I, ?> automaton,
316                        Collection<? extends I> inputs) {
317                List<Word<I>> all = new ArrayList<Word<I>>(automaton.size() * inputs.size());
318                cover(automaton, inputs, all, all);
319                return all;
320        }
321        
322        
323        
324        public static <S,I>
325        Iterator<TransRef<S,I>> allDefinedTransitionsIterator(
326                        DeterministicAutomaton<S, I, ?> automaton,
327                        Iterable<? extends I> inputs) {
328                return allDefinedTransitionsIterator(automaton, automaton.iterator(), inputs);
329        }
330        
331        public static <S,I>
332        Iterable<TransRef<S,I>> allDefinedTransitions(
333                        DeterministicAutomaton<S, I, ?> automaton,
334                        Iterable<? extends I> inputs) {
335                return allDefinedTransitions(automaton, automaton, inputs);
336        }
337        
338        public static <S,I>
339        Iterator<TransRef<S,I>> allUndefinedTransitionsIterator(
340                        DeterministicAutomaton<S, I, ?> automaton,
341                        Iterable<? extends I> inputs) {
342                return allUndefinedTransitionsIterator(automaton, automaton.iterator(), inputs);
343        }
344        
345        public static <S,I>
346        Iterable<TransRef<S,I>> allUndefinedTransitions(
347                        DeterministicAutomaton<S, I, ?> automaton,
348                        Iterable<? extends I> inputs) {
349                return allUndefinedTransitions(automaton, automaton, inputs);
350        }
351}