How to include system state information in generated state nodes & customized modifications?

[tao2years]

I have been studying a custom class automaton by referring to java/de/learnlib/example/Example2.java. I would like to know if it is possible to include system state information in the generated state nodes.

For example, at a certain node, I would like to display the values of certain variables in the system. For instance, at the initial node, there are two variables A and B, and their values are false. After transitioning to another node, let's say A is true and B is false. Assuming that I can access the values of A and B in the system, how can I incorporate these values into the nodes?

In addition to my previous question, I would like to know which parts of my code can be modified. Specifically, I do not want to instrument a pre-defined class and instead, I want to simulate the interaction of inputs and outputs in a black-box system. How can I achieve this and incorporate the results into my algorithm/code?

Without a detailed documentation, I am unsure about how to make customized modifications and adaptations. Could you please provide guidance on how to achieve this?

Below is my code and the results:

package testLearnLib;

import de.learnlib.algorithms.lstar.mealy.ExtensibleLStarMealyBuilder;
import de.learnlib.api.SUL;
import de.learnlib.api.algorithm.LearningAlgorithm;
import de.learnlib.api.oracle.EquivalenceOracle;
import de.learnlib.api.statistic.StatisticSUL;
import de.learnlib.drivers.reflect.MethodInput;
import de.learnlib.drivers.reflect.MethodOutput;
import de.learnlib.drivers.reflect.SimplePOJOTestDriver;
import de.learnlib.filter.cache.sul.SULCaches;
import de.learnlib.filter.statistic.sul.ResetCounterSUL;
import de.learnlib.oracle.equivalence.mealy.RandomWalkEQOracle;
import de.learnlib.oracle.membership.SULOracle;
import de.learnlib.util.Experiment;
import de.learnlib.util.statistics.SimpleProfiler;
import net.automatalib.automata.transducers.MealyMachine;
import net.automatalib.serialization.dot.GraphDOT;
import net.automatalib.visualization.Visualization;
import net.automatalib.words.Word;

import java.io.IOException;
import java.lang.reflect.InvocationTargetException;
import java.lang.reflect.Method;
import java.util.ArrayList;
import java.util.List;
import java.util.Random;

public class CMExample {
    private static final double RESET_PROBABILITY = 0.05;
    private static final int MAX_STEPS = 10_000;
    private static final int RANDOM_SEED = 46_346_293;

    private CMExample() {}

    public static void main(String[] args) throws NoSuchMethodException, IOException {
        SimplePOJOTestDriver driver = new SimplePOJOTestDriver(CoffeeExample.class);
        // create learning alphabet
        Method mWater = CoffeeExample.class.getMethod("water");
        Method mPod = CoffeeExample.class.getMethod("pod");
        Method mButton = CoffeeExample.class.getMethod("button");
        Method mClean = CoffeeExample.class.getMethod("clean");

        // construct input alphabet
        MethodInput water = driver.addInput("water", mWater);
        MethodInput pod = driver.addInput("pod", mPod);
        MethodInput button = driver.addInput("button", mButton);
        MethodInput clean = driver.addInput("clean", mClean);

        // oracle for counting queries wraps sul
        StatisticSUL<MethodInput, MethodOutput> statisticSul =
                new ResetCounterSUL<>("membership queries", driver);

        SUL<MethodInput, MethodOutput> effectiveSul = statisticSul;
        // use caching in order to avoid duplicate queries
        effectiveSul = SULCaches.createCache(driver.getInputs(), effectiveSul);

        SULOracle<MethodInput, MethodOutput> mqOracle = new SULOracle<>(effectiveSul);

        // create initial set of suffixes
        List<Word<MethodInput>> suffixes = new ArrayList<>();
        suffixes.add(Word.fromSymbols(water));
        suffixes.add(Word.fromSymbols(pod));
        suffixes.add(Word.fromSymbols(button));
        suffixes.add(Word.fromSymbols(clean));

        // construct L* instance (almost classic Mealy version)
        // almost: we use words (Word<String>) in cells of the table
        // instead of single outputs.
        LearningAlgorithm.MealyLearner<MethodInput, MethodOutput> lstar =
                new ExtensibleLStarMealyBuilder<MethodInput, MethodOutput>().withAlphabet(driver.getInputs()) // input alphabet
                        .withOracle(mqOracle) // membership oracle
                        .withInitialSuffixes(suffixes) // initial suffixes
                        .create();


        // create random walks equivalence test
        EquivalenceOracle.MealyEquivalenceOracle<MethodInput, MethodOutput> randomWalks =
                new RandomWalkEQOracle<>(driver, // system under learning
                        RESET_PROBABILITY, // reset SUL w/ this probability before a step
                        MAX_STEPS, // max steps (overall)
                        false, // reset step count after counterexample
                        new Random(RANDOM_SEED) // make results reproducible
                );

        // construct a learning experiment from
        // the learning algorithm and the random walks test.
        // The experiment will execute the main loop of
        // active learning
        Experiment.MealyExperiment<MethodInput, MethodOutput> experiment =
                new Experiment.MealyExperiment<>(lstar, randomWalks, driver.getInputs());

        // turn on time profiling
        experiment.setProfile(true);

        // enable logging of models
        experiment.setLogModels(true);

        // run experiment
        experiment.run();

        // get learned model
        MealyMachine<?, MethodInput, ?, MethodOutput> result = experiment.getFinalHypothesis();

        // report results
        System.out.println("-------------------------------------------------------");

        // profiling
        SimpleProfiler.logResults();

        // learning statistics
        System.out.println(experiment.getRounds().getSummary());
        System.out.println(statisticSul.getStatisticalData().getSummary());

        // model statistics
        System.out.println("States: " + result.size());
        System.out.println("Sigma: " + driver.getInputs().size());

        // show model
        System.out.println();
        System.out.println("Model: ");

        GraphDOT.write(result, driver.getInputs(), System.out); // may throw IOException!
        Visualization.visualize(result, driver.getInputs());

        System.out.println("-------------------------------------------------------");
    }

