Skip to content

Regression in DetermineEquivalenceTest::findSeparatingWord affecting AutomataLib 0.12.0 but not 0.11.0 #88

@pfg666

Description

@pfg666

Bug Description
net.automatalib.util.automaton.equivalence.DeterministicEquivalenceTest::findSeparatingWord generates an exception when given certain non-equivalent DFAs . This exception only happens in AutomataLib 0.12.0 and not in AutomataLib 0.11.0.

To Reproduce
I uploaded a ZIP archive containing a Java Main class, two DOT automata, plus Maven boilerplate that can be used reproduce the bug. The Main class simply parses the DOT automata into CompactDFAs, which it supplies to findSeparatingWord. Instead of returning a separating word, the method throws the exception below.

Exception in thread "main" java.lang.ArrayIndexOutOfBoundsException: Index 99 out of bounds for length 11
	at net.automatalib.util.automaton.equivalence.DeterministicEquivalenceTest$ArrayRegistry.putPred(DeterministicEquivalenceTest.java:212)
	at net.automatalib.util.automaton.equivalence.DeterministicEquivalenceTest.findSeparatingWord(DeterministicEquivalenceTest.java:79)
	at findseparatingwordbug.Main.main(Main.java:30)

If you run this same code with AutomataLib 0.11.0 (after making the necessary adjustments to package paths), you will get a correct separating sequence.

Desktop (please complete the following information):

  • OS: Windows, Ubuntu
  • Java version: 17, 21
  • AutomataLib version: 0.12.0

Context
We discovered this as we attempted to port StateMachineBugFinder to the latest version of AutomataLib. We make extensive use of findSeparatingWord.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions