21.0.0

Strix 21 is the first release after the move to GitHub and corresponds to the version of Strix that participated in SYNTCOMP 2021.

Changed

• Complete rewrite of Strix in Rust.
• Use new LTL-to-DPA translation in Owl based on Zielonka split-trees and Alternating Cycle Decomposition (ACD).
• Output of controller as machine now uses the HOA format instead of KISS format.

Added

• Additional machine minimization better exploiting non-determinism, can be controlled with option --minimize.
• Enable usage of structured labels on minimized machines.
• Option --solver to use different parity game solvers: FPI, Zielonka's algorithm and Strategy Iteration, with FPI as the default. Zielonka's algorithm can currently only be used for checking realizability.
• Option --onthefly to control interleaving of solver with on-the-fly exploration.
• Option --lookahead to control application of Zielonka tree and ACD construction.

Removed

• HOA input for solving parity games in extended HOA format.
• Filtering of exploration queue based on reachable border nodes.
• Declaration of winning and losing states for realizability propagation in DPA.

Internal

• Move project structure to GitHub.
• Closer integration of bundled ABC library to reduce build size and time.
• Verification tests now have a different but reduced set of dependencies.