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 net.automatalib.incremental.ConflictException; 020import net.automatalib.words.Alphabet; 021import net.automatalib.words.Word; 022 023/** 024 * Incrementally builds an (acyclic) DFA, from a set of positive and negative words. 025 * Using {@link #insert(Word, boolean)}, either the set of words definitely in the target language 026 * or definitely <i>not</i> in the target language is augmented. The {@link #lookup(Word)} method 027 * then returns, for a given word, whether this word is in the set of definitely accepted 028 * words ({@link Acceptance#TRUE}), definitely rejected words ({@link Acceptance#FALSE}), or 029 * neither ({@link Acceptance#DONT_KNOW}). 030 * 031 * @author Malte Isberner <malte.isberner@gmail.com> 032 * 033 * @param <I> input symbol class 034 */ 035public class IncrementalDFABuilder<I> extends AbstractIncrementalDFABuilder<I> { 036 037 /** 038 * Constructor. Initializes the incremental builder. 039 * @param inputAlphabet the input alphabet to use 040 */ 041 public IncrementalDFABuilder(Alphabet<I> inputAlphabet) { 042 super(inputAlphabet); 043 } 044 045 046 /** 047 * Checks the ternary acceptance status for a given word. 048 * @param word the word to check 049 * @return the acceptance status for the given word 050 */ 051 @Override 052 public Acceptance lookup(Word<I> word) { 053 State s = getState(word); 054 if(s == null) 055 return Acceptance.DONT_KNOW; 056 return s.getAcceptance(); 057 } 058 059 /** 060 * Inserts a word into either the set of accepted or rejected words. 061 * @param word the word to insert 062 * @param accepting whether to insert this word into the set of accepted or rejected words. 063 */ 064 @Override 065 public void insert(Word<I> word, boolean accepting) { 066 int len = word.length(); 067 Acceptance acc = Acceptance.fromBoolean(accepting); 068 069 State curr = init; 070 State conf = null; 071 072 int confIndex = -1; 073 074 int prefixLen = 0; 075 for(I sym : word) { 076 if(conf == null && curr.isConfluence()) { 077 conf = curr; 078 confIndex = prefixLen; 079 } 080 081 int idx = inputAlphabet.getSymbolIndex(sym); 082 State succ = curr.getSuccessor(idx); 083 if(succ == null) 084 break; 085 curr = succ; 086 prefixLen++; 087 } 088 089 if(prefixLen == len) { 090 Acceptance currAcc = curr.getAcceptance(); 091 if(currAcc == acc) 092 return; 093 else if(conf == null) { 094 if(currAcc == Acceptance.DONT_KNOW) { 095 if(curr == init) { 096 updateInitSignature(acc); 097 return; 098 } 099 State upd = updateSignature(curr, acc); 100 if(upd == curr) 101 return; 102 curr = upd; 103 } 104 else 105 throw new ConflictException("Incompatible acceptances: " + currAcc + " vs. " + acc); 106 } 107 } 108 109 110 Word<I> suffix = word.subWord(prefixLen); 111 112 State last; 113 114 State suffixState = null; 115 State endpoint = null; 116 int suffTransIdx = -1; 117 if(!suffix.isEmpty()) { 118 if(conf != null) 119 suffixState = createSuffix(suffix.subWord(1), acc); 120 else { 121 SuffixInfo suffixRes = createSuffix2(suffix.subWord(1), acc); 122 suffixState = suffixRes.last; 123 endpoint = suffixRes.end; 124 } 125 I sym = suffix.getSymbol(0); 126 suffTransIdx = inputAlphabet.getSymbolIndex(sym); 127 } 128 129 int currentIndex; 130 if(conf != null) { 131 if(suffTransIdx == -1) 132 last = clone(curr, acc); 133 else 134 last = clone(curr, suffTransIdx, suffixState); 135 136 for(int i = prefixLen - 1; i >= confIndex; i--) { 137 State s = getState(word.prefix(i)); 138 I sym = word.getSymbol(i); 139 int idx = inputAlphabet.getSymbolIndex(sym); 140 last = clone(s, idx, last); 141 } 142 143 currentIndex = confIndex; 144 } 145 else { 146 if(suffTransIdx == -1) 147 last = curr; 148 else if(endpoint == curr) 149 last = clone(curr, suffTransIdx, suffixState); 150 else if(curr == init) { 151 updateInitSignature(suffTransIdx, suffixState); 152 return; 153 } 154 else 155 last = updateSignature(curr, suffTransIdx, suffixState); 156 currentIndex = prefixLen; 157 } 158 159 while(--currentIndex > 0) { 160 State state = getState(word.prefix(currentIndex)); 161 I sym = word.getSymbol(currentIndex); 162 int idx = inputAlphabet.getSymbolIndex(sym); 163 last = updateSignature(state, idx, last); 164 if(state == last) 165 return; 166 } 167 168 I sym = word.getSymbol(0); 169 int idx = inputAlphabet.getSymbolIndex(sym); 170 updateInitSignature(idx, last); 171 } 172 173 174 175 /** 176 * Retrieves the state reached by a given word. 177 * @param word the word 178 * @return the state reached by the given word, or <tt>null</tt> if no state is reachable 179 * by that word 180 */ 181 @Override 182 protected State getState(Word<I> word) { 183 State s = init; 184 185 for(I sym : word) { 186 int idx = inputAlphabet.getSymbolIndex(sym); 187 s = s.getSuccessor(idx); 188 if(s == null) 189 return null; 190 } 191 return s; 192 } 193 194 195 196 197 /** 198 * Creates a suffix state sequence, i.e., a linear sequence of states connected by transitions 199 * labeled by the letters of the given suffix word. 200 * @param suffix the suffix word 201 * @param acc the acceptance status of the final state 202 * @return the first state in the sequence 203 */ 204 private State createSuffix(Word<I> suffix, Acceptance acc) { 205 StateSignature sig = new StateSignature(alphabetSize, acc); 206 sig.updateHashCode(); 207 State last = replaceOrRegister(sig); 208 209 int len = suffix.length(); 210 for(int i = len - 1; i >= 0; i--) { 211 sig = new StateSignature(alphabetSize, Acceptance.DONT_KNOW); 212 I sym = suffix.getSymbol(i); 213 int idx = inputAlphabet.getSymbolIndex(sym); 214 sig.successors[idx] = last; 215 sig.updateHashCode(); 216 last = replaceOrRegister(sig); 217 } 218 219 return last; 220 } 221 222 private static final class SuffixInfo { 223 private final State last; 224 private final State end; 225 226 public SuffixInfo(State last, State end) { 227 this.last = last; 228 this.end = end; 229 } 230 231 /* (non-Javadoc) 232 * @see java.lang.Object#hashCode() 233 */ 234 @Override 235 public int hashCode() { 236 final int prime = 31; 237 int result = 1; 238 result = prime * result + ((end == null) ? 0 : end.hashCode()); 239 result = prime * result + ((last == null) ? 0 : last.hashCode()); 240 return result; 241 } 242 243 /* (non-Javadoc) 244 * @see java.lang.Object#equals(java.lang.Object) 245 */ 246 @Override 247 public boolean equals(Object obj) { 248 if (this == obj) 249 return true; 250 if (obj == null) 251 return false; 252 if (obj.getClass() != SuffixInfo.class) 253 return false; 254 SuffixInfo other = (SuffixInfo)obj; 255 256 257 // State has identity equals-semantics! 258 if(last != other.last) 259 return false; 260 261 return (end == other.end); 262 } 263 264 265 } 266 267 private SuffixInfo createSuffix2(Word<I> suffix, Acceptance acc) { 268 StateSignature sig = new StateSignature(alphabetSize, acc); 269 sig.updateHashCode(); 270 State last = replaceOrRegister(sig); 271 State end = last; 272 273 int len = suffix.length(); 274 for(int i = len - 1; i >= 0; i--) { 275 sig = new StateSignature(alphabetSize, Acceptance.DONT_KNOW); 276 I sym = suffix.getSymbol(i); 277 int idx = inputAlphabet.getSymbolIndex(sym); 278 sig.successors[idx] = last; 279 sig.updateHashCode(); 280 last = replaceOrRegister(sig); 281 } 282 283 return new SuffixInfo(last, end); 284 } 285 286 287}