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; 018 019import java.util.ArrayList; 020import java.util.Collection; 021import java.util.Collections; 022import java.util.Iterator; 023import java.util.List; 024 025import net.automatalib.automata.Automaton; 026import net.automatalib.automata.DeterministicAutomaton; 027import net.automatalib.automata.MutableDeterministic; 028import net.automatalib.automata.UniversalAutomaton; 029import net.automatalib.automata.UniversalDeterministicAutomaton; 030import net.automatalib.automata.graphs.TransitionEdge; 031import net.automatalib.graphs.Graph; 032import net.automatalib.graphs.UniversalGraph; 033import net.automatalib.util.automata.asgraph.AutomatonAsGraph; 034import net.automatalib.util.automata.asgraph.UniversalAutomatonAsGraph; 035import net.automatalib.util.automata.equivalence.CharacterizingSets; 036import net.automatalib.util.automata.equivalence.NearLinearEquivalenceTest; 037import net.automatalib.util.minimizer.Block; 038import net.automatalib.util.minimizer.BlockMap; 039import net.automatalib.util.minimizer.MinimizationResult; 040import net.automatalib.util.minimizer.Minimizer; 041import net.automatalib.util.ts.TS; 042import net.automatalib.words.Word; 043 044public class Automata extends TS { 045 046 public static <S, I, T> 047 Graph<S, TransitionEdge<I, T>> asGraph( 048 Automaton<S, I, T> automaton, Collection<? extends I> inputs) { 049 return new AutomatonAsGraph<S, I, T,Automaton<S,I,T>>(automaton, inputs); 050 } 051 052 public static <S,I,T,SP,TP> 053 UniversalGraph<S,TransitionEdge<I,T>,SP,TransitionEdge.Property<I,TP>> asUniversalGraph( 054 UniversalAutomaton<S, I, T, SP, TP> automaton, Collection<? extends I> inputs) { 055 return new UniversalAutomatonAsGraph<S, I, T, SP, TP, UniversalAutomaton<S,I,T,SP,TP>>(automaton, inputs); 056 } 057 058 059 public static <S, I, T, SP, TP, SO, TO, A extends MutableDeterministic<SO, ? super I, TO, ? super SP, ? super TP>> 060 A minimize( 061 UniversalDeterministicAutomaton<S, I, T, SP, TP> automaton, 062 Collection<? extends I> inputs, 063 A output) { 064 065 UniversalGraph<S, TransitionEdge<I,T>, SP, TransitionEdge.Property<I,TP>> aag = asUniversalGraph(automaton, inputs); 066 067 MinimizationResult<S, TransitionEdge.Property<I,TP>> mr = Minimizer.minimize(aag, Collections.singleton(automaton.getInitialState())); 068 output.clear(); 069 070 S init = automaton.getInitialState(); 071 Block<S,TransitionEdge.Property<I,TP>> initBlock = mr.getBlockForState(init); 072 BlockMap<SO> bm = new BlockMap<SO>(mr); 073 074 for(Block<S, TransitionEdge.Property<I,TP>> block : mr.getBlocks()) { 075 S rep = mr.getRepresentative(block); 076 SO state; 077 SP repProp = automaton.getStateProperty(rep); 078 if(block == initBlock) 079 state = output.addInitialState(repProp); 080 else 081 state = output.addState(repProp); 082 bm.put(block, state); 083 } 084 085 for(Block<S,TransitionEdge.Property<I,TP>> block : mr.getBlocks()) { 086 S rep = mr.getRepresentative(block); 087 SO state = bm.get(block); 088 for(I input : inputs) { 089 T trans = automaton.getTransition(rep, input); 090 TP prop = automaton.getTransitionProperty(trans); 091 S oldSucc = automaton.getSuccessor(trans); 092 Block<S,TransitionEdge.Property<I,TP>> succBlock = mr.getBlockForState(oldSucc); 093 SO newSucc = bm.get(succBlock); 094 output.addTransition(state, input, newSucc, prop); 095 } 096 } 097 return output; 098 } 099 100 private static final class ResultTransRecord<TP> { 101 public final int targetId; 102 public final TP property; 103 104 public ResultTransRecord(int targetId, TP property) { 105 this.targetId = targetId; 106 this.property = property; 107 } 108 } 109 110 private static final class ResultStateRecord<SP,TP> { 111 public final SP property; 112 public final ResultTransRecord<TP>[] transitions; 113 114 @SuppressWarnings("unchecked") 115 public ResultStateRecord(int numInputs, SP property) { 116 this.property = property; 117 this.transitions = new ResultTransRecord[numInputs]; 118 } 119 } 120 121 @SuppressWarnings("unchecked") 122 public static <S, I, T, SP, TP, A extends MutableDeterministic<S, I, T, SP, TP>> 123 A invasiveMinimize(A automaton, Collection<? extends I> inputs) { 124 125 List<? extends I> inputList; 126 if(inputs instanceof List) 127 inputList = (List<? extends I>)inputs; 128 else 129 inputList = new ArrayList<I>(inputs); 130 131 int numInputs = inputs.size(); 132 133 UniversalGraph<S, TransitionEdge<I,T>, SP, TransitionEdge.Property<I,TP>> aag = asUniversalGraph(automaton, inputs); 134 135 MinimizationResult<S, TransitionEdge.Property<I,TP>> mr = Minimizer.minimize(aag, automaton.getInitialStates()); 136 137 S init = automaton.getInitialState(); 138 int initId = mr.getBlockForState(init).getId(); 139 140 ResultStateRecord<SP,TP>[] records = new ResultStateRecord[mr.getNumBlocks()]; 141 142 for(Block<S,TransitionEdge.Property<I,TP>> blk : mr.getBlocks()) { 143 int id = blk.getId(); 144 S state = mr.getRepresentative(blk); 145 SP prop = automaton.getStateProperty(state); 146 ResultStateRecord<SP,TP> rec = new ResultStateRecord<>(numInputs, prop); 147 records[id] = rec; 148 for(int i = 0; i < numInputs; i++) { 149 I input = inputList.get(i); 150 T trans = automaton.getTransition(state, input); 151 if(trans == null) 152 continue; 153 154 TP transProp = automaton.getTransitionProperty(trans); 155 S succ = automaton.getSuccessor(trans); 156 int tgtId = mr.getBlockForState(succ).getId(); 157 rec.transitions[i] = new ResultTransRecord<TP>(tgtId, transProp); 158 } 159 } 160 161 automaton.clear(); 162 163 Object[] states = new Object[records.length]; 164 for(int i = 0; i < records.length; i++) { 165 ResultStateRecord<SP, TP> rec = records[i]; 166 SP prop = rec.property; 167 S state; 168 if(i == initId) 169 state = automaton.addInitialState(prop); 170 else 171 state = automaton.addState(prop); 172 states[i] = state; 173 } 174 175 for(int i = 0; i < records.length; i++) { 176 ResultStateRecord<SP, TP> rec = records[i]; 177 S state = (S)states[i]; 178 179 for(int j = 0; j < numInputs; j++) { 180 ResultTransRecord<TP> transRec = rec.transitions[j]; 181 if(transRec == null) 182 continue; 183 S succ = (S)states[transRec.targetId]; 184 I input = inputList.get(j); 185 automaton.addTransition(state, input, succ, transRec.property); 186 } 187 } 188 return automaton; 189 } 190 191 /* 192 public static <S, I, T, SP, TP, A extends MutableDeterministic<S, I, T, SP, TP>> A minimize( 193 A automaton, Collection<? extends I> inputs) { 194 return minimize(automaton, inputs, automaton); 195 }*/ 196 197 /** 198 * Finds a separating word for two automata. A separating word is a word that exposes 199 * a difference (differing state or transition properties, or a transition undefined in 200 * only one of the automata) between the two automata. 201 * 202 * @param reference the one automaton to consider 203 * @param other the other automaton to consider 204 * @param inputs the input symbols to consider 205 * @return a separating word, or <tt>null</tt> if no such word could be found. 206 */ 207 public static <I> Word<I> findSeparatingWord( 208 UniversalDeterministicAutomaton<?, I, ?, ?, ?> reference, 209 UniversalDeterministicAutomaton<?, I, ?, ?, ?> other, 210 Collection<? extends I> inputs) { 211 return NearLinearEquivalenceTest.findSeparatingWord(reference, other, inputs); 212 } 213 214 /** 215 * Finds a separating word for two states in an automaton. A separating word is a word 216 * that exposes a difference (differing state or transition properties, or a transition 217 * undefined in only one of the paths) between the two states. 218 * @param automaton the automaton containing the states 219 * @param state1 the one state 220 * @param state2 the other state 221 * @param inputs the input symbols to consider 222 * @return a separating word, or <tt>null</tt> if no such word could be found 223 */ 224 public static <S,I> Word<I> findSeparatingWord( 225 UniversalDeterministicAutomaton<S, I, ?, ?, ?> automaton, 226 S state1, S state2, 227 Collection<? extends I> inputs) { 228 return NearLinearEquivalenceTest.findSeparatingWord(automaton, state1, state2, inputs); 229 } 230 231 /** 232 * Computes a characterizing set for the given automaton. 233 * <p> 234 * This is a convenience method acting as a shortcut to 235 * {@link CharacterizingSets#findCharacterizingSet(UniversalDeterministicAutomaton, Collection, Collection)}. 236 * 237 * @see CharacterizingSets 238 * 239 * @param automaton the automaton for which to determine the characterizing set 240 * @param inputs the input symbols to consider 241 * @param result the collection in which to store the characterizing words 242 */ 243 public static <I> void characterizingSet(UniversalDeterministicAutomaton<?, I, ?, ?, ?> automaton, 244 Collection<? extends I> inputs, 245 Collection<? super Word<I>> result) { 246 CharacterizingSets.findCharacterizingSet(automaton, inputs, result); 247 } 248 249 /** 250 * Computes a characterizing set, and returns it as a {@link List}. 251 * 252 * @see CharacterizingSets 253 * 254 * @param automaton the automaton for which to determine the characterizing set 255 * @param inputs the input symbols to consider 256 * @return a list containing the characterizing words 257 */ 258 public static <I> List<Word<I>> characterizingSet(UniversalDeterministicAutomaton<?, I, ?, ?, ?> automaton, 259 Collection<? extends I> inputs) { 260 List<Word<I>> result = new ArrayList<Word<I>>(); 261 characterizingSet(automaton, inputs, result); 262 return result; 263 } 264 265 /** 266 * Computes a characterizing set for a single state. 267 * <p> 268 * This is a convenience method acting as a shortcut to 269 * {@link CharacterizingSets#findCharacterizingSet(UniversalDeterministicAutomaton, Collection, Object, Collection)}. 270 * 271 * @see CharacterizingSets 272 * 273 * @param automaton the automaton containing the state 274 * @param inputs the input symbols to consider 275 * @param state the state for which to determine a characterizing set 276 * @param result the collection in which to store the characterizing words 277 */ 278 public static <S,I> void stateCharacterizingSet(UniversalDeterministicAutomaton<S, I, ?, ?, ?> automaton, 279 Collection<? extends I> inputs, 280 S state, 281 Collection<? super Word<I>> result) { 282 CharacterizingSets.findCharacterizingSet(automaton, inputs, state, result); 283 } 284 285 /** 286 * Computes a characterizing set for a single state, and returns it as a {@link List}. 287 * 288 * @see CharacterizingSets 289 * 290 * @param automaton the automaton containing the state 291 * @param inputs the input symbols to consider 292 * @param state the state for which to determine a characterizing set 293 * @return a list containing the characterizing words 294 */ 295 public static <S,I> List<Word<I>> stateCharacterizingSet(UniversalDeterministicAutomaton<S, I, ?, ?, ?> automaton, 296 Collection<? extends I> inputs, 297 S state) { 298 List<Word<I>> result = new ArrayList<Word<I>>(); 299 stateCharacterizingSet(automaton, inputs, state, result); 300 return result; 301 } 302 303 public static <I> void cover(DeterministicAutomaton<?, I, ?> automaton, 304 Collection<? extends I> inputs, Collection<? super Word<I>> states, Collection<? super Word<I>> transitions) { 305 Covers.cover(automaton, inputs, states, transitions); 306 } 307 308 public static <I> List<Word<I>> stateCover(DeterministicAutomaton<?, I, ?> automaton, 309 Collection<? extends I> inputs) { 310 List<Word<I>> states = new ArrayList<Word<I>>(automaton.size()); 311 cover(automaton, inputs, states, null); 312 return states; 313 } 314 315 public static <I> List<Word<I>> transitionCover(DeterministicAutomaton<?, I, ?> automaton, 316 Collection<? extends I> inputs) { 317 List<Word<I>> all = new ArrayList<Word<I>>(automaton.size() * inputs.size()); 318 cover(automaton, inputs, all, all); 319 return all; 320 } 321 322 323 324 public static <S,I> 325 Iterator<TransRef<S,I>> allDefinedTransitionsIterator( 326 DeterministicAutomaton<S, I, ?> automaton, 327 Iterable<? extends I> inputs) { 328 return allDefinedTransitionsIterator(automaton, automaton.iterator(), inputs); 329 } 330 331 public static <S,I> 332 Iterable<TransRef<S,I>> allDefinedTransitions( 333 DeterministicAutomaton<S, I, ?> automaton, 334 Iterable<? extends I> inputs) { 335 return allDefinedTransitions(automaton, automaton, inputs); 336 } 337 338 public static <S,I> 339 Iterator<TransRef<S,I>> allUndefinedTransitionsIterator( 340 DeterministicAutomaton<S, I, ?> automaton, 341 Iterable<? extends I> inputs) { 342 return allUndefinedTransitionsIterator(automaton, automaton.iterator(), inputs); 343 } 344 345 public static <S,I> 346 Iterable<TransRef<S,I>> allUndefinedTransitions( 347 DeterministicAutomaton<S, I, ?> automaton, 348 Iterable<? extends I> inputs) { 349 return allUndefinedTransitions(automaton, automaton, inputs); 350 } 351}