Skip to content

v0.2.0

Latest
Latest

Choose a tag to compare

View all tags
@rizumita rizumita released this 28 Jun 19:39
· 2 commits to main since this release
v0.2.0
3419aa9
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

This release fixes several soundness bugs in the core LTL model checker, substantially improving the reliability of verification results.

🔴 Correctness fixes (model checking)

  • Fix operand transposition in the NNF negation of Until / WeakUntil. Formulas involving Until / Eventually / WeakUntil could return wrong results — e.g. p U r was incorrectly reported as HOLDS. (#16)
  • Fix the Release tableau-expansion branches, which assigned the operands incorrectly. (#17)
  • Fix check()'s not(.atomic) special case to use universal (not existential) quantification over the initial states. (#18)
  • Unify Büchi emptiness checking on a single standard Nested DFS (Holzmann–Peled–Yannakakis / CVWY), removing the non-standard pre-order implementation and the redundant SCC-based fallback. (#21)

⚠️ Robustness

  • Tableau construction now throws an error when the GBA state-count limit is exceeded, instead of silently truncating (which could yield an incorrect HOLDS). (#20)

🧹 Maintenance

  • Remove debug cruft and dead code (−368 lines in #23; −227 net from the NestedDFS unification in #21). (#21, #23)
  • Add the MIT LICENSE file. (#25)
  • Add an Apple-platform (macOS) CI job. (#26)

⚠️ Breaking changes

  • Removed the unused LTLModelCheckerError.algorithmsNotImplemented case.
  • Due to the correctness fixes above, some formulas that previously (incorrectly) returned HOLDS/FAILS now return the correct verdict.

Full Changelog: v0.1.0...v0.2.0

Assets 2
Loading