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}