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.eqtests.basic;
018
019import java.util.ArrayList;
020import java.util.Collection;
021import java.util.Collections;
022import java.util.List;
023import java.util.Objects;
024
025import net.automatalib.automata.UniversalDeterministicAutomaton;
026import net.automatalib.automata.concepts.Output;
027import net.automatalib.commons.util.collections.CollectionsUtil;
028import net.automatalib.commons.util.mappings.MutableMapping;
029import net.automatalib.util.automata.Automata;
030import net.automatalib.words.Word;
031import net.automatalib.words.WordBuilder;
032import de.learnlib.api.EquivalenceOracle;
033import de.learnlib.api.MembershipOracle;
034import de.learnlib.oracles.DefaultQuery;
035
036/**
037 * Implements an equivalence test by applying the Wp-method test on the given hypothesis automaton,
038 * as described in "Test Selection Based on Finite State Models" by S. Fujiwara et al.
039 * 
040 * @author Malte Isberner <malte.isberner@gmail.com>
041 *
042 * @param <A> automaton class
043 * @param <I> input symbol class
044 * @param <O> output class
045 */
046public class WpMethodEQOracle<A extends UniversalDeterministicAutomaton<?, I, ?, ?, ?> & Output<I,O>,I,O>
047                implements EquivalenceOracle<A, I, O> {
048        
049        private final int maxDepth;
050        private final MembershipOracle<I, O> sulOracle;
051        
052        /**
053         * Constructor.
054         * @param maxDepth the maximum length of the "middle" part of the test cases
055         * @param sulOracle interface to the system under learning
056         */
057        public WpMethodEQOracle(int maxDepth, MembershipOracle<I,O> sulOracle) {
058                this.maxDepth = maxDepth;
059                this.sulOracle = sulOracle;
060        }
061
062        /*
063         * (non-Javadoc)
064         * @see de.learnlib.api.EquivalenceOracle#findCounterExample(java.lang.Object, java.util.Collection)
065         */
066        @Override
067        public DefaultQuery<I, O> findCounterExample(A hypothesis,
068                        Collection<? extends I> inputs) {
069                UniversalDeterministicAutomaton<?, I, ?, ?, ?> aut = hypothesis;
070                Output<I,O> out = hypothesis;
071                return doFindCounterExample(aut, out, inputs);
072        }
073        
074        
075        /*
076         * Delegate target, used to bind the state-parameter of the automaton
077         */
078        private <S> DefaultQuery<I,O> doFindCounterExample(UniversalDeterministicAutomaton<S, I, ?, ?, ?> hypothesis,
079                        Output<I,O> output, Collection<? extends I> inputs) {
080                
081                List<Word<I>> stateCover = new ArrayList<Word<I>>(hypothesis.size());
082                List<Word<I>> transitions = new ArrayList<Word<I>>(hypothesis.size() * (inputs.size() - 1));
083                
084                Automata.cover(hypothesis, inputs, stateCover, transitions);
085                
086                List<Word<I>> globalSuffixes = Automata.characterizingSet(hypothesis, inputs);
087                if(globalSuffixes.isEmpty())
088                        globalSuffixes = Collections.singletonList(Word.<I>epsilon());
089        
090                WordBuilder<I> wb = new WordBuilder<>();
091                
092                
093                // Phase 1: state cover * middle part * global suffixes
094                for(List<? extends I> middle : CollectionsUtil.allTuples(inputs, 1, maxDepth)) {
095                        for(Word<I> as : stateCover) {
096                                for(Word<I> suffix : globalSuffixes) {
097                                        wb.append(as).append(middle).append(suffix);
098                                        Word<I> queryWord = wb.toWord();
099                                        wb.clear();
100                                        DefaultQuery<I,O> query = new DefaultQuery<>(queryWord);
101                                        O hypOutput = output.computeOutput(queryWord);
102                                        sulOracle.processQueries(Collections.singleton(query));
103                                        if(!Objects.equals(hypOutput, query.getOutput()))
104                                                return query;
105                                }
106                        }
107                }
108
109                // Phase 2: transitions (not in state cover) * middle part * local suffixes
110                MutableMapping<S,List<Word<I>>> localSuffixSets
111                        = hypothesis.createStaticStateMapping();
112                
113                for(List<? extends I> middle : CollectionsUtil.allTuples(inputs, 1, maxDepth)) {
114                        for(Word<I> trans : transitions) {
115                                S state = hypothesis.getState(trans);
116                                List<Word<I>> localSuffixes = localSuffixSets.get(state);
117                                if(localSuffixes == null) {
118                                        localSuffixes = Automata.stateCharacterizingSet(hypothesis, inputs, state);
119                                        if(localSuffixes.isEmpty())
120                                                localSuffixes = Collections.singletonList(Word.<I>epsilon());
121                                        localSuffixSets.put(state, localSuffixes);
122                                }
123                                
124                                for(Word<I> suffix : localSuffixes) {
125                                        wb.append(trans).append(middle).append(suffix);
126                                        Word<I> queryWord = wb.toWord();
127                                        wb.clear();
128                                        DefaultQuery<I,O> query = new DefaultQuery<>(queryWord);
129                                        O hypOutput = output.computeOutput(queryWord);
130                                        sulOracle.processQueries(Collections.singleton(query));
131                                        if(!Objects.equals(hypOutput, query.getOutput()))
132                                                return query;
133                                }
134                        }
135                }
136                
137                return null;
138        }
139
140}