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.MealyEquivalenceOracle; 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 MealyEquivalenceOracle<I,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 boolean first = true; 127 sul.pre(); 128 while (steps < maxSteps) { 129 130 // restart? 131 double restart = random.nextDouble(); 132 if (restart < restartProbability) { 133 if (first) { 134 first = false; 135 } 136 else { 137 sul.post(); 138 } 139 sul.pre(); 140 cur = hypothesis.getInitialState(); 141 wbIn.clear(); 142 wbOut.clear(); 143 } 144 145 // step 146 steps++; 147 I in = choices.get(random.nextInt(bound)); 148 O outSul = sul.step(in); 149 T hypTrans = hypothesis.getTransition(cur, in); 150 O outHyp = hypothesis.getTransitionOutput(hypTrans); 151 wbIn.add(in); 152 wbOut.add(outSul); 153 154 // ce? 155 if (!outSul.equals(outHyp)) { 156 DefaultQuery<I, Word<O>> ce = new DefaultQuery<>(wbIn.toWord()); 157 ce.answer(wbOut.toWord()); 158 sul.post(); 159 return ce; 160 } 161 cur = hypothesis.getSuccessor(cur, in); 162 } 163 sul.post(); 164 return null; 165 } 166}