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.cache.mealy; 018 019import java.util.ArrayList; 020import java.util.Collection; 021import java.util.Collections; 022import java.util.Comparator; 023import java.util.Iterator; 024import java.util.List; 025 026import net.automatalib.commons.util.comparison.CmpUtil; 027import net.automatalib.commons.util.mappings.Mapping; 028import net.automatalib.incremental.mealy.IncrementalMealyBuilder; 029import net.automatalib.words.Alphabet; 030import net.automatalib.words.Word; 031import net.automatalib.words.WordBuilder; 032import de.learnlib.api.MembershipOracle; 033import de.learnlib.api.MembershipOracle.MealyMembershipOracle; 034import de.learnlib.api.Query; 035 036/** 037 * Mealy cache. This cache is implemented as a membership oracle: upon construction, it is 038 * provided with a delegate oracle. Queries that can be answered from the cache are answered 039 * directly, others are forwarded to the delegate oracle. When the delegate oracle has finished 040 * processing these remaining queries, the results are incorporated into the cache. 041 * 042 * This oracle additionally enables the user to define a Mealy-style prefix-closure filter: 043 * a {@link Mapping} from output symbols to output symbols may be provided, with the following 044 * semantics: If in an output word a symbol for which the given mapping has a non-null value 045 * is encountered, all symbols <i>after</i> this symbol are replaced by the respective value. 046 * The rationale behind this is that the concrete error message (key in the mapping) is still 047 * reflected in the learned model, it is forced to result in a sink state with only a single 048 * repeating output symbol (value in the mapping). 049 * 050 * @author Malte Isberner <malte.isberner@gmail.com> 051 * 052 * @param <I> input symbol class 053 * @param <O> output symbol class 054 */ 055public class MealyCacheOracle<I, O> implements MealyMembershipOracle<I,O> { 056 057 private static final class ReverseLexCmp<I> implements Comparator<Query<I,?>> { 058 private final Alphabet<I> alphabet; 059 060 public ReverseLexCmp(Alphabet<I> alphabet) { 061 this.alphabet = alphabet; 062 } 063 064 @Override 065 public int compare(Query<I, ?> o1, Query<I, ?> o2) { 066 return -CmpUtil.lexCompare(o1.getInput(), o2.getInput(), alphabet); 067 } 068 } 069 070 private final MembershipOracle<I,Word<O>> delegate; 071 private final IncrementalMealyBuilder<I, O> incMealy; 072 private final Comparator<? super Query<I,?>> queryCmp; 073 private final Mapping<? super O,? extends O> errorSyms; 074 075 /** 076 * Constructor. 077 * @param alphabet the input alphabet for the cache 078 * @param delegate the delegate Mealy oracle 079 */ 080 public MealyCacheOracle(Alphabet<I> alphabet, MembershipOracle<I,Word<O>> delegate) { 081 this(alphabet, null, delegate); 082 } 083 084 /** 085 * Constructor. 086 * @param alphabet the input alphabet for the cache 087 * @param errorSyms the error symbol mapping (see class description) 088 * @param delegate the delegate Mealy oracle 089 */ 090 public MealyCacheOracle(Alphabet<I> alphabet, Mapping<? super O, ? extends O> errorSyms, MembershipOracle<I,Word<O>> delegate) { 091 this.delegate = delegate; 092 this.incMealy = new IncrementalMealyBuilder<>(alphabet); 093 this.queryCmp = new ReverseLexCmp<>(alphabet); 094 this.errorSyms = errorSyms; 095 } 096 097 public int getCacheSize() { 098 return incMealy.size(); 099 } 100 101 /** 102 * Creates an equivalence oracle that checks an hypothesis for consistency with the 103 * contents of this cache. Note that the returned oracle is backed by the cache data structure, 104 * i.e., it is sufficient to call this method once after creation of the cache. 105 * @return the cache consistency test backed by the contents of this cache. 106 */ 107 public MealyCacheConsistencyTest<I, O> createCacheConsistencyTest() { 108 return new MealyCacheConsistencyTest<>(incMealy); 109 } 110 111 /* 112 * (non-Javadoc) 113 * @see de.learnlib.api.MembershipOracle#processQueries(java.util.Collection) 114 */ 115 @Override 116 public void processQueries(Collection<? extends Query<I, Word<O>>> queries) { 117 if(queries.isEmpty()) 118 return; 119 120 List<Query<I,Word<O>>> qrys = new ArrayList<Query<I,Word<O>>>(queries); 121 Collections.sort(qrys, queryCmp); 122 123 List<MasterQuery<I,O>> masterQueries = new ArrayList<>(); 124 125 Iterator<Query<I,Word<O>>> it = qrys.iterator(); 126 Query<I,Word<O>> q = it.next(); 127 Word<I> ref = q.getInput(); 128 MasterQuery<I,O> master = createMasterQuery(ref); 129 if(master.getAnswer() == null) 130 masterQueries.add(master); 131 master.addSlave(q); 132 133 while(it.hasNext()) { 134 q = it.next(); 135 Word<I> curr = q.getInput(); 136 if(!curr.isPrefixOf(ref)) { 137 master = createMasterQuery(curr); 138 if(master.getAnswer() == null) 139 masterQueries.add(master); 140 } 141 142 master.addSlave(q); 143 ref = curr; 144 } 145 146 delegate.processQueries(masterQueries); 147 148 for(MasterQuery<I,O> m : masterQueries) 149 postProcess(m); 150 } 151 152 private void postProcess(MasterQuery<I,O> master) { 153 Word<I> word = master.getSuffix(); 154 Word<O> answer = master.getAnswer(); 155 156 if(errorSyms == null) { 157 incMealy.insert(word, answer); 158 return; 159 } 160 161 int answLen = answer.length(); 162 int i = 0; 163 while(i < answLen) { 164 O sym = answer.getSymbol(i++); 165 if(errorSyms.get(sym) != null) 166 break; 167 } 168 169 if(i == answLen) 170 incMealy.insert(word, answer); 171 else 172 incMealy.insert(word.prefix(i), answer.prefix(i)); 173 } 174 175 private MasterQuery<I,O> createMasterQuery(Word<I> word) { 176 WordBuilder<O> wb = new WordBuilder<O>(); 177 if(incMealy.lookup(word, wb)) 178 return new MasterQuery<>(word, wb.toWord()); 179 180 if(errorSyms == null) 181 return new MasterQuery<>(word); 182 int wbSize = wb.size(); 183 O repSym; 184 if(wbSize == 0 || (repSym = errorSyms.get(wb.getSymbol(wbSize - 1))) == null) 185 return new MasterQuery<>(word, errorSyms); 186 187 wb.repeatAppend(word.length() - wbSize, repSym); 188 return new MasterQuery<>(word, wb.toWord()); 189 } 190 191}