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}