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