LearnLib / automatalib

A free, open-source Java library for modeling automata, graphs, and transition systems
http://automatalib.net
Apache License 2.0
92 stars 34 forks source link

Incorrect characterizing set for Mealy machine #36

Closed tmaarse closed 4 years ago

tmaarse commented 4 years ago

When running CharacterizingSets.findCharacterizingSet it finds {[a], [a, a]} as characterizing set for the following automaton: image However, these words do not characterize states 1 and 2. Note that even a distinguishing sequence exists: [a, a, b, a, a].

I used the following code to generate the image and the characterizing set using the latest version available on Maven (0.8.0), as I did not see commits since then related to this issue.

import java.util.ArrayList;
import java.util.Arrays;

import net.automatalib.util.automata.builders.AutomatonBuilders;
import net.automatalib.util.automata.equivalence.CharacterizingSets;
import net.automatalib.visualization.Visualization;
import net.automatalib.words.Alphabet;
import net.automatalib.words.Word;
import net.automatalib.words.impl.SimpleAlphabet;

public class Main {
    public static void main(String[] args) {
        Alphabet<String> inputs = new SimpleAlphabet<>();
        inputs.addAll(Arrays.asList("a", "b"));

        var machine = AutomatonBuilders.newMealy(inputs)
                .withInitial("0")
                .from("0")
                    .on("a").withOutput("a").to("1")
                    .on("b").withOutput("b").to("0")
                .from("1")
                    .on("a").withOutput("b").to("2")
                    .on("b").withOutput("b").to("3")
                .from("2")
                    .on("a").withOutput("b").to("1")
                    .on("b").withOutput("b").to("0")
                .from("3")
                    .on("a").withOutput("a").to("0")
                    .on("b").withOutput("b").to("0")
                .create();

        Visualization.visualize(machine);

        var set = new ArrayList<Word<String>>();
        CharacterizingSets.findCharacterizingSet(machine, inputs, set);
        System.out.println("Found characterizing set:");
        set.forEach(a -> System.out.println(a.asList()));
    }
}

I presume I have made an error somewhere, but I have (tried to) check everything.

mtf90 commented 4 years ago

Hi Timo,

thanks for reporting this issue. This indeed looks like a bug in the latest release and is still present on the current development branch.

Unfortunately, our tests didn't properly check the characterizing property of the computed sequences. I have fixed the tests locally and things fail elsewhere, too. I'll look into it in the upcoming days.

tmaarse commented 4 years ago

@mtf90 thank you for the quick response and fix!

mtf90 commented 4 years ago

No worries. We are looking forward to our (at least) annual release some time around Febuary. So the fix should be publicly available in a timely fashion, if you are not too fond of using development versions.

Am Mi, 29.01.2020, 14:11 schrieb Timo Maarse:

@mtf90 thank you for the quick response and fix!

-- You are receiving this because you were mentioned. Reply to this email directly or view it on GitHub: https://github.com/LearnLib/automatalib/issues/36#issuecomment-579748529