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
023public class IncrementalPCDFABuilder<I> extends AbstractIncrementalDFABuilder<I> {
024        
025        public IncrementalPCDFABuilder(Alphabet<I> inputAlphabet) {
026                super(inputAlphabet);
027        }
028        
029        /*
030         * (non-Javadoc)
031         * @see net.automatalib.incremental.dfa.AbstractIncrementalDFABuilder#getState(net.automatalib.words.Word)
032         */
033        @Override
034        protected State getState(Word<I> word) {
035                State s = init;
036                
037                for(I sym : word) {
038                        int idx = inputAlphabet.getSymbolIndex(sym);
039                        s = s.getSuccessor(idx);
040                        if(s == null || s == sink)
041                                return s;
042                }
043                return s;
044        }
045        
046        /*
047         * (non-Javadoc)
048         * @see net.automatalib.incremental.dfa.AbstractIncrementalDFABuilder#lookup(net.automatalib.words.Word)
049         */
050        @Override
051        public Acceptance lookup(Word<I> word) {
052                State s = getState(word);
053                if(s == null)
054                        return Acceptance.DONT_KNOW;
055                return (s != sink) ? s.getAcceptance() : Acceptance.FALSE;
056        }
057        
058        /*
059         * (non-Javadoc)
060         * @see net.automatalib.incremental.dfa.AbstractIncrementalDFABuilder#insert(net.automatalib.words.Word, boolean)
061         */
062        @Override
063        public void insert(Word<I> word, boolean accepting) {
064                int len = word.length();
065                Acceptance acc = Acceptance.fromBoolean(accepting);
066                
067                State curr = init;
068                State conf = null;
069                
070                int confIndex = -1;
071                
072                int prefixLen = 0;
073                for(I sym : word) {
074                        if(curr == sink)
075                                break;
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(curr == sink) {
090                        if(accepting)
091                                throw new RuntimeException("Conflict");
092                        return;
093                }
094                
095                if(prefixLen == len) {
096                        Acceptance currAcc = curr.getAcceptance();
097                        if(currAcc == acc)
098                                return;
099                        else if(conf == null) {
100                                if(currAcc == Acceptance.DONT_KNOW) {
101                                        if(accepting) {
102                                                State upd = updateSignature(curr, Acceptance.TRUE);
103                                                if(upd == curr)
104                                                        return;
105                                                curr = upd;
106                                        }
107                                        else {
108                                                purge(curr);
109                                                curr = sink;
110                                        }
111                                }
112                                else
113                                        throw new ConflictException("Incompatible acceptances: " + currAcc + " vs " + acc);
114                        }
115                }
116                
117                
118                Word<I> suffix = word.subWord(prefixLen); 
119                
120                State last;
121                
122                State suffixState = null;
123                int suffTransIdx = -1;
124                if(!suffix.isEmpty()) {
125                        suffixState = createSuffix(suffix.subWord(1), accepting);
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 /* if(accepting) */
135                                last = clone(curr, Acceptance.TRUE, 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                                if(accepting)
142                                        last = clone(s, Acceptance.TRUE, idx, last);
143                                else
144                                        last = clone(s, idx, last);
145                        }
146                        
147                        currentIndex = confIndex;
148                }
149                else {
150                        if(suffTransIdx == -1)
151                                last = updateSignature(curr, acc);
152                        else /* if(accepting) */
153                                last = updateSignature(curr, Acceptance.TRUE, suffTransIdx, suffixState);
154                        currentIndex = prefixLen;
155                }
156                
157                while(--currentIndex >= 0) {
158                        State state = getState(word.prefix(currentIndex));
159                        I sym = word.getSymbol(currentIndex);
160                        int idx = inputAlphabet.getSymbolIndex(sym);
161                        if(accepting) {
162                                Acceptance lastAcc = last.getAcceptance();
163                                last = updateSignature(state, Acceptance.TRUE, idx, last);
164                                if(state == last && lastAcc == Acceptance.TRUE)
165                                        break;
166                        }
167                        else {
168                                last = updateSignature(state, idx, last);
169                                if(state == last)
170                                        break;
171                        }
172                }
173        }
174                
175        /**
176         * Removes a state and all of its successors from the register.
177         * @param state the state to purge
178         */
179        private void purge(State state) {
180                StateSignature sig = state.getSignature();
181                if(register.remove(sig) == null)
182                        return;
183                for(int i = 0; i < alphabetSize; i++) {
184                        State succ = sig.successors[i];
185                        if(succ != null)
186                                purge(succ);
187                        sig.successors[i] = null;
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 whether or not the final state should be accepting
196         * @return the first state in the sequence
197         */
198        private State createSuffix(Word<I> suffix, boolean accepting) {
199                State last;
200                Acceptance intermediate;
201                if(!accepting) {
202                        if(sink == null)
203                                sink = new State(null);
204                        last = sink;
205                        intermediate = Acceptance.DONT_KNOW;
206                }
207                else {
208                        StateSignature sig = new StateSignature(alphabetSize, Acceptance.TRUE);
209                        last = replaceOrRegister(sig);
210                        intermediate = Acceptance.TRUE;
211                }
212                
213                int len = suffix.length();
214                for(int i = len - 1; i >= 0; i--) {
215                        StateSignature sig = new StateSignature(alphabetSize, intermediate);
216                        I sym = suffix.getSymbol(i);
217                        int idx = inputAlphabet.getSymbolIndex(sym);
218                        sig.successors[idx] = last;
219                        last = replaceOrRegister(sig);
220                }
221                
222                return last;
223        }
224
225}