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}