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