A small example for learning a very basic TurtleBot system

TurtleBotExample.java

package de.learnlib.examples;

import de.learnlib.algorithms.ttt.mealy.TTTLearnerMealyBuilder;
import de.learnlib.api.SUL;
import de.learnlib.api.algorithm.LearningAlgorithm.MealyLearner;
import de.learnlib.api.exception.SULException;
import de.learnlib.api.oracle.EquivalenceOracle.MealyEquivalenceOracle;
import de.learnlib.api.oracle.MembershipOracle.MealyMembershipOracle;
import de.learnlib.api.query.DefaultQuery;
import de.learnlib.examples.TurtleBotExample.TurtleSUL.Input;
import de.learnlib.oracle.equivalence.WpMethodEQOracle.MealyWpMethodEQOracle;
import de.learnlib.oracle.membership.SULOracle;
import net.automatalib.automata.transout.MealyMachine;
import net.automatalib.visualization.Visualization;
import net.automatalib.words.Alphabet;
import net.automatalib.words.Word;
import net.automatalib.words.impl.Alphabets;

public class TurtleBotExample {

    public static void main(String[] args) {

        /*
        Define the input alphabet. The membership oracle needs to be able to answer queries over Sigma*. Since our
        oracle will effectively delegate all queries to our TurtleSUL, just use all inputs, that the TurtleSUL
        understands.
         */
        final Alphabet<Input> sigma = Alphabets.fromEnum(Input.class);

        // Setup the membership oracle to answer queries from the learner
        final MealyMembershipOracle<Input, Boolean> mqOracle = new SULOracle<>(new TurtleSUL());

        // Setup the learner. We choose the (compared to L*) more incremental TTT algorithm.
        final MealyLearner<Input, Boolean> ttt =
                new TTTLearnerMealyBuilder<Input, Boolean>().withAlphabet(sigma) // input alphabet
                                                            .withOracle(mqOracle) // membership oracle
                                                            .create();

        // Setup the EQ oracle. Since we already know an upper bound for the number of states, just use the Wp-method.
        final MealyEquivalenceOracle<Input, Boolean> eqOracle = new MealyWpMethodEQOracle<>(mqOracle, 5);

        // Trigger the initial hypothesis construction.
        ttt.startLearning();

        // Let's look at the initial hypothesis.
        MealyMachine<?, Input, ?, Boolean> hyp = ttt.getHypothesisModel();
        System.out.println("Displaying initial hypothesis");
        Visualization.visualize(hyp.transitionGraphView(sigma));

        // Let's see if we find counterexamples and are able to refine the hypothesis.
        DefaultQuery<Input, Word<Boolean>> ce;
        while ((ce = eqOracle.findCounterExample(hyp, sigma)) != null) {
            System.out.println("Found counterexample " + ce);
            ttt.refineHypothesis(ce);

            hyp = ttt.getHypothesisModel();
            System.out.println("Showing new hypothesis");
            Visualization.visualize(hyp.transitionGraphView(sigma));
        }

        System.out.println("No more counterexamples found");
    }

    static class TurtleSUL implements SUL<TurtleSUL.Input, Boolean> {

        enum Input {
            NORTH,
            EAST,
            SOUTH,
            WEST
        }

        enum State {
            P0,
            P1,
            P2,
            P3,
            P4
        }

        private State internalState = State.P0;

        @Override
        public void pre() {
            // we 'reset' our SUL during the pre-phase to ensure independence of runs.
            internalState = State.P0;
        }

        @Override
        public void post() {}

        @Override
        public Boolean step(Input in) throws SULException {
            // comply to the transition semantics of https://groups.google.com/group/learnlib-qa/attach/13f72691c2bba/Position%20Map%20-%20Turtlesim.PNG?part=0.1&view=1
            switch (in) {
                case NORTH:
                    switch (internalState) {
                        case P1:
                        case P2:
                        case P4:
                            return false;
                        case P0:
                            internalState = State.P1;
                            return true;
                        case P3:
                            internalState = State.P0;
                            return true;
                    }
                case EAST:
                    switch (internalState) {
                        case P1:
                        case P4:
                        case P3:
                            return false;
                        case P2:
                            internalState = State.P0;
                            return true;
                        case P0:
                            internalState = State.P4;
                            return true;
                    }
                case SOUTH:
                    switch (internalState) {
                        case P2:
                        case P3:
                        case P4:
                            return false;
                        case P1:
                            internalState = State.P0;
                            return true;
                        case P0:
                            internalState = State.P3;
                            return true;
                    }
                case WEST:
                    switch (internalState) {
                        case P1:
                        case P2:
                        case P3:
                            return false;
                        case P0:
                            internalState = State.P2;
                            return true;
                        case P4:
                            internalState = State.P0;
                            return true;
                    }
                default:
                    throw new IllegalArgumentException("Unknown input " + in);
            }
        }
    }
}