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.UnionFind; 027import net.automatalib.words.Word; 028import net.automatalib.words.WordBuilder; 029 030public class NearLinearEquivalenceTest<I> { 031 032 private static final class Record<S,S2,I> { 033 private final S state1; 034 private final S2 state2; 035 private final I reachedBy; 036 private final Record<S,S2,I> reachedFrom; 037 private final int depth; 038 039 public Record(S state1, S2 state2) { 040 this(state1, state2, null, null); 041 } 042 043 public Record(S state1, S2 state2, I reachedBy, Record<S,S2,I> reachedFrom) { 044 this.state1 = state1; 045 this.state2 = state2; 046 this.reachedBy = reachedBy; 047 this.reachedFrom = reachedFrom; 048 this.depth = (reachedFrom != null) ? reachedFrom.depth + 1 : 0; 049 } 050 } 051 052 private final UniversalDeterministicAutomaton<?, I, ?, ?, ?> target; 053 054 public NearLinearEquivalenceTest(UniversalDeterministicAutomaton<?, I, ?, ?, ?> target) { 055 this.target = target; 056 } 057 058 public Word<I> findSeparatingWord(UniversalDeterministicAutomaton<?, I, ?, ?, ?> other, Collection<? extends I> inputs) { 059 return findSeparatingWord(target, other, inputs); 060 } 061 062 public static <S,S2,I,T,T2> Word<I> findSeparatingWord(UniversalDeterministicAutomaton<S,I,T,?,?> target, 063 UniversalDeterministicAutomaton<S2,I,T2,?,?> other, Collection<? extends I> inputs) { 064 int targetStates = target.size(); 065 UnionFind uf = new UnionFind(targetStates + other.size()); 066 067 S init1 = target.getInitialState(); 068 S2 init2 = other.getInitialState(); 069 070 Object sprop1 = target.getStateProperty(init1); 071 Object sprop2 = other.getStateProperty(init2); 072 073 if(!Objects.equals(sprop1, sprop2)) 074 return Word.epsilon(); 075 076 StateIDs<S> targetStateIds = target.stateIDs(); 077 StateIDs<S2> otherStateIds = other.stateIDs(); 078 079 int id1 = targetStateIds.getStateId(init1); 080 int id2 = otherStateIds.getStateId(init2) + targetStates; 081 082 uf.link(id1, id2); 083 084 Queue<Record<S,S2,I>> queue = new ArrayDeque<Record<S,S2,I>>(); 085 086 queue.offer(new Record<S,S2,I>(init1, init2)); 087 088 I lastSym = null; 089 090 Record<S,S2,I> current; 091 092explore:while((current = queue.poll()) != null) { 093 S state1 = current.state1; 094 S2 state2 = current.state2; 095 096 for(I sym : inputs) { 097 T trans1 = target.getTransition(state1, sym); 098 T2 trans2 = other.getTransition(state2, sym); 099 100 if(trans1 == null) { 101 if(trans2 == null) 102 continue; 103 lastSym = sym; 104 break explore; 105 } 106 else if(trans2 == null) { 107 lastSym = sym; 108 break explore; 109 } 110 111 Object tprop1 = target.getTransitionProperty(trans1); 112 Object tprop2 = other.getTransitionProperty(trans2); 113 114 if(!Objects.equals(tprop1, tprop2)) { 115 lastSym = sym; 116 break explore; 117 } 118 119 S succ1 = target.getSuccessor(trans1); 120 S2 succ2 = other.getSuccessor(trans2); 121 122 id1 = targetStateIds.getStateId(succ1); 123 id2 = otherStateIds.getStateId(succ2) + targetStates; 124 125 int r1 = uf.find(id1), r2 = uf.find(id2); 126 127 if(r1 == r2) 128 continue; 129 130 131 sprop1 = target.getStateProperty(succ1); 132 sprop2 = other.getStateProperty(succ2); 133 134 if(!Objects.equals(sprop1, sprop2)) { 135 lastSym = sym; 136 break explore; 137 } 138 139 uf.link(r1, r2); 140 141 queue.offer(new Record<>(succ1, succ2, sym, current)); 142 } 143 } 144 145 if(current == null) 146 return null; 147 148 int ceLength = current.depth; 149 if(lastSym != null) 150 ceLength++; 151 152 WordBuilder<I> wb = new WordBuilder<I>(null, ceLength); 153 154 int index = ceLength; 155 156 if(lastSym != null) 157 wb.setSymbol(--index, lastSym); 158 159 while(current.reachedFrom != null) { 160 wb.setSymbol(--index, current.reachedBy); 161 current = current.reachedFrom; 162 } 163 164 return wb.toWord(); 165 } 166 167 168 public static <S,I,T> Word<I> findSeparatingWord(UniversalDeterministicAutomaton<S,I,T,?,?> target, 169 S init1, S init2, Collection<? extends I> inputs) { 170 UnionFind uf = new UnionFind(target.size()); 171 172 Object sprop1 = target.getStateProperty(init1); 173 Object sprop2 = target.getStateProperty(init2); 174 175 if(!Objects.equals(sprop1, sprop2)) 176 return Word.epsilon(); 177 178 StateIDs<S> stateIds = target.stateIDs(); 179 180 int id1 = stateIds.getStateId(init1), id2 = stateIds.getStateId(init2); 181 182 uf.link(id1, id2); 183 184 Queue<Record<S,S,I>> queue = new ArrayDeque<Record<S,S,I>>(); 185 186 queue.offer(new Record<S,S,I>(init1, init2)); 187 188 I lastSym = null; 189 Record<S,S,I> current; 190 191explore:while((current = queue.poll()) != null) { 192 S state1 = current.state1; 193 S state2 = current.state2; 194 195 for(I sym : inputs) { 196 T trans1 = target.getTransition(state1, sym); 197 T trans2 = target.getTransition(state2, sym); 198 199 if(trans1 == null) { 200 if(trans2 == null) 201 continue; 202 lastSym = sym; 203 break explore; 204 } 205 else if(trans2 == null) { 206 lastSym = sym; 207 break explore; 208 } 209 210 Object tprop1 = target.getTransitionProperty(trans1); 211 Object tprop2 = target.getTransitionProperty(trans2); 212 213 if(!Objects.equals(tprop1, tprop2)) { 214 lastSym = sym; 215 break explore; 216 } 217 218 S succ1 = target.getSuccessor(trans1); 219 S succ2 = target.getSuccessor(trans2); 220 221 id1 = stateIds.getStateId(succ1); 222 id2 = stateIds.getStateId(succ2); 223 224 int r1 = uf.find(id1), r2 = uf.find(id2); 225 226 if(r1 == r2) 227 continue; 228 229 230 sprop1 = target.getStateProperty(succ1); 231 sprop2 = target.getStateProperty(succ2); 232 233 if(!Objects.equals(sprop1, sprop2)) { 234 lastSym = sym; 235 break explore; 236 } 237 238 uf.link(r1, r2); 239 240 queue.offer(new Record<>(succ1, succ2, sym, current)); 241 } 242 } 243 244 if(current == null) 245 return null; 246 247 int ceLength = current.depth; 248 if(lastSym != null) 249 ceLength++; 250 251 WordBuilder<I> wb = new WordBuilder<I>(null, ceLength); 252 253 int index = ceLength; 254 255 if(lastSym != null) 256 wb.setSymbol(--index, lastSym); 257 258 while(current.reachedFrom != null) { 259 wb.setSymbol(--index, current.reachedBy); 260 current = current.reachedFrom; 261 } 262 263 return wb.toWord(); 264 } 265}