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.dhc.mealy;
018
019import java.util.ArrayDeque;
020import java.util.ArrayList;
021import java.util.Collections;
022import java.util.HashMap;
023import java.util.LinkedHashSet;
024import java.util.List;
025import java.util.Map;
026import java.util.Queue;
027import java.util.logging.Level;
028import java.util.logging.Logger;
029
030import net.automatalib.automata.transout.MealyMachine;
031import net.automatalib.automata.transout.impl.compact.CompactMealy;
032import net.automatalib.commons.util.mappings.MutableMapping;
033import net.automatalib.words.Alphabet;
034import net.automatalib.words.Word;
035import de.learnlib.algorithms.dhc.Deduplicator;
036import de.learnlib.api.AccessSequenceTransformer;
037import de.learnlib.api.LearningAlgorithm.MealyLearner;
038import de.learnlib.api.MembershipOracle;
039import de.learnlib.counterexamples.GlobalSuffixFinder;
040import de.learnlib.counterexamples.GlobalSuffixFinders;
041import de.learnlib.oracles.DefaultQuery;
042
043/**
044 *
045 * @author Maik Merten <maikmerten@googlemail.com>
046 */
047public class MealyDHC<I, O> implements MealyLearner<I,O>,
048                AccessSequenceTransformer<I> {
049
050        private static final Logger log = Logger.getLogger( MealyDHC.class.getName() );
051        
052        private final Alphabet<I> alphabet;
053        private final MembershipOracle<I, Word<O>> oracle;
054        private LinkedHashSet<Word<I>> splitters = new LinkedHashSet<>();
055        private CompactMealy<I, O> hypothesis;
056        private MutableMapping<Integer, QueueElement<I,O>> accessSequences;
057        private GlobalSuffixFinder<? super I,? super Word<O>> suffixFinder;
058
059
060        private static class QueueElement<I,O> {
061                private Integer parentState;
062                private QueueElement<I,O> parentElement;
063                private I transIn;
064                private O transOut;
065                private int depth;
066
067                private QueueElement(Integer parentState, QueueElement<I,O> parentElement, I transIn, O transOut) {
068                        this.parentState = parentState;
069                        this.parentElement = parentElement;
070                        this.transIn = transIn;
071                        this.transOut = transOut;
072                        this.depth = (parentElement != null) ? parentElement.depth+1 : 0;
073                }
074        }
075
076        public MealyDHC(Alphabet<I> alphabet, MembershipOracle<I, Word<O>> oracle) {
077                this.alphabet = alphabet;
078                this.oracle = oracle;
079                this.suffixFinder = GlobalSuffixFinders.RIVEST_SCHAPIRE;
080                for(I symbol : alphabet) {
081                        splitters.add(Word.fromLetter(symbol));
082                }
083        }
084
085        @Override
086        public void startLearning() {
087                // initialize structure to store state output signatures
088                Map<List<Word<O>>, Integer> signatures = new HashMap<>();
089
090                // set up new hypothesis machine
091                hypothesis = new CompactMealy<>(alphabet);
092
093                // initialize exploration queue
094                Queue<QueueElement<I,O>> queue = new ArrayDeque<>();
095                
096                // initialize storage for access sequences
097                accessSequences = hypothesis.createDynamicStateMapping();
098
099                // first element to be explored represents the initial state with no predecessor
100                queue.add(new QueueElement<I,O>(null, null, null, null));
101
102                Deduplicator<Word<O>> deduplicator = new Deduplicator<>();
103                
104                while (!queue.isEmpty()) {
105                        // get element to be explored from queue
106                        QueueElement<I,O> elem = queue.poll();
107
108                        // determine access sequence for state
109                        Word<I> access = assembleAccessSequence(elem);
110
111                        // assemble queries
112                        ArrayList<DefaultQuery<I, Word<O>>> queries = new ArrayList<>(splitters.size());
113                        for (Word<I> suffix : splitters) {
114                                queries.add(new DefaultQuery<I, Word<O>>(access, suffix));
115                        }
116
117                        // retrieve answers
118                        oracle.processQueries(queries);
119
120                        // assemble output signature
121                        List<Word<O>> sig = new ArrayList<>(splitters.size());
122                        for (DefaultQuery<I, Word<O>> query : queries) {
123                                sig.add(deduplicator.deduplicate(query.getOutput()));
124                        }
125
126                        Integer sibling = signatures.get(sig);
127
128                        if (sibling != null) {
129                                // this element does not possess a new output signature
130                                // create a transition from parent state to sibling
131                                hypothesis.addTransition(elem.parentState, elem.transIn, sibling, elem.transOut);
132                        } else {
133                                // this is actually an observably distinct state! Progress!
134                                // Create state and connect via transition to parent
135                                Integer state = elem.parentElement == null ? hypothesis.addInitialState() : hypothesis.addState();
136                                if (elem.parentElement != null) {
137                                        hypothesis.addTransition(elem.parentState, elem.transIn, state, elem.transOut);
138                                }
139                                signatures.put(sig, state);
140                                accessSequences.put(state, elem);
141
142                                scheduleSuccessors(elem, state, queue, sig);
143                        }
144                }
145        }
146
147        private Word<I> assembleAccessSequence(QueueElement<I,O> elem) {
148                List<I> word = new ArrayList<>(elem.depth);
149                
150                QueueElement<I,O> pre = elem.parentElement;
151                I sym = elem.transIn;
152                while(pre != null && sym != null) {
153                        word.add(sym);
154                        sym = pre.transIn;
155                        pre = pre.parentElement;
156                }
157                
158                Collections.reverse(word);
159                return Word.fromList(word);
160        }
161
162        private void scheduleSuccessors(QueueElement<I,O> elem, Integer state, Queue<QueueElement<I,O>> queue, List<Word<O>> sig) throws IllegalArgumentException {
163                for (int i = 0; i < alphabet.size(); ++i) {
164                        // retrieve I/O for transition
165                        I input = alphabet.getSymbol(i);
166                        O output = sig.get(i).getSymbol(0);
167
168                        // create successor element and schedule for exploration
169                        queue.add(new QueueElement<>(state, elem, input, output));
170                }
171        }
172        
173        private void checkInternalState() {
174                if (hypothesis == null) {
175                        throw new IllegalStateException("No hypothesis learned yet");
176                }
177        }
178
179        @Override
180        public boolean refineHypothesis(DefaultQuery<I, Word<O>> ceQuery) {
181                checkInternalState();
182
183                int oldsize = hypothesis.size();
184                
185                for(Word<I> suf : suffixFinder.findSuffixes(ceQuery, this, hypothesis, oracle)) {
186                        if(!splitters.contains(suf)) {
187                                splitters.add(suf);
188                                log.log(Level.FINE, "added suffix: {0}", suf);
189                        }
190                }
191
192                startLearning();
193
194                return oldsize != hypothesis.size();
195        }
196
197        @Override
198        public MealyMachine<?, I, ?, O> getHypothesisModel() {
199                checkInternalState();
200                return hypothesis;
201        }
202        
203        @Override
204        public Word<I> transformAccessSequence(Word<I> word) {
205                checkInternalState();
206                Integer state = hypothesis.getSuccessor(hypothesis.getInitialState(), word);
207                return assembleAccessSequence(accessSequences.get(state));
208        }
209
210        @Override
211        public boolean isAccessSequence(Word<I> word) {
212                checkInternalState();
213                Word<I> canonical = transformAccessSequence(word);
214                return canonical.equals(word);
215        }
216
217}