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.Random;
024
025import net.automatalib.automata.concepts.OutputAutomaton;
026import net.automatalib.automata.fsa.DFA;
027import net.automatalib.automata.transout.MealyMachine;
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 *
036 * @author Maik Merten <maikmerten@googlemail.com>
037 */
038public class RandomWordsEQOracle<I, O, A extends OutputAutomaton<?, I, ?, O>> implements EquivalenceOracle<A, I, O> {
039        
040        public static class DFARandomWordsEQOracle<I> extends RandomWordsEQOracle<I,Boolean,DFA<?,I>>
041                        implements DFAEquivalenceOracle<I> {
042                public DFARandomWordsEQOracle(MembershipOracle<I, Boolean> mqOracle,
043                                int minLength, int maxLength, int maxTests, Random random) {
044                        super(mqOracle, minLength, maxLength, maxTests, random);
045                }
046        }
047        
048        public static class MealyRandomWordsEQOracle<I,O> extends RandomWordsEQOracle<I,Word<O>,MealyMachine<?,I,?,O>>
049                        implements MealyEquivalenceOracle<I,O> {
050                public MealyRandomWordsEQOracle(MembershipOracle<I, Word<O>> mqOracle,
051                                int minLength, int maxLength, int maxTests, Random random) {
052                        super(mqOracle, minLength, maxLength, maxTests, random);
053                }
054        }
055
056        private MembershipOracle<I, O> oracle;
057        private int maxTests, minLength, maxLength;
058        private final Random random;
059
060        public RandomWordsEQOracle(MembershipOracle<I, O> mqOracle, int minLength, int maxLength, int maxTests, Random random) {
061                this.oracle = mqOracle;
062                this.maxTests = maxTests;
063                this.minLength = minLength;
064                this.maxLength = maxLength;
065                this.random = random;
066        }
067
068        @Override
069        public DefaultQuery<I, O> findCounterExample(A hypothesis, Collection<? extends I> alpha) {
070
071                List<? extends I> symbolList;
072                if (alpha instanceof List) {
073                        symbolList = (List<? extends I>) alpha;
074                } else {
075                        symbolList = new ArrayList<>(alpha);
076                }
077                
078                int numSyms = symbolList.size();
079
080                for (int i = 0; i < maxTests; ++i) {
081                        int length = minLength + random.nextInt((maxLength - minLength) + 1);
082
083                        WordBuilder<I> testtrace = new WordBuilder<>(length);
084                        for (int j = 0; j < length; ++j) {
085                                int symidx = random.nextInt(numSyms);
086                                I sym = symbolList.get(symidx);
087                                testtrace.append(sym);
088                        }
089
090                        DefaultQuery<I, O> query = new DefaultQuery<>(testtrace.toWord());
091
092                        // query oracle
093                        oracle.processQueries(Collections.singletonList(query));
094                        O oracleoutput = query.getOutput();
095
096                        // trace hypothesis
097                        O hypOutput = hypothesis.computeOutput(testtrace.toWord());
098
099                        // compare output of hypothesis and oracle
100                        if (!oracleoutput.equals(hypOutput)) {
101                                return query;
102                        }
103                }
104
105                // no counterexample found
106                return null;
107        }
108}