    public static class CoffeeExample {
        private boolean waterReady;
        private boolean podReady;

        public CoffeeExample(){}

        public String water(){
            this.waterReady = true;
            return "*";
        }

        public String pod(){
            this.podReady = true;
            return "*";
        }

        public String button(){
            if (this.waterReady && this.podReady)
                return "OK";
            else
                return "Error";
        }

        public String clean(){
            this.podReady = false;
            this.waterReady = false;
            return "*";
        }
    }
}

Results:

Model: 
digraph g {
	s0 [shape="circle" label="0"];
	s1 [shape="circle" label="1"];
	s2 [shape="circle" label="2"];
	s3 [shape="circle" label="3"];
	s0 -> s3 [label="water[] / *"];
	s0 -> s1 [label="pod[] / *"];
	s0 -> s0 [label="button[] / Error"];
	s0 -> s0 [label="clean[] / *"];
	s1 -> s2 [label="water[] / *"];
	s1 -> s1 [label="pod[] / *"];
	s1 -> s1 [label="button[] / Error"];
	s1 -> s0 [label="clean[] / *"];
	s2 -> s2 [label="water[] / *"];
	s2 -> s2 [label="pod[] / *"];
	s2 -> s2 [label="button[] / OK"];
	s2 -> s0 [label="clean[] / *"];
	s3 -> s3 [label="water[] / *"];
	s3 -> s2 [label="pod[] / *"];
	s3 -> s3 [label="button[] / Error"];
	s3 -> s0 [label="clean[] / *"];

	__start0 [label="" shape="none" width="0" height="0"];
	__start0 -> s0;
}

Thank you for your assistance!

[mtf90]

To your first question: It sounds like a Moore machine would suite your scenario better than a Mealy machine. Your state outputs would then be of a more complex class (than, e.g., String). For example, Set<P> or List<P> where P denotes the type of your proposition variables.

A combined approach for general UniversalDeterministicAutomatons (with transition outputs and state outputs) is currently not provided by LearnLib. It should be possible to implemented it yourself, but you would have to implement some of the internal work of the algorithms as well (e.g., for L*, the management of the observation table and the hypothesis construction).

To your second question: The learning algorithms and (most of the) equivalence oracles only require a MembershipOracle to interact with the SUL. It is totally up to you how you implement it. In your example, you use the reflective POJO driver to construct a SUL and then wrap it in a SULOracle. As long as you can provide the "input to output" function, any implementation is fine. You should only be careful with the output semantics of the different automaton types, e.g., for Mealy machines n input symbol result in n output symbols, for Moore machines, n input symbols result in n+1 output symbols. You may also use the SingleQueryOracle interface for a simpler implementation.

[tao2years]

For the second question, I have known that I should provide an "input to output" function. However, I would like more specific guidance on how to implement it and which APIs in LearnLib should I use.

For example, I have implement a send() method to send instructions to the black-box system and a get() method to retrieve the results. I am wondering how to integrate these two methods with LearnLib's API to generate the target automaton. Is there any reference for demos? I couldn't figure out how to integrate it from the official examples.

[mtf90]

Just a small sketch of how it could be implemented:

public class TaoOracle implements SingleQueryOracle<I, Word<O>> {

    private SUL sul = ...;

    @Override
    public Word<O> answerQuery(Word<I> prefix, Word<I> suffix) {

        // transfer sul to its initial state
        sul.reset();

        // progress sul to the state reached by the prefix
        for (I i : prefix) {
            sul.send(i);
        }

        final WordBuilder<O> wb = new WordBuilder<>(suffix.length() + 1);

        // state output for the current state
        wb.append(sul.get());

        // collect subsequent suffix state-outputs
        for (I i : suffix) {
            sul.send(i);
            wb.append(sul.get());
        }

        return wb.toWord();
    }
}

If you want Mealy semantics, you may skip adding the current state output before the suffix-loop.

[tao2years]

After I implement the SingleQueryOracle, how can I integrate it with different learning algorithms, such as Lstar. I think I shoud replace the membership oracle, but I do not know how to implement the specific details.

[mtf90]

The SingleQueryOracle interface extends the MembershipOracle interface so you should be able to put your TaoOracle everywhere where a MembersipOracle is exptected.