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.baselinelstar; 018 019import java.util.ArrayList; 020import java.util.HashMap; 021import java.util.LinkedHashSet; 022import java.util.List; 023import java.util.Map; 024 025import net.automatalib.automata.fsa.DFA; 026import net.automatalib.automata.fsa.impl.FastDFA; 027import net.automatalib.automata.fsa.impl.FastDFAState; 028import net.automatalib.words.Alphabet; 029import net.automatalib.words.Word; 030 031/** 032 * The internal storage mechanism for {@link BaselineLStar}. 033 * 034 * @param <I> 035 * input symbol class. 036 */ 037public class ObservationTable<I> { 038 039 private LinkedHashSet<Word<I>> states; // S 040 private LinkedHashSet<Word<I>> candidates; // SA 041 private List<Word<I>> suffixes; // E 042 043 private Map<Word<I>, ObservationTableRow> rows; 044 045 public ObservationTable() { 046 Word<I> emptyWord = Word.epsilon(); 047 048 states = new LinkedHashSet<>(); 049 states.add(emptyWord); 050 051 candidates = new LinkedHashSet<>(); 052 053 suffixes = new ArrayList<>(); 054 suffixes.add(emptyWord); 055 056 rows = new HashMap<>(); 057 } 058 059 /** 060 * The set of states in the observation table, often called "S". 061 * 062 * @return The set of states. 063 */ 064 LinkedHashSet<Word<I>> getStates() { 065 return states; 066 } 067 068 /** 069 * The set of states in the observation table, often called "SA" or "S Sigma". 070 * 071 * @return The set of candidates. 072 */ 073 LinkedHashSet<Word<I>> getCandidates() { 074 return candidates; 075 } 076 077 /** 078 * The set of suffixes in the observation table, often called "E". 079 * 080 * @return The set of candidates. 081 */ 082 List<Word<I>> getSuffixes() { 083 return suffixes; 084 } 085 086 /** 087 * Adds the result of a membership query to this table. 088 * 089 * @param prefix 090 * The prefix of the {@link Word} asked with the membership query. 091 * @param suffix 092 * The prefix of the {@link Word} asked with the membership query. 093 * @param result 094 * The result of the query. 095 */ 096 void addResult(Word<I> prefix, Word<I> suffix, boolean result) { 097 if (!suffixes.contains(suffix)) { 098 throw new IllegalStateException("Suffix " + suffix + " is not part of the suffixes set"); 099 } 100 101 final int suffixPosition = suffixes.indexOf(suffix); 102 103 if (rows.containsKey(prefix)) { 104 addResultToRow(result, suffixPosition, rows.get(prefix)); 105 } 106 else { 107 if (suffixPosition > 0) { 108 throw new IllegalStateException("Unable to set position " + suffixPosition + " for an empty row."); 109 } 110 111 ObservationTableRow row = new ObservationTableRow(); 112 row.addValue(result); 113 114 rows.put(prefix, row); 115 } 116 } 117 118 private static void addResultToRow(boolean result, int suffixPosition, ObservationTableRow row) { 119 final List<Boolean> values = row.getValues(); 120 if (values.size() > suffixPosition) { 121 if (values.get(suffixPosition) != result) { 122 throw new IllegalStateException( 123 "New result " + values.get(suffixPosition) + " differs from old result " + result); 124 } 125 } 126 else { 127 row.addValue(result); 128 } 129 } 130 131 /** 132 * @return if the table is currently closed. 133 */ 134 boolean isClosed() { 135 return findUnclosedState() == null; 136 } 137 138 /** 139 * Determines the next state for which the observation table needs to be closed. 140 * 141 * @return The next state for which the observation table needs to be closed. If the 142 * table is closed, this returns {@code null}. 143 */ 144 Word<I> findUnclosedState() { 145 List<ObservationTableRow> stateRows = new ArrayList<>(states.size()); 146 147 for (Word<I> state : states) { 148 stateRows.add(getRowForPrefix(state)); 149 } 150 151 for (Word<I> candidate : candidates) { 152 boolean found = false; 153 154 ObservationTableRow row = getRowForPrefix(candidate); 155 for (ObservationTableRow stateRow : stateRows) { 156 if (row.equals(stateRow)) { 157 found = true; 158 break; 159 } 160 } 161 162 if (!found) { 163 return candidate; 164 } 165 } 166 167 return null; 168 } 169 170 /** 171 * @param alphabet 172 * The {@link Alphabet} for which the consistency is checked 173 * @return if the observation table is consistent with the given alphabet. 174 */ 175 boolean isConsistentWithAlphabet(Alphabet<I> alphabet) { 176 return findInconsistentSymbol(alphabet) == null; 177 } 178 179 InconsistencyDataHolder<I> findInconsistentSymbol(Alphabet<I> alphabet) { 180 List<Word<I>> allStates = new ArrayList<>(states); 181 182 for (I symbol : alphabet) { 183 for (int firstStateCounter = 0; firstStateCounter < states.size(); firstStateCounter++) { 184 Word<I> firstState = allStates.get(firstStateCounter); 185 186 for (int secondStateCounter = firstStateCounter + 1; secondStateCounter < states.size(); 187 secondStateCounter++) { 188 Word<I> secondState = allStates.get(secondStateCounter); 189 190 if (checkInconsistency(firstState, secondState, symbol)) { 191 return new InconsistencyDataHolder<>(firstState, secondState, symbol); 192 } 193 } 194 } 195 } 196 197 return null; 198 } 199 200 private boolean checkInconsistency(Word<I> firstState, Word<I> secondState, I alphabetSymbol) { 201 ObservationTableRow rowForFirstState = getRowForPrefix(firstState); 202 ObservationTableRow rowForSecondState = getRowForPrefix(secondState); 203 204 if (!rowForFirstState.equals(rowForSecondState)) { 205 return false; 206 } 207 208 Word<I> extendedFirstState = firstState.append(alphabetSymbol); 209 Word<I> extendedSecondState = secondState.append(alphabetSymbol); 210 ObservationTableRow rowForExtendedFirstState = getRowForPrefix(extendedFirstState); 211 ObservationTableRow rowForExtendedSecondState = getRowForPrefix(extendedSecondState); 212 213 return !rowForExtendedFirstState.equals(rowForExtendedSecondState); 214 } 215 216 Word<I> determineWitnessForInconsistency(InconsistencyDataHolder<I> dataHolder) { 217 if (dataHolder == null) { 218 throw new IllegalArgumentException("Dataholder must not be null!"); 219 } 220 221 Word<I> firstState = dataHolder.getFirstState().append(dataHolder.getDifferingSymbol()); 222 Word<I> secondState = dataHolder.getSecondState().append(dataHolder.getDifferingSymbol()); 223 224 ObservationTableRow firstRow = getRowForPrefix(firstState); 225 ObservationTableRow secondRow = getRowForPrefix(secondState); 226 227 for (int i = 0; i < firstRow.getValues().size(); i++) { 228 if (firstRow.getValues().get(i) != secondRow.getValues().get(i)) { 229 return suffixes.get(i); 230 } 231 } 232 233 throw new IllegalStateException("Both rows are identical, unable to determine a witness!"); 234 } 235 236 ObservationTableRow getRowForPrefix(Word<I> state) { 237 return rows.get(state); 238 } 239 240 /** 241 * Creates a hypothesis automaton based on the current state of the observation table. 242 * 243 * @param alphabet 244 * The alphabet of the automaton. 245 * @return The current hypothesis automaton. 246 */ 247 DFA<?, I> toAutomaton(Alphabet<I> alphabet) { 248 FastDFA<I> automaton = new FastDFA<>(alphabet); 249 Map<ObservationTableRow, FastDFAState> dfaStates = new HashMap<>((int) (1.5 * states.size())); 250 251 for (Word<I> state : states) { 252 if (dfaStates.containsKey(getRowForPrefix(state))) { 253 continue; 254 } 255 256 FastDFAState dfaState; 257 258 if (state.isEmpty()) { 259 dfaState = automaton.addInitialState(); 260 } 261 else { 262 dfaState = automaton.addState(); 263 } 264 265 Word<I> emptyWord = Word.epsilon(); 266 int positionOfEmptyWord = suffixes.indexOf(emptyWord); 267 dfaState.setAccepting(rows.get(state).getValues().get(positionOfEmptyWord)); 268 dfaStates.put(getRowForPrefix(state), dfaState); 269 } 270 271 for (Word<I> state : states) { 272 FastDFAState dfaState = dfaStates.get(getRowForPrefix(state)); 273 for (I alphabetSymbol : alphabet) { 274 Word<I> word = state.append(alphabetSymbol); 275 276 final int index = alphabet.getSymbolIndex(alphabetSymbol); 277 dfaState.setTransition(index, dfaStates.get(getRowForPrefix(word))); 278 } 279 } 280 281 return automaton; 282 } 283}