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}