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