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.Collection;
020import java.util.Collections;
021import java.util.List;
022import java.util.Objects;
023
024import net.automatalib.automata.UniversalDeterministicAutomaton;
025import net.automatalib.automata.concepts.Output;
026import net.automatalib.commons.util.collections.CollectionsUtil;
027import net.automatalib.util.automata.Automata;
028import net.automatalib.words.Word;
029import net.automatalib.words.WordBuilder;
030import de.learnlib.api.EquivalenceOracle;
031import de.learnlib.api.MembershipOracle;
032import de.learnlib.oracles.DefaultQuery;
033
034/**
035 * Implements an equivalence test by applying the W-method test on the given
036 * hypothesis automaton, as described in "Testing software design modelled by finite state machines"
037 * by T.S. Chow.
038 * 
039 * @author Malte Isberner <malte.isberner@gmail.com>
040 *
041 * @param <A> automaton class
042 * @param <I> input symbol class
043 * @param <O> output class
044 */
045public class WMethodEQOracle<A extends UniversalDeterministicAutomaton<?, I, ?, ?,?> & Output<I,O>, I, O>
046        implements EquivalenceOracle<A, I, O> {
047        
048        private int maxDepth;
049        private final MembershipOracle<I,O> sulOracle;
050        
051        /**
052         * Constructor.
053         * @param maxDepth the maximum length of the "middle" part of the test cases
054         * @param sulOracle interface to the system under learning
055         */
056        public WMethodEQOracle(int maxDepth, MembershipOracle<I,O> sulOracle) {
057                this.maxDepth = maxDepth;
058                this.sulOracle = sulOracle;
059        }
060
061        /*
062         * (non-Javadoc)
063         * @see de.learnlib.api.EquivalenceOracle#findCounterExample(java.lang.Object, java.util.Collection)
064         */
065        @Override
066        public DefaultQuery<I, O> findCounterExample(A hypothesis,
067                        Collection<? extends I> inputs) {
068                
069                List<Word<I>> transCover = Automata.transitionCover(hypothesis, inputs);
070                List<Word<I>> charSuffixes = Automata.characterizingSet(hypothesis, inputs);
071                
072                // Special case: List of characterizing suffixes may be empty,
073                // but in this case we still need to test!
074                if(charSuffixes.isEmpty())
075                        charSuffixes = Collections.singletonList(Word.<I>epsilon());
076                
077                
078                WordBuilder<I> wb = new WordBuilder<>();
079                
080                for(List<? extends I> middle : CollectionsUtil.allTuples(inputs, 1, maxDepth)) {
081                        for(Word<I> trans : transCover) {
082                                for(Word<I> suffix : charSuffixes) {
083                                        wb.append(trans).append(middle).append(suffix);
084                                        Word<I> queryWord = wb.toWord();
085                                        wb.clear();
086                                        DefaultQuery<I,O> query = new DefaultQuery<>(queryWord);
087                                        O hypOutput = hypothesis.computeOutput(queryWord);
088                                        sulOracle.processQueries(Collections.singleton(query));
089                                        if(!Objects.equals(hypOutput, query.getOutput()))
090                                                return query;
091                                }
092                        }
093                }
094                
095                return null;
096        }
097        
098}