learnlib/automatalib

A free, open-source Java library for modeling automata, graphs, and transition systems

AutomataLib

AutomataLib is a free, open source (Apache License, v2.0) Java library for modeling automata, graphs, and transition systems.

About

AutomataLib is developed at TU Dortmund University, Germany. Its original purpose is to serve as the automaton framework for the LearnLib automata learning library. However, it is completely independent of LearnLib and can be used for other projects as well.

AutomataLib supports modeling a variety of graph-based structures. Currently, it covers generic transition systems, Deterministic Finite Automata (DFAs) and Mealy machines as well as more advanced structures such as Modal Transition Systems (MTSs), Subsequential Transducers (SSTs), Visibly Pushdown Automata (VPAs) and Procedural Systems (SPAs, SBAs, SPMMs).

Models of AutomataLib can be (de-)serialized (from) to one of the various supported serialization formats and may be visualized using either the GraphViz or JUNG library. Furthermore, a plethora of graph-/automata-based algorithms is implemented, covering the following topics:

• graph theory (traversal, shortest paths, strongly-connected components)
• automata theory (equivalence, minimization)
• model-based testing (adaptive distinguishing sequences, W(p)Method, characterizing sets, state/transition covers)
• model verification (LTL checking (via LTSMin), CTL & µ-calculus checking (via M3C & ADDlib))

While we strive to deliver code at a high quality, please note that there exist parts of the library that still need thorough testing. Contributions -- whether it is in the form of new features, better documentation or tests -- are welcome.

Build Instructions

For simply using AutomataLib you may use the Maven artifacts which are available in the Maven Central repository. It is also possible to download a bundled distribution artifact if you want to use AutomataLib without Maven support. Note that AutomataLib requires Java 11 (or newer) to build but still supports Java 8 at runtime.

Building development versions

If you intend to use development versions of AutomataLib, you can either use the deployed SNAPSHOT artifacts from the continuous integration server (see Using Development Versions) or build them yourself. Simply clone the development branch of the repository

git clone -b develop --single-branch https://github.com/LearnLib/automatalib.git

and run a single mvn clean install. This will build all the required maven artifacts and will install them in your local Maven repository so that you can reference them in other projects.

If you plan to use a development version of AutomataLib in an environment where no Maven support is available, simply run mvn clean package -Pbundles. The respective JARs are then available under distribution/target/bundles.

Developing AutomataLib

For developing the code base of AutomataLib it is suggested to use one of the major Java IDEs which come with out-of-the-box Maven support.

• For IntelliJ IDEA:

  1. Select File -> New -> Project from existing sources and select the folder containing the development checkout.
  2. Choose "Import Project from external model", select "Maven" and click Create.

• For Eclipse:

  1. Note: AutomataLib uses annotation processing on several occasions throughout the build process. This is usually handled correctly by Maven, however, for Eclipse you need to install the m2e-apt-plugin and activate annotation processing afterward (see the LearnLib issue #32).
  2. Select File -> Import... and select "Existing Maven Projects".
  3. Select the folder containing the development checkout as the root directory and click Finish.

Documentation

• Maven Project Site: latest release | older versions
• API Documentation: latest release | older versions

Questions?

If you have any questions regarding the usage of AutomataLib or if you want to discuss new and exciting ideas for future contributions, feel free to use the Discussions page to get in touch with the AutomataLib community.

Maintainers

• Markus Frohme (2017 - )
• Malte Isberner (2013 - 2015)

automatalib's Issues

Javadoc missing

Hello. This wiki page says very assuredly "Here you will find the online Javadoc for AutomataLib", yet there you will not find the online Javadoc for AutomataLib!

Add support for Java 17 (LTS) to CI pipeline

With Java 17, we have a new LTS version of Java that should be tested continuously.

Substract current automaton size to Wp-method's maxDepth

I probably got it wrong, but after checking the original paper it seems that the "middle part" length is the difference between implementation's bound on number of states (m) and the current spec size (n), so when using Wp-method as equivalence query the maxDepth could be shrunk dynamically (by substracting the current automaton.size()). Right?

Right now the length is fixed idependently of the candidate automaton: https://github.com/LearnLib/automatalib/blob/master/util/src/main/java/net/automatalib/util/automata/conformance/WpMethodTestsIterator.java#L81

I just started looking at the code base, so I'm might be missing something. Should/Can I update the equivalence oracle inside my learning loop to reduce the max depth?

M3CParser fails when ID is a formula token

Describe the bug
When calling M3CParser#parse with a formula that uses a token as a symbol identifier, the parser fails with a net.automatalib.modelchecker.m3c.formula.parser.ParseException.

To Reproduce
Parsing any formula that uses a token as an ID, e.g.,

• <E>true
• <U>true
• <W>true
• <AF>true
• [mu]true
• etc.

Expected behavior
Formula should be parsed without any issues an actually interpret the token as a valid action label.

Desktop (please complete the following information):

• OS: Linux
• Java version: 11, 17, 21
• AutomataLib version: 0.11.0

Use UTF-8 in TAF serialization

Currently, the serialization module for the TAF format relies on the system encoding, when writing to/reading from files. This is mainly due to the generated javaCC parser used for deserialization, which either does not support selecting a specific encoding or is not yet configured to do so.

With this ticket, the encoding for both writing and reading files should be switched to UTF-8. This either means, the javaCC parser (or rather the generation of the parser) should be configured accordingly, or (worst case) switch to a parser (-generator) that supports setting file encodings.

This also includes remove the corresponding DM_DEFAULT_ENCODING rule in automatalib-findbugs-exclusions.xml, which originally found the issue.

PaigeTarjanMinimization.minimizeDFA does not guarantee minimal result

The following code snippet creates and then minimizes a simple DFA:

public static void main(String[] args) throws IOException {
	CompactDFA<String> dfa = new CompactDFA<>(new ArrayAlphabet<>("e1", "e2", "e3"));
	
	int s0 = dfa.addInitialState(true);
	int s1 = dfa.addState(false);
	int s2 = dfa.addState(false);
	
	dfa.addTransition(s0, "e1", s1);
	dfa.addTransition(s1, "e2", s2);
	dfa.addTransition(s2, "e3", s1);
	
	StringBuilder b = new StringBuilder();
	GraphDOT.write(dfa, dfa.getInputAlphabet(), b);
	
	CompactDFA<String> minimalDfa = PaigeTarjanMinimization.minimizeDFA(dfa);
	GraphDOT.write(minimalDfa, minimalDfa.getInputAlphabet(), b);
	
	System.out.println(b.toString());
}

Output:

digraph g {

	s0 [shape="doublecircle" label="0"];
	s1 [shape="circle" label="1"];
	s2 [shape="circle" label="2"];
	s0 -> s1 [label="e1"];
	s1 -> s2 [label="e2"];
	s2 -> s1 [label="e3"];

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

}
digraph g {

	s0 [shape="doublecircle" label="0"];
	s1 [shape="circle" label="1"];
	s0 -> s1 [label="e1"];
	s1 -> s1 [label="e2"];

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

}

However since dfa only accepts the empty string its minimal representation would only have one initial accepting state and no transitions. So the output of PaigeTarjanMinimization.minimizeDFA does not seem minimal.

CompactMealyTransition does not extend MealyTransition

Both CompactMealyTransition and MealyTransition have a successor and an output. But CompactMealyTransition does not extend MealyTransition, which means transitions can not be treated in a general way. I think CompactMealyTransition should extend MealyTransition. And maybe other transition classes can benefit from similar changes.

IndexOutOfBoundsException in IncrementalMealyDAGBuilder when input word is longer than output word

Describe the bug
When using automatalib, an IndexOutOfBoundsException occured when on inserting a pair in IncrementalMealyDAGBuilder.

To Reproduce

import net.automatalib.alphabet.Alphabet;
import net.automatalib.alphabet.ArrayAlphabet;
import net.automatalib.incremental.mealy.dag.IncrementalMealyDAGBuilder;
import net.automatalib.word.Word;

public class Debug {
    public static void main(String[] args) {
        Alphabet<Symbol> alphabet = new ArrayAlphabet<>(Symbol.A);
        IncrementalMealyDAGBuilder<Symbol, Symbol> dagBuilder = new IncrementalMealyDAGBuilder<>(alphabet);
        dagBuilder.insert(Word.fromSymbols(Symbol.A, Symbol.A), Word.fromSymbols(Symbol.A));
    }

    public enum Symbol {
        A
    }
}

Expected behavior
Inserting to work as expected without crashing.

Stack Trace

Exception in thread "main" java.lang.IndexOutOfBoundsException: 0
	at net.automatalib.word.EmptyWord.getSymbol(EmptyWord.java:60)
	at net.automatalib.incremental.mealy.dag.IncrementalMealyDAGBuilder.createSuffix(IncrementalMealyDAGBuilder.java:377)
	at net.automatalib.incremental.mealy.dag.IncrementalMealyDAGBuilder.insert(IncrementalMealyDAGBuilder.java:209)
	at Debug.main(Debug.java:13)

Desktop (please complete the following information):

• OS: Linux
• Java version: 11
• AutomataLib version: 0.11.0

Additional context
Originally, I was using automatalib through learnlib (with the issue occuring in SULCache), so I'm not totally sure to which project this issue belongs. However, I didn't find any documentation that this behavior is wanted over here.

Hide transitions in DOT output based on outputs

It should be possible to hide certain transitions from a DOT file, e.g. error branches.

How to minimize a chained mealy automata

Hi, I want to minimize the following mealy machine:

public static void main(String[] args) throws IOException {
    Alphabet<Character> alphabet = Alphabets.characters('a', 'b');
    CompactMealy<Character, Integer> mealy = AutomatonBuilders.<Character, Integer>newMealy(alphabet).withInitial(0)
                                                                            .from(0).on('a').withOutput(1).to(1)
                                                                            .from(1).on('b').withOutput(2).to(2)
                                                                            .from(2).on('a').withOutput(1).to(3).from(3).on('b').withOutput(2).to(4)
            .create();
    StringBuilder b = new StringBuilder();
    GraphDOT.write(mealy, mealy.getInputAlphabet(), b);
    System.out.println(b.toString());
    
}             

with dot graph:

digraph g {

        s0 [shape="circle" label="0"];
        s1 [shape="circle" label="1"];
        s2 [shape="circle" label="2"];
        s3 [shape="circle" label="3"];
        s4 [shape="circle" label="4"];
        s0 -> s1 [label="a / 1"];
        s1 -> s2 [label="b / 2"];
        s2 -> s3 [label="a / 1"];
        s3 -> s4 [label="b / 2"];

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

}

The expected minimized machine is:

digraph g {

        s0 [shape="circle" label="0"];
        s1 [shape="circle" label="1"];
        s0 -> s1 [label="a / 1"];
        s1 -> s0 [label="b / 2"];

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

}

How to achieve this? Thanks.

Make an automaton out of a AUT

Hello. Can I create an automaton from the AUT format explained here?
Thank you

CompactMoore

A compilation error occurred when we build install the automatalib. As described next:

Description	Resource	Path	Location	Type
Duplicate methods named addTransition with the parameters (S, I, T) and (S, I, T) are defined by the type MutableDeterministic<Integer,I,Integer,O,Void>	CompactMoore.java	/automata-core/src/main/java/net/automatalib/automata/transducers/impl/compact	line 24	Java Problem
Description	Resource	Path	Location	Type
Duplicate methods named fullIntAbstraction with the parameters (int, IntFunction<? extends I>) and (int, IntFunction<? extends I>) are defined by the type MutableDeterministic<Integer,I,Integer,O,Void>	CompactMoore.java	/automata-core/src/main/java/net/automatalib/automata/transducers/impl/compact	line 24	Java Problem
The compile enviroment is jdk1.8.

Has anyone encountered this problem?

bug in DAGIncrementalBuilder

In certain situations the DAGBuilder introduces loops into the data structure.

AUTParser only adds states with outgoing transitions

Given the following AUT input:

des(0,4,3)  
(0,input,1)
(0,output,2)
(1,input,2)
(1,output,0)

the current AUT parser creates a SimpleAutomaton with only two states, 0 and 1. State 2 is omitted.

In general, states with no outgoing transitions are ignored by the AUT parser—in InternalAutParser.java the following lines of code are responsible for adding states to the outputted automaton, but only states that correspond to keys in the transitionMap (i.e. states that have outgoing transitions) are iterated over.

final CompactNFA<I> result = new CompactNFA<>(alphabet, transitionMap.size());

for (int i = 0; i < transitionMap.size(); i++) {
    result.addState();
}

Write a parser for LTSmin formulae

Currently, any LTL formula used with LTSmin is directly passed to the binary as-is. Hence, any errors regarding a malformed expression result in a failed invocation of the executable.

We could provide better user feedback / input validation by writing a parser (e.g. by using javaCC and the LTSmin LTL grammar definition) that allows us and potential users to check a formula for syntactical correctness

Incorrect characterizing set for Mealy machine

When running CharacterizingSets.findCharacterizingSet it finds {[a], [a, a]} as characterizing set for the following automaton:

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.

TAF writer does not enquote outputs of mealy machines

Serializing a mealy machine with an output symbol like "Element Not Found" runs without error, but produces non parsable text.

Deviation in the BBC functionality between (at least) LearnLib 0.14.0 and 0.16.0

Due to the update of AbstractLTSminMonitorMealy in 75b1987, the behavior of the BBC functionality in LearnLib changed (at least) between 0.14.0 and 0.16.0. (Sorry, I have not tried 0.15.0) I believe that the previous behavior is the expected one.

Here is a concrete example to reproduce this deviation + a summary of the reason for the deviation in my understanding: https://github.com/MasWag/deviation-LearnLib-0.14.0-vs-0.16.0

Issues with IntRangeIterator

List list = CollectionsUtil.intRange(0, 10);

int iterationsViaList = 0;
for (int i=0; i<=list.size()-1; i++) {
iterationsViaList += 1;
}

int iterationsViaIterator = 0;
Iterator iterator = list.iterator(); // IntRangeIterator
while (iterator.hasNext()) {
iterationsViaIterator += 1;
iterator.next();
}

There seems to be an issue with ListRangeIterator. The for-loop runs through 10 elements but the iterator only over one element. This causes problems when persisting mealy machines and plotting them via dot (only one state will be redered / stored)...

Java Building ERROR

I cannot build this code in NetBeans.
the error infomation is:

net/automatalib/graphs/IndefiniteGraph.java:[45,25] method transform in class com.google.common.collect.Iterators cannot be applied to given types;
  required: java.util.Iterator<F>,com.google.common.base.Function<? super F,? extends T>
  found: java.util.Iterator<E>,this::getTarget
  reason: cannot infer type-variable(s) F,T
    (argument mismatch; invalid method reference
      incompatible types: ? super F cannot be converted to E)
1 error
-------------------------------------------------------------
------------------------------------------------------------------------
BUILD FAILURE
------------------------------------------------------------------------

How can I fix it?

Implement Register Automata

Implement support for register automata (as defined by Cassel et al.) and extensions (Register Mealy Machines etc.).
Required for LearnLib Issue #3

Write test cases

Create TestNG test cases

Sorry...

Sorry this is a SPAM issue since my account doesn't seen to work... please remove me...

Dot export issues with CompactMealy

Dot rendering of CompactMealy structures seems to malfunction on currently deployed snapshots. Demonstrator code:

@Test
public void testCompactMealyDotExport() throws IOException {

    Symbol in_a = new Symbol("a");
    Symbol in_b = new Symbol("b");
    Symbol in_c = new Symbol("c");
    Symbol in_d = new Symbol("d");

    String out_off = "off";
    String out_on = "on";

    Alphabet<Symbol> alphabet = new FastAlphabet<>(in_a, in_b, in_c, in_d);

    CompactMealy<Symbol, String> cm = new CompactMealy<>(alphabet);
    Integer cm_a = cm.addInitialState(), cm_b = cm.addState();

    cm.addTransition(cm_a, in_a, cm_a, out_off);
    cm.addTransition(cm_a, in_b, cm_a, out_off);
    cm.addTransition(cm_a, in_c, cm_b, out_on);
    cm.addTransition(cm_a, in_d, cm_b, out_on);

    cm.addTransition(cm_b, in_a, cm_b, out_on);
    cm.addTransition(cm_b, in_b, cm_a, out_off);
    cm.addTransition(cm_b, in_c, cm_b, out_on);
    cm.addTransition(cm_b, in_d, cm_b, out_on);


    System.out.println(cm.size());
    Writer w = DOT.createDotWriter(true);
    GraphDOT.write(cm, alphabet, w);
    w.close();

}

This code will produce the following output:

Expected, however, is following output (created by constructing the same automaton as FastMealy instance):

As can be observed, it appears that transitions to other states than the initial state will be omitted. Perhaps this is an issue happening when traversing the automaton?

Minimizer.minimize overload without start states is broken

Using this code:

import java.io.IOException;

import net.automatalib.automata.fsa.impl.FastDFA;
import net.automatalib.automata.fsa.impl.FastDFAState;
import net.automatalib.serialization.dot.GraphDOT;
import net.automatalib.util.minimizer.MinimizationResult;
import net.automatalib.util.minimizer.Minimizer;
import net.automatalib.words.impl.GrowingMapAlphabet;

public class MinimizerTest {
	public static void main(String[] args) throws IOException {
		GrowingMapAlphabet<String> alphabet = new GrowingMapAlphabet<>();
		alphabet.add("a");
		alphabet.add("b");
		FastDFA<String> dfa = new FastDFA<>(alphabet);
		dfa.addInitialState(false);
		FastDFAState stateAfterA = dfa.addState(true);
		FastDFAState stateAfterB = dfa.addState(true);
		dfa.setTransition(dfa.getInitialState(), "a", stateAfterA);
		dfa.setTransition(dfa.getInitialState(), "b", stateAfterB);

		StringBuilder b = new StringBuilder();
		GraphDOT.write(dfa, dfa.getInputAlphabet(), b);
		System.out.println(b.toString());

		MinimizationResult<FastDFAState, ?> rslt = Minimizer.minimize(dfa.transitionGraphView());
		System.out.println(rslt.getNumBlocks());
	}
}

Prints:

digraph g {

	s0 [shape="circle" label="s0"];
	s1 [shape="doublecircle" label="s1"];
	s2 [shape="doublecircle" label="s2"];
	s0 -> s1 [label="a"];
	s0 -> s2 [label="b"];

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

}

0

Obviously 0 blocks is wrong.

net.automatalib.util.minimizer.Minimizer.minimize(UniversalGraph<S, ?, ?, L>) uses an empty list to as 2nd argument for net.automatalib.util.minimizer.Minimizer.minimize(UniversalGraph<S, ?, ?, L>, Collection<? extends S>), which invokes net.automatalib.util.minimizer.Minimizer.performMinimization(UniversalGraph<S, ?, ?, L>, Collection<? extends S>), which invokes net.automatalib.util.minimizer.Minimizer.initialize(UniversalGraph<S, E, ?, L>, Collection<? extends S>) which initializes with 0 blocks, meaning minimization will also result in 0 blocks.

net.automatalib.util.minimizer.Minimizer.performMinimization(UniversalGraph<S, E, ?, L>) seems to have a similar issue.

I used AutomataLib 0.9 distribution. AutomataLib 0.7.1 did not have this issue.

NFA determinization

Add support for NFA determinization

Error testing serilaization-dot

Hi I faced the following error during a mvn clean install. The setup is JDK 1.8 on Windows 7 x64.

[INFO] -------------------------------------------------------
[INFO]  T E S T S
[INFO] -------------------------------------------------------
[INFO] Running net.automatalib.serialization.dot.DOTSerializationTest
SLF4J: Failed to load class "org.slf4j.impl.StaticLoggerBinder".
SLF4J: Defaulting to no-operation (NOP) logger implementation
SLF4J: See http://www.slf4j.org/codes.html#StaticLoggerBinder for further details.
[ERROR] Tests run: 2, Failures: 2, Errors: 0, Skipped: 0, Time elapsed: 0.648 s <<< FAILURE! - in net.automatalib.serialization.dot.DOTSerializationTest
[ERROR] testRegularExport(net.automatalib.serialization.dot.DOTSerializationTest)  Time elapsed: 0.087 s  <<< FAILURE!
java.lang.AssertionError:
expected [digraph g {

        s0 [shape="circle" label="0"];
        s1 [shape="circle" label="1"];
        s2 [shape="circle" label="2"];
        s0 -> s1 [label="a / 1"];
        s1 -> s2 [label="b / 2"];
        s2 -> s0 [label="c / 3"];

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

}
] but found [digraph g {

        s0 [shape="circle" label="0"];
        s1 [shape="circle" label="1"];
        s2 [shape="circle" label="2"];
        s0 -> s1 [label="a / 1"];
        s1 -> s2 [label="b / 2"];
        s2 -> s0 [label="c / 3"];

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

}
]
        at net.automatalib.serialization.dot.DOTSerializationTest.checkDOTOutput(DOTSerializationTest.java:96)
        at net.automatalib.serialization.dot.DOTSerializationTest.testRegularExport(DOTSerializationTest.java:59)

[ERROR] testVisualizationHelper(net.automatalib.serialization.dot.DOTSerializationTest)  Time elapsed: 0.014 s  <<< FAILURE!
java.lang.AssertionError:
expected [digraph g {
// this is a preamble

        s0 [shape="doublecircle" label="0"];
        s1 [shape="circle" label="1"];
        s2 [shape="doublecircle" label="2"];
        s3 [shape="circle" label="3"];
        s4 [shape="doublecircle" label="4"];
        s5 [shape="circle" label="5"];
        s6 [shape="doublecircle" label="6"];
        s7 [shape="circle" label="7"];
        s8 [shape="doublecircle" label="8"];
        s9 [shape="circle" label="9"];
        s10 [shape="doublecircle" label="10"];
        s0 -> s1 [color="red" label="null"];
        s1 -> s2 [color="red" label="null"];
        s2 -> s3 [color="red" label="null"];
        s3 -> s4 [color="red" label="null"];
        s4 -> s5 [color="red" label="null"];
        s5 -> s6 [color="red" label="null"];
        s6 -> s7 [color="red" label="null"];
        s7 -> s8 [color="red" label="null"];
        s8 -> s9 [color="red" label="null"];
        s9 -> s10 [color="red" label="null"];
        s10 -> s0 [color="red" label="null"];

// this is a postamble

}
] but found [digraph g {
// this is a preamble

        s0 [shape="doublecircle" label="0"];
        s1 [shape="circle" label="1"];
        s2 [shape="doublecircle" label="2"];
        s3 [shape="circle" label="3"];
        s4 [shape="doublecircle" label="4"];
        s5 [shape="circle" label="5"];
        s6 [shape="doublecircle" label="6"];
        s7 [shape="circle" label="7"];
        s8 [shape="doublecircle" label="8"];
        s9 [shape="circle" label="9"];
        s10 [shape="doublecircle" label="10"];
        s0 -> s1 [color="red" label="null"];
        s1 -> s2 [color="red" label="null"];
        s2 -> s3 [color="red" label="null"];
        s3 -> s4 [color="red" label="null"];
        s4 -> s5 [color="red" label="null"];
        s5 -> s6 [color="red" label="null"];
        s6 -> s7 [color="red" label="null"];
        s7 -> s8 [color="red" label="null"];
        s8 -> s9 [color="red" label="null"];
        s9 -> s10 [color="red" label="null"];
        s10 -> s0 [color="red" label="null"];

// this is a postamble

}
]
        at net.automatalib.serialization.dot.DOTSerializationTest.checkDOTOutput(DOTSerializationTest.java:96)
        at net.automatalib.serialization.dot.DOTSerializationTest.testVisualizationHelper(DOTSerializationTest.java:82)

[INFO]
[INFO] Results:
[INFO]
[ERROR] Failures:
[ERROR]   DOTSerializationTest.testRegularExport:59->checkDOTOutput:96 expected [digraph g {

        s0 [shape="circle" label="0"];
        s1 [shape="circle" label="1"];
        s2 [shape="circle" label="2"];
        s0 -> s1 [label="a / 1"];
        s1 -> s2 [label="b / 2"];
        s2 -> s0 [label="c / 3"];

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

}
] but found [digraph g {

        s0 [shape="circle" label="0"];
        s1 [shape="circle" label="1"];
        s2 [shape="circle" label="2"];
        s0 -> s1 [label="a / 1"];
        s1 -> s2 [label="b / 2"];
        s2 -> s0 [label="c / 3"];

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

}
]
[ERROR]   DOTSerializationTest.testVisualizationHelper:82->checkDOTOutput:96 expected [digraph g {
// this is a preamble

        s0 [shape="doublecircle" label="0"];
        s1 [shape="circle" label="1"];
        s2 [shape="doublecircle" label="2"];
        s3 [shape="circle" label="3"];
        s4 [shape="doublecircle" label="4"];
        s5 [shape="circle" label="5"];
        s6 [shape="doublecircle" label="6"];
        s7 [shape="circle" label="7"];
        s8 [shape="doublecircle" label="8"];
        s9 [shape="circle" label="9"];
        s10 [shape="doublecircle" label="10"];
        s0 -> s1 [color="red" label="null"];
        s1 -> s2 [color="red" label="null"];
        s2 -> s3 [color="red" label="null"];
        s3 -> s4 [color="red" label="null"];
        s4 -> s5 [color="red" label="null"];
        s5 -> s6 [color="red" label="null"];
        s6 -> s7 [color="red" label="null"];
        s7 -> s8 [color="red" label="null"];
        s8 -> s9 [color="red" label="null"];
        s9 -> s10 [color="red" label="null"];
        s10 -> s0 [color="red" label="null"];

// this is a postamble

}
] but found [digraph g {
// this is a preamble

        s0 [shape="doublecircle" label="0"];
        s1 [shape="circle" label="1"];
        s2 [shape="doublecircle" label="2"];
        s3 [shape="circle" label="3"];
        s4 [shape="doublecircle" label="4"];
        s5 [shape="circle" label="5"];
        s6 [shape="doublecircle" label="6"];
        s7 [shape="circle" label="7"];
        s8 [shape="doublecircle" label="8"];
        s9 [shape="circle" label="9"];
        s10 [shape="doublecircle" label="10"];
        s0 -> s1 [color="red" label="null"];
        s1 -> s2 [color="red" label="null"];
        s2 -> s3 [color="red" label="null"];
        s3 -> s4 [color="red" label="null"];
        s4 -> s5 [color="red" label="null"];
        s5 -> s6 [color="red" label="null"];
        s6 -> s7 [color="red" label="null"];
        s7 -> s8 [color="red" label="null"];
        s8 -> s9 [color="red" label="null"];
        s9 -> s10 [color="red" label="null"];
        s10 -> s0 [color="red" label="null"];

// this is a postamble

}
]
[INFO]
[ERROR] Tests run: 2, Failures: 2, Errors: 0, Skipped: 0
[INFO]
[INFO] ------------------------------------------------------------------------
[INFO] Reactor Summary:
[INFO]
[INFO] AutomataLib ........................................ SUCCESS [  1.144 s]
[INFO] AutomataLib :: Build Parent ........................ SUCCESS [  0.023 s]
[INFO] AutomataLib :: Commons ............................. SUCCESS [  0.031 s]
[INFO] AutomataLib :: Commons :: Utilities ................ SUCCESS [  6.547 s]
[INFO] AutomataLib :: API ................................. SUCCESS [  5.936 s]
[INFO] AutomataLib :: Adapters ............................ SUCCESS [  0.025 s]
[INFO] AutomataLib :: Adapters :: BRICS ................... SUCCESS [  2.485 s]
[INFO] AutomataLib :: Commons :: Smart Collections ........ SUCCESS [  1.834 s]
[INFO] AutomataLib :: Core ................................ SUCCESS [  7.390 s]
[INFO] AutomataLib :: Utilities ........................... SUCCESS [  8.460 s]
[INFO] AutomataLib :: Incremental ......................... SUCCESS [  2.516 s]
[INFO] AutomataLib :: Serialization ....................... SUCCESS [  0.035 s]
[INFO] AutomataLib :: Serialization :: ETF ................ SUCCESS [  1.877 s]
[INFO] AutomataLib :: Serialization :: FSM ................ SUCCESS [  1.912 s]
[INFO] AutomataLib :: Model Checking ...................... SUCCESS [  0.028 s]
[INFO] AutomataLib :: Model Checking :: LTSmin ............ SUCCESS [  2.445 s]
[INFO] AutomataLib :: Serialization :: Core ............... SUCCESS [  0.361 s]
[INFO] AutomataLib :: Serialization :: AUT ................ SUCCESS [  1.911 s]
[INFO] AutomataLib :: Serialization :: DOT ................ FAILURE [  1.707 s]
[INFO] AutomataLib :: Serialization :: LearnLibV2 ......... SKIPPED
[INFO] AutomataLib :: Serialization :: SAF ................ SKIPPED
[INFO] AutomataLib :: Serialization :: TAF ................ SKIPPED
[INFO] AutomataLib :: Visualization ....................... SKIPPED
[INFO] AutomataLib :: Visualization :: DOT Visualizer ..... SKIPPED
[INFO] AutomataLib :: Visualization :: JUNG Visualizer .... SKIPPED
[INFO] AutomataLib :: Distribution ........................ SKIPPED
[INFO] AutomataLib :: Archetypes .......................... SKIPPED
[INFO] AutomataLib :: Archetypes :: Basic ................. SKIPPED
[INFO] AutomataLib :: Archetypes :: Complete .............. SKIPPED
[INFO] AutomataLib :: Build Tools ......................... SKIPPED
[INFO] AutomataLib :: Examples ............................ SKIPPED
[INFO] ------------------------------------------------------------------------
[INFO] BUILD FAILURE
[INFO] ------------------------------------------------------------------------
[INFO] Total time: 47.118 s
[INFO] Finished at: 2018-07-10T13:54:30+02:00
[INFO] Final Memory: 54M/1028M
[INFO] ------------------------------------------------------------------------
[ERROR] Failed to execute goal org.apache.maven.plugins:maven-surefire-plugin:2.20:test (default-test) on project automata-serialization-dot: There are test failures.
[ERROR]
[ERROR] Please refer to C:\eclipse\workspace\automatalib\serialization\dot\target\surefire-reports for the individual test results.
[ERROR] Please refer to dump files (if any exist) [date]-jvmRun[N].dump, [date].dumpstream and [date]-jvmRun[N].dumpstream.
[ERROR] -> [Help 1]
[ERROR]
[ERROR] To see the full stack trace of the errors, re-run Maven with the -e switch.
[ERROR] Re-run Maven using the -X switch to enable full debug logging.
[ERROR]
[ERROR] For more information about the errors and possible solutions, please read the following articles:
[ERROR] [Help 1] http://cwiki.apache.org/confluence/display/MAVEN/MojoFailureException
[ERROR]
[ERROR] After correcting the problems, you can resume the build with the command
[ERROR]   mvn <goals> -rf :automata-serialization-dot

DOTParsers.mealy() not parsing all transitions

Hi there,

I was wondering if I could get some help with some behaviour that I am not understanding completely.

Consider the DOT file below that was created by GraphDOT.write() from a learned model:

digraph g {

	s0 [shape="circle" label="0"];
	s1 [shape="circle" label="1"];
	s2 [shape="circle" label="2"];
	s3 [shape="circle" label="3"];
	s4 [shape="circle" label="4"];
	s5 [shape="circle" label="5"];
	s6 [shape="circle" label="6"];
	s0 -> s0 [label="HANDSHAKE(0xff00001d)[ACK,CRYPTO] / EMPTY"];
	s0 -> s0 [label="INITIAL(0xff00001d)[ACK,PING] / INITIAL(0xff00001d)[ACK]"];
	s0 -> s1 [label="INITIAL(0xff00001d)[CRYPTO] / INITIAL(0xff00001d)[ACK,CRYPTO]+HANDSHAKE(0xff00001d)[CRYPTO]+HANDSHAKE(0xff00001d)[CRYPTO]"];
	s0 -> s0 [label="SHORT(0xff00001d)[ACK,STREAM] / EMPTY"];
	s1 -> s2 [label="HANDSHAKE(0xff00001d)[ACK,CRYPTO] / SHORT(0xff00001d)[STREAM]+SHORT(0xff00001d)[STREAM]+SHORT(0xff00001d)[HANDSHAKE_DONE,CRYPTO,STREAM]+HANDSHAKE(0xff00001d)[ACK]"];
	s1 -> s1 [label="INITIAL(0xff00001d)[ACK,PING] / INITIAL(0xff00001d)[ACK]"];
	s1 -> s3 [label="INITIAL(0xff00001d)[CRYPTO] / HANDSHAKE(0xff00001d)[CONNECTION_CLOSE]"];
	s1 -> s6 [label="SHORT(0xff00001d)[ACK,STREAM] / EMPTY"];
	s2 -> s3 [label="HANDSHAKE(0xff00001d)[ACK,CRYPTO] / SHORT(0xff00001d)[CONNECTION_CLOSE]"];
	s2 -> s2 [label="INITIAL(0xff00001d)[ACK,PING] / EMPTY"];
	s2 -> s2 [label="INITIAL(0xff00001d)[CRYPTO] / EMPTY"];
	s2 -> s4 [label="SHORT(0xff00001d)[ACK,STREAM] / SHORT(0xff00001d)[ACK]"];
	s3 -> s3 [label="HANDSHAKE(0xff00001d)[ACK,CRYPTO] / EMPTY"];
	s3 -> s3 [label="INITIAL(0xff00001d)[ACK,PING] / EMPTY"];
	s3 -> s3 [label="INITIAL(0xff00001d)[CRYPTO] / EMPTY"];
	s3 -> s3 [label="SHORT(0xff00001d)[ACK,STREAM] / EMPTY"];
	s4 -> s4 [label="HANDSHAKE(0xff00001d)[ACK,CRYPTO] / EMPTY"];
	s4 -> s4 [label="INITIAL(0xff00001d)[ACK,PING] / EMPTY"];
	s4 -> s4 [label="INITIAL(0xff00001d)[CRYPTO] / EMPTY"];
	s4 -> s4 [label="SHORT(0xff00001d)[ACK,STREAM] / SHORT(0xff00001d)[ACK,STREAM]"];
	s5 -> s3 [label="HANDSHAKE(0xff00001d)[ACK,CRYPTO] / SHORT(0xff00001d)[CONNECTION_CLOSE]"];
	s5 -> s5 [label="INITIAL(0xff00001d)[ACK,PING] / EMPTY"];
	s5 -> s5 [label="INITIAL(0xff00001d)[CRYPTO] / EMPTY"];
	s5 -> s4 [label="SHORT(0xff00001d)[ACK,STREAM] / SHORT(0xff00001d)[ACK,STREAM]"];
	s6 -> s5 [label="HANDSHAKE(0xff00001d)[ACK,CRYPTO] / SHORT(0xff00001d)[STREAM]+SHORT(0xff00001d)[STREAM]+SHORT(0xff00001d)[HANDSHAKE_DONE,CRYPTO,STREAM]+HANDSHAKE(0xff00001d)[ACK]"];
	s6 -> s6 [label="INITIAL(0xff00001d)[ACK,PING] / INITIAL(0xff00001d)[ACK]"];
	s6 -> s3 [label="INITIAL(0xff00001d)[CRYPTO] / HANDSHAKE(0xff00001d)[CONNECTION_CLOSE]"];
	s6 -> s6 [label="SHORT(0xff00001d)[ACK,STREAM] / EMPTY"];

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

}

If we read and then write it again using the following code:

package util.learnlib;

import net.automatalib.automata.transducers.impl.compact.CompactMealy;
import net.automatalib.serialization.InputModelData;
import net.automatalib.serialization.InputModelDeserializer;
import net.automatalib.serialization.dot.DOTParsers;
import net.automatalib.serialization.dot.GraphDOT;

import java.io.BufferedWriter;
import java.io.File;
import java.io.FileWriter;
import java.io.IOException;

public class Test {
	private static String DOT_IN = "input.dot";
	private static String DOT_OUT = "output.dot";

	public static CompactMealy<String, String> readFile(String filename) throws IOException {
		File file = new File(filename);
		InputModelDeserializer<String, CompactMealy<String,String>> parser = DOTParsers.mealy();
		InputModelData<String, CompactMealy<String, String>> machine = parser.readModel(file);
		return machine.model;
	}

	private static <I> void saveToFile(String filename, CompactMealy<String, String> model) {
		try (BufferedWriter out = new BufferedWriter(new FileWriter(filename))) {
			GraphDOT.write(model, model.getInputAlphabet(), out);
		} catch (IOException exception) {
			exception.printStackTrace();
		}
	}

	public static void main(String[] args) throws IOException {
		CompactMealy<String, String> mealyMachine = readFile(DOT_IN);
		saveToFile(DOT_OUT, mealyMachine);
	}
}

We get the following output:

digraph g {

	s0 [shape="circle" label="0"];
	s1 [shape="circle" label="1"];
	s2 [shape="circle" label="2"];
	s3 [shape="circle" label="3"];
	s4 [shape="circle" label="4"];
	s5 [shape="circle" label="5"];
	s6 [shape="circle" label="6"];
	s0 -> s0 [label="SHORT(0xff00001d)[ACK,STREAM] / EMPTY"];
	s0 -> s1 [label="INITIAL(0xff00001d)[CRYPTO] / INITIAL(0xff00001d)[ACK,CRYPTO]+HANDSHAKE(0xff00001d)[CRYPTO]+HANDSHAKE(0xff00001d)[CRYPTO]"];
	s1 -> s6 [label="SHORT(0xff00001d)[ACK,STREAM] / EMPTY"];
	s1 -> s2 [label="HANDSHAKE(0xff00001d)[ACK,CRYPTO] / SHORT(0xff00001d)[STREAM]+SHORT(0xff00001d)[STREAM]+SHORT(0xff00001d)[HANDSHAKE_DONE,CRYPTO,STREAM]+HANDSHAKE(0xff00001d)[ACK]"];
	s1 -> s1 [label="INITIAL(0xff00001d)[ACK,PING] / INITIAL(0xff00001d)[ACK]"];
	s1 -> s3 [label="INITIAL(0xff00001d)[CRYPTO] / HANDSHAKE(0xff00001d)[CONNECTION_CLOSE]"];
	s2 -> s4 [label="SHORT(0xff00001d)[ACK,STREAM] / SHORT(0xff00001d)[ACK]"];
	s2 -> s3 [label="HANDSHAKE(0xff00001d)[ACK,CRYPTO] / SHORT(0xff00001d)[CONNECTION_CLOSE]"];
	s2 -> s2 [label="INITIAL(0xff00001d)[CRYPTO] / EMPTY"];
	s3 -> s3 [label="SHORT(0xff00001d)[ACK,STREAM] / EMPTY"];
	s4 -> s4 [label="SHORT(0xff00001d)[ACK,STREAM] / SHORT(0xff00001d)[ACK,STREAM]"];
	s5 -> s4 [label="SHORT(0xff00001d)[ACK,STREAM] / SHORT(0xff00001d)[ACK,STREAM]"];
	s5 -> s3 [label="HANDSHAKE(0xff00001d)[ACK,CRYPTO] / SHORT(0xff00001d)[CONNECTION_CLOSE]"];
	s5 -> s5 [label="INITIAL(0xff00001d)[CRYPTO] / EMPTY"];
	s6 -> s6 [label="SHORT(0xff00001d)[ACK,STREAM] / EMPTY"];
	s6 -> s5 [label="HANDSHAKE(0xff00001d)[ACK,CRYPTO] / SHORT(0xff00001d)[STREAM]+SHORT(0xff00001d)[STREAM]+SHORT(0xff00001d)[HANDSHAKE_DONE,CRYPTO,STREAM]+HANDSHAKE(0xff00001d)[ACK]"];
	s6 -> s3 [label="INITIAL(0xff00001d)[CRYPTO] / HANDSHAKE(0xff00001d)[CONNECTION_CLOSE]"];

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

}

As you can see, some transitions seem to be missing. Am I doing something wrong?

Thank you for your help,
Tiago

Add support for lazy test-sequence generations

Currently many methods for generating test sequences (such as characterizing sets or transition covers) are computed in bulk operations. With this ticket, support for a lazy computation of these sequences (by means of an Itera{ble,tor}) should be added.

This would allow for a better performance in cases with large target automata. Also, this would nicely integrate with the lazy equivalence oracles of LearnLib, which have been added in LearnLib/learnlib@0bd5d78c (and they should be updated too, once this is implemented).

Currently, the following sequences can be computed and therefore need a lazyfied version

• State cover
  • normal version
  • incremental version
• Transition cover
  • normal version
  • incremental version
• CharacterizingSet
  • normal version
  • incremental version

Graphviz DOT output

Since the models learnlib infers are AFAIK always some kind of automaton, the DOT output should look like an automaton. Here is an example how this could be realized:

digraph DFA {
  node [shape=circle,width=0.35,height=0.35,fixedsize=true]
  edge [arrowhead=vee]

  q0 [label=<q<SUB>0</SUB>>];
  q0 -> q1[label=AUI,penwidth=4,color=red]
  q0 -> q2[label=UDI]
  q1 [label=<q<SUB>1</SUB>>];
  q1 -> q3[label=SR,penwidth=4,color=red]
  q1 -> q4[label=UDI]
  q2 [label=<q<SUB>2</SUB>>];
  q2 -> q4[label=AUI]
  q3 [label=<q<SUB>3</SUB>>];
  q3 -> q5[label=UDI]
  q4 [label=<q<SUB>4</SUB>>];
  q4 -> q5[label=SR]
  q5 [label=<q<SUB>5</SUB>>,shape=doublecircle];
}

Bug in the strongly connected component algorithm

Due to incorrect backtracking on the stack, wrong components are put together using TarjanSCCVisitor.

The initial bug triggering example was the following graph:

nodes: a,b,c,d,e

edges:
a -> b
b -> c
b -> e
c -> d
d -> b

I expected the following three sccs: {a}, {b,c,d} {e}, but got {a}, {b, e}, {c, d}.

Replace JSR305 annotations

JSR305 contains javax annotations that have never officially been approved/published by the JSR group, thus shipping them with AutomataLib violates against Oracle's binary code license:

F. JAVA TECHNOLOGY RESTRICTIONS. You may not create, modify, or change the behavior of, or authorize your licensees to create, modify, or change the behavior of, classes, interfaces, or subpackages that are in any way identified as "java", "javax", "sun", “oracle” or similar convention as specified by Oracle in any naming convention designation.

This prevents end-users from bundling AutomataLib in binary releases with Oracle JVMs. We should replace them with an alternative.

Some candidates may be the checker framework or the upcoming SpotBugs 4.0.0's own set of annotations.

This ticket also depends on misberner/duzzt#6, since on newer JREs, the user is required to provide @javax.annotation.Generated which suffers from the same problem.

Fail on javadoc warnings and improve documentation

We should use the automated detection capabilities of the javadoc-plugin and fail the build whenever the documentation is inconsistent (missing tags, etc.). This would of course first require to fix all existing inconsistencies.

Renaming COPYING.txt to LICENSE

To clean up the licensing of the project, I would recommend you rename this file.

M3C does not run on M1 MacBooks

Java 17 and Maven 3.9.5
There is issue while installing the automatalib --> mvn clean install