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}