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