Full changelog

Fixed

• Updated links to the JUNG documentation.
• Updated dead links to the FSM format (see #87).
• Fixed a bug in the index computation of DeterministicEquivalenceTest (see #88).

Full changelog

Added

• AutomataLib now supports JPMS modules. Many of the artifacts now provide a module-info descriptor with the exception of automata-brics and automata-jung-visualizer which do not have modular dependencies and only provide an Automatic-Module-Name in their respective MANIFEST.MFs. As a consequence of this, the distribution artifacts (for Maven-less environments) also only provide an Automatic-Module-Name. Note that while this is a Java 9+ feature, AutomataLib still supports Java 8 byte code for the remaining class files.
• Added TabakovVardiRandomAutomata that allows for creating Tabakov-Vardi random automata, in particular, NFAs (thanks to @jn1z).
• Added (de-) serializers for the BA format supported by tools such as SPOT, RABIT, Walnut, etc. (thanks to @jn1z).
• Added Valmari's algorithm for solving the coarsest relational partition problem in O(m + log n). This includes utility classes such as ValmariInitializers and ValmariExtractors for, e.g., convenient quotienting of NFAs via bi-similarity (thanks to @mtf90).

Changed

• The JPMS support introduces several changes:
  • You now require at least a JDK 11 to build AutomataLib.
  • We use modules to better structure the aggregated JavaDoc. Since there exist breaking changes between Java 8 and Java 9 regarding documentation (see package-list vs. element-list), you can no longer link against the AutomataLib documentation on JDK 8 builds.
  • Split packages had to be refactored. This mainly concerns code from the automata-core artifact whose packages have been extended by a .impl suffix. This somewhat reverts the refactorings of the previous release (sorry for the back and forth) but since it only affects import statements, it should be fairly easy to address with IDE automation.
• The Alphabets#toGrowingAlphabetOrThrowException method has been moved to Alphabet#asGrowingAlphabetOrThrowException so that one does not require an automata-core dependency for a simple cast.
• The AutomatonBuilderImpl#withStateProperty method has had its parameter order flipped.
• The AWUtil class has been moved from net.automatalib.common.util.array to net.automatalib.common.smartcollection (in the automata-commons-smartcollections artifact).
• The ArrayStorage and ArrayUtil classes have been moved from net.automatalib.common.smartcollection to net.automatalib.common.util.array (in the automata-commons-util artifact).
• CollectionsUtil#allTuples has been moved to IterableUtil#allTuples.
• CollectionsUtil#cartesianProduct has been moved to IterableUtil#cartesianProduct.
• CollectionsUtil has been renamed to CollectionUtil.
• The DirectPowersetDTS class has been renamed to PowersetView.
• The FormatException is now a checked exception because we can reasonably expect clients to recover from this error. Furthermore, all parsing-related code has been aligned to use the FormatException instead of leaking implementation details (such as the ParseExceptions generated by JavaCC).
• The MutableGraph class has been aligned with its MutableAutomaton counterpart in that we no longer force nullable edge properties (see removed section). Furthermore the graph implementations have been renamed accordingly:
  • {,Abstract}Compact{,Bidi}Graph has been renamed to {,Abstract}CompactUniversal{,Bidi}Graph.
  • CompactGraph now is a graph with void node properties and edge properties, i.e., it only stores adjacency information.
• OneSEVPAMinimizer has been moved from net.automatalib.util.minimizer to net.automatalib.util.automaton.minimizer.
• The PaigeTarjanMinimization class (including all supporting classes such as PaigeTarjanInitializers) has been removed because, despite its name, the class never implemented Paige-Tarjan's algorithm for solving the relational coarsest partition problem but the functional one instead. Most of the previous functionality has been migrated to the (now correctly named) HopcroftMinimizer class.
• The serializers have been overhauled to allow for better integration of custom automaton types (especially when parsing). Some of the changes introduce new factory methods which may require some refactoring but the previous functionality is still available. As a part of this streamlining, many parsers no longer automatically un-compress or buffer the input streams to reduce overhead. The need for this can be determined best where the streams are created (in user-land).
• The RecursiveADSNode#{get,set}HypothesisState methods have been renamed to RecursiveADSNode#{get,set}State. Furthermore, getState() and getSymbol() no longer return null but throw an UnsupportedOperationException in case of an illegal access.
• The ResizingArrayStorage class has been merged with ArrayStorage.
• The SimpleMapGraph class no longer implements ShrinkableGraph since it cannot correctly implement createDynamicNodeMapping().
• The Visualization factory has been moved from the automata-core artifact to the automata-api artifact. Furthermore, the previous DummyVP has been replaced with a NoopVP that does not show a swing window anymore when no proper VisualizationProvider is configured but instead logs an error message. This allows us to drop the java.desktop (module) dependency for headless setups and only require it in actual visualizers (DOT, JUNG, etc.).
• AutomataLib's settings have been carved out in a separate automata-commons-settings module.
• The net:automatalib.tooling:automata-build-tools module has been renamed to net.automatalib:automata-build-config.

Removed

• The BlockAutomaton has been removed from Béal-Crochemore's minimization algorithm. The class never was a full automaton (in the AutomataLib sense) and could not become one without access to the original automaton at which point the transformations are the same as already implemented in the Automata class.
• The method Covers#incrementalStructuralCover has been removed because it is not possible to correctly compute the set without a distinction between state cover and transition cover elements. Users may use Covers#incrementalCover instead.
• The method DeterministicEquivalenceTest#findSeparatingWordLarge has been removed. The normal findSeparatingWord method now correctly adapts to various sizes.
• The methods xor, impl, equiv, and combine of NFAs have been removed since the product automaton constructions do not correspond to the respective language operations.
• The method MutableGraph#connect(N source, N target) has been removed. If you want to explicitly set a null property, you may denote your edge property type as @Nullable and use connect(N source, N target, EP property) accordingly. The same goes for MutableGraph's IntAbstraction.
• SimpleTS#getSuccessors(S state, Iterable<? extends I> input) has been removed. In order to traverse a (non-deterministic) transition system, use TransitionSystem#powersetView instead.
• TAFParseDiagnosticListener has been removed. Reporting is now done via (slf4j) logging.
• The net.automatalib:automata-serialization-core artifact has been dropped. Its contents are now part of the net.automatalib:automata-api artifact.

Fixed

• Fixed a bug in SBAs#toCFMPS which would allow the returned view to reach a final node on a non-return symbol.
• Fixed (another) inconsistency bug in Incremental*DAGBuilders.
• The AUTParser now correctly reads non-deterministic automata.
• The TAFParsers now correctly support wildcard transition definitions for DFAs.

Full changelog

Added

• Added the incremental AdaptiveMealyBuilder that allows for overriding previous traces (#56, thanks to @tiferrei).
• Added modal transition systems (MTSs) including related utilities such as composition, conjunction, refinement (thanks to @mjasper, @Conturing, and @dvs23).
• Added the M3C model-checker for verifying µ-calculus and CTL formulas on context-free modal process systems (thanks to @AlnisM).
• Added the ability to M3C to generate witnesses for negated safety properties (thanks to @Viperish-byte).
• Added support for procedural systems (SPAs, SBA, SPMMs) as well as related concepts such as verification, testing, and transformations thereof (thanks to @mtf90).
• Added SubsequentialTransducer interface and implementations/utilities (thanks to @mtf90).

Changed

• Refactorings

  • Many AutomataLib packages have been refactored from plural-based keywords to singular-based keywords. Some examples are

    • renamed net.automatalib.automata.* to net.automatalib.automaton.*.
    • renamed net.automatalib.automata.concepts.* to net.automatalib.automaton.concept.*.
    • renamed net.automatalib.automata.graphs.* to net.automatalib.automaton.graph.*.
    • renamed net.automatalib.automata.helpers.* to net.automatalib.automaton.helper.*.
    • renamed net.automatalib.automata.transducers.* to net.automatalib.automaton.transducer.*.
    • renamed net.automatalib.graphs.* to net.automatalib.graph.*.
    • renamed net.automatalib.graph.concepts.* to net.automatalib.graph.concept.*.
    • renamed net.automatalib.graph.helpers.* to net.automatalib.graph.helper.*.
    • renamed net.automatalib.ts.acceptors.* to net.automatalib.ts.acceptor.*.
    • renamed net.automatalib.settignssources.* to net.automatalib.settingsource.*.
    • renamed net.automatalib.words.* to net.automatalib.word.*.
    • renamed net.automatalib.commons.smartcollections.* to net.automatalib.common.smartcollection.*.
    • renamed net.automatalib.commons.util.* to net.automatalib.common.util.*.
    • renamed net.automatalib.modelcheckers.* to net.automatalib.modelchecker.*.
    • renamed net.automatalib.util.automata.* to net.automatalib.util.automaton.*.
    • etc.

    While this may cause some refactoring, it should only affect import statements as the names of most classes remain identical.

  • Some actual re-namings concern

    • all code around visibly push-down automata which now uses the "vpa" acronym (previously "vpda"). This includes package names, class names and (Maven) module names.
    • many of the automata-core packages have been aligned with their corresponding automata-api ones which often results in dropping the .impl or .compact sub-packages.
    • Alphabet-related code which has been moved from the net.automatlib.word package to the net.automatalib.alphabet package.
    • net.automatalib.automata.transducers.impl.compact.CompactMealyTransition -> net.automatalib.automaton.CompactTransition.
    • net.automatalib.commons.util.BitSetIterator -> net.automatalib.common.util.collection.BitSetIterator.
    • net.automatalib.graphs.base.compact.AbstractCompactGraph#getNodeProperties(int) -> net.automatalib.graph.base.AbstractCompactGraph#getNodeProperty(int).
    • net.automatalib.graphs.FiniteKTS -> net.automatalib.ts.FiniteKTS and FiniteKTS no longer extends the Graph interface but the Automaton interface and has its type variables re-ordered.
    • net.automatalib.graphs.FiniteLTS -> net.automatalib.graph.FiniteLabeledGraph.
    • GraphTraversal#dfIterator -> GraphTraversal#depthFirstIterator.
    • moved the net.automatalib.incremental.mealy.dynamic.* classes to net.automatalib.incremental.mealy.
    • moved the net.automatalib.settingssource.* classes to net.automatalib.
    • moved SupportsGrowingAlphabet class to net.automatalib.alphabet.
    • moved the package net.automatalib.ts.comp to net.automatalib.util.ts.comp in the automata-util module.
    • moved TS#bfs{Order,Iterator} to TSTraversal#breadthFirst{Order,Iterator}.
• AbstractOneSEVPA no longer implements the Graph interface, but SEVPAs are now GraphViewable.
• The automata-dot-visualizer module has been refactored and many Swing-related classes have been made package-private. The DOT class is now the central factory class to access the functionality of the module. The previous DOTFrame (whose functionality is now accessible via, e.g., DOT#renderDOTStrings) is now based on a JDialog which offers blocking modal semantics (e.g., for debugging purposes).
• The {Deterministc,NearLinear}EquivalenceTest classes have become factories that cannot be instantiated anymore and only offer static methods.
• Graph's adjacentTarget{,Iterator} (and related) methods have been renamed to getAdjacentNodes{,Iterator}.
• Many classes of the automata-incremental artifact have been cleaned up to no longer expose internal classes in public interfaces.
• The Indefinite{,Simple}Graph classes no longer have Collection-based getters but Iterable-based ones since indefinite structures typically cannot specify sizes. The Collection-based getters are delegated to the Graph class.
• Minimizer no longer provides a getInstance() method but can be instantiated directly.
• The OneSEVPA interface has been generalized to an arbitrary (k-)SEVPA interface. The old OneSEVPA specialization is still available and unchanged.
• The OneSEVPAUtils class has been merged into the OneSEVPAs class.
• The RandomUtil class has been made a factory (non-instantiable, only static methods) and its methods now require the random object as first parameter.
• AutomataLib classes no longer implement Serializable. We never fully supported the semantics of the interface and never intended to do so. In fact, the old approach failed miserably if any class was involved where we missed an "implements Serializable" statement. In order to prevent confusion by promising false contracts, implementing this markup interface has been removed. Serialization should now be done in user-land via one of the many external (and more optimizable) serialization frameworks such as FST, XStream, etc.
• ShortestPaths now offers fewer but less confusing methods. Previously there were methods such as shortestPath that took an initial node and multiple target nodes which much better fits to the idea of computing shortestPath*s* rather than any shortest path to one of the target nodes. The old behavior can still be replicated with the generic Predicate-based versions.
• StrictPriorityQueue is now package-private as it is only meant for internal use.
• Symbol now has a type-safe user object and id-based hashcode/equals semantics.

Removed

• Removed the (package-private) classes net.automatalib.util.automata.predicates.{AcceptanceStatePredicate,OutputSatisfies,TransitionPropertySatisfies}.
• Removed the IndefiniteSimpleGraph#asNormalGraph() method. Existing code should not need the transformation.
• Removed AbstractCompactNPGraph, use AbstractCompactGraph instead.
• Removed AbstractCompactSimpleGraph. All functionality is provided in CompactSimpleGraph.
• Removed CmpUtil#safeComparator. Use Comparators#nullsFirst or Comparators#nullsLast instead.
• Removed DelegateVisualizationHelper without replacement. Instead, directly override/extend the VisualizationHelper you want to delegate to.
• Removed the DFS-specific DFSTraversalVisitor (and related classes) without replacement. Client-code that relied on this class can re-implement the functionality by providing an own implementation of the more general GraphTraversalVisitor. See the changes on the DFSExample for reference.
• Removed (unused) DisjointSetForestInt class without replacement.
• Removed non-static methods on RandomAutomata factory (including the getInstance() method).
• Removed net.automatalib.graphs.IndefiniteLTS.java. By naming, this class should denote a TransitionSystem and not a Graph structure. However, since TransitionSystems are inherently labeled, this class serves no more real purpose. To re-establish the previous functionality, simply implement Graph and EdgeLabels.
• The Stream-based getters of Indefinite{,Simple}Graph have been removed in favor of the Iterator-based ones.
• Removed (unused) SuffixTrie class without replacement. Similar functionality can be achieved with AutomataLib's incremental module.
• The automata-dot-visualizer module has been refactored and many Swing-related classes have been made package-private. The DOT class is now the central factory class to access the functionality of the module. The previous DOTFrame (whose functionality is now accessible via, e.g., DOT#renderDOTStrings) is now based on a JDialog which offers blocking modal semantics (e.g., for debugging purposes).

Fixed

• Fixed a regression in AbstractLTSminMonitorMealy regarding BBC (#46).
• Fixed a bug in CharacterizingSets which ignored the semantics of acceptors, i.e., not all states of an acceptor could be distinguished solely based on acceptance.
• Fixed a bug in Covers#transitionCoverIterator which previously included undefined transitions.
• Fixed a cache consistency bug in various DAG-based incremental builders.

New Contributors

• @AlnisM made their first contribution in #47
• @tiferrei made their first contribution in #50
• @ericcccsliu made their first contribution in #52
• @MokonaNico made their first contribution in https://github.com/LearnLib/automatalib/pull...

Full changelog

Added

• All de-serializers now can also parse GZIP'ed contents from either InputStreams, Files, URLs or byte[]s.

Changed

• We overhauled the handling of input and output streams for all (de-)serializers. Input and output streams are no longer closed automatically. This is to prevent asymmetric code where we would close a stream that we haven't opened. This is problematic in cases where e.g. System.out is passed as an output stream to simply print a serialized automaton and the System.out stream would be closed afterwards. Since input and output streams are usually opened in client-code, they should be closed in client-code as well. We suggest to simply wrap calls to the serializers in a try-with-resource block.
• Due to the DOT parsers rewrite (see Fixed), the attribute parsers now receive a Map<String, String> instead of a Map<String, Object>.
• The State class (used by the OneSEVPA automaton) not longer supports the notion of a sink state. The AbstractOneSEVPA class now conforms with the default semantics of a DeterministicTransitionSystem that undefined transitions simply return null.

Removed

• Removed IOUtil#copy, IOUtil#skip, NullOutputStream. Use the Guava equivalents from ByteStreams and CharStreams.

Fixed

• Correctly enquote outputs containing whitespaces in TAFWriter (#37, thanks to @aschieweck)
• Fixed a bug in the Graph representation of AbstractOneSEVPAs (#39, thanks to @DonatoClun)
• Fixed wrong default values in the overloaded methods of the Minimizer class (#41).
• Replaced the 3rd-party DOT parser with our own implementation to fix the issue that multi-edges between nodes were not properly handled.

Full changelog

Added

• A new alphabet implementation MapAlphabet that is based on the old SimpleAlphabet but without implementing the GrowingAlphabet interface.
• IntRangeIterator now implements PrimitiveIterator.OfInt.
• A parser for dot files has been added and is available in the automata-serialization-dot module via the DOTParsers factory.
• A new PaigeTarjanMinimization factory that offers convenience methods for PaigeTarjan-based automata minimization (with support for e.g. partial automata) has been added.
• Performance improvements for some alphabet implementations (DefaultVPDAlphabet, ListAlphabet, {Int,Char}Range, ...).
• An LTSminLTLParser to verify if LTL properties match the expected syntax of LTSmin.
• A WordCollector for collecting words from symbol Streams.

Changed

• Refactored the following packages/classes:
  • net.automatalib.words.impl.SimpleAlphabet -> net.automatalib.words.impl.GrowingMapAlphabet
  • net.automatalib.serialization.AutomatonSerializationException -> net.automatalib.serialization.FormatException
  • net.automatalib.serialization.fsm.parser.FSMParseException -> net.automatalib.serialization.fsm.parser.FSMFormatException
  • net.automatalib.serialization.taf.parser.TAFParseException -> net.automatalib.serialization.taf.parser.TAFFormatException
  • net.automatalib.automata.transducers.impl.map.SimpleMapGraph -> net.automatalib.graphs.map.SimpleMapGraph
• The BackedGeneralPriorityQueue(Class<T> c) constructor was replaced with a more idiomatic BackedGeneralPriorityQueue(Supplier<T> s) constructor.
• The TAF serialization code now forwards (i.e. throws) IOExceptions that occur when reading from the various data sources.
• JSR305 annotations have been replaced with checker-framework annotations.
  • AutomataLib now follows checker-framework's convention that (non-annotated) types are usually considered non-null unless explicitly annotated with @Nullable.
  • AutomataLib no longer has a (runtime-) dependency on JSR305 (and other javax.*) annotations or includes them in the distribution artifact. This now makes AutomataLib compliant with Oracle's binary code license and allows AutomataLib artifacts as-is to be bundled in binary distributions with Oracle's JDKs/JREs.

Removed

• StringIndexGenerator has been removed. Its (streamlined) functionality is now available as Mapping via Mappings#stringToIndex and Mappings#indexToString.
• DelegatingIterator: If you used this class, switch to Guavas equivalent ForwardingIterator.
• ParameterMismatchException: Was unused and never thrown.
• StateIDDynamicMapping: Equivalent functionality is provided by ArrayMapping.
• ResizingIntArray: Internal data structure was unused.
• The VPDAlphabet interface no longer specifies the get{Internal,Call,Return}Symbols() methods, as the get{Internal,Call,Return}Alphabet() methods supersede their functionality.
• PaigeTarjan{Initializers,Extractors} methods for non IntAbstractions have been removed. You may use the new convenience methods provided by PaigeTarjanMinimization.
• Further @Deprecated methods have been removed.
• Removed ProbMealyTransition and replaced it with the generic MealyTransition directly carrying the ProbabilisticOutput. It is no longer allowed to pass null as transition property.
• Removed OutputAndLocalInputs, StateLocalInputIncrementalMealyTreeBuilder and StateLocalInputMealyUtil. The (LearnLib) code related to inferring partial Mealy machines no longer requires these transformed automata. Whoever used this code for transforming a partial Mealy machine to a complete one, may use MealyMachines#complete instead.

Fixed

• Fixed a bug, where the PaigeTarjan-based minimization would return a wrong automaton when pruning was enabled and the initial automaton was partial.
• Fixed a bug in our Tarjan SCC implementation (#35, thanks to Malte Mues)
• Fixed a bug in the computation of characterizing sets (#36).
• Several (null-related) bugs detected by our ongoing efforts to write tests.

Full changelog

Added

• Added support for model checking automata using the LTSmin model checker (thanks to Jeroen Meijer).
• Added a CompactMoore implementation.
• Added an AutomatonBuilder for Moore Machines.
• Added support for adding input symbols to incremental constructions (tree caches, DAG caches).
• Support for Java 11. Note: AutomataLib still targets Java 8, and thus needs classes provided by this environment (specifically: annotations from javax.annotation). If you plan to use AutomataLib in a Java 11+ environment, make sure to provide these classes. They are not shipped with AutomataLib.

Changed

• Refactored the following packages/classes:
  • net.automatalib.automata.transout -> net.automatalib.automata.transducers
  • net.automatalib.ts.transout -> net.automatalib.ts.output
  • net.automatalib.util.automata.transout -> net.automatalib.util.automata.transducers
  • net.automatalib.automata.GrowableAlphabetAutomaton -> net.automatalib.SupportsGrowingAlphabet
• Some runtime properties for dynamically configuring AutomataLib have been renamed. There now exists the AutomataLibProperty enum as a single reference point for all available properties.
• Several of the AbstractCompact* automata classes have been refactored to share common functionality. While this shouldn't affect its implementations (such as CompactDFA or CompactMealy) user-land code using the abstract classes may break.
• The BricsDFA wrapper previously allowed (via a boolean flag) to trigger determinization of the BRICS automaton. This determinization is now performed automatically if necessary. Instead the boolean flag now triggers a totalization of the transition function, which allows to properly use BricsDFAs in structural equivalence tests (as BRICS automata do not allow to limit their input alphabet to certain characters).
• Adding new symbols to automata (via the SupportsGrowingAlphabet interface) now requires the automaton to be initialized with a GrowingAlphabet instance. This is to make sure that the user has full control over which alphabet instance should be used instead of AutomataLib making decisions on behalf of the user.

Removed

• The mutable Pair class has been removed. The previously immutable pair class IPair has been renamed to Pair.
• Some utility classes and functions (especially from the automata-common-util package) have been removed without replacement, since equivalent functionality is provided by the Google Guava library we depend on. If you used any of this code, switch to the Guava equivalent.
• RichArray has been removed. At least regarding storage, ArrayStorage can be used as a replacement.
• SymbolHidingAlphabet has been removed without replacement. Changes to the logic of adding new input symbols should no longer make this class necessary.

Fixed

• Serializers now use platform dependent newlines. This shouldn't affect deserialization code.
• Several bugs detected by our ongoing efforts to write tests.

Full changelog

Added

• Added SymbolHidingAlphabet, which is required for a bugfix release of LearnLib.

Fixed

• Fixed an issue where initial states were not copied in copy-constructor of NFAs.
• Fixed an NPE when traversing partially defined NFAs.
• Fixed an issue, where input alphabets were unnecessarily wrapped in SimpleAlphabets in compact automata implementations.
• Fixed an out-of-bounds error in incremental automata builders.
• Fixed an error in Paige/Tarjan algorithm for partially defined automata.
• Fixed wrong computation of strongly connected components (see #21).
• General consolidations (typos, wrong documentation, etc.).

Full changelog

Added

• Added algorithms for computing adaptive distinguishing sequences for Mealy machines.
• Added support for adding alphabet symbols after initial automaton construction.
• Added support for Visibly Push-Down Automata (VPDA) in form of 1-SEVPAs.
• Added (de-)serializers for the AUT format (see #14).
• Added lazy (iterator based) methods for computing state- and transition covers, W-Method and Wp-Method tests.
• Added a serializer for the SAF format.

Changed

• Refactored the Maven artifact and Java package structure. Have a look at the List of AutomataLib Artifacts for an updated overview of available artifacts. In general, no functionality should have been removed (except of code marked with @Deprecated). The easiest way to migrate your code to the new version is probably by using the Auto-Import feature of your IDE of choice.

  The non-trivial refactorings include:

  • API methods no longer use wildcards in generic return parameters. This allows your code to not having to deal with them.
  • The visualization facade has been generified. Any getGraphDOTHelper() related code has been renamed to the more general getVisualizationHelper() terminology. The Visualization class now works by providing either the automata-dot-visualizer or automata-jung-visualizer JAR at runtime. This allows for potentially more visualizers in the future.

• Replaced System.out logging, with calls to an SLF4j facade.

• Code improvements due to employment of several static code-analysis plugins (findbugs, checkstyle, PMD, etc.) as well as setting up continuous integration at Travis CI.

Removed

• Several classes and methods annotated with @Deprecated.

Fixed

• Several bugs detected either by our newly employed static code-analysis toolchain or by our ongoing efforts to write tests.