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.ArrayList; 021import java.util.Collection; 022import java.util.HashMap; 023import java.util.Iterator; 024import java.util.List; 025import java.util.Map; 026import java.util.Objects; 027import java.util.Queue; 028 029import net.automatalib.automata.UniversalDeterministicAutomaton; 030import net.automatalib.util.automata.Automata; 031import net.automatalib.words.Word; 032 033 034/** 035 * Operations for calculating <i>characterizing sets</i>. 036 * <p> 037 * A characterizing set for a whole automaton is a set <i>W</i> of words such that for every two states 038 * <i>s<sub>1</sub></i> and <i>s<sub>2</sub></i>, there exists a word <i>w ∈ W</i> such that 039 * <i>w</i> exposes a difference between <i>s<sub>1</sub></i> and <i>s<sub>2</sub></i> (i.e., 040 * either covers a transition with differing property (or not defined in only one case), 041 * or reaching a successor state with differing properties), or there exists no such word at all. 042 * <p> 043 * A characterizing set for a single state <i>s</i> is a set <i>W</i> of words such that 044 * for every state <i>t</i>, there exists a word <i>w ∈ W</i> such that <i>w</i> exposes 045 * a difference between <i>s</i> and <i>t</i>, or there exists no such word at all. 046 * 047 * @author Malte Isberner <malte.isberner@gmail.com> 048 * 049 */ 050public class CharacterizingSets { 051 052 private static <S,I,T> List<Object> buildTrace(UniversalDeterministicAutomaton<S, I, T, ?, ?> automaton, 053 S state, 054 Word<I> suffix) { 055 List<Object> trace = new ArrayList<Object>(2*suffix.length()); 056 057 S curr = state; 058 059 for(I sym : suffix) { 060 T trans = automaton.getTransition(curr, sym); 061 062 if(trans == null) 063 break; 064 065 Object prop = automaton.getTransitionProperty(trans); 066 trace.add(prop); 067 068 curr = automaton.getSuccessor(trans); 069 prop = automaton.getStateProperty(curr); 070 trace.add(prop); 071 } 072 073 return trace; 074 } 075 076 private static <S,I,T> boolean checkTrace(UniversalDeterministicAutomaton<S, I, T, ?, ?> automaton, 077 S state, 078 Word<I> suffix, 079 List<Object> trace) { 080 081 Iterator<Object> it = trace.iterator(); 082 S curr = state; 083 084 for(I sym : suffix) { 085 T trans = automaton.getTransition(curr, sym); 086 087 if(!it.hasNext()) 088 return (trans == null); 089 090 Object prop = automaton.getTransitionProperty(trans); 091 092 if(!Objects.equals(prop, it.next())) 093 return false; 094 095 curr = automaton.getSuccessor(trans); 096 prop = automaton.getStateProperty(curr); 097 098 if(!Objects.equals(prop, it.next())) 099 return false; 100 } 101 102 return true; 103 } 104 105 private static <S,I,T> void cluster(UniversalDeterministicAutomaton<S, I, T, ?, ?> automaton, 106 Word<I> suffix, 107 Iterator<S> stateIt, 108 Map<List<Object>,List<S>> bucketMap) { 109 110 while(stateIt.hasNext()) { 111 S state = stateIt.next(); 112 List<Object> trace = buildTrace(automaton, state, suffix); 113 List<S> bucket = bucketMap.get(trace); 114 if(bucket == null) { 115 bucket = new ArrayList<S>(); 116 bucketMap.put(trace, bucket); 117 } 118 bucket.add(state); 119 } 120 } 121 122 /** 123 * Computes a characterizing set for a specified state in the given automaton. 124 * @param automaton the automaton containing the state 125 * @param inputs the input alphabets to consider 126 * @param state the state for which to determine the characterizing set 127 * @param result the collection in which to store the characterizing words 128 */ 129 public static <S,I,T> void findCharacterizingSet(UniversalDeterministicAutomaton<S, I, T, ?, ?> automaton, 130 Collection<? extends I> inputs, 131 S state, Collection<? super Word<I>> result) { 132 133 Object prop = automaton.getStateProperty(state); 134 135 List<S> currentBlock = new ArrayList<S>(); 136 137 boolean multipleStateProps = false; 138 139 for(S s : automaton) { 140 if(Objects.equals(s, state)) 141 continue; 142 143 Object sProp = automaton.getStateProperty(s); 144 if(!Objects.equals(sProp, prop)) 145 multipleStateProps = true; 146 else 147 currentBlock.add(s); 148 } 149 150 if(multipleStateProps) 151 result.add(Word.<I>epsilon()); 152 153 while(!currentBlock.isEmpty()) { 154 List<S> nextBlock = new ArrayList<S>(); 155 156 Iterator<S> it = currentBlock.iterator(); 157 158 Word<I> suffix = null; 159 while(it.hasNext() && suffix == null) { 160 S s = it.next(); 161 suffix = Automata.findSeparatingWord(automaton, state, s, inputs); 162 } 163 164 if(suffix == null) 165 return; 166 167 168 result.add(suffix); 169 170 List<Object> trace = buildTrace(automaton, state, suffix); 171 172 while(it.hasNext()) { 173 S s = it.next(); 174 if(checkTrace(automaton, s, suffix, trace)) 175 nextBlock.add(s); 176 } 177 178 currentBlock = nextBlock; 179 } 180 } 181 182 /** 183 * Computes a characterizing set for the given automaton. 184 * @param automaton the automaton for which to determine the characterizing set. 185 * @param inputs the input alphabets to consider 186 * @param result the collection in which to store the characterizing words 187 */ 188 public static <S,I,T> void findCharacterizingSet(UniversalDeterministicAutomaton<S, I, T, ?, ?> automaton, 189 Collection<? extends I> inputs, 190 Collection<? super Word<I>> result) { 191 192 Map<Object,List<S>> initBlockMap = new HashMap<Object,List<S>>(); 193 194 Queue<List<S>> blocks = new ArrayDeque<List<S>>(); 195 196 for(S state : automaton) { 197 Object prop = automaton.getStateProperty(state); 198 199 List<S> initBlock = initBlockMap.get(prop); 200 if(initBlock == null) { 201 initBlock = new ArrayList<S>(); 202 blocks.offer(initBlock); 203 initBlockMap.put(prop, initBlock); 204 } 205 206 initBlock.add(state); 207 } 208 209 if(blocks.size() > 1) 210 result.add(Word.<I>epsilon()); 211 212 213 List<S> currBlock; 214 215 while((currBlock = blocks.poll()) != null) { 216 Iterator<S> it = currBlock.iterator(); 217 218 S ref = it.next(); 219 220 Word<I> suffix = null; 221 S state = null; 222 while(it.hasNext() && suffix == null) { 223 state = it.next(); 224 suffix = Automata.findSeparatingWord(automaton, ref, state, inputs); 225 } 226 227 if(suffix == null) 228 continue; 229 230 result.add(suffix); 231 232 int otherBlocks = blocks.size(); 233 234 Map<List<Object>,List<S>> buckets = new HashMap<List<Object>,List<S>>(); 235 236 List<S> firstBucket = new ArrayList<S>(); 237 List<S> secondBucket = new ArrayList<S>(); 238 firstBucket.add(ref); 239 buckets.put(buildTrace(automaton, ref, suffix), firstBucket); 240 secondBucket.add(state); 241 buckets.put(buildTrace(automaton, state, suffix), secondBucket); 242 243 cluster(automaton, suffix, it, buckets); 244 245 blocks.addAll(buckets.values()); 246 247 while(otherBlocks-- > 0) { 248 List<S> block = blocks.poll(); 249 buckets.clear(); 250 cluster(automaton, suffix, block.iterator(), buckets); 251 blocks.addAll(buckets.values()); 252 } 253 } 254 } 255 256}