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}