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}