001/* Copyright (C) 2013 TU Dortmund 002 * This file is part of LearnLib, http://www.learnlib.de/. 003 * 004 * LearnLib 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 * LearnLib 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 LearnLib; if not, see 015 * <http://www.gnu.de/documents/lgpl.en.html>. 016 */ 017package de.learnlib.counterexamples; 018 019import java.util.Collections; 020import java.util.List; 021 022import net.automatalib.automata.concepts.SuffixOutput; 023import net.automatalib.words.Word; 024import de.learnlib.api.AccessSequenceTransformer; 025import de.learnlib.api.MembershipOracle; 026import de.learnlib.api.Query; 027 028/** 029 * A collection of suffix-based global counterexample analyzers. 030 * 031 * @see GlobalSuffixFinder 032 * 033 * @author Malte Isberner <malte.isberner@gmail.com> 034 */ 035public abstract class GlobalSuffixFinders { 036 037 /** 038 * Adds all suffixes of the input word, as suggested by Mahler & Pnueli. 039 * @see #findMahlerPnueli(Query) 040 */ 041 public static final GlobalSuffixFinder<Object,Object> MAHLER_PNUELI 042 = new GlobalSuffixFinder<Object,Object>() { 043 @Override 044 public <RI,RO> 045 List<Word<RI>> findSuffixes( 046 Query<RI, RO> ceQuery, 047 AccessSequenceTransformer<RI> asTransformer, 048 SuffixOutput<RI, RO> hypOutput, 049 MembershipOracle<RI, RO> oracle) { 050 return findMahlerPnueli(ceQuery); 051 } 052 }; 053 054 /** 055 * Adds all suffixes of the remainder of the input word, after stripping a maximal 056 * one-letter extension of an access sequence 057 * @see #findShahbaz(Query, AccessSequenceTransformer) 058 */ 059 public static final GlobalSuffixFinder<Object,Object> SHAHBAZ 060 = new GlobalSuffixFinder<Object,Object>() { 061 @Override 062 public <RI,RO> 063 List<Word<RI>> findSuffixes( 064 Query<RI, RO> ceQuery, 065 AccessSequenceTransformer<RI> asTransformer, 066 SuffixOutput<RI, RO> hypOutput, 067 MembershipOracle<RI, RO> oracle) { 068 return findShahbaz(ceQuery, asTransformer); 069 } 070 }; 071 072 /** 073 * Adds the single suffix found by the access sequence transformation 074 * in ascending linear order. 075 * @see #findLinear(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle, boolean) 076 */ 077 public static final GlobalSuffixFinder<Object,Object> FIND_LINEAR 078 = fromLocalFinder(LocalSuffixFinders.FIND_LINEAR, false); 079 080 /** 081 * Adds the suffix found by the access sequence transformation 082 * in ascending linear order, and all of its suffixes. 083 * @see #findLinear(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle, boolean) 084 */ 085 public static final GlobalSuffixFinder<Object,Object> FIND_LINEAR_ALLSUFFIXES 086 = fromLocalFinder(LocalSuffixFinders.FIND_LINEAR, true); 087 088 /** 089 * Adds the single suffix found by the access sequence transformation 090 * in descending linear order. 091 * @see #findLinearReverse(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle, boolean) 092 */ 093 public static final GlobalSuffixFinder<Object,Object> FIND_LINEAR_REVERSE 094 = fromLocalFinder(LocalSuffixFinders.FIND_LINEAR_REVERSE, false); 095 096 /** 097 * Adds the suffix found by the access sequence transformation 098 * in descending linear order, and all of its suffixes. 099 * @see #findLinearReverse(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle, boolean) 100 */ 101 public static final GlobalSuffixFinder<Object,Object> FIND_LINEAR_REVERSE_ALLSUFFIXES 102 = fromLocalFinder(LocalSuffixFinders.FIND_LINEAR_REVERSE, true); 103 104 /** 105 * Adds the single suffix found by the access sequence transformation 106 * using binary search. 107 * @see #findRivestSchapire(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle, boolean) 108 */ 109 public static final GlobalSuffixFinder<Object,Object> RIVEST_SCHAPIRE 110 = fromLocalFinder(LocalSuffixFinders.RIVEST_SCHAPIRE, false); 111 112 /** 113 * Adds the suffix found by the access sequence transformation 114 * using binary search, and all of its suffixes. 115 * @see #findRivestSchapire(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle, boolean) 116 */ 117 public static final GlobalSuffixFinder<Object,Object> RIVEST_SCHAPIRE_ALLSUFFIXES 118 = fromLocalFinder(LocalSuffixFinders.RIVEST_SCHAPIRE, true); 119 120 121 /** 122 * Transforms a {@link LocalSuffixFinder} into a global one. Since local suffix finders 123 * only return a single suffix, suffix-closedness of the set of distinguishing suffixes 124 * might not be preserved. Note that for correctly implemented local suffix finders, this 125 * does not impair correctness of the learning algorithm. However, without suffix closedness, 126 * intermediate hypothesis models might be non-canonical, if no additional precautions 127 * are taken. For that reasons, the <tt>allSuffixes</tt> parameter can be specified to control 128 * whether or not the list returned by 129 * {@link GlobalSuffixFinder#findSuffixes(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle)} 130 * of the returned global suffix finder should not only contain the single suffix, but also 131 * all of its suffixes, ensuring suffix-closedness. 132 * 133 * @param localFinder the local suffix finder 134 * @param allSuffixes whether or not all suffixes of the found local suffix should be added 135 * @return a global suffix finder using the analysis method from the specified local suffix finder 136 */ 137 public static <I,O> GlobalSuffixFinder<I,O> fromLocalFinder( 138 final LocalSuffixFinder<I,O> localFinder, 139 final boolean allSuffixes) { 140 141 return new GlobalSuffixFinder<I,O>() { 142 @Override 143 public <RI extends I,RO extends O> 144 List<Word<RI>> findSuffixes(Query<RI, RO> ceQuery, 145 AccessSequenceTransformer<RI> asTransformer, 146 SuffixOutput<RI, RO> hypOutput, MembershipOracle<RI, RO> oracle) { 147 int idx = localFinder.findSuffixIndex(ceQuery, asTransformer, hypOutput, oracle); 148 return suffixesForLocalOutput(ceQuery, idx, allSuffixes); 149 } 150 }; 151 } 152 153 /** 154 * Transforms a {@link LocalSuffixFinder} into a global one. This is a convenience method, 155 * behaving like <tt>fromLocalFinder(localFinder, false)</tt>. 156 * @see #fromLocalFinder(LocalSuffixFinder, boolean) 157 */ 158 public static <I,O> GlobalSuffixFinder<I,O> fromLocalFinder(LocalSuffixFinder<I,O> localFinder) { 159 return fromLocalFinder(localFinder, false); 160 } 161 162 163 /** 164 * Returns all suffixes of the counterexample word as distinguishing suffixes, as suggested 165 * by Mahler & Pnueli. 166 * @param ceQuery the counterexample query 167 * @return all suffixes of the counterexample input 168 */ 169 public static <I,O> List<Word<I>> findMahlerPnueli(Query<I,O> ceQuery) { 170 return ceQuery.getInput().suffixes(false); 171 } 172 173 /** 174 * Returns all suffixes of the counterexample word as distinguishing suffixes, after 175 * stripping a maximal one-letter extension of an access sequence, as suggested by 176 * Shahbaz. 177 * @param ceQuery the counterexample query 178 * @param asTransformer the access sequence transformer 179 * @return all suffixes from the counterexample after stripping a maximal one-letter 180 * extension of an access sequence. 181 */ 182 public static <I,O> List<Word<I>> findShahbaz(Query<I,O> ceQuery, 183 AccessSequenceTransformer<I> asTransformer) { 184 Word<I> queryWord = ceQuery.getInput(); 185 int queryLen = queryWord.length(); 186 187 Word<I> prefix = ceQuery.getPrefix(); 188 int i = prefix.length(); 189 190 while(i <= queryLen) { 191 Word<I> nextPrefix = queryWord.prefix(i); 192 193 if(!asTransformer.isAccessSequence(nextPrefix)) 194 break; 195 i++; 196 } 197 198 return queryWord.subWord(i).suffixes(false); 199 } 200 201 /** 202 * Returns the suffix (plus all of its suffixes, if <tt>allSuffixes</tt> is true) found by 203 * the access sequence transformation in ascending linear order. 204 * @param ceQuery the counterexample query 205 * @param asTransformer the access sequence transformer 206 * @param hypOutput interface to the hypothesis output 207 * @param oracle interface to the SUL output 208 * @param allSuffixes whether or not to include all suffixes of the found suffix 209 * @return the distinguishing suffixes 210 * @see LocalSuffixFinders#findLinear(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle) 211 */ 212 public static <I,O> List<Word<I>> findLinear(Query<I,O> ceQuery, 213 AccessSequenceTransformer<I> asTransformer, 214 SuffixOutput<I,O> hypOutput, 215 MembershipOracle<I, O> oracle, 216 boolean allSuffixes) { 217 int idx = LocalSuffixFinders.findLinear(ceQuery, asTransformer, hypOutput, oracle); 218 return suffixesForLocalOutput(ceQuery, idx, allSuffixes); 219 } 220 221 /** 222 * Returns the suffix (plus all of its suffixes, if <tt>allSuffixes</tt> is true) found by 223 * the access sequence transformation in descending linear order. 224 * @param ceQuery the counterexample query 225 * @param asTransformer the access sequence transformer 226 * @param hypOutput interface to the hypothesis output 227 * @param oracle interface to the SUL output 228 * @param allSuffixes whether or not to include all suffixes of the found suffix 229 * @return the distinguishing suffixes 230 * @see LocalSuffixFinders#findLinearReverse(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle) 231 */ 232 public static <I,O> List<Word<I>> findLinearReverse(Query<I,O> ceQuery, 233 AccessSequenceTransformer<I> asTransformer, 234 SuffixOutput<I,O> hypOutput, 235 MembershipOracle<I, O> oracle, 236 boolean allSuffixes) { 237 int idx = LocalSuffixFinders.findLinearReverse(ceQuery, asTransformer, hypOutput, oracle); 238 return suffixesForLocalOutput(ceQuery, idx, allSuffixes); 239 } 240 241 /** 242 * Returns the suffix (plus all of its suffixes, if <tt>allSuffixes</tt> is true) found by 243 * the binary search access sequence transformation. 244 * @param ceQuery the counterexample query 245 * @param asTransformer the access sequence transformer 246 * @param hypOutput interface to the hypothesis output 247 * @param oracle interface to the SUL output 248 * @param allSuffixes whether or not to include all suffixes of the found suffix 249 * @return the distinguishing suffixes 250 * @see LocalSuffixFinders#findRivestSchapire(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle) 251 */ 252 public static <I,O> List<Word<I>> findRivestSchapire(Query<I,O> ceQuery, 253 AccessSequenceTransformer<I> asTransformer, 254 SuffixOutput<I,O> hypOutput, 255 MembershipOracle<I, O> oracle, 256 boolean allSuffixes) { 257 int idx = LocalSuffixFinders.findRivestSchapire(ceQuery, asTransformer, hypOutput, oracle); 258 return suffixesForLocalOutput(ceQuery, idx, allSuffixes); 259 } 260 261 262 /** 263 * Transforms a suffix index returned by a {@link LocalSuffixFinder} into a list containing 264 * the single distinguishing suffix. 265 */ 266 public static <I,O> List<Word<I>> suffixesForLocalOutput(Query<I,O> ceQuery, 267 int localSuffixIdx) { 268 return suffixesForLocalOutput(ceQuery, localSuffixIdx, false); 269 } 270 271 /** 272 * Transforms a suffix index returned by a {@link LocalSuffixFinder} into a list of distinguishing 273 * suffixes. This list always contains the corresponding local suffix. Since local suffix finders 274 * only return a single suffix, suffix-closedness of the set of distinguishing suffixes 275 * might not be preserved. Note that for correctly implemented local suffix finders, this 276 * does not impair correctness of the learning algorithm. However, without suffix closedness, 277 * intermediate hypothesis models might be non-canonical, if no additional precautions 278 * are taken. For that reasons, the <tt>allSuffixes</tt> parameter can be specified to control 279 * whether or not the list returned by 280 * {@link GlobalSuffixFinder#findSuffixes(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle)} 281 * of the returned global suffix finder should not only contain the single suffix, but also 282 * all of its suffixes, ensuring suffix-closedness. 283 */ 284 public static <I,O> List<Word<I>> suffixesForLocalOutput(Query<I,O> ceQuery, 285 int localSuffixIdx, boolean allSuffixes) { 286 287 if(localSuffixIdx == -1) 288 return Collections.emptyList(); 289 290 Word<I> suffix = ceQuery.getInput().subWord(localSuffixIdx); 291 292 if(!allSuffixes) 293 return Collections.singletonList(suffix); 294 295 return suffix.suffixes(false); 296 } 297 298 299 // Prevent inheritance 300 private GlobalSuffixFinders() {} 301 302}