How to find the Equivalence queries

[VishalPatel43]

package com.experiment;

import com.experiment.dfas.DFAOperation;
import de.learnlib.algorithms.lstar.dfa.ClassicLStarDFA;
import de.learnlib.algorithms.lstar.dfa.ClassicLStarDFABuilder;

import de.learnlib.api.oracle.MembershipOracle.DFAMembershipOracle;

import de.learnlib.datastructure.observationtable.writer.ObservationTableASCIIWriter;

import de.learnlib.filter.statistic.oracle.DFACounterOracle;
import de.learnlib.oracle.equivalence.DFAWMethodEQOracle;
import de.learnlib.oracle.membership.SimulatorOracle.DFASimulatorOracle;
import de.learnlib.util.Experiment.DFAExperiment;
import de.learnlib.util.statistics.SimpleProfiler;
import net.automatalib.automata.fsa.DFA;
import net.automatalib.automata.fsa.impl.compact.CompactDFA;
import net.automatalib.serialization.dot.GraphDOT;
import net.automatalib.words.Alphabet;


import java.io.File;
import java.io.IOException;
import java.util.List;

public class LStarExperiment {

    private static final int EXPLORATION_DEPTH = 4;
    private static DFAOperation dfaOperation = new DFAOperation();

    public static void main(String[] args) throws IOException {

        // Folder containing serialized DFAs
        File dfasFolder = new File("random_dfas");
        // Load DFAs from the serialized file
        List<CompactDFA<Character>> loadedDFAs = dfaOperation.loadDFAsFromFile(new File(dfasFolder, "dfas.ser"));

        // Iterate over loaded DFAs and run L* on each
        for (int i = 0; i < loadedDFAs.size(); i++) {
            if (i == 1) break;
            CompactDFA<Character> currentDFA = loadedDFAs.get(i);

            System.out.println("Running L* on DFA " + (i + 1));
            runLStar(currentDFA);
        }
    }

    private static void runLStar(CompactDFA<Character> target) throws IOException {
        // Alphabet for the target DFA
//        Alphabet<Character> inputs = target.getInputAlphabet(); // make this function and re-use it

        Alphabet<Character> inputs = dfaOperation.getInputAlphabets(target);
        // Construct a simulator membership query oracle
        DFAMembershipOracle<Character> sul = new DFASimulatorOracle<>(target);
//        MembershipOracle<Character, Boolean> sul = new DFASimulatorOracle<>(target);


        // Oracle for counting queries wraps SUL
        DFACounterOracle<Character> mqOracle = new DFACounterOracle<>(sul, "membership queries");
//        CounterOracle<Character, Boolean> mqOracle = new CounterOracle<>(sul, "membership queries");

        // Construct L* instance
        ClassicLStarDFA<Character> lstar =
                new ClassicLStarDFABuilder<Character>().withAlphabet(inputs)
                        .withOracle(mqOracle)
                        .create();


        // Construct a W-method conformance test
        DFAWMethodEQOracle<Character> wMethod = new DFAWMethodEQOracle<>(mqOracle, EXPLORATION_DEPTH);

        // Construct a learning experiment
        DFAExperiment<Character> experiment = new DFAExperiment<>(lstar, wMethod, inputs);

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

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

        // Run the experiment
        experiment.run();

        // Get learned model
        DFA<?, Character> result = experiment.getFinalHypothesis();

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

        // Profiling
        System.out.println("Profiling Results:");
        System.out.println(SimpleProfiler.getResults());

        // Learning statistics
        System.out.println("Learning Statistics:");

        System.out.println(experiment.getRounds().getSummary());

        // membership queries
        System.out.println(mqOracle.getStatisticalData().getSummary());
//        System.out.println("Membership queries: A" + mqOracle.getCounter());
//        System.out.println("Membership queries: B" + mqOracle.getCount());


        // Model statistics
        System.out.println("Model Statistics:");
        System.out.println("States: " + result.size());
        System.out.println("Sigma: " + inputs.size());

        // Show model
        System.out.println("Learned Model:");
        GraphDOT.write(result, inputs, System.out);

        System.out.println("Final observation table:");
        new ObservationTableASCIIWriter<>().write(lstar.getObservationTable(), System.out);

        // also store the generated model in the list of DFA and store the reference and dot file
        // convert into dot file and pdf
        System.out.println("-------------------------------------------------------");
    }
}

