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.Objects;
020
021import net.automatalib.automata.concepts.SuffixOutput;
022import net.automatalib.words.Word;
023import de.learnlib.api.AccessSequenceTransformer;
024import de.learnlib.api.MembershipOracle;
025import de.learnlib.api.Query;
026import de.learnlib.oracles.MQUtil;
027
028/**
029 * A collection of suffix-based local counterexample analyzers.
030 * 
031 * @see LocalSuffixFinder
032 * 
033 * @author Malte Isberner <malte.isberner@gmail.com>
034 */
035public abstract class LocalSuffixFinders {
036        
037        /**
038         * Searches for a distinguishing suffixes by checking for counterexample yielding
039         * access sequence transformations in linear ascending order.
040         * @see #findLinear(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle)
041         */
042        public static final LocalSuffixFinder<Object,Object> FIND_LINEAR
043                = new LocalSuffixFinder<Object,Object>() {
044                        @Override
045                        public <RI,RO>
046                        int findSuffixIndex(Query<RI, RO> ceQuery,
047                                        AccessSequenceTransformer<RI> asTransformer,
048                                        SuffixOutput<RI,RO> hypOutput,
049                                        MembershipOracle<RI, RO> oracle) {
050                                return findLinear(ceQuery, asTransformer, hypOutput, oracle);
051                        }
052        };
053        
054        /**
055         * Searches for a distinguishing suffixes by checking for counterexample yielding
056         * access sequence transformations in linear descending order.
057         * @see #findLinearReverse(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle)
058         */
059        public static final LocalSuffixFinder<Object,Object> FIND_LINEAR_REVERSE
060                = new LocalSuffixFinder<Object,Object>() {
061                        @Override
062                        public <RI,RO>
063                        int findSuffixIndex(Query<RI, RO> ceQuery,
064                                        AccessSequenceTransformer<RI> asTransformer,
065                                        SuffixOutput<RI,RO> hypOutput,
066                                        MembershipOracle<RI, RO> oracle) {
067                                return findLinearReverse(ceQuery, asTransformer, hypOutput, oracle);
068                        }
069        };
070        
071        /**
072         * Searches for a distinguishing suffixes by checking for counterexample yielding
073         * access sequence transformations using a binary search, as proposed by Rivest & Schapire.
074         * @see #findRivestSchapire(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle)
075         */
076        public static final LocalSuffixFinder<Object,Object> RIVEST_SCHAPIRE
077                = new LocalSuffixFinder<Object,Object>() {
078                        @Override
079                        public <RI,RO>
080                        int findSuffixIndex(Query<RI, RO> ceQuery,
081                                        AccessSequenceTransformer<RI> asTransformer,
082                                        SuffixOutput<RI,RO> hypOutput,
083                                        MembershipOracle<RI, RO> oracle) {
084                                return findRivestSchapire(ceQuery, asTransformer, hypOutput, oracle);
085                        }
086        };
087
088        
089        
090        /**
091         * Searches for a distinguishing suffixes by checking for counterexample yielding
092         * access sequence transformations in linear ascending order.
093         * 
094         * @param ceQuery the initial counterexample query
095         * @param asTransformer the access sequence transformer
096         * @param hypOutput interface to the hypothesis output, for checking whether the oracle output
097         * contradicts the hypothesis
098         * @param oracle interface to the SUL
099         * @return the index of the respective suffix, or <tt>-1</tt> if no
100         * counterexample could be found
101         * @see LocalSuffixFinder
102         */
103        public static <S,I,O> int findLinear(Query<I,O> ceQuery,
104                        AccessSequenceTransformer<I> asTransformer,
105                        SuffixOutput<I,O> hypOutput,
106                        MembershipOracle<I, O> oracle) {
107                
108                Word<I> queryWord = ceQuery.getInput();
109                int queryLen = queryWord.length();
110                
111                Word<I> prefix = ceQuery.getPrefix();
112                int prefixLen = prefix.length();
113                
114                // If the prefix is an access sequence (i.e., a short prefix),
115                // then we can omit the first step, as transforming won't change
116                int min = asTransformer.isAccessSequence(prefix) ? prefixLen+1 : prefixLen;
117                
118                for(int i = min; i <= queryLen; i++) {
119                        Word<I> nextPrefix = queryWord.prefix(i);
120                        Word<I> as = asTransformer.transformAccessSequence(nextPrefix);
121                        
122                        Word<I> nextSuffix = queryWord.subWord(i);
123                        
124                        O hypOut = hypOutput.computeSuffixOutput(as, nextSuffix);
125                        O mqOut = MQUtil.output(oracle, as, nextSuffix);
126                        
127                        if(Objects.equals(hypOut, mqOut))
128                                return i;
129                }
130                
131                return -1;
132        }
133        
134        /**
135         * Searches for a distinguishing suffixes by checking for counterexample yielding
136         * access sequence transformations in linear descending order.
137         * 
138         * @param ceQuery the initial counterexample query
139         * @param asTransformer the access sequence transformer
140         * @param hypOutput interface to the hypothesis output, for checking whether the oracle output
141         * contradicts the hypothesis
142         * @param oracle interface to the SUL
143         * @return the index of the respective suffix, or <tt>-1</tt> if no
144         * counterexample could be found
145         * @see LocalSuffixFinder
146         */
147        public static <I,O> int findLinearReverse(Query<I,O> ceQuery,
148                        AccessSequenceTransformer<I> asTransformer,
149                        SuffixOutput<I,O> hypOutput,
150                        MembershipOracle<I, O> oracle) {
151                
152                Word<I> queryWord = ceQuery.getInput();
153                int queryLen = queryWord.length();
154                
155                Word<I> prefix = ceQuery.getPrefix();
156                int prefixLen = prefix.length();
157                
158                // If the prefix is no access sequence (i.e., a long prefix),
159                // then we also need to consider that breakage only occurs
160                // by transforming this long prefix into a short one
161                int min = asTransformer.isAccessSequence(prefix) ? prefixLen : prefixLen-1;
162                
163                for(int i = queryLen - 1; i >= min; i--) {
164                        Word<I> nextPrefix = queryWord.prefix(i);
165                        Word<I> as = asTransformer.transformAccessSequence(nextPrefix);
166                        Word<I> nextSuffix = queryWord.subWord(i);
167                        
168                        O hypOut = hypOutput.computeSuffixOutput(as, nextSuffix);
169                        O mqOut = MQUtil.output(oracle, as, nextSuffix);
170                        
171                        if(!Objects.equals(hypOut, mqOut))
172                                return i+1;
173                }
174                
175                return -1;
176        }
177        
178        
179        /**
180         * Searches for a distinguishing suffixes by checking for counterexample yielding
181         * access sequence transformations using a binary search, as proposed by Rivest & Schapire.
182         * 
183         * @param ceQuery the initial counterexample query
184         * @param asTransformer the access sequence transformer
185         * @param hypOutput interface to the hypothesis output, for checking whether the oracle output
186         * contradicts the hypothesis
187         * @param oracle interface to the SUL
188         * @return the index of the respective suffix, or <tt>-1</tt> if no
189         * counterexample could be found
190         * @see LocalSuffixFinder
191         */
192        public static <I,O> int findRivestSchapire(Query<I,O> ceQuery,
193                        AccessSequenceTransformer<I> asTransformer,
194                        SuffixOutput<I,O> hypOutput,
195                        MembershipOracle<I, O> oracle) {
196
197                Word<I> queryWord = ceQuery.getInput();
198                int queryLen = queryWord.length();
199                
200                Word<I> prefix = ceQuery.getPrefix();
201                int prefixLen = prefix.length();
202                
203                
204                int low = asTransformer.isAccessSequence(prefix) ? prefixLen : prefixLen-1;
205                
206                int high = queryLen;
207                
208                while((high - low) > 1) {
209                        int mid = low + (high - low + 1)/2;
210                        
211                        
212                        Word<I> nextPrefix = queryWord.prefix(mid);
213                        Word<I> as = asTransformer.transformAccessSequence(nextPrefix);
214                        
215                        Word<I> nextSuffix = queryWord.subWord(mid);
216                        
217                        O hypOut = hypOutput.computeSuffixOutput(as, nextSuffix);
218                        O ceOut = MQUtil.output(oracle, as, nextSuffix);
219                        
220                        if(!Objects.equals(hypOut, ceOut))
221                                low = mid;
222                        else
223                                high = mid;
224                }
225                
226                // FIXME: No check if actually found CE
227                return low+1;
228        }
229        
230        
231        // Prevent inheritance
232        private LocalSuffixFinders() {}
233}