automatalib-13.0.0

Full changelog

Added

• A new formalism for Mealy machines with local timers (MMLTs) including means for conformance testing and equivalence checking has been added (thanks to @pdev55).
• With the introduction of MMLTs which are finite-state systems structurally but infinite-state systems semantically, AutomataLib now more rigorously distinguishes between these two concepts by introducing (and at some points requiring) specific {Finite,}Semantics types. Both concepts are conveniently accessible via new RegularAutomaton types. For automaton types that are inherently finite-state (e.g., DFAs, MealyMachines, etc.), this should not require any refactoring.
• Added a new automata-serialization-mata module for serializing (explicit) NFAs in the .mata format as used by the mata library.
• automata-modelchecking-m3c now supports ARM-based macOS systems.
• automata-modelchecking-m3c can now be included in jlink images.
• Added KWay{State,Transition}CoverTestsIterators to automata-util as a new means for conformance testing.
• Added CollectionUtil#allCombintationsIterator and CollectionUtil#allPermutationsIterator for computing k-combinations and k-permutations.
• Added NFAs#canonize to canonize NFAs via Brzozowski's algorithm.
• Added a DOT parser for ContextFreeModalProcessSystems.
• For nondeterministic model types, DOTParsers now contains methods that accept an initial node prefix, in case the number of initial nodes is not known beforehand.

Changed

• AutomataLib shifted version numbers to more prominently communicate breaking changes with major versions.
• AutomataLib now requires Java 17 at runtime.
  • The following classes have been refactored to records:
    • BricsTransitionProperty
    • TransitionEdge{,.Property}
    • ProbabilisticOutput
    • LTSminVersion
  • The following class hierarchies have been made sealed:
    • CommonAttrs
    • CommonStyles
• SEVPAs have been adjusted to the new structure/semantics split, by now implementing UniversalAutomaton and DeterministicSemantics.
• AbstractDDSolver no longer implements the ModelChecker interface to prevent possible conflicts with how systems are managed (an AbstractDDSolver is inherently linked to a specific CFMPS instance, whereas a ModelChecker should handle arbitrary ones). Instead, obtain M3C-based model checkers via the new M3CChecker factory.
• IncrementalConstruction#asTransitionSystem now returns a finite automaton view. This is in line with #asGraph which already required a finite representation before.
• The IntAbstraction interfaces have been moved to their respective implementations in the net.automatalib.automaton.abstraction package.
• The ShrinkableAutomaton interface has been replaced with the Shrinkable concept.
• The compute{State,Suffix,}Output concepts from Det{Suffix,}OutputAutomaton have been lifted to infinite-state transition systems. As part of this refactoring, some inconsistencies have been addressed. Previously, for Word-output systems, computeSuffixOutput threw an UndefinedPropertyAccessException if the prefix traversed an undefined transition but not if the suffix did (here, the output would only be cut short). Now, both methods simply early-exit output computation. Furthermore, these changes also include the following renamings:
  • DetOutputAutomaton -> DeterministicOutputAutomaton
  • DetSuffixOutputAutomaton -> DeterministicSuffixOutputAutomaton
  • DeterministicOutputTS -> DeterministicTraceableTS
• ProcessUtil#invokeProcess now handles consumers for stdout and stderr separately.
• RandomAutomata#randomDeterministic has been renamed to RandomAutomata#randomRegularDeterministic.

Removed

• IOUtil#copy(Reader, Writer) has been removed. Use Reader#transferTo(Writer) instead.
• JVMUtil has been removed. Use Runtime.version().feature() for its previously (only) provided method.
• StackState#SINK has been removed as procedural systems now better handle undefined transitions.
• DFAs#minimize has been removed. Use HopcroftMinimizer#minimizeDFA instead.

Fixed

• SPAConverter.ConversionResult is now publicly accessible.

New Contributors

• @pdev55 made their first contribution in #96