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.mealy; 018 019import java.util.ArrayDeque; 020import java.util.ArrayList; 021import java.util.Collection; 022import java.util.Collections; 023import java.util.Deque; 024import java.util.HashMap; 025import java.util.Iterator; 026import java.util.List; 027import java.util.Map; 028import java.util.Objects; 029import java.util.Queue; 030 031import net.automatalib.automata.abstractimpl.AbstractDeterministicAutomaton; 032import net.automatalib.automata.concepts.StateIDs; 033import net.automatalib.automata.concepts.TransitionOutput; 034import net.automatalib.automata.graphs.AbstractAutomatonGraph; 035import net.automatalib.automata.graphs.TransitionEdge.Property; 036import net.automatalib.automata.transout.MealyMachine; 037import net.automatalib.automata.transout.impl.compact.CompactMealy; 038import net.automatalib.commons.util.UnionFind; 039import net.automatalib.commons.util.mappings.MutableMapping; 040import net.automatalib.graphs.UniversalGraph; 041import net.automatalib.graphs.concepts.NodeIDs; 042import net.automatalib.graphs.dot.DOTPlottableGraph; 043import net.automatalib.graphs.dot.GraphDOTHelper; 044import net.automatalib.incremental.ConflictException; 045import net.automatalib.incremental.IncrementalConstruction; 046import net.automatalib.words.Alphabet; 047import net.automatalib.words.Word; 048import net.automatalib.words.WordBuilder; 049 050/** 051 * Incrementally builds an (acyclic) Mealy machine, from a set of input and corresponding 052 * output words. 053 * 054 * @author Malte Isberner <malte.isberner@gmail.com> 055 * 056 * @param <I> input symbol class 057 * @param <O> output symbol class 058 */ 059public class IncrementalMealyBuilder<I, O> extends 060 AbstractDeterministicAutomaton<State, I, TransitionRecord> implements 061 TransitionOutput<TransitionRecord, O>, 062 UniversalGraph<State, TransitionRecord, Void, Property<I,O>>, 063 DOTPlottableGraph<State, TransitionRecord>, 064 IncrementalConstruction<MealyMachine<?,I,?,O>, I> { 065 066 067 private final Map<StateSignature, State> register = new HashMap<>(); 068 069 private final Alphabet<I> inputAlphabet; 070 private final int alphabetSize; 071 private final State init; 072 073 /** 074 * Constructor. 075 * @param inputAlphabet the input alphabet to use 076 */ 077 public IncrementalMealyBuilder(Alphabet<I> inputAlphabet) { 078 this.inputAlphabet = inputAlphabet; 079 this.alphabetSize = inputAlphabet.size(); 080 StateSignature initSig = new StateSignature(alphabetSize); 081 this.init = new State(initSig); 082 register.put(null, init); 083 } 084 085 /* 086 * (non-Javadoc) 087 * @see net.automatalib.automata.abstractimpl.AbstractDeterministicAutomaton#size() 088 */ 089 @Override 090 public int size() { 091 return register.size(); 092 } 093 094 /** 095 * Retrieves the (internal) state reached by the given input word, 096 * or <tt>null</tt> if no information about the input word is present. 097 * @param word the input word 098 * @return the corresponding state 099 */ 100 private State getState(Word<I> word) { 101 State s = init; 102 103 for (I sym : word) { 104 int idx = inputAlphabet.getSymbolIndex(sym); 105 s = s.getSuccessor(idx); 106 if (s == null) 107 return null; 108 } 109 return s; 110 } 111 112 /** 113 * Checks whether there exists secured information about the output 114 * for the given word. 115 * @param word the input word 116 * @return a boolean indicating whether information about the output for the 117 * given input word exists. 118 */ 119 public boolean isComplete(Word<I> word) { 120 State s = getState(word); 121 return (s != null); 122 } 123 124 /** 125 * Retrieves the output word for the given input word. If no definitive information 126 * for the input word exists, the output for the longest known prefix will be returned. 127 * @param word the input word 128 * @param output a {@link WordBuilder} for constructing the output word 129 * @return <tt>true</tt> if the information contained was complete (in this case, 130 * <code>word.length() == output.size()</code> will hold), <tt>false</tt> otherwise. 131 */ 132 @SuppressWarnings("unchecked") 133 public boolean lookup(Word<I> word, WordBuilder<O> output) { 134 State curr = init; 135 for(I sym : word) { 136 int idx = inputAlphabet.getSymbolIndex(sym); 137 State succ = curr.getSuccessor(idx); 138 if(succ == null) 139 return false; 140 output.append((O)curr.getOutput(idx)); 141 curr = succ; 142 } 143 144 return true; 145 } 146 147 148 /** 149 * Incorporates a pair of input/output words into the stored information. 150 * @param word the input word 151 * @param outputWord the corresponding output word 152 * @throws ConflictException if this information conflicts with information already stored 153 */ 154 public void insert(Word<I> word, Word<O> outputWord) { 155 int len = word.length(); 156 157 State curr = init; 158 State conf = null; 159 160 Deque<PathElem> path = new ArrayDeque<>(); 161 162 // Find the internal state in the automaton that can be reached by a 163 // maximal prefix of the word (i.e., a path of secured information) 164 Iterator<O> outWordIterator = outputWord.iterator(); 165 for (I sym : word) { 166 // During this, store the *first* confluence state (i.e., state with 167 // multiple incoming edges). 168 if (conf == null && curr.isConfluence()) { 169 conf = curr; 170 } 171 172 int idx = inputAlphabet.getSymbolIndex(sym); 173 State succ = curr.getSuccessor(idx); 174 if (succ == null) 175 break; 176 177 // If a transition exists for the input symbol, it also has an output symbol. 178 // Check if this matches the provided one, otherwise there is a conflict 179 O outSym = outWordIterator.next(); 180 if(!Objects.equals(outSym, curr.getOutput(idx))) { 181 throw new ConflictException("Error inserting " + word.prefix(path.size()+1) + " / " + outputWord.prefix(path.size()+1) + ": Incompatible output symbols: " + outSym + " vs " + curr.getOutput(idx)); 182 } 183 path.push(new PathElem(curr, idx)); 184 curr = succ; 185 } 186 187 State last = curr; 188 189 int prefixLen = path.size(); 190 191 // The information was already present - we do not need to continue 192 if (prefixLen == len) { 193 return; 194 } 195 196 if(conf != null) { 197 if(conf == last) { 198 conf = null; 199 } 200 last = hiddenClone(last); 201 } 202 else if(last != init) { 203 hide(last); 204 } 205 206 // We then create a suffix path, i.e., a linear sequence of states corresponding to 207 // the suffix (more precisely: the suffix minus the first symbol, since this is the 208 // transition which is used for gluing the suffix path to the existing automaton). 209 Word<I> suffix = word.subWord(prefixLen); 210 Word<O> suffixOut = outputWord.subWord(prefixLen); 211 212 // Here we prepare the "gluing" transition 213 I sym = suffix.firstSymbol(); 214 int suffTransIdx = inputAlphabet.getSymbolIndex(sym); 215 O suffTransOut = suffixOut.firstSymbol(); 216 217 State suffixState = createSuffix(suffix.subWord(1), suffixOut.subWord(1)); 218 219 if(last != init) { 220 last = unhide(last, suffTransIdx, suffixState, suffTransOut); 221 } 222 else { 223 updateInitSignature(suffTransIdx, suffixState, suffTransOut); 224 } 225 226 if(path.isEmpty()) { 227 return; 228 } 229 230 if (conf != null) { 231 // If there was a confluence state, we have to clone all nodes on 232 // the prefix path up to this state, in order to separate it from 233 // other 234 // prefixes reaching the confluence state (we do not know anything 235 // about them 236 // plus the suffix). 237 PathElem next; 238 do { 239 next = path.pop(); 240 State state = next.state; 241 int idx = next.transIdx; 242 state = clone(state, idx, last); 243 last = state; 244 } while(next.state != conf); 245 } 246 247 // Finally, we have to refresh all the signatures, iterating backwards 248 // until the updating becomes stable. 249 while(path.size() > 1) { 250 PathElem next = path.pop(); 251 State state = next.state; 252 int idx = next.transIdx; 253 State updated = updateSignature(state, idx, last); 254 if(state == updated) 255 return; 256 last = updated; 257 } 258 259 int finalIdx = path.pop().transIdx; 260 261 updateInitSignature(finalIdx, last); 262 } 263 264 265 /** 266 * Update the signature of the initial state. This requires special handling, as the 267 * initial state is not stored in the register (since it can never legally act as a predecessor). 268 * @param idx the transition index being changed 269 * @param succ the new successor state 270 */ 271 private void updateInitSignature(int idx, State succ) { 272 StateSignature sig = init.getSignature(); 273 State oldSucc = sig.successors[idx]; 274 if(oldSucc == succ) 275 return; 276 if(oldSucc != null) 277 oldSucc.decreaseIncoming(); 278 sig.successors[idx] = succ; 279 succ.increaseIncoming(); 280 } 281 282 /** 283 * Update the signature of a state, changing only the successor state of a single transition 284 * index. 285 * @param state the state which's signature to update 286 * @param idx the transition index to modify 287 * @param succ the new successor state 288 * @return the resulting state, which can either be the same as the input state (if the new 289 * signature is unique), or the result of merging with another state. 290 */ 291 private State updateSignature(State state, int idx, State succ) { 292 StateSignature sig = state.getSignature(); 293 if (sig.successors[idx] == succ) 294 return state; 295 296 register.remove(sig); 297 if(sig.successors[idx] != null) 298 sig.successors[idx].decreaseIncoming(); 299 sig.successors[idx] = succ; 300 succ.increaseIncoming(); 301 sig.updateHashCode(); 302 return replaceOrRegister(state); 303 } 304 305 private State unhide(State state, int idx, State succ, O out) { 306 StateSignature sig = state.getSignature(); 307 State prevSucc = sig.successors[idx]; 308 if(prevSucc != null) { 309 prevSucc.decreaseIncoming(); 310 } 311 sig.successors[idx] = succ; 312 if(succ != null) { 313 succ.increaseIncoming(); 314 } 315 sig.outputs[idx] = out; 316 sig.updateHashCode(); 317 return replaceOrRegister(state); 318 } 319 320 /** 321 * Updates the signature of the initial state, changing both the successor state 322 * and the output symbol. 323 * @param idx the transition index to change 324 * @param succ the new successor state 325 * @param out the output symbol 326 */ 327 private void updateInitSignature(int idx, State succ, O out) { 328 StateSignature sig = init.getSignature(); 329 State oldSucc = sig.successors[idx]; 330 if(oldSucc == succ && Objects.equals(out, sig.outputs[idx])) { 331 return; 332 } 333 if(oldSucc != null) { 334 oldSucc.decreaseIncoming(); 335 } 336 sig.successors[idx] = succ; 337 sig.outputs[idx] = out; 338 succ.increaseIncoming(); 339 } 340 341 342 343 private State clone(State other, int idx, State succ) { 344 StateSignature sig = other.getSignature(); 345 if (sig.successors[idx] == succ) 346 return other; 347 sig = sig.clone(); 348 sig.successors[idx] = succ; 349 sig.updateHashCode(); 350 return replaceOrRegister(sig); 351 } 352 353 private State hiddenClone(State other) { 354 StateSignature sig = other.getSignature().clone(); 355 356 for(int i = 0; i < alphabetSize; i++) { 357 State succ = sig.successors[i]; 358 if(succ != null) { 359 succ.increaseIncoming(); 360 } 361 } 362 return new State(sig); 363 } 364 365 private State replaceOrRegister(StateSignature sig) { 366 State state = register.get(sig); 367 if (state != null) 368 return state; 369 370 register.put(sig, state = new State(sig)); 371 for (int i = 0; i < sig.successors.length; i++) { 372 State succ = sig.successors[i]; 373 if (succ != null) 374 succ.increaseIncoming(); 375 } 376 return state; 377 } 378 379 private void hide(State state) { 380 assert state != init; 381 StateSignature sig = state.getSignature(); 382 383 register.remove(sig); 384 } 385 386 private State replaceOrRegister(State state) { 387 StateSignature sig = state.getSignature(); 388 State other = register.get(sig); 389 if (other != null) { 390 if (state != other) { 391 for (int i = 0; i < sig.successors.length; i++) { 392 State succ = sig.successors[i]; 393 if(succ != null) 394 succ.decreaseIncoming(); 395 } 396 } 397 return other; 398 } 399 400 register.put(sig, state); 401 return state; 402 } 403 404 private State createSuffix(Word<I> suffix, Word<O> suffixOut) { 405 StateSignature sig = new StateSignature(alphabetSize); 406 sig.updateHashCode(); 407 State last = replaceOrRegister(sig); 408 409 int len = suffix.length(); 410 for (int i = len - 1; i >= 0; i--) { 411 sig = new StateSignature(alphabetSize); 412 I sym = suffix.getSymbol(i); 413 O outsym = suffixOut.getSymbol(i); 414 int idx = inputAlphabet.getSymbolIndex(sym); 415 sig.successors[idx] = last; 416 sig.outputs[idx] = outsym; 417 sig.updateHashCode(); 418 last = replaceOrRegister(sig); 419 } 420 421 return last; 422 } 423 424 425 /* 426 * (non-Javadoc) 427 * @see net.automatalib.ts.TransitionSystem#getSuccessor(java.lang.Object) 428 */ 429 @Override 430 public State getSuccessor(TransitionRecord transition) { 431 return transition.source.getSuccessor(transition.transIdx); 432 } 433 434 /* 435 * (non-Javadoc) 436 * @see net.automatalib.ts.SimpleDTS#getInitialState() 437 */ 438 @Override 439 public State getInitialState() { 440 return init; 441 } 442 443 /* 444 * (non-Javadoc) 445 * @see net.automatalib.graphs.UniversalGraph#getNodeProperties(java.lang.Object) 446 */ 447 @Override 448 public Void getNodeProperty(State node) { 449 return null; 450 } 451 452 /* 453 * (non-Javadoc) 454 * @see net.automatalib.graphs.UniversalGraph#getEdgeProperties(java.lang.Object) 455 */ 456 @Override 457 @SuppressWarnings("unchecked") 458 public Property<I, O> getEdgeProperty(TransitionRecord edge) { 459 I input = inputAlphabet.getSymbol(edge.transIdx); 460 O out = (O)edge.source.getOutput(edge.transIdx); 461 return new Property<>(input, out); 462 } 463 464 /* 465 * (non-Javadoc) 466 * @see net.automatalib.graphs.IndefiniteGraph#getOutgoingEdges(java.lang.Object) 467 */ 468 @Override 469 public Collection<TransitionRecord> getOutgoingEdges(State node) { 470 List<TransitionRecord> edges = new ArrayList<TransitionRecord>(); 471 for(int i = 0; i < alphabetSize; i++) { 472 if(node.getSuccessor(i) != null) 473 edges.add(new TransitionRecord(node, i)); 474 } 475 return edges; 476 } 477 478 /* 479 * (non-Javadoc) 480 * @see net.automatalib.graphs.IndefiniteGraph#getTarget(java.lang.Object) 481 */ 482 @Override 483 public State getTarget(TransitionRecord edge) { 484 return edge.source.getSuccessor(edge.transIdx); 485 } 486 487 /* 488 * (non-Javadoc) 489 * @see net.automatalib.automata.concepts.TransitionOutput#getTransitionOutput(java.lang.Object) 490 */ 491 @Override 492 @SuppressWarnings("unchecked") 493 public O getTransitionOutput(TransitionRecord transition) { 494 return (O)transition.source.getOutput(transition.transIdx); 495 } 496 497 /* 498 * (non-Javadoc) 499 * @see net.automatalib.ts.DeterministicTransitionSystem#getTransition(java.lang.Object, java.lang.Object) 500 */ 501 @Override 502 public TransitionRecord getTransition(State state, I input) { 503 int idx = inputAlphabet.getSymbolIndex(input); 504 if(state.getSuccessor(idx) != null) 505 return new TransitionRecord(state, idx); 506 return null; 507 } 508 509 /* 510 * (non-Javadoc) 511 * @see net.automatalib.graphs.dot.DOTPlottableGraph#getHelper() 512 */ 513 @Override 514 public GraphDOTHelper<State, TransitionRecord> getGraphDOTHelper() { 515 return new DOTHelper(inputAlphabet, init); 516 } 517 518 /* 519 * (non-Javadoc) 520 * @see net.automatalib.ts.SimpleFiniteTS#getStates() 521 */ 522 @Override 523 public Collection<State> getStates() { 524 return Collections.unmodifiableCollection(register.values()); 525 } 526 527 /* 528 * (non-Javadoc) 529 * @see net.automatalib.graphs.FiniteGraph#getNodes() 530 */ 531 @Override 532 public Collection<State> getNodes() { 533 return Collections.unmodifiableCollection(register.values()); 534 } 535 536 /* 537 * (non-Javadoc) 538 * @see net.automatalib.incremental.IncrementalConstruction#getInputAlphabet() 539 */ 540 @Override 541 public Alphabet<I> getInputAlphabet() { 542 return inputAlphabet; 543 } 544 545 /* 546 * (non-Javadoc) 547 * @see net.automatalib.incremental.IncrementalConstruction#findSeparatingWord(java.lang.Object, java.util.Collection, boolean) 548 */ 549 @Override 550 public Word<I> findSeparatingWord(MealyMachine<?, I, ?, O> target, 551 Collection<? extends I> inputs, boolean omitUndefined) { 552 return doFindSeparatingWord(target, inputs, omitUndefined); 553 } 554 555 /* 556 * (non-Javadoc) 557 * @see net.automatalib.incremental.IncrementalConstruction#toAutomaton() 558 */ 559 @Override 560 @SuppressWarnings("unchecked") 561 public CompactMealy<I, O> toAutomaton() { 562 CompactMealy<I,O> result = new CompactMealy<I,O>(inputAlphabet, register.size()); 563 564 Map<State,Integer> stateMap = new HashMap<>(); 565 566 for(State s : register.values()) { 567 Integer id; 568 if(s == init) 569 id = result.addInitialState(); 570 else 571 id = result.addState(); 572 stateMap.put(s, id); 573 } 574 575 for(Map.Entry<State,Integer> e : stateMap.entrySet()) { 576 State s = e.getKey(); 577 Integer id = e.getValue(); 578 579 for(int i = 0; i < alphabetSize; i++) { 580 State succ = s.getSuccessor(i); 581 if(succ == null) 582 continue; 583 I sym = inputAlphabet.getSymbol(i); 584 O out = (O)s.getOutput(i); 585 Integer succId = stateMap.get(succ); 586 result.addTransition(id, sym, succId, out); 587 } 588 } 589 590 return result; 591 } 592 593 /* 594 * (non-Javadoc) 595 * @see net.automatalib.incremental.IncrementalConstruction#hasDefinitiveInformation(net.automatalib.words.Word) 596 */ 597 @Override 598 public boolean hasDefinitiveInformation(Word<I> word) { 599 State s = getState(word); 600 return (s != null); 601 } 602 603 /////////////////////////////////////////////////////////////////////// 604 // Equivalence test // 605 /////////////////////////////////////////////////////////////////////// 606 607 private static int getStateId(State state, Map<State,Integer> ids) { 608 Integer id = ids.get(state); 609 if(id == null) { 610 id = ids.size(); 611 ids.put(state, id); 612 } 613 return id.intValue(); 614 } 615 616 private static final class Record<S,I> { 617 private final State state1; 618 private final S state2; 619 private final I reachedVia; 620 private final Record<S,I> reachedFrom; 621 private final int depth; 622 623 public Record(State state1, S state2, Record<S,I> reachedFrom, I reachedVia) { 624 this.state1 = state1; 625 this.state2 = state2; 626 this.reachedFrom = reachedFrom; 627 this.reachedVia = reachedVia; 628 this.depth = (reachedFrom != null) ? reachedFrom.depth + 1 : 0; 629 } 630 631 public Record(State state1, S state2) { 632 this(state1, state2, null, null); 633 } 634 } 635 636 private <S,T> Word<I> doFindSeparatingWord(MealyMachine<S,I,T,O> mealy, Collection<? extends I> inputs, boolean omitUndefined) { 637 int thisStates = register.size(); 638 639 UnionFind uf = new UnionFind(thisStates + mealy.size()); 640 641 Map<State,Integer> ids = new HashMap<State,Integer>(); 642 643 State init1 = init; 644 S init2 = mealy.getInitialState(); 645 646 if(init2 == null) 647 return omitUndefined ? null : Word.<I>epsilon(); 648 649 StateIDs<S> mealyIds = mealy.stateIDs(); 650 651 int id1 = getStateId(init1, ids), id2 = mealyIds.getStateId(init2) + thisStates; 652 653 uf.link(id1, id2); 654 655 Queue<Record<S,I>> queue = new ArrayDeque<Record<S,I>>(); 656 657 queue.offer(new Record<S,I>(init1, init2)); 658 659 I lastSym = null; 660 661 Record<S,I> current; 662 663explore:while((current = queue.poll()) != null) { 664 State state1 = current.state1; 665 S state2 = current.state2; 666 667 for(I sym : inputs) { 668 int idx = inputAlphabet.getSymbolIndex(sym); 669 State succ1 = state1.getSuccessor(idx); 670 if(succ1 == null) 671 continue; 672 673 T trans2 = mealy.getTransition(state2, sym); 674 if(trans2 == null) { 675 if(omitUndefined) 676 continue; 677 lastSym = sym; 678 break explore; 679 } 680 681 Object out1 = state1.getOutput(idx); 682 Object out2 = mealy.getTransitionOutput(trans2); 683 if(!Objects.equals(out1, out2)) { 684 lastSym = sym; 685 break explore; 686 } 687 688 S succ2 = mealy.getSuccessor(trans2); 689 690 id1 = getStateId(succ1, ids); 691 id2 = mealyIds.getStateId(succ2) + thisStates; 692 693 int r1 = uf.find(id1), r2 = uf.find(id2); 694 695 if(r1 == r2) 696 continue; 697 698 uf.link(r1, r2); 699 700 queue.offer(new Record<>(succ1, succ2, current, sym)); 701 } 702 } 703 704 if(current == null) 705 return null; 706 707 int ceLength = current.depth; 708 if(lastSym != null) 709 ceLength++; 710 711 WordBuilder<I> wb = new WordBuilder<I>(null, ceLength); 712 713 int index = ceLength; 714 715 if(lastSym != null) 716 wb.setSymbol(--index, lastSym); 717 718 while(current.reachedFrom != null) { 719 wb.setSymbol(--index, current.reachedVia); 720 current = current.reachedFrom; 721 } 722 723 return wb.toWord(); 724 } 725 726 @Override 727 public NodeIDs<State> nodeIDs() { 728 return AbstractAutomatonGraph.nodeIDs(this); 729 } 730 731 @Override 732 public <V> MutableMapping<State, V> createStaticNodeMapping() { 733 return AbstractAutomatonGraph.createDynamicNodeMapping(this); 734 } 735 736 @Override 737 public <V> MutableMapping<State, V> createDynamicNodeMapping() { 738 return AbstractAutomatonGraph.createDynamicNodeMapping(this); 739 } 740 741 742}