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