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.ArrayList;
021import java.util.Collection;
022import java.util.Collections;
023import java.util.HashMap;
024import java.util.List;
025import java.util.Map;
026import java.util.Queue;
027
028import net.automatalib.automata.abstractimpl.AbstractDeterministicAutomaton;
029import net.automatalib.automata.concepts.StateIDs;
030import net.automatalib.automata.fsa.DFA;
031import net.automatalib.automata.fsa.impl.compact.CompactDFA;
032import net.automatalib.automata.graphs.AbstractAutomatonGraph;
033import net.automatalib.commons.util.UnionFind;
034import net.automatalib.commons.util.mappings.MutableMapping;
035import net.automatalib.graphs.UniversalGraph;
036import net.automatalib.graphs.concepts.NodeIDs;
037import net.automatalib.graphs.dot.DOTPlottableGraph;
038import net.automatalib.graphs.dot.GraphDOTHelper;
039import net.automatalib.incremental.ConflictException;
040import net.automatalib.incremental.IncrementalConstruction;
041import net.automatalib.words.Alphabet;
042import net.automatalib.words.Word;
043import net.automatalib.words.WordBuilder;
044
045public abstract class AbstractIncrementalDFABuilder<I> extends
046                AbstractDeterministicAutomaton<State, I, State> implements
047                UniversalGraph<State, EdgeRecord, Acceptance, I>,
048                DOTPlottableGraph<State, EdgeRecord>,
049                IncrementalConstruction<DFA<?, I>, I> {
050
051        protected final Map<StateSignature, State> register = new HashMap<>();
052
053        protected final Alphabet<I> inputAlphabet;
054        protected final int alphabetSize;
055        protected final State init;
056        protected State sink;
057        
058        public AbstractIncrementalDFABuilder(Alphabet<I> inputAlphabet) {
059                this.inputAlphabet = inputAlphabet;
060                this.alphabetSize = inputAlphabet.size();
061                StateSignature sig = new StateSignature(alphabetSize, Acceptance.DONT_KNOW);
062                this.init = new State(sig);
063                register.put(null, init);
064        }
065        
066        public abstract Acceptance lookup(Word<I> word);
067        
068        public abstract void insert(Word<I> word, boolean accepting) throws ConflictException;
069        
070        /**
071         * Inserts a word into the set of accepted words.
072         * @param word the word to insert
073         * @throws ConflictException if the word is already contained in the set of definitely
074         * rejected words
075         */
076        public final void insert(Word<I> word) throws ConflictException {
077                insert(word, true);
078        }
079        
080        /*
081         * (non-Javadoc)
082         * @see net.automatalib.ts.abstractimpl.AbstractFiniteDTS#size()
083         */
084        @Override
085        public int size() {
086                return register.size() + ((sink != null) ? 1 : 0);
087        }
088        
089        @Override
090        public Collection<State> getNodes() {
091                if(sink == null)
092                        return Collections.unmodifiableCollection(register.values());
093                List<State> result = new ArrayList<>(register.size() + 1);
094                result.addAll(register.values());
095                result.add(sink);
096                return result;
097        }
098        
099        @Override
100        public Collection<EdgeRecord> getOutgoingEdges(State node) {
101                List<EdgeRecord> edges = new ArrayList<EdgeRecord>();
102                for(int i = 0; i < alphabetSize; i++) {
103                        if((sink != null && node == sink) || node.getSuccessor(i) != null)
104                                edges.add(new EdgeRecord(node, i));
105                }
106                return edges;
107        }
108        
109        @Override
110        public State getTarget(EdgeRecord edge) {
111                if(sink != null && edge.source == sink)
112                        return edge.source;
113                return edge.source.getSuccessor(edge.transIdx);
114        }
115        
116        @Override
117        public Acceptance getNodeProperty(State node) {
118                if(sink != null && node == sink)
119                        return Acceptance.FALSE;
120                return node.getAcceptance();
121        }
122        
123        @Override
124        public I getEdgeProperty(EdgeRecord edge) {
125                return inputAlphabet.getSymbol(edge.transIdx);
126        }
127        
128        @Override
129        public State getTransition(State state, I input) {
130                if(sink != null && state == sink)
131                        return sink;
132                int idx = inputAlphabet.getSymbolIndex(input);
133                return state.getSuccessor(idx);
134        }
135        
136        @Override
137        public State getSuccessor(State transition) {
138                return transition;
139        }
140        
141        @Override
142        public State getInitialState() {
143                return init;
144        }
145        
146        @Override
147        public Collection<State> getStates() {
148                return getNodes();
149        }
150        
151        @Override
152        public Alphabet<I> getInputAlphabet() {
153                return inputAlphabet;
154        }
155        
156        @Override
157        public Word<I> findSeparatingWord(DFA<?, I> target, Collection<? extends I> inputs, boolean omitUndefined) {
158                return doFindSeparatingWord(target, inputs, omitUndefined);
159        }
160        
161        @Override
162        public DFA<?, I> toAutomaton() {
163                CompactDFA<I> result = new CompactDFA<>(inputAlphabet, register.size() + ((sink != null) ? 1 : 0));
164                Map<State,Integer> stateMap = new HashMap<>();
165                
166                for(State s : register.values()) {
167                        Integer id;
168                        boolean acc = (s.getAcceptance() == Acceptance.TRUE);
169                        if(s == init)
170                                id = result.addInitialState(acc);
171                        else
172                                id = result.addState(acc);
173                        stateMap.put(s, id);
174                }
175                
176                if(sink != null)
177                        stateMap.put(sink, result.addState(false));
178                
179                for(Map.Entry<State,Integer> e : stateMap.entrySet()) {
180                        State s = e.getKey();
181                        
182                        Integer srcId = e.getValue();
183                        for(int i = 0; i < inputAlphabet.size(); i++) {
184                                State succ;
185                                if(s == sink)
186                                        succ = sink;
187                                else {
188                                        succ = s.getSuccessor(i);
189                                        if(succ == null)
190                                                continue;
191                                }
192                                I sym = inputAlphabet.getSymbol(i);
193                                Integer succId = stateMap.get(succ);
194                                result.addTransition(srcId, sym, succId);
195                        }
196                }
197                
198                return result;
199        }
200        
201        /*
202         * (non-Javadoc)
203         * @see net.automatalib.incremental.IncrementalConstruction#hasDefinitiveInformation(net.automatalib.words.Word)
204         */
205        @Override
206        public boolean hasDefinitiveInformation(Word<I> word) {
207                State s = getState(word);
208                if(s == null)
209                        return false;
210                if(s == sink)
211                        return true;
212                return (s.getAcceptance() != Acceptance.DONT_KNOW);
213        }
214        
215        /*
216         * (non-Javadoc)
217         * @see net.automatalib.graphs.dot.DOTPlottableGraph#getGraphDOTHelper()
218         */
219        @Override
220        public GraphDOTHelper<State, EdgeRecord> getGraphDOTHelper() {
221                return new DOTHelper(inputAlphabet, init);
222        }
223        
224        
225        @Override
226        public NodeIDs<State> nodeIDs() {
227                return AbstractAutomatonGraph.nodeIDs(this);
228        }
229        
230        @Override
231        public <T> MutableMapping<State,T> createStaticNodeMapping() {
232                return AbstractAutomatonGraph.createStaticNodeMapping(this);
233        }
234        
235        @Override
236        public <T> MutableMapping<State,T> createDynamicNodeMapping() {
237                return AbstractAutomatonGraph.createDynamicNodeMapping(this);
238        }
239        
240        private static int getStateId(State s, Map<State,Integer> idMap) {
241                Integer id = idMap.get(s);
242                if(id != null)
243                        return id.intValue();
244                idMap.put(s, id = idMap.size());
245                return id.intValue();
246        }
247        
248        private static final class Record<S,I> {
249                public final State state1;
250                public final S state2;
251                public final I reachedVia;
252                public final Record<S,I> reachedFrom;
253                public final int depth;
254                
255                public Record(State state1, S state2) {
256                        this.state1 = state1;
257                        this.state2 = state2;
258                        this.reachedVia = null;
259                        this.reachedFrom = null;
260                        this.depth = 0;
261                }
262                
263                public Record(State state1, S state2, I reachedVia, Record<S,I> reachedFrom) {
264                        this.state1 = state1;
265                        this.state2 = state2;
266                        this.reachedVia = reachedVia;
267                        this.reachedFrom = reachedFrom;
268                        this.depth = reachedFrom.depth + 1;
269                }
270        }
271        
272        private <S> Word<I> doFindSeparatingWord(DFA<S,I> target, Collection<? extends I> inputs, boolean omitUndefined) {
273                int thisStates = register.size();
274                Map<State,Integer> stateIds = new HashMap<>();
275                if(sink != null) {
276                        stateIds.put(sink, 0);
277                        thisStates++;
278                }
279                int targetStates = target.size();
280                if(!omitUndefined)
281                        targetStates++;
282                
283                UnionFind uf = new UnionFind(thisStates + targetStates);
284
285                State init1 = init;
286                S init2 = target.getInitialState();
287                
288                if(init2 == null && omitUndefined)
289                        return null;
290                
291                boolean acc = target.isAccepting(init2);
292                if(init1.getAcceptance().conflicts(acc))
293                        return Word.epsilon();
294                
295                StateIDs<S> tgtIds = target.stateIDs();
296                int id1 = getStateId(init1, stateIds);
297                int id2 = ((init2 != null) ? tgtIds.getStateId(init2) : (targetStates - 1)) + thisStates;
298                
299                uf.link(id1, id2);
300                
301                Queue<Record<S,I>> queue = new ArrayDeque<>();
302                
303                queue.offer(new Record<S,I>(init1, init2));
304                
305                I lastSym = null;
306                
307                Record<S,I> current;
308                
309explore:while((current = queue.poll()) != null) {
310                        State state1 = current.state1;
311                        S state2 = current.state2;
312                        
313                        for(I sym : inputs) {
314                                S succ2 = (state2 != null) ? target.getSuccessor(state2, sym) : null;
315                                if(succ2 == null && omitUndefined)
316                                        continue;
317                                
318                                int idx = inputAlphabet.getSymbolIndex(sym);
319                                State succ1 = (state1 != sink) ? state1.getSuccessor(idx) : sink;
320                                
321                                if(succ1 == null)
322                                        continue;
323                                
324                                id1 = getStateId(succ1, stateIds);
325                                id2 = ((succ2 != null) ? tgtIds.getStateId(succ2) : (targetStates-1)) + thisStates;
326                                
327                                int r1 = uf.find(id1), r2 = uf.find(id2);
328                                
329                                if(r1 == r2)
330                                        continue;
331                                
332                                if(succ1 == sink) {
333                                        if(succ2 == null)
334                                                continue;
335                                        if(target.isAccepting(succ2)) {
336                                                lastSym = sym;
337                                                break explore;
338                                        }
339                                }
340                                else {
341                                        boolean succ2acc = (succ2 != null) ? target.isAccepting(succ2) : false;
342                                        if(succ1.getAcceptance().conflicts(succ2acc)) {
343                                                lastSym = sym;
344                                                break explore;
345                                        }
346                                }
347                                
348                                uf.link(r1, r2);
349                                
350                                queue.offer(new Record<>(succ1, succ2, sym, current));
351                        }
352        }
353                
354                if(current == null)
355                        return null;
356                
357                int ceLength = current.depth;
358                if(lastSym != null)
359                        ceLength++;
360                
361                WordBuilder<I> wb = new WordBuilder<I>(null, ceLength);
362                
363                int index = ceLength;
364                
365                if(lastSym != null)
366                        wb.setSymbol(--index, lastSym);
367                
368                while(current.reachedFrom != null) {
369                        wb.setSymbol(--index, current.reachedVia);
370                        current = current.reachedFrom;
371                }
372                
373                return wb.toWord();
374        }
375        
376        
377        
378        protected abstract State getState(Word<I> word);
379        
380        /**
381         * Returns (and possibly creates) the canonical state for the given signature.
382         * @param sig the signature
383         * @return the canonical state for the given signature
384         */
385        protected State replaceOrRegister(StateSignature sig) {
386                State state = register.get(sig);
387                if(state != null)
388                        return state;
389                
390                register.put(sig, state = new State(sig));
391                for(int i = 0; i < sig.successors.length; i++) {
392                        State succ = sig.successors[i];
393                        if(succ != null)
394                                succ.increaseIncoming();
395                }
396                return state;
397        }
398        
399        /**
400         * Returns the canonical state for the given state's signature, or registers the
401         * state as canonical if no state with that signature exists.
402         * @param state the state
403         * @return the canonical state for the given state's signature
404         */
405        protected State replaceOrRegister(State state) {
406                StateSignature sig = state.getSignature();
407                State other = register.get(sig);
408                if(other != null) {
409                        if(state != other) {
410                                for(int i = 0; i < sig.successors.length; i++) {
411                                        State succ = sig.successors[i];
412                                        if(succ != null)
413                                                succ.decreaseIncoming();
414                                }
415                        }
416                        return other;
417                }
418                
419                register.put(sig, state);
420                return state;
421        }
422        
423        protected void updateInitSignature(Acceptance acc) {
424                StateSignature sig = init.getSignature();
425                sig.acceptance = acc;
426        }
427        
428
429        /**
430         * Updates the signature for a given state.
431         * @param state the state
432         * @param acc the new acceptance value
433         * @return the canonical state for the updated signature
434         */
435        protected State updateSignature(State state, Acceptance acc) {
436                StateSignature sig = state.getSignature();
437                if(sig.acceptance == acc)
438                        return state;
439                register.remove(sig);
440                sig.acceptance = acc;
441                sig.updateHashCode();
442                return replaceOrRegister(state);
443        }
444        
445        protected void updateInitSignature(int idx, State succ) {
446                StateSignature sig = init.getSignature();
447                State oldSucc = sig.successors[idx];
448                if(oldSucc == succ)
449                        return;
450                if(oldSucc != null)
451                        oldSucc.decreaseIncoming();
452                sig.successors[idx] = succ;
453                succ.increaseIncoming();
454        }
455        
456        /**
457         * Updates the signature for a given state.
458         * @param state the state
459         * @param idx the index of the transition to change
460         * @param succ the new successor for the above index
461         * @return the canonical state for the updated signature
462         */
463        protected State updateSignature(State state, int idx, State succ) {
464                StateSignature sig = state.getSignature();
465                if(sig.successors[idx] == succ)
466                        return state;
467                register.remove(sig);
468                if(sig.successors[idx] != null)
469                        sig.successors[idx].decreaseIncoming();
470                
471                sig.successors[idx] = succ;
472                succ.increaseIncoming();
473                sig.updateHashCode();
474                return replaceOrRegister(state);
475        }
476        
477        protected State updateSignature(State state, Acceptance acc, int idx, State succ) {
478                StateSignature sig = state.getSignature();
479                if(sig.successors[idx] == succ && sig.acceptance == acc)
480                        return state;
481                register.remove(sig);
482                sig.successors[idx] = succ;
483                sig.acceptance = acc;
484                return replaceOrRegister(state);
485        }
486        
487        /**
488         * Clones a state, changing the signature.
489         * @param other the state to clone
490         * @param acc the new acceptance value
491         * @return the canonical state for the derived signature
492         */
493        protected State clone(State other, Acceptance acc) {
494                StateSignature sig = other.getSignature();
495                if(sig.acceptance == acc)
496                        return other;
497                sig = sig.clone();
498                sig.acceptance = acc;
499                sig.updateHashCode();
500                return replaceOrRegister(sig);
501        }
502        
503        /**
504         * Clones a state, changing the signature.
505         * @param other the state to clone
506         * @param idx the index of the transition to change
507         * @param succ the new successor state
508         * @return the canonical state for the derived signature
509         */
510        protected State clone(State other, int idx, State succ) {
511                StateSignature sig = other.getSignature();
512                if(sig.successors[idx] == succ)
513                        return other;
514                sig = sig.clone();
515                sig.successors[idx] = succ;
516                sig.updateHashCode();
517                return replaceOrRegister(sig);
518        }
519        
520        protected State clone(State other, Acceptance acc, int idx, State succ) {
521                StateSignature sig = other.getSignature();
522                if(sig.successors[idx] == succ && sig.acceptance == acc)
523                        return other;
524                sig = sig.clone();
525                sig.successors[idx] = succ;
526                sig.acceptance = acc;
527                return replaceOrRegister(sig);
528        }
529
530}