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}