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}