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.List;
023
024import net.automatalib.automata.Automaton;
025import net.automatalib.automata.DeterministicAutomaton;
026import net.automatalib.automata.MutableDeterministic;
027import net.automatalib.automata.UniversalAutomaton;
028import net.automatalib.automata.UniversalDeterministicAutomaton;
029import net.automatalib.commons.util.Pair;
030import net.automatalib.graphs.Graph;
031import net.automatalib.graphs.UniversalGraph;
032import net.automatalib.util.automata.asgraph.AutomatonAsGraph;
033import net.automatalib.util.automata.asgraph.UniversalAutomatonAsGraph;
034import net.automatalib.util.automata.equivalence.CharacterizingSets;
035import net.automatalib.util.automata.equivalence.NearLinearEquivalenceTest;
036import net.automatalib.util.minimizer.Block;
037import net.automatalib.util.minimizer.BlockMap;
038import net.automatalib.util.minimizer.MinimizationResult;
039import net.automatalib.util.minimizer.Minimizer;
040import net.automatalib.words.Word;
041
042public class Automata {
043
044        public static <S, I, T>
045        Graph<S, Pair<I, T>> asGraph(
046                        Automaton<S, I, T> automaton, Collection<? extends I> inputs) {
047                return new AutomatonAsGraph<S, I, T,Automaton<S,I,T>>(automaton, inputs);
048        }
049        
050        public static <S,I,T,SP,TP>
051        UniversalGraph<S,Pair<I,T>,SP,Pair<I,TP>> asUniversalGraph(
052                        UniversalAutomaton<S, I, T, SP, TP> automaton, Collection<? extends I> inputs) {
053                return new UniversalAutomatonAsGraph<S, I, T, SP, TP, UniversalAutomaton<S,I,T,SP,TP>>(automaton, inputs);
054        }
055        
056
057        public static <S, I, T, SP, TP, SO, TO, A extends MutableDeterministic<SO, ? super I, TO, ? super SP, ? super TP>>
058        A minimize(
059                        UniversalDeterministicAutomaton<S, I, T, SP, TP> automaton,
060                        Collection<? extends I> inputs,
061                        A output) {
062
063                UniversalGraph<S, Pair<I,T>, SP, Pair<I,TP>> aag = asUniversalGraph(automaton, inputs);
064                
065                MinimizationResult<S, Pair<I,TP>> mr = Minimizer.minimize(aag, Collections.singleton(automaton.getInitialState()));
066                output.clear();
067                
068                S init = automaton.getInitialState();
069                Block<S,Pair<I,TP>> initBlock = mr.getBlockForState(init);
070                BlockMap<SO> bm = new BlockMap<SO>(mr);
071                
072                for(Block<S, Pair<I,TP>> block : mr.getBlocks()) {
073                        S rep = mr.getRepresentative(block);
074                        SO state;
075                        SP repProp = automaton.getStateProperty(rep);
076                        if(block == initBlock)
077                                state = output.addInitialState(repProp);
078                        else
079                                state = output.addState(repProp);
080                        bm.put(block, state);
081                }
082                
083                for(Block<S,Pair<I,TP>> block : mr.getBlocks()) {
084                        S rep = mr.getRepresentative(block);
085                        SO state = bm.get(block);
086                        for(I input : inputs) {
087                                T trans = automaton.getTransition(rep, input);
088                                TP prop = automaton.getTransitionProperty(trans);
089                                S oldSucc = automaton.getSuccessor(trans);
090                                Block<S,Pair<I,TP>> succBlock = mr.getBlockForState(oldSucc);
091                                SO newSucc = bm.get(succBlock);
092                                output.addTransition(state, input, newSucc, prop);
093                        }
094                }
095                return output;
096        }
097        
098        private static final class ResultTransRecord<TP> {
099                public final int targetId;
100                public final TP property;
101                
102                public ResultTransRecord(int targetId, TP property) {
103                        this.targetId = targetId;
104                        this.property = property;
105                }
106        }
107        
108        private static final class ResultStateRecord<SP,TP> {
109                public final SP property;
110                public final ResultTransRecord<TP>[] transitions;
111
112                @SuppressWarnings("unchecked")
113                public ResultStateRecord(int numInputs, SP property) {
114                        this.property = property;
115                        this.transitions = new ResultTransRecord[numInputs];
116                }
117        }
118        
119        @SuppressWarnings("unchecked")
120        public static <S, I, T, SP, TP, A extends MutableDeterministic<S, I, T, SP, TP>>
121        A invasiveMinimize(A automaton, Collection<? extends I> inputs) {
122                
123                List<? extends I> inputList;
124                if(inputs instanceof List)
125                        inputList = (List<? extends I>)inputs;
126                else
127                        inputList = new ArrayList<I>(inputs);
128                
129                int numInputs = inputs.size();
130
131                UniversalGraph<S, Pair<I,T>, SP, Pair<I,TP>> aag = asUniversalGraph(automaton, inputs);
132                
133                MinimizationResult<S, Pair<I,TP>> mr = Minimizer.minimize(aag, automaton.getInitialStates());
134                
135                S init = automaton.getInitialState();
136                int initId = mr.getBlockForState(init).getId();
137                
138                ResultStateRecord<SP,TP>[] records = new ResultStateRecord[mr.getNumBlocks()];
139                
140                for(Block<S,Pair<I,TP>> blk : mr.getBlocks()) {
141                        int id = blk.getId();
142                        S state = mr.getRepresentative(blk);
143                        SP prop = automaton.getStateProperty(state);
144                        ResultStateRecord<SP,TP> rec = new ResultStateRecord<>(numInputs, prop);
145                        records[id] = rec;
146                        for(int i = 0; i < numInputs; i++) {
147                                I input = inputList.get(i);
148                                T trans = automaton.getTransition(state, input);
149                                if(trans == null)
150                                        continue;
151                                
152                                TP transProp = automaton.getTransitionProperty(trans);
153                                S succ = automaton.getSuccessor(trans);
154                                int tgtId = mr.getBlockForState(succ).getId();
155                                rec.transitions[i] = new ResultTransRecord<TP>(tgtId, transProp);
156                        }
157                }
158                
159                automaton.clear();
160                
161                Object[] states = new Object[records.length];
162                for(int i = 0; i < records.length; i++) {
163                        ResultStateRecord<SP, TP> rec = records[i];
164                        SP prop = rec.property;
165                        S state;
166                        if(i == initId)
167                                state = automaton.addInitialState(prop);
168                        else
169                                state = automaton.addState(prop);
170                        states[i] = state;
171                }
172                
173                for(int i = 0; i < records.length; i++) {
174                        ResultStateRecord<SP, TP> rec = records[i];
175                        S state = (S)states[i];
176                        
177                        for(int j = 0; j < numInputs; j++) {
178                                ResultTransRecord<TP> transRec = rec.transitions[j];
179                                if(transRec == null)
180                                        continue;
181                                S succ = (S)states[transRec.targetId];
182                                I input = inputList.get(j);
183                                automaton.addTransition(state, input, succ, transRec.property);
184                        }
185                }
186                return automaton;
187        }
188        
189        /*
190        public static <S, I, T, SP, TP, A extends MutableDeterministic<S, I, T, SP, TP>> A minimize(
191                        A automaton, Collection<? extends I> inputs) {
192                return minimize(automaton, inputs, automaton);
193        }*/
194        
195        /**
196         * Finds a separating word for two automata. A separating word is a word that exposes
197         * a difference (differing state or transition properties, or a transition undefined in
198         * only one of the automata) between the two automata.
199         * 
200         * @param reference the one automaton to consider
201         * @param other the other automaton to consider
202         * @param inputs the input symbols to consider
203         * @return a separating word, or <tt>null</tt> if no such word could be found.
204         */
205        public static <I> Word<I> findSeparatingWord(
206                        UniversalDeterministicAutomaton<?, I, ?, ?, ?> reference,
207                        UniversalDeterministicAutomaton<?, I, ?, ?, ?> other,
208                        Collection<? extends I> inputs) {
209                return NearLinearEquivalenceTest.findSeparatingWord(reference, other, inputs);
210        }
211        
212        /**
213         * Finds a separating word for two states in an automaton. A separating word is a word
214         * that exposes a difference (differing state or transition properties, or a transition
215         * undefined in only one of the paths) between the two states.
216         * @param automaton the automaton containing the states
217         * @param state1 the one state
218         * @param state2 the other state
219         * @param inputs the input symbols to consider
220         * @return a separating word, or <tt>null</tt> if no such word could be found
221         */
222        public static <S,I> Word<I> findSeparatingWord(
223                        UniversalDeterministicAutomaton<S, I, ?, ?, ?> automaton,
224                        S state1, S state2,
225                        Collection<? extends I> inputs) {
226                return NearLinearEquivalenceTest.findSeparatingWord(automaton, state1, state2, inputs);
227        }
228        
229        /**
230         * Computes a characterizing set for the given automaton.
231         * <p>
232         * This is a convenience method acting as a shortcut to
233         * {@link CharacterizingSets#findCharacterizingSet(UniversalDeterministicAutomaton, Collection, Collection)}.
234         * 
235         * @see CharacterizingSets
236         * 
237         * @param automaton the automaton for which to determine the characterizing set
238         * @param inputs the input symbols to consider
239         * @param result the collection in which to store the characterizing words
240         */
241        public static <I> void characterizingSet(UniversalDeterministicAutomaton<?, I, ?, ?, ?> automaton,
242                        Collection<? extends I> inputs,
243                        Collection<? super Word<I>> result) {
244                CharacterizingSets.findCharacterizingSet(automaton, inputs, result);
245        }
246        
247        /**
248         * Computes a characterizing set, and returns it as a {@link List}.
249         * 
250         * @see CharacterizingSets
251         * 
252         * @param automaton the automaton for which to determine the characterizing set
253         * @param inputs the input symbols to consider
254         * @return a list containing the characterizing words
255         */
256        public static <I> List<Word<I>> characterizingSet(UniversalDeterministicAutomaton<?, I, ?, ?, ?> automaton,
257                        Collection<? extends I> inputs) {
258                List<Word<I>> result = new ArrayList<Word<I>>();
259                characterizingSet(automaton, inputs, result);
260                return result;
261        }
262        
263        /**
264         * Computes a characterizing set for a single state.
265         * <p>
266         * This is a convenience method acting as a shortcut to
267         * {@link CharacterizingSets#findCharacterizingSet(UniversalDeterministicAutomaton, Collection, Object, Collection)}.
268         * 
269         * @see CharacterizingSets
270         * 
271         * @param automaton the automaton containing the state
272         * @param inputs the input symbols to consider
273         * @param state the state for which to determine a characterizing set
274         * @param result the collection in which to store the characterizing words
275         */
276        public static <S,I> void stateCharacterizingSet(UniversalDeterministicAutomaton<S, I, ?, ?, ?> automaton,
277                        Collection<? extends I> inputs,
278                        S state,
279                        Collection<? super Word<I>> result) {
280                CharacterizingSets.findCharacterizingSet(automaton, inputs, state, result);
281        }
282        
283        /**
284         * Computes a characterizing set for a single state, and returns it as a {@link List}.
285         * 
286         * @see CharacterizingSets
287         * 
288         * @param automaton the automaton containing the state
289         * @param inputs the input symbols to consider
290         * @param state the state for which to determine a characterizing set
291         * @return a list containing the characterizing words
292         */
293        public static <S,I> List<Word<I>> stateCharacterizingSet(UniversalDeterministicAutomaton<S, I, ?, ?, ?> automaton,
294                        Collection<? extends I> inputs,
295                        S state) {
296                List<Word<I>> result = new ArrayList<Word<I>>();
297                stateCharacterizingSet(automaton, inputs, state, result);
298                return result;
299        }
300        
301        public static <I> void cover(DeterministicAutomaton<?, I, ?> automaton,
302                        Collection<? extends I> inputs, Collection<? super Word<I>> states, Collection<? super Word<I>> transitions) {
303                Covers.cover(automaton, inputs, states, transitions);
304        }
305        
306        public static <I> List<Word<I>> stateCover(DeterministicAutomaton<?, I, ?> automaton,
307                        Collection<? extends I> inputs) {
308                List<Word<I>> states = new ArrayList<Word<I>>(automaton.size());
309                cover(automaton, inputs, states, null);
310                return states;
311        }
312        
313        public static <I> List<Word<I>> transitionCover(DeterministicAutomaton<?, I, ?> automaton,
314                        Collection<? extends I> inputs) {
315                List<Word<I>> all = new ArrayList<Word<I>>(automaton.size() * inputs.size());
316                cover(automaton, inputs, all, all);
317                return all;
318        }
319}