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.algorithms.lstargeneric.ce; 018 019import java.util.Collections; 020import java.util.List; 021 022import net.automatalib.automata.concepts.SuffixOutput; 023import net.automatalib.words.Word; 024import de.learnlib.algorithms.lstargeneric.table.ObservationTable; 025import de.learnlib.algorithms.lstargeneric.table.Row; 026import de.learnlib.api.MembershipOracle; 027import de.learnlib.api.Query; 028import de.learnlib.counterexamples.GlobalSuffixFinder; 029import de.learnlib.counterexamples.GlobalSuffixFinders; 030import de.learnlib.counterexamples.LocalSuffixFinder; 031import de.learnlib.counterexamples.LocalSuffixFinders; 032import de.learnlib.oracles.DefaultQuery; 033 034public class ObservationTableCEXHandlers { 035 036 public static ObservationTableCEXHandler<Object,Object> CLASSIC_LSTAR 037 = new ObservationTableCEXHandler<Object, Object>() { 038 @Override 039 public <RI,RO> List<List<Row<RI>>> handleCounterexample( 040 DefaultQuery<RI, RO> ceQuery, 041 ObservationTable<RI, RO> table, 042 SuffixOutput<RI, RO> hypOutput, 043 MembershipOracle<RI, RO> oracle) { 044 return handleClassicLStar(ceQuery, table, oracle); 045 } 046 @Override 047 public boolean needsConsistencyCheck() { 048 return true; 049 } 050 }; 051 052 public static ObservationTableCEXHandler<Object,Object> SUFFIX1BY1 053 = new ObservationTableCEXHandler<Object,Object>() { 054 @Override 055 public <RI,RO> 056 List<List<Row<RI>>> handleCounterexample( 057 DefaultQuery<RI, RO> ceQuery, 058 ObservationTable<RI, RO> table, 059 SuffixOutput<RI, RO> hypOutput, 060 MembershipOracle<RI, RO> oracle) { 061 return handleSuffix1by1(ceQuery, table, oracle); 062 } 063 @Override 064 public boolean needsConsistencyCheck() { 065 return false; 066 } 067 }; 068 069 public static ObservationTableCEXHandler<Object,Object> MAHLER_PNUELI 070 = fromGlobalSuffixFinder(GlobalSuffixFinders.MAHLER_PNUELI); 071 072 public static ObservationTableCEXHandler<Object,Object> SHAHBAZ 073 = fromGlobalSuffixFinder(GlobalSuffixFinders.SHAHBAZ); 074 075 public static ObservationTableCEXHandler<Object,Object> FIND_LINEAR 076 = fromLocalSuffixFinder(LocalSuffixFinders.FIND_LINEAR, false); 077 078 public static ObservationTableCEXHandler<Object,Object> FIND_LINEAR_ALLSUFFIXES 079 = fromLocalSuffixFinder(LocalSuffixFinders.FIND_LINEAR, true); 080 081 public static ObservationTableCEXHandler<Object,Object> FIND_LINEAR_REVERSE 082 = fromLocalSuffixFinder(LocalSuffixFinders.FIND_LINEAR_REVERSE, false); 083 084 public static ObservationTableCEXHandler<Object,Object> FIND_LINEAR_REVERSE_ALLSUFFIXES 085 = fromLocalSuffixFinder(LocalSuffixFinders.FIND_LINEAR_REVERSE, true); 086 087 public static ObservationTableCEXHandler<Object,Object> RIVEST_SCHAPIRE 088 = fromLocalSuffixFinder(LocalSuffixFinders.RIVEST_SCHAPIRE, false); 089 090 public static ObservationTableCEXHandler<Object,Object> RIVEST_SCHAPIRE_ALLSUFFIXES 091 = fromLocalSuffixFinder(LocalSuffixFinders.RIVEST_SCHAPIRE, true); 092 093 094 095 public static <I,O> 096 ObservationTableCEXHandler<I, O> fromGlobalSuffixFinder(final GlobalSuffixFinder<I,O> globalFinder) { 097 return new ObservationTableCEXHandler<I, O>() { 098 @Override 099 public <RI extends I,RO extends O> 100 List<List<Row<RI>>> handleCounterexample( 101 DefaultQuery<RI,RO> ceQuery, ObservationTable<RI,RO> table, 102 SuffixOutput<RI,RO> hypOutput, MembershipOracle<RI,RO> oracle) { 103 List<Word<RI>> suffixes = globalFinder.findSuffixes(ceQuery, table, hypOutput, oracle); 104 return handleGlobalSuffixes(table, suffixes, oracle); 105 } 106 @Override 107 public boolean needsConsistencyCheck() { 108 return false; 109 } 110 }; 111 } 112 113 public static <I,O> 114 ObservationTableCEXHandler<I, O> fromLocalSuffixFinder(final LocalSuffixFinder<I,O> localFinder, final boolean allSuffixes) { 115 return new ObservationTableCEXHandler<I, O>() { 116 @Override 117 public <RI extends I,RO extends O> 118 List<List<Row<RI>>> handleCounterexample( 119 DefaultQuery<RI,RO> ceQuery, ObservationTable<RI,RO> table, 120 SuffixOutput<RI,RO> hypOutput, MembershipOracle<RI,RO> oracle) { 121 int suffixIdx = localFinder.findSuffixIndex(ceQuery, table, hypOutput, oracle); 122 return handleLocalSuffix(ceQuery, table, suffixIdx, allSuffixes, oracle); 123 } 124 @Override 125 public boolean needsConsistencyCheck() { 126 return false; 127 } 128 }; 129 } 130 131 132 133 public static <I,O> 134 ObservationTableCEXHandler<I, O> fromLocalSuffixFinder(final LocalSuffixFinder<I,O> localFinder) { 135 return fromLocalSuffixFinder(localFinder, false); 136 } 137 138 public static <I,O> 139 List<List<Row<I>>> handleClassicLStar(DefaultQuery<I, O> ceQuery, 140 ObservationTable<I, O> table, MembershipOracle<I, O> oracle) { 141 142 List<Word<I>> prefixes = ceQuery.getInput().prefixes(false); 143 144 return table.addShortPrefixes(prefixes, oracle); 145 } 146 147 public static <I,O> 148 List<List<Row<I>>> handleSuffix1by1(DefaultQuery<I, O> ceQuery, 149 ObservationTable<I, O> table, MembershipOracle<I, O> oracle) { 150 List<List<Row<I>>> unclosed = Collections.emptyList(); 151 152 List<Word<I>> suffixes = table.getSuffixes(); 153 154 Word<I> ceWord = ceQuery.getInput(); 155 int ceLen = ceWord.length(); 156 157 for(int i = 1; i <= ceLen; i++) { 158 Word<I> suffix = ceWord.suffix(i); 159 if(suffixes != null) { 160 if(suffixes.contains(suffix)) 161 continue; 162 suffixes = null; 163 } 164 165 unclosed = table.addSuffix(suffix, oracle); 166 if(!unclosed.isEmpty()) 167 break; 168 } 169 170 return unclosed; 171 } 172 173 public static <I,O> 174 List<List<Row<I>>> handleGlobalSuffixes(ObservationTable<I,O> table, List<Word<I>> suffixes, 175 MembershipOracle<I,O> oracle) { 176 return table.addSuffixes(suffixes, oracle); 177 } 178 179 public static <I,O> 180 List<List<Row<I>>> handleLocalSuffix(Query<I,O> ceQuery, ObservationTable<I,O> table, 181 int suffixIndex, boolean allSuffixes, MembershipOracle<I,O> oracle) { 182 List<Word<I>> suffixes 183 = GlobalSuffixFinders.suffixesForLocalOutput(ceQuery, suffixIndex, allSuffixes); 184 return handleGlobalSuffixes(table, suffixes, oracle); 185 } 186 187 public static <I,O> 188 List<List<Row<I>>> handleLocalSuffix(Query<I,O> ceQuery, ObservationTable<I,O> table, 189 int suffixIndex, MembershipOracle<I,O> oracle) { 190 return handleLocalSuffix(ceQuery, table, suffixIndex, false, oracle); 191 } 192}