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}