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.minimizer;
018
019import java.util.Collection;
020import java.util.HashMap;
021import java.util.Iterator;
022import java.util.List;
023import java.util.Map;
024
025import net.automatalib.commons.smartcollections.DefaultLinkedList;
026import net.automatalib.commons.smartcollections.ElementReference;
027import net.automatalib.commons.smartcollections.IntrusiveLinkedList;
028import net.automatalib.commons.smartcollections.UnorderedCollection;
029import net.automatalib.commons.util.mappings.MutableMapping;
030import net.automatalib.graphs.UniversalGraph;
031import net.automatalib.util.graphs.traversal.GraphTraversal;
032
033
034/**
035 * Automaton minimizer. The automata are accessed via the 
036 * {@link AutomatonInterface}, and may be partially defined. Note that
037 * undefined transitions are preserved, thus, they have no semantics that
038 * could be modeled otherwise wrt. this algorithm.
039 * <p>
040 * The implemented algorithm is described in the paper "Minimizing incomplete
041 * automata" by Marie-Pierre Beal and Maxime Crochemore.
042 * 
043 * @author Malte Isberner <malte.isberner@gmail.com>
044 *
045 * @param <S> state class.
046 * @param <L> transition label class.
047 */
048public class Minimizer<S,L> {
049        
050        private static final ThreadLocal<Minimizer<Object,Object>> LOCAL_INSTANCE
051                = new ThreadLocal<Minimizer<Object,Object>>() {
052                        @Override
053                        protected Minimizer<Object, Object> initialValue() {
054                                return new Minimizer<Object, Object>();
055                        }
056        };
057        
058        
059        /**
060         * Retrieves the local instance of this minimizer.
061         * 
062         * The minimizer acts like a singleton of which each thread possesses their
063         * own. The minimizer instance returned by this method is the one belonging
064         * to the calling thread. Therefore, it is not safe to share such an instance
065         * between two threads.
066         * 
067         * @param <S> state class.
068         * @param <L> transition label class.
069         * @return The minimizers local instance.
070         */
071        @SuppressWarnings("unchecked")
072        public static <S,L> Minimizer<S,L> getLocalInstance() {
073                return (Minimizer<S,L>)LOCAL_INSTANCE.get();
074        }
075        
076        /**
077         * Minimizes an automaton. The automaton is not minimized directly, instead,
078         * a {@link MinimizationResult} structure is returned. The automaton is
079         * interfaced using an adapter implementing the {@link AutomatonInterface}
080         * interface.
081         * 
082         * @param <S> state class.
083         * @param <L> transition label class.
084         * @param graph the automaton interface.
085         * @return the result structure.
086         */
087        public static <S,L> MinimizationResult<S, L> minimize(UniversalGraph<S, ?, ?, L> graph) {
088                return minimize(graph, null);
089        }
090        
091        public static <S,L> MinimizationResult<S, L> minimize(UniversalGraph<S, ?, ?, L> graph, Collection<? extends S> start) {
092                Minimizer<S,L> minimizer = getLocalInstance();
093                return minimizer.performMinimization(graph, start);
094        }
095        
096        // These attributes belong to a specific minimization process.
097        private MutableMapping<S,State<S,L>> stateStorage;
098        private UnorderedCollection<Block<S,L>> partition;
099        private int numBlocks;
100        
101        // The following attributes may be reused. Most of them are used
102        // as local variables in the split() method, but storing them
103        // as attributes helps to avoid costly re-allocations. 
104        private final DefaultLinkedList<Block<S,L>> splitters
105                = new DefaultLinkedList<Block<S,L>>();
106        private final IntrusiveLinkedList<TransitionLabel<S, L>> letterList
107                = new IntrusiveLinkedList<TransitionLabel<S,L>>();
108        private final IntrusiveLinkedList<State<S,L>> stateList
109                = new IntrusiveLinkedList<State<S,L>>();
110        private final IntrusiveLinkedList<Block<S,L>> splitBlocks
111                = new IntrusiveLinkedList<Block<S,L>>();
112        private final IntrusiveLinkedList<Block<S,L>>  newBlocks
113                = new IntrusiveLinkedList<Block<S,L>>();
114        private final IntrusiveLinkedList<State<S,L>> finalList
115                = new IntrusiveLinkedList<State<S,L>>();
116        
117        
118        
119        /**
120         * Default constructor.
121         * @deprecated Public instantiation is deprecated. Use {@link #getLocalInstance()}
122         * or {@link #apply(AutomatonInterface)}
123         */
124        @Deprecated
125        public Minimizer() {
126        }
127        
128        
129        
130        public final <E> MinimizationResult<S,L> performMinimization(UniversalGraph<S,E,?,L> graph) {
131                return performMinimization(graph, null);
132        }
133        
134        /**
135         * Performs the minimization of an automaton.
136         * 
137         * The automaton is accessed via an {@link AutomatonInterface}. The result
138         * of the minimization process is effectively a partition on the set of
139         * states, each element (block) in this partition contains equivalent
140         * states that can be merged in a minimized automaton.
141         * 
142         * @param <E> edge identifier class.
143         * @param graph the automaton interface.
144         * @return a {@link MinimizationResult} structure, containing the
145         * state partition.
146         */
147        public final <E>
148                        MinimizationResult<S,L> performMinimization(UniversalGraph<S,E,?,L> graph, Collection<? extends S> initialNodes) {
149                // Initialize the data structures (esp. state records) and build
150                // the initial partition.
151                Collection<Block<S,L>> initialBlocks
152                        = initialize(graph, initialNodes);
153                
154                // Add all blocks from the initial partition as an element
155                // of the partition, and as a potential splitter.
156                partition = new UnorderedCollection<Block<S,L>>(initialBlocks.size());
157                ///splitters.hintNextCapacity(initialBlocks.size());
158                
159                for(Block<S,L> block : initialBlocks) {
160                        if(block == null || block.isEmpty())
161                                continue;
162                        addToPartition(block);
163                        addToSplitterQueue(block);
164                        numBlocks++;
165                }
166                
167                // Split the blocks of the partition, until no splitters
168                // remain
169                while(!splitters.isEmpty()) {
170                        Block<S,L> block = splitters.choose();
171                        removeFromSplitterQueue(block);
172                        
173                        split(block);
174                        updateBlocks();
175                }
176                
177                // Return the result.
178                MinimizationResult<S,L> result = new MinimizationResult<S, L>(stateStorage, partition);
179                
180                // Ensure the garbage collection isn't hampered
181                stateStorage = null;
182                partition = null;
183                numBlocks = 0;
184                
185                return result;
186        }
187        
188        /*
189         * Sets the blockReference-attribute of each state in the collection
190         * to the corresponding ElementReference of the collection.
191         */
192        private static <S,L> void updateBlockReferences(Block<S,L> block) {
193                UnorderedCollection<State<S,L>> states = block.getStates();
194                for(ElementReference ref : states.references()) {
195                        State<S,L> state = states.get(ref);
196                        state.setBlockReference(ref);
197                        state.setBlock(block);
198                }
199        }
200        
201        /*
202         * Builds the initial data structures and performs the initial
203         * partitioning.
204         */
205        private <E> Collection<Block<S,L>> initialize(UniversalGraph<S,E,?,L> graph, Collection<? extends S> initialNodes) {
206                Iterable<? extends S> origStates;
207                if(initialNodes == null || initialNodes.isEmpty())
208                        origStates = graph.getNodes();
209                else
210                        origStates = GraphTraversal.depthFirstOrder(graph, initialNodes);
211                
212                Map<L,TransitionLabel<S,L>> transitionMap = new HashMap<L,TransitionLabel<S,L>>();
213                
214                stateStorage = graph.createStaticNodeMapping();
215                
216                int numStates = 0;
217                for(S origState : origStates) {
218                        State<S,L> state = new State<S,L>(numStates++, origState);
219                        stateStorage.put(origState, state);
220                        stateList.add(state);
221                }
222                
223                
224                InitialPartitioning<S, L> initPartitioning = new HashMapInitialPartitioning<S, L>(graph);
225                
226                
227                for(State<S,L> state : stateList) {
228                        S origState = state.getOriginalState();
229                        
230                        Block<S,L> block = initPartitioning.getBlock(origState);
231                        block.addState(state);
232                        
233                        for(E edge : graph.getOutgoingEdges(origState)) {
234                                S origTarget = graph.getTarget(edge);
235                                State<S,L> target = stateStorage.get(origTarget);
236                                L label = graph.getEdgeProperty(edge);
237                                TransitionLabel<S,L> transition = transitionMap.get(label);
238                                if(transition == null) {
239                                        transition = new TransitionLabel<S,L>(label);
240                                        transitionMap.put(label, transition);
241                                }
242                                Edge<S,L> edgeObj = new Edge<S,L>(state, target, transition);
243                                state.addOutgoingEdge(edgeObj);
244                                target.addIncomingEdge(edgeObj);
245                        }
246                }
247                stateList.quickClear();
248                
249                return initPartitioning.getInitialBlocks();
250        }
251        
252        
253        
254        /*
255         * Adds a block to the partition.
256         */
257        private void addToPartition(Block<S,L> block) {
258                ElementReference ref = partition.referencedAdd(block);
259                block.setPartitionReference(ref);
260        }
261        
262        
263        /*
264         * Adds a block as a potential splitter.
265         */
266        private void addToSplitterQueue(Block<S,L> block) {
267                ElementReference ref = splitters.referencedAdd(block);
268                block.setSplitterQueueReference(ref);
269        }
270        
271        /*
272         * Removes a block from the splitter queue. This is done when it is
273         * split completely and thus no longer existant.
274         */
275        private boolean removeFromSplitterQueue(Block<S,L> block) {
276                ElementReference ref = block.getSplitterQueueReference();
277                if(ref == null)
278                        return false;
279                
280                splitters.remove(ref);
281                block.setSplitterQueueReference(null);
282                
283                return true;
284        }
285        
286        /*
287         * Adds all but the largest block of a given collection
288         * to the splitter queue.
289         */
290        private void addAllToSplitterQueue(Collection<Block<S,L>> blocks) {
291                for(Block<S,L> block : blocks)
292                        addToSplitterQueue(block);
293        }
294        
295        private void addAllButLargest(Collection<Block<S,L>>  blocks) {
296                Block<S,L> largest = null;
297                
298                for(Block<S,L> block : blocks) {
299                        if(largest == null)
300                                largest = block;
301                        else if(block.size() > largest.size()) {
302                                addToSplitterQueue(largest);
303                                largest = block;
304                        }
305                        else
306                                addToSplitterQueue(block);
307                }
308        }
309        
310        /*
311         * This method performs the actual splitting of blocks, using the
312         * sub block information stored in each block object.
313         */
314        private void updateBlocks() {
315                for(Block<S,L> block : splitBlocks) {
316                        // Ignore blocks that have no elements in their sub blocks.
317                        int inSubBlocks = block.getElementsInSubBlocks();
318                        if(inSubBlocks == 0)
319                                continue;
320                
321                        boolean blockRemains = (inSubBlocks < block.size());
322                        
323                        boolean reuseBlock = !blockRemains;
324                        
325                        List<UnorderedCollection<State<S,L>>> subBlocks = block.getSubBlocks();
326                        // If there is only one sub block which contains all elements of
327                        // the block, then no split needs to be performed.
328                        if(!blockRemains && subBlocks.size() == 1) {
329                                block.clearSubBlocks();
330                                continue;
331                        }
332                        
333                        Iterator<UnorderedCollection<State<S,L>>> subBlockIt = subBlocks.iterator();
334                        
335                        if(reuseBlock) {
336                                UnorderedCollection<State<S,L>> first
337                                        = subBlockIt.next();
338                                block.getStates().swap(first);
339                                updateBlockReferences(block);
340                        }
341                        
342                        while(subBlockIt.hasNext()) {
343                                UnorderedCollection<State<S,L>> subBlockStates = subBlockIt.next();
344                
345                                if(blockRemains) {
346                                        for(State<S,L> state : subBlockStates)
347                                                block.removeState(state.getBlockReference());
348                                }
349                                
350                                
351                                Block<S,L> subBlock = new Block<S,L>(numBlocks++, subBlockStates);
352                                updateBlockReferences(subBlock);
353                                newBlocks.add(subBlock);
354                                addToPartition(subBlock);
355                        }
356        
357                        newBlocks.add(block);
358                        block.clearSubBlocks();
359                        
360                        // If the split block previously was in the queue, add all newly
361                        // created blocks to the queue. Otherwise, it's enough to add
362                        // all but the largest
363                        if(removeFromSplitterQueue(block))
364                                addAllToSplitterQueue(newBlocks);
365                        else
366                                addAllButLargest(newBlocks);
367                        newBlocks.clear();
368                }
369                
370                splitBlocks.clear();
371        }
372        
373        /*
374         * This method realizes the core of the actual minimization, the "split"
375         * procedure.
376         * 
377         * A split separates in each block the states, if any, which have different
378         * transition characteristics wrt. a specified block, the splitter.
379         * 
380         * This method does not perform actual splits, but instead it modifies
381         * the splitBlocks attribute to containing the blocks that could
382         * potentially be split. The information
383         * on the subsets into which a block is split is contained in the
384         * sub-blocks of the blocks in the result list.
385         * 
386         * The actual splitting is performed by the method updateBlocks().
387         */
388        private void split(Block<S,L> splitter) {
389                // STEP 1: Collect the states that have outgoing edges
390                // pointing to states inside the currently considered blocks.
391                // Also, a list of transition labels occuring on these
392                // edges is created.
393                for(State<S,L> state : splitter.getStates()) {
394                        for(Edge<S,L> edge : state.getIncoming()) {
395                                TransitionLabel<S,L> transition = edge.getTransitionLabel();
396                                State<S,L> newState = edge.getSource();
397                                // Blocks that only contain a single state cannot
398                                // be split any further, and thus are of no
399                                // interest.
400                                if(newState.isSingletonBlock())
401                                        continue; //continue;
402                                if(transition.addToSet(newState))
403                                        letterList.add(transition);
404                        }
405                }
406                
407                // STEP 2: Build the signatures. A signature of a state
408                // is a sequence of the transition labels of its outgoing
409                // edge that point into the considered split block.
410                // The iteration over the label list in the outer loop
411                // guarantees a consistent ordering of the transition labels.
412                for(TransitionLabel<S,L> letter : letterList) {
413                        for(State<S,L> state : letter.getSet()) {
414                                if(state.addToSignature(letter)) {
415                                        stateList.add(state);
416                                        state.setSplitPoint(false);
417                                }
418                        }
419                        letter.clearSet();
420                }
421                letterList.clear();
422                
423                
424                // STEP 3: Discriminate the states. This is done by weak
425                // sorting the states. At the end of the weak sort, the finalList
426                // will contain the states in such an order that only states belonging
427                // to the same block having the same signature will be contiguous.
428                
429                // First, initialize the buckets of each block. This is done
430                // for grouping the states by their corresponding block.
431                for(State<S,L> state : stateList) {
432                        Block<S,L> block = state.getBlock();
433                        if(block.addToBucket(state))
434                                splitBlocks.add(block);
435                }
436                stateList.clear();
437                
438                
439                for(Block<S,L> block : splitBlocks)
440                        stateList.concat(block.getBucket());
441                
442                
443                // Now, the states are ordered according to their signatures
444                int i = 0;
445                
446                while(!stateList.isEmpty()) {
447                        for(State<S,L> state : stateList) {
448                                TransitionLabel<S,L> letter = state.getSignatureLetter(i);
449                                if(letter == null)
450                                        finalList.pushBack(state);
451                                else if(letter.addToBucket(state))
452                                        letterList.add(letter);
453                                
454                                // If this state was the first to be added to the respective
455                                // bucket, or it differs from the previous entry in the previous
456                                // letter, it is a split point.
457                                if(state.getPrev() == null)
458                                        state.setSplitPoint(true);
459                                else if(i > 0 && state.getPrev().getSignatureLetter(i-1) != state.getSignatureLetter(i-1))
460                                        state.setSplitPoint(true);
461                        }
462                        stateList.clear();
463                        
464                        for(TransitionLabel<S,L> letter : letterList)
465                                stateList.concat(letter.getBucket());
466                        letterList.clear();
467                        
468                        i++;
469                }
470                
471                
472                Block<S,L> prevBlock = null;
473                
474                State<S,L> prev = null;
475                for(State<S,L> state : finalList) {
476                        Block<S,L> currBlock = state.getBlock();
477                        if(currBlock != prevBlock) {
478                                currBlock.createSubBlock();
479                                prevBlock = currBlock;
480                        }
481                        else if(state.isSplitPoint())
482                                currBlock.createSubBlock();
483                        currBlock.addToSubBlock(state);
484                        if(prev != null)
485                                prev.reset();
486                        prev = state;
487                }
488                if(prev != null)
489                        prev.reset();
490                finalList.clear();
491                
492                // Step 4 of the algorithm is done in the method
493                // updateBlocks()
494        }
495
496}