Skip to content

automatalib-0.11.0

Latest
Latest
Compare
Choose a tag to compare
@mtf90 mtf90 released this 06 Nov 12:16
· 50 commits to develop since this release
automatalib-0.11.0
62bbfcc

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

Contributors

MasWag, dvs23, and 9 other contributors
Assets 2