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.mealy;
018
019import java.util.Collection;
020import java.util.List;
021import java.util.Random;
022
023import net.automatalib.automata.transout.MealyMachine;
024import net.automatalib.commons.util.collections.CollectionsUtil;
025import net.automatalib.words.Word;
026import net.automatalib.words.WordBuilder;
027import de.learnlib.api.EquivalenceOracle;
028import de.learnlib.api.SUL;
029import de.learnlib.oracles.DefaultQuery;
030
031/**
032 * Performs a random walk over the hypothesis. A random walk restarts with a
033 * fixed probability after every step and terminates after a fixed number of
034 * steps or with a counterexample. The number of steps to termination may be
035 * reset for every new search.
036 * 
037 * @param <A>
038 *            hypothesis format
039 * @param <I>
040 *            input symbols class
041 * @param <O>
042 *            output symbol class
043 * 
044 * @author falkhowar
045 */
046public class RandomWalkEQOracle<I, O>
047                implements EquivalenceOracle<MealyMachine<?,I,?,O>, I, Word<O>> {
048
049        /**
050         * probability to restart before step.
051         */
052        private final double restartProbability;
053
054        /**
055         * maximum number of steps.
056         */
057        private final long maxSteps;
058
059        /**
060         * step counter.
061         */
062        private long steps = 0;
063
064        /**
065         * flag for reseting step count after every search.
066         */
067        private boolean resetStepCount;
068
069        /**
070         * RNG.
071         */
072        private final Random random;
073
074        /**
075         * System under learning.
076         */
077        private final SUL<I, O> sul;
078
079        /**
080         * Constructor.
081         * 
082         * @param restartProbability
083         * @param maxSteps
084         * @param random
085         * @param sul
086         */
087        public RandomWalkEQOracle(double restartProbability, long maxSteps,
088                        Random random, SUL<I, O> sul) {
089                this.restartProbability = restartProbability;
090                this.maxSteps = maxSteps;
091                this.random = random;
092                this.sul = sul;
093        }
094
095        public RandomWalkEQOracle(double restartProbability, long maxSteps,
096                        boolean resetStepCount, Random random, SUL<I, O> sul) {
097                this(restartProbability, maxSteps, random, sul);
098                this.resetStepCount = resetStepCount;
099        }
100
101        /**
102         * 
103         * @param hypothesis
104         * @param inputs
105         * @return null or a counterexample
106         */
107        @Override
108        public DefaultQuery<I, Word<O>> findCounterExample(MealyMachine<?,I,?,O> hypothesis,
109                        Collection<? extends I> inputs) {
110                return doFindCounterExample(hypothesis, inputs);
111        }
112
113        private <S, T> DefaultQuery<I, Word<O>> doFindCounterExample(
114                        MealyMachine<S, I, T, O> hypothesis, Collection<? extends I> inputs) {
115                // reset termination counter?
116                if (resetStepCount) {
117                        steps = 0;
118                }
119
120                List<? extends I> choices = CollectionsUtil.randomAccessList(inputs);
121                int bound = choices.size();
122                S cur = hypothesis.getInitialState();
123                WordBuilder<I> wbIn = new WordBuilder<>();
124                WordBuilder<O> wbOut = new WordBuilder<>();
125
126                while (steps < maxSteps) {
127
128                        // restart?
129                        double restart = random.nextDouble();
130                        if (restart < restartProbability) {
131                                sul.reset();
132                                cur = hypothesis.getInitialState();
133                                wbIn.clear();
134                                wbOut.clear();
135                        }
136
137                        // step
138                        steps++;
139                        I in = choices.get(random.nextInt(bound));
140                        O outSul = sul.step(in);
141                        T hypTrans = hypothesis.getTransition(cur, in);
142                        O outHyp = hypothesis.getTransitionOutput(hypTrans);
143                        wbIn.add(in);
144                        wbOut.add(outSul);
145
146                        // ce?
147                        if (!outSul.equals(outHyp)) {
148                                DefaultQuery<I, Word<O>> ce = new DefaultQuery<>(wbIn.toWord());
149                                ce.answer(wbOut.toWord());
150                                return ce;
151                        }
152                        cur = hypothesis.getSuccessor(cur, in);
153                }
154
155                return null;
156        }
157}