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}