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}