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.incremental.dfa; 018 019import java.util.ArrayDeque; 020import java.util.ArrayList; 021import java.util.Collection; 022import java.util.Collections; 023import java.util.HashMap; 024import java.util.List; 025import java.util.Map; 026import java.util.Queue; 027 028import net.automatalib.automata.abstractimpl.AbstractDeterministicAutomaton; 029import net.automatalib.automata.concepts.StateIDs; 030import net.automatalib.automata.fsa.DFA; 031import net.automatalib.automata.fsa.impl.compact.CompactDFA; 032import net.automatalib.automata.graphs.AbstractAutomatonGraph; 033import net.automatalib.commons.util.UnionFind; 034import net.automatalib.commons.util.mappings.MutableMapping; 035import net.automatalib.graphs.UniversalGraph; 036import net.automatalib.graphs.concepts.NodeIDs; 037import net.automatalib.graphs.dot.DOTPlottableGraph; 038import net.automatalib.graphs.dot.GraphDOTHelper; 039import net.automatalib.incremental.ConflictException; 040import net.automatalib.incremental.IncrementalConstruction; 041import net.automatalib.words.Alphabet; 042import net.automatalib.words.Word; 043import net.automatalib.words.WordBuilder; 044 045public abstract class AbstractIncrementalDFABuilder<I> extends 046 AbstractDeterministicAutomaton<State, I, State> implements 047 UniversalGraph<State, EdgeRecord, Acceptance, I>, 048 DOTPlottableGraph<State, EdgeRecord>, 049 IncrementalConstruction<DFA<?, I>, I> { 050 051 protected final Map<StateSignature, State> register = new HashMap<>(); 052 053 protected final Alphabet<I> inputAlphabet; 054 protected final int alphabetSize; 055 protected final State init; 056 protected State sink; 057 058 public AbstractIncrementalDFABuilder(Alphabet<I> inputAlphabet) { 059 this.inputAlphabet = inputAlphabet; 060 this.alphabetSize = inputAlphabet.size(); 061 StateSignature sig = new StateSignature(alphabetSize, Acceptance.DONT_KNOW); 062 this.init = new State(sig); 063 register.put(null, init); 064 } 065 066 public abstract Acceptance lookup(Word<I> word); 067 068 public abstract void insert(Word<I> word, boolean accepting) throws ConflictException; 069 070 /** 071 * Inserts a word into the set of accepted words. 072 * @param word the word to insert 073 * @throws ConflictException if the word is already contained in the set of definitely 074 * rejected words 075 */ 076 public final void insert(Word<I> word) throws ConflictException { 077 insert(word, true); 078 } 079 080 /* 081 * (non-Javadoc) 082 * @see net.automatalib.ts.abstractimpl.AbstractFiniteDTS#size() 083 */ 084 @Override 085 public int size() { 086 return register.size() + ((sink != null) ? 1 : 0); 087 } 088 089 @Override 090 public Collection<State> getNodes() { 091 if(sink == null) 092 return Collections.unmodifiableCollection(register.values()); 093 List<State> result = new ArrayList<>(register.size() + 1); 094 result.addAll(register.values()); 095 result.add(sink); 096 return result; 097 } 098 099 @Override 100 public Collection<EdgeRecord> getOutgoingEdges(State node) { 101 List<EdgeRecord> edges = new ArrayList<EdgeRecord>(); 102 for(int i = 0; i < alphabetSize; i++) { 103 if((sink != null && node == sink) || node.getSuccessor(i) != null) 104 edges.add(new EdgeRecord(node, i)); 105 } 106 return edges; 107 } 108 109 @Override 110 public State getTarget(EdgeRecord edge) { 111 if(sink != null && edge.source == sink) 112 return edge.source; 113 return edge.source.getSuccessor(edge.transIdx); 114 } 115 116 @Override 117 public Acceptance getNodeProperty(State node) { 118 if(sink != null && node == sink) 119 return Acceptance.FALSE; 120 return node.getAcceptance(); 121 } 122 123 @Override 124 public I getEdgeProperty(EdgeRecord edge) { 125 return inputAlphabet.getSymbol(edge.transIdx); 126 } 127 128 @Override 129 public State getTransition(State state, I input) { 130 if(sink != null && state == sink) 131 return sink; 132 int idx = inputAlphabet.getSymbolIndex(input); 133 return state.getSuccessor(idx); 134 } 135 136 @Override 137 public State getSuccessor(State transition) { 138 return transition; 139 } 140 141 @Override 142 public State getInitialState() { 143 return init; 144 } 145 146 @Override 147 public Collection<State> getStates() { 148 return getNodes(); 149 } 150 151 @Override 152 public Alphabet<I> getInputAlphabet() { 153 return inputAlphabet; 154 } 155 156 @Override 157 public Word<I> findSeparatingWord(DFA<?, I> target, Collection<? extends I> inputs, boolean omitUndefined) { 158 return doFindSeparatingWord(target, inputs, omitUndefined); 159 } 160 161 @Override 162 public DFA<?, I> toAutomaton() { 163 CompactDFA<I> result = new CompactDFA<>(inputAlphabet, register.size() + ((sink != null) ? 1 : 0)); 164 Map<State,Integer> stateMap = new HashMap<>(); 165 166 for(State s : register.values()) { 167 Integer id; 168 boolean acc = (s.getAcceptance() == Acceptance.TRUE); 169 if(s == init) 170 id = result.addInitialState(acc); 171 else 172 id = result.addState(acc); 173 stateMap.put(s, id); 174 } 175 176 if(sink != null) 177 stateMap.put(sink, result.addState(false)); 178 179 for(Map.Entry<State,Integer> e : stateMap.entrySet()) { 180 State s = e.getKey(); 181 182 Integer srcId = e.getValue(); 183 for(int i = 0; i < inputAlphabet.size(); i++) { 184 State succ; 185 if(s == sink) 186 succ = sink; 187 else { 188 succ = s.getSuccessor(i); 189 if(succ == null) 190 continue; 191 } 192 I sym = inputAlphabet.getSymbol(i); 193 Integer succId = stateMap.get(succ); 194 result.addTransition(srcId, sym, succId); 195 } 196 } 197 198 return result; 199 } 200 201 /* 202 * (non-Javadoc) 203 * @see net.automatalib.incremental.IncrementalConstruction#hasDefinitiveInformation(net.automatalib.words.Word) 204 */ 205 @Override 206 public boolean hasDefinitiveInformation(Word<I> word) { 207 State s = getState(word); 208 if(s == null) 209 return false; 210 if(s == sink) 211 return true; 212 return (s.getAcceptance() != Acceptance.DONT_KNOW); 213 } 214 215 /* 216 * (non-Javadoc) 217 * @see net.automatalib.graphs.dot.DOTPlottableGraph#getGraphDOTHelper() 218 */ 219 @Override 220 public GraphDOTHelper<State, EdgeRecord> getGraphDOTHelper() { 221 return new DOTHelper(inputAlphabet, init); 222 } 223 224 225 @Override 226 public NodeIDs<State> nodeIDs() { 227 return AbstractAutomatonGraph.nodeIDs(this); 228 } 229 230 @Override 231 public <T> MutableMapping<State,T> createStaticNodeMapping() { 232 return AbstractAutomatonGraph.createStaticNodeMapping(this); 233 } 234 235 @Override 236 public <T> MutableMapping<State,T> createDynamicNodeMapping() { 237 return AbstractAutomatonGraph.createDynamicNodeMapping(this); 238 } 239 240 private static int getStateId(State s, Map<State,Integer> idMap) { 241 Integer id = idMap.get(s); 242 if(id != null) 243 return id.intValue(); 244 idMap.put(s, id = idMap.size()); 245 return id.intValue(); 246 } 247 248 private static final class Record<S,I> { 249 public final State state1; 250 public final S state2; 251 public final I reachedVia; 252 public final Record<S,I> reachedFrom; 253 public final int depth; 254 255 public Record(State state1, S state2) { 256 this.state1 = state1; 257 this.state2 = state2; 258 this.reachedVia = null; 259 this.reachedFrom = null; 260 this.depth = 0; 261 } 262 263 public Record(State state1, S state2, I reachedVia, Record<S,I> reachedFrom) { 264 this.state1 = state1; 265 this.state2 = state2; 266 this.reachedVia = reachedVia; 267 this.reachedFrom = reachedFrom; 268 this.depth = reachedFrom.depth + 1; 269 } 270 } 271 272 private <S> Word<I> doFindSeparatingWord(DFA<S,I> target, Collection<? extends I> inputs, boolean omitUndefined) { 273 int thisStates = register.size(); 274 Map<State,Integer> stateIds = new HashMap<>(); 275 if(sink != null) { 276 stateIds.put(sink, 0); 277 thisStates++; 278 } 279 int targetStates = target.size(); 280 if(!omitUndefined) 281 targetStates++; 282 283 UnionFind uf = new UnionFind(thisStates + targetStates); 284 285 State init1 = init; 286 S init2 = target.getInitialState(); 287 288 if(init2 == null && omitUndefined) 289 return null; 290 291 boolean acc = target.isAccepting(init2); 292 if(init1.getAcceptance().conflicts(acc)) 293 return Word.epsilon(); 294 295 StateIDs<S> tgtIds = target.stateIDs(); 296 int id1 = getStateId(init1, stateIds); 297 int id2 = ((init2 != null) ? tgtIds.getStateId(init2) : (targetStates - 1)) + thisStates; 298 299 uf.link(id1, id2); 300 301 Queue<Record<S,I>> queue = new ArrayDeque<>(); 302 303 queue.offer(new Record<S,I>(init1, init2)); 304 305 I lastSym = null; 306 307 Record<S,I> current; 308 309explore:while((current = queue.poll()) != null) { 310 State state1 = current.state1; 311 S state2 = current.state2; 312 313 for(I sym : inputs) { 314 S succ2 = (state2 != null) ? target.getSuccessor(state2, sym) : null; 315 if(succ2 == null && omitUndefined) 316 continue; 317 318 int idx = inputAlphabet.getSymbolIndex(sym); 319 State succ1 = (state1 != sink) ? state1.getSuccessor(idx) : sink; 320 321 if(succ1 == null) 322 continue; 323 324 id1 = getStateId(succ1, stateIds); 325 id2 = ((succ2 != null) ? tgtIds.getStateId(succ2) : (targetStates-1)) + thisStates; 326 327 int r1 = uf.find(id1), r2 = uf.find(id2); 328 329 if(r1 == r2) 330 continue; 331 332 if(succ1 == sink) { 333 if(succ2 == null) 334 continue; 335 if(target.isAccepting(succ2)) { 336 lastSym = sym; 337 break explore; 338 } 339 } 340 else { 341 boolean succ2acc = (succ2 != null) ? target.isAccepting(succ2) : false; 342 if(succ1.getAcceptance().conflicts(succ2acc)) { 343 lastSym = sym; 344 break explore; 345 } 346 } 347 348 uf.link(r1, r2); 349 350 queue.offer(new Record<>(succ1, succ2, sym, current)); 351 } 352 } 353 354 if(current == null) 355 return null; 356 357 int ceLength = current.depth; 358 if(lastSym != null) 359 ceLength++; 360 361 WordBuilder<I> wb = new WordBuilder<I>(null, ceLength); 362 363 int index = ceLength; 364 365 if(lastSym != null) 366 wb.setSymbol(--index, lastSym); 367 368 while(current.reachedFrom != null) { 369 wb.setSymbol(--index, current.reachedVia); 370 current = current.reachedFrom; 371 } 372 373 return wb.toWord(); 374 } 375 376 377 378 protected abstract State getState(Word<I> word); 379 380 /** 381 * Returns (and possibly creates) the canonical state for the given signature. 382 * @param sig the signature 383 * @return the canonical state for the given signature 384 */ 385 protected State replaceOrRegister(StateSignature sig) { 386 State state = register.get(sig); 387 if(state != null) 388 return state; 389 390 register.put(sig, state = new State(sig)); 391 for(int i = 0; i < sig.successors.length; i++) { 392 State succ = sig.successors[i]; 393 if(succ != null) 394 succ.increaseIncoming(); 395 } 396 return state; 397 } 398 399 /** 400 * Returns the canonical state for the given state's signature, or registers the 401 * state as canonical if no state with that signature exists. 402 * @param state the state 403 * @return the canonical state for the given state's signature 404 */ 405 protected State replaceOrRegister(State state) { 406 StateSignature sig = state.getSignature(); 407 State other = register.get(sig); 408 if(other != null) { 409 if(state != other) { 410 for(int i = 0; i < sig.successors.length; i++) { 411 State succ = sig.successors[i]; 412 if(succ != null) 413 succ.decreaseIncoming(); 414 } 415 } 416 return other; 417 } 418 419 register.put(sig, state); 420 return state; 421 } 422 423 protected void updateInitSignature(Acceptance acc) { 424 StateSignature sig = init.getSignature(); 425 sig.acceptance = acc; 426 } 427 428 429 /** 430 * Updates the signature for a given state. 431 * @param state the state 432 * @param acc the new acceptance value 433 * @return the canonical state for the updated signature 434 */ 435 protected State updateSignature(State state, Acceptance acc) { 436 StateSignature sig = state.getSignature(); 437 if(sig.acceptance == acc) 438 return state; 439 register.remove(sig); 440 sig.acceptance = acc; 441 sig.updateHashCode(); 442 return replaceOrRegister(state); 443 } 444 445 protected void updateInitSignature(int idx, State succ) { 446 StateSignature sig = init.getSignature(); 447 State oldSucc = sig.successors[idx]; 448 if(oldSucc == succ) 449 return; 450 if(oldSucc != null) 451 oldSucc.decreaseIncoming(); 452 sig.successors[idx] = succ; 453 succ.increaseIncoming(); 454 } 455 456 /** 457 * Updates the signature for a given state. 458 * @param state the state 459 * @param idx the index of the transition to change 460 * @param succ the new successor for the above index 461 * @return the canonical state for the updated signature 462 */ 463 protected State updateSignature(State state, int idx, State succ) { 464 StateSignature sig = state.getSignature(); 465 if(sig.successors[idx] == succ) 466 return state; 467 register.remove(sig); 468 if(sig.successors[idx] != null) 469 sig.successors[idx].decreaseIncoming(); 470 471 sig.successors[idx] = succ; 472 succ.increaseIncoming(); 473 sig.updateHashCode(); 474 return replaceOrRegister(state); 475 } 476 477 protected State updateSignature(State state, Acceptance acc, int idx, State succ) { 478 StateSignature sig = state.getSignature(); 479 if(sig.successors[idx] == succ && sig.acceptance == acc) 480 return state; 481 register.remove(sig); 482 sig.successors[idx] = succ; 483 sig.acceptance = acc; 484 return replaceOrRegister(state); 485 } 486 487 /** 488 * Clones a state, changing the signature. 489 * @param other the state to clone 490 * @param acc the new acceptance value 491 * @return the canonical state for the derived signature 492 */ 493 protected State clone(State other, Acceptance acc) { 494 StateSignature sig = other.getSignature(); 495 if(sig.acceptance == acc) 496 return other; 497 sig = sig.clone(); 498 sig.acceptance = acc; 499 sig.updateHashCode(); 500 return replaceOrRegister(sig); 501 } 502 503 /** 504 * Clones a state, changing the signature. 505 * @param other the state to clone 506 * @param idx the index of the transition to change 507 * @param succ the new successor state 508 * @return the canonical state for the derived signature 509 */ 510 protected State clone(State other, int idx, State succ) { 511 StateSignature sig = other.getSignature(); 512 if(sig.successors[idx] == succ) 513 return other; 514 sig = sig.clone(); 515 sig.successors[idx] = succ; 516 sig.updateHashCode(); 517 return replaceOrRegister(sig); 518 } 519 520 protected State clone(State other, Acceptance acc, int idx, State succ) { 521 StateSignature sig = other.getSignature(); 522 if(sig.successors[idx] == succ && sig.acceptance == acc) 523 return other; 524 sig = sig.clone(); 525 sig.successors[idx] = succ; 526 sig.acceptance = acc; 527 return replaceOrRegister(sig); 528 } 529 530}