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.util.automata.equivalence;
018
019import java.util.ArrayDeque;
020import java.util.Collection;
021import java.util.Objects;
022import java.util.Queue;
023
024import net.automatalib.automata.UniversalDeterministicAutomaton;
025import net.automatalib.automata.concepts.StateIDs;
026import net.automatalib.commons.util.Pair;
027import net.automatalib.words.Word;
028import net.automatalib.words.WordBuilder;
029
030
031
032public class DeterministicEquivalenceTest<I> {
033        private final UniversalDeterministicAutomaton<?, I, ?, ?, ?> reference;
034        
035        public DeterministicEquivalenceTest(UniversalDeterministicAutomaton<?, I, ?, ?, ?> reference) {
036                this.reference = reference;
037        }
038        
039        public Word<I> findSeparatingWord(UniversalDeterministicAutomaton<?,I,?,?,?> other,
040                        Collection<? extends I> inputs) {
041                return findSeparatingWord(reference, other, inputs);
042        }
043        
044        @SuppressWarnings("unchecked")
045        public static <I,S,T,S2,T2>
046        Word<I> findSeparatingWord(UniversalDeterministicAutomaton<S,I,T,?,?> reference,
047                        UniversalDeterministicAutomaton<S2,I,T2,?,?> other,
048                        Collection<? extends I> inputs) {
049                Queue<Pair<S,S2>> bfsQueue = new ArrayDeque<Pair<S,S2>>();
050                
051                S refInit = reference.getInitialState();
052                S2 otherInit = other.getInitialState();
053                
054                Object refStateProp = reference.getStateProperty(refInit),
055                                otherStateProp = other.getStateProperty(otherInit);
056                
057                if(!Objects.equals(refStateProp, otherStateProp))
058                        return Word.epsilon();
059                
060                bfsQueue.offer(Pair.make(refInit, otherInit));
061                
062                int refSize = reference.size();
063                int totalStates = refSize * other.size();
064                
065                StateIDs<S> refStateIds = reference.stateIDs();
066                StateIDs<S2> otherStateIds = other.stateIDs();
067                
068                Pair<S,S2> currPair = null;
069                int lastId = otherStateIds.getStateId(otherInit) * refSize + refStateIds.getStateId(refInit);
070                
071                Pair<Integer,I>[] preds = (Pair<Integer,I>[])new Pair<?,?>[totalStates];
072                preds[lastId] = Pair.make(-1, null);
073                
074                int currDepth = 0;
075                int inCurrDepth = 1;
076                int inNextDepth = 0;
077                
078                I lastSym = null;
079                
080bfs:    while((currPair = bfsQueue.poll()) != null) {
081                        S refState = currPair.getFirst();
082                        S2 otherState = currPair.getSecond();
083                        
084                        
085                        int currId = otherStateIds.getStateId(otherState) * refSize + refStateIds.getStateId(refState);
086                        lastId = currId;
087                        
088                        
089                        for(I in : inputs) {
090                                lastSym = in;
091                                T refTrans = reference.getTransition(refState, in);
092                                T2 otherTrans = other.getTransition(otherState, in);
093                                
094                                if((refTrans == null || otherTrans == null) && refTrans != otherTrans)
095                                        break bfs;
096                                
097                                Object refProp = reference.getTransitionProperty(refTrans);
098                                Object otherProp = other.getTransitionProperty(otherTrans);
099                                if(!Objects.equals(refProp, otherProp))
100                                        break bfs;
101                                
102                                
103                                S refSucc = reference.getSuccessor(refTrans);
104                                S2 otherSucc = other.getSuccessor(otherTrans);
105                                
106                                int succId = otherStateIds.getStateId(otherSucc) * refSize + refStateIds.getStateId(refSucc);
107                                
108                                if(preds[succId] == null) {
109                                        refStateProp = reference.getStateProperty(refSucc);
110                                        otherStateProp = other.getStateProperty(otherSucc);
111                                        
112                                        if(!Objects.equals(refStateProp, otherStateProp))
113                                                break bfs;
114                                        
115                                        preds[succId] = Pair.make(currId, in);
116                                        bfsQueue.offer(Pair.make(refSucc, otherSucc));
117                                        inNextDepth++;
118                                }
119                        }
120                        
121                        lastSym = null;
122                        
123                        
124                        // Next level in BFS reached
125                        if(--inCurrDepth == 0) {
126                                inCurrDepth = inNextDepth;
127                                inNextDepth = 0;
128                                currDepth++;
129                        }
130                }
131                
132                if(lastSym == null)
133                        return null;
134                
135                WordBuilder<I> sep = new WordBuilder<I>(null, currDepth+1);
136                int index = currDepth;
137                sep.setSymbol(index--, lastSym);
138                
139                Pair<Integer,I> pred = preds[lastId];
140                I sym = pred.getSecond();
141                while(sym != null) {
142                        sep.setSymbol(index--, sym);
143                        pred = preds[pred.getFirst()];
144                        sym = pred.getSecond();
145                }
146                
147                
148                return sep.toWord();
149        } 
150}