package com.experiment;


import com.experiment.dfas.DFAOperation;
import com.google.common.collect.Lists;
import de.learnlib.algorithms.nlstar.NLStarLearner;
import de.learnlib.algorithms.nlstar.ObservationTable;

import de.learnlib.api.oracle.MembershipOracle;
import de.learnlib.filter.statistic.oracle.CounterOracle;
import de.learnlib.oracle.equivalence.SampleSetEQOracle;
import de.learnlib.oracle.membership.SimulatorOracle;
import de.learnlib.util.Experiment;;
import de.learnlib.util.statistics.SimpleProfiler;
import net.automatalib.automata.fsa.NFA;
import net.automatalib.automata.fsa.impl.compact.CompactDFA;

import net.automatalib.serialization.dot.GraphDOT;
import net.automatalib.util.automata.conformance.WMethodTestsIterator;

import net.automatalib.words.Alphabet;


import java.io.File;
import java.io.IOException;
import java.util.List;

public class NLStarExperiment {
    public static void main(String[] args) throws IOException {

        DFAOperation dfaOperation = new DFAOperation();

        // Folder containing serialized DFAs
        File dfasFolder = new File("random_dfas");
        // Load DFAs from the serialized file
        List<CompactDFA<Character>> loadedDFAs = dfaOperation.loadDFAsFromFile(new File(dfasFolder, "dfas.ser"));

        CompactDFA<Character> dfa = loadedDFAs.get(0);
        Alphabet<Character> alphabet = dfa.getInputAlphabet();


        final MembershipOracle<Character, Boolean> mqo = new SimulatorOracle<>(dfa);

//        final CounterOracle<Character, Boolean> lstarCounter = new CounterOracle<>(mqo, "membership queries");
        final CounterOracle<Character, Boolean> nlstarCounter = new CounterOracle<>(mqo, "membership queries");

//        final ClassicLStarDFA<Character> lstar = new ClassicLStarDFA<>(alphabet, lstarCounter);
        final NLStarLearner<Character> nlstar = new NLStarLearner<>(alphabet, nlstarCounter);


        // the challenge is to find an equivalence oracle that works for DFAs and NFAs
        // here, we simply use the W-method tests based on the determinized RegExp
        final SampleSetEQOracle<Character, Boolean> eqo = new SampleSetEQOracle<>(false);
        eqo.addAll(mqo, Lists.newArrayList(new WMethodTestsIterator<>(dfa, alphabet, 4)));

//        final Experiment<DFA<?, Character>> lstarExp = new Experiment<>(lstar, eqo, alphabet);
        final Experiment<NFA<?, Character>> nlstarExp = new Experiment<>(nlstar, eqo, alphabet);

        // Turn on time profiling
        nlstarExp.setProfile(true);

        // Enable logging of models
        nlstarExp.setLogModels(true);

//        lstarExp.run();
        nlstarExp.run();

//        System.out.println("LStar");
//        System.out.println(lstarCounter.getStatisticalData().getDetails());
        System.out.println("NLStar");
//        System.out.println(nlstarCounter.getStatisticalData().getDetails());

//        Visualization.visualize(lstarExp.getFinalHypothesis(), alphabet);
//        Visualization.visualize(nlstarExp.getFinalHypothesis(), alphabet);

        NFA<?, Character> result = nlstarExp.getFinalHypothesis();
        String dotFileName = "nfa_1" + ".dot";
        dfaOperation.generateDOTFileNFA(result, alphabet, dotFileName);
        dfaOperation.convertDotToPDF(dotFileName, "nfa_1" + ".pdf");
        // convert into dot file and pdf
        // more nfa then convert into the store in list of NFA and store the ref


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

        // Profiling
        System.out.println("Profiling Results:");
        System.out.println(SimpleProfiler.getResults());

        // Learning statistics
        System.out.println("Learning Statistics:");
        System.out.println(nlstarExp.getRounds().getSummary());
        // membership queries
        System.out.println(nlstarCounter.getStatisticalData().getSummary());
//        System.out.println("Membership queries: A" + mqOracle.getCounter());
//        System.out.println("Membership queries: B" + mqOracle.getCount());


        // Model statistics
        System.out.println("Model Statistics:");
        System.out.println("States: " + result.size());
        System.out.println("Sigma: " + alphabet.size());

        // Show model
        System.out.println("Learned Model:");
        GraphDOT.write(result, alphabet, System.out);

        System.out.println("Final observation table:");

        ObservationTable<Character> observationTable = nlstar.getObservationTable();

        // Print the final observation table

        // also store the generated model in the list of NFA and store the reference and dot file
        // convert into dot file and pdf
    }
}

package com.experiment.dfas;

import net.automatalib.automata.fsa.DFA;
import net.automatalib.automata.fsa.NFA;
import net.automatalib.automata.fsa.impl.compact.CompactDFA;
import net.automatalib.util.automata.equivalence.DeterministicEquivalenceTest;
import net.automatalib.util.automata.minimizer.hopcroft.HopcroftMinimization;
import net.automatalib.util.automata.random.RandomAutomata;
import net.automatalib.words.Alphabet;
import net.automatalib.words.Word;
import net.automatalib.words.impl.GrowingMapAlphabet;

import java.io.;
import java.util.;

public class DFAOperation {

// generate random DFA

// public CompactDFA generateRandomDFA() {
// // Define the alphabet
// Alphabet alphabet = new GrowingMapAlphabet<>();
//
// // Add symbols to the alphabet
// alphabet.add('a');
// alphabet.add('b');
//
// // Set the number of states and create a random DFA
// int numStates = 1000;
// Random random = new Random();
//// DFA<?, Character> randomDFA = RandomAutomata.randomDFA(random, numStates, alphabet);
// CompactDFA randomDFA = RandomAutomata.randomDFA(random, numStates, alphabet);
//
// // Generate DOT file
// String dotFileName = "randomDFA.dot";
// generateDOTFile(randomDFA, alphabet, dotFileName);
//
// return randomDFA;
// }

// generate random DFA

public CompactDFA<Character> generateRandomDFA() {
    // Define the alphabet
    Alphabet<Character> alphabet = new GrowingMapAlphabet<>();

    // Add symbols to the alphabet
    alphabet.add('a');
    alphabet.add('b');

    // Set the number of states randomly between 10 and 200

// int numStates = new Random().nextInt(191) + 10;
int numStates = 10;

    // Ensure there are at least 5 accepting states
    int numAcceptingStates = Math.max(5, new Random().nextInt(numStates));

    // Create a random set of accepting states
    Set<Integer> acceptingStates = new HashSet<>();
    Random random = new Random();
    while (acceptingStates.size() < numAcceptingStates) {
        acceptingStates.add(random.nextInt(numStates));
    }

    // Create a random DFA
    CompactDFA<Character> randomDFA = RandomAutomata.randomDFA(random, numStates, alphabet);

    // Set the accepting states
    acceptingStates.forEach(state -> randomDFA.setAccepting(state, true));

    // Generate DOT file

// String dotFileName = "randomDFA.dot";
// generateDOTFile(randomDFA, alphabet, dotFileName);

    return randomDFA;
}

public Alphabet<Character> getInputAlphabets(CompactDFA<Character> dfa) {
    return dfa.getInputAlphabet();
}

// minimize DFA
public CompactDFA<Character> minimizeDFA(CompactDFA<Character> dfa, Alphabet<Character> alphabet) {
    CompactDFA<Character> minimizedDFA = HopcroftMinimization.minimizeDFA(dfa, alphabet);
    return minimizedDFA;
}

// check equivalence dfa
public <I> String checkDFAEquivalenceString(DFA<?, I> dfa1, DFA<?, I> dfa2, Alphabet<I> alphabet) {
    // Create an instance of DeterministicEquivalenceTest
    DeterministicEquivalenceTest<I> equivalenceTest = new DeterministicEquivalenceTest<>(dfa1);

    // Check for equivalence and get a separating word
    Word<I> separatingWord = equivalenceTest.findSeparatingWord(dfa2, alphabet);

    if (separatingWord == null) {
        return "DFAs are equivalent";
    } else {
        return "DFAs are not equivalent. Separating word: " + separatingWord;
    }
}

// print dfa
public <S, I> void printDFA(DFA<S, I> dfa, Alphabet<I> alphabet) {
    System.out.println("Random DFA:");

    S initialState = dfa.getInitialState();

    for (S state : dfa.getStates()) {
        System.out.print("State " + state + ": ");

        // Mark the initial state
        if (state.equals(initialState)) {
            System.out.print("(Initial) ");
        }

        // Mark final states
        if (dfa.isAccepting(state)) {
            System.out.print("(Final) ");
        }

        for (I input : alphabet) {
            S successor = dfa.getSuccessor(state, input);
            System.out.print("(" + input + " -> " + successor + ") ");
        }
        System.out.println();
    }
}


// generate dot file
public <S, I> void generateDOTFileDFA(DFA<S, I> dfa, Alphabet<I> alphabet, String fileName) {
    try (PrintWriter writer = new PrintWriter(new FileWriter(fileName))) {
        writer.println("digraph RandomDFA {");

        // Add starting state
        writer.println("  __start0 [label=\"\", shape=none];");
        writer.println("  __start0 -> " + dfa.getInitialState() + " [label=\"\"];");

        for (S state : dfa.getStates()) {
            writer.print("  " + state);

            // Mark the initial state
            if (state.equals(dfa.getInitialState())) {
                writer.print(" [shape=circle]");
            }

            // Mark final states
            if (dfa.isAccepting(state)) {
                writer.print(" [shape=doublecircle]");
            }

            writer.println();

            for (I input : alphabet) {
                S successor = dfa.getSuccessor(state, input);
                writer.println("  " + state + " -> " + successor + " [label=\"" + input + "\"]");
            }
        }
        writer.println("}");
    } catch (IOException e) {
        e.printStackTrace();
    }
    System.out.println("DOT file generated: " + fileName);
}

// NFA to dot file
public <S, I> void generateDOTFileNFA(NFA<S, I> nfa, Alphabet<I> alphabet, String fileName) {
    try (PrintWriter writer = new PrintWriter(new FileWriter(fileName))) {
        writer.println("digraph RandomNFA {");

        // Add starting state
        writer.println("  __start0 [label=\"\", shape=none];");

        // Connect starting state to each initial state
        for (S initialState : nfa.getInitialStates()) {
            writer.println("  __start0 -> " + initialState + " [label=\"\"];");
        }

        for (S state : nfa.getStates()) {
            writer.print("  " + state);

            // Mark the initial states
            if (nfa.getInitialStates().contains(state)) {
                writer.print(" [shape=circle]");
            }

            // Mark final states
            if (nfa.isAccepting(state)) {
                writer.print(" [shape=doublecircle]");
            }

            writer.println();

            for (I input : alphabet) {
                for (S successor : nfa.getSuccessors(state, input)) {
                    writer.println("  " + state + " -> " + successor + " [label=\"" + input + "\"]");
                }
            }
        }
        writer.println("}");
    } catch (IOException e) {
        e.printStackTrace();
    }
    System.out.println("DOT file generated: " + fileName);
}


// convert dot to pdf
public void convertDotToPDF(String dotFileName, String pdfFileName) {
    try {
        ProcessBuilder processBuilder = new ProcessBuilder("dot", "-Tpdf", dotFileName, "-o", pdfFileName);
        Process process = processBuilder.start();
        process.waitFor();
        System.out.println("PDF file generated: " + pdfFileName);
    } catch (IOException | InterruptedException e) {
        e.printStackTrace();
    }
}

public void deletePreviousFiles(File folder) {
    File[] files = folder.listFiles();
    if (files != null) {
        for (File file : files) {
            if (!file.isDirectory()) {
                file.delete();
            }
        }
    }

    // Delete dfas.ser data
    File dataFile = new File(folder, "dfas.ser");
    dataFile.delete();
}

public void saveDFAsToFile(List<CompactDFA<Character>> dfas, File file) {
    try (ObjectOutputStream oos = new ObjectOutputStream(new FileOutputStream(file))) {
        oos.writeObject(dfas);
        System.out.println("DFAs saved to file: " + file);
    } catch (IOException e) {
        e.printStackTrace();
    }
}

public List<CompactDFA<Character>> loadDFAsFromFile(File file) {
    try (ObjectInputStream ois = new ObjectInputStream(new FileInputStream(file))) {
        return (List<CompactDFA<Character>>) ois.readObject();
    } catch (IOException | ClassNotFoundException e) {
        e.printStackTrace();
        return new ArrayList<>();
    }
}

}

4) 

package com.experiment;

import com.experiment.dfas.DFAOperation;
import net.automatalib.automata.fsa.impl.compact.CompactDFA;

import java.io.*;
import java.util.ArrayList;
import java.util.List;

public class Main {

// not print but save in the log file

public static void main(String[] args) {
    // Create a folder for random DFAs
    File dfasFolder = new File("random_dfas");

    // create the folder if it does not exist
    dfasFolder.mkdirs();

    // Set the number of DFAs to generate
    int numDFAs = 10;

    // Create a list to store the DFAs
    List<CompactDFA<Character>> dfaList = new ArrayList<>();
    DFAOperation dfaOperation = new DFAOperation();

    // Delete previous DOT files and dfas.ser data
    dfaOperation.deletePreviousFiles(dfasFolder);

    // Create and store random DFAs
    for (int i = 0; i < numDFAs; i++) {
        // Adjust the number of states as needed
        CompactDFA<Character> randomDFA = dfaOperation.generateRandomDFA();
        dfaList.add(randomDFA);

        // Save DOT files in folders named random_dfa_i
        String dotFileName = "random_dfas/random_dfa_" + (i + 1) + ".dot";
        dfaOperation.generateDOTFileDFA(randomDFA, randomDFA.getInputAlphabet(), dotFileName);
        dfaOperation.convertDotToPDF(dotFileName, "random_dfas/random_dfa_" + (i + 1) + ".pdf");
    }

    // Serialize and save DFAs to a file
    dfaOperation.saveDFAsToFile(dfaList, new File(dfasFolder, "dfas.ser"));

    // Later, you can load the DFAs from the file

// List<CompactDFA> loadedDFAs = dfaOperation.loadDFAsFromFile(new File(dfasFolder, "dfas.ser"));

    // check equivalence

// String answer = dfaOperation.checkDFAEquivalenceString(dfaList.get(1), loadedDFAs.get(0), loadedDFAs.get(0).getInputAlphabet());
// System.out.println(answer);

    // Now you can use the loaded DFAs as needed
}

}

[VishalPatel43]

Please how provide how to calcaulate the equivalence queries
Is it System.out.println(experiment.getRounds().getSummary());

There is issue while print the observation table of the nlstar
ObservationTable observationTable = nlstar.getObservationTable();

If you wanted I can provide the link of the my repo

[mtf90]

Yes, the Experiment#getRounds counter returns the number of equivalence queries. However, note that this also includes the final equivalence query which usually detects the equivalence and does not result in any refinement.

The issue with the NLStar ObservationTable probably is that it does not extend the de.learnlib.datastructure.observationtable.ObersvationTable interface which is needed by the ObservationTableASCIIWriter. This is because the NLStar OT differs in some few details which do not have a direct counterpart in the "regular" OT. We may have a look at this in the future. If you really need to visualize the NLStar OT in your benchmark (which I highly doubt), you may copy the ObservationTableASCIIWriter code and adjust it for the NLStar OT.

[mtf90]

Do you still need guidance, or can we mark this thread as resolved?