learnlib/automatalib

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

automatalib's Issues

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)...

Sorry...

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

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.

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.

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.

Renaming COPYING.txt to LICENSE

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

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.

NFA determinization

Add support for NFA determinization

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.

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();
}

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];
}

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?

IncrementalDAGBuilder fails for traces with cyclic repetitions longer than 2

Describe the bug
Inserting certain traces into an Incremental(Mealy)DAGBuilder throws a ConflictException.

To Reproduce

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

public class IncrementalMealyDAGError {

    public static void main(String[] args) {

        final Alphabet<Character> alphabet = Alphabets.characters('0', '3');

        final Word<Character> in1 = Word.fromString("12");
        final Word<Character> in2 = Word.fromString("302");
        final Word<Character> in3 = Word.fromString("3023102");
        final Word<Character> in4 = Word.fromString("30231023");

        final Word<Character> out1 = Word.fromString("21");
        final Word<Character> out2 = Word.fromString("101");
        final Word<Character> out3 = Word.fromString("1013201");
        final Word<Character> out4 = Word.fromString("10132010");

        final IncrementalMealyDAGBuilder<Character, Character> builder = new IncrementalMealyDAGBuilder<>(alphabet);

        builder.insert(in1, out1);
        builder.insert(in2, out2);
        builder.insert(in3, out3);
        builder.insert(in4, out4); // boom
    }
}

Expected behavior
No exception should be thrown.

Desktop (please complete the following information):

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

Additional context
This issue was originally reported as LearnLib/learnlib#126.

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

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!

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.

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.

M3C does not run on M1 MacBooks

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

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?

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?

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

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

Make an automaton out of a AUT

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

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

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.

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

Write test cases

Create TestNG test cases

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?

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

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}.

Hide transitions in DOT output based on outputs

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

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.

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

bug in DAGIncrementalBuilder

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

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.

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.