Skip to content

Stand-alone tool + longest trace
Compare
Choose a tag to compare
@MortenSchou MortenSchou released this 01 Mar 16:46
· 134 commits to master since this release
v1.0.0
32a3fc9
This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
GPG key ID: 4AEE18F83AFDEB23
Expired
Verified
Learn about vigilant mode.

This release extends the library with parsers (and printers) and a main binary, so it can be used as a stand alone pushdown verifier tool.
On the algorithm side, we can now compute longest trace and detect loops (infinite trace) using a fixed-point version of pre*. (Returning the looping pattern in case of infinite trace is not yet implemented.)
Finally, there has been a major restructuring of the code.

What's Changed

  • Stand-alone PDAAAL bin + Parsers + Printers + fixed-point-pre* + bug fixes by @MortenSchou in #22
  • Update dependencies by @MortenSchou in #23
  • TraceInfoType + more AutomatonPath + AutomatonTraceBack by @MortenSchou in #24
  • Move find_path[_shortest] to PAutomaton + fix algorithm + make AutomatonPath nullable by @MortenSchou in #25
  • Move internal code to namespace pdaaal::internal by @MortenSchou in #26
  • Renaming that removes 'Typed' prefix from PDA, PAutomaton, and PDAFactory by @MortenSchou in #27
  • All CEGAR things are in specific folder by @MortenSchou in #28
  • Add JSON parser for Solver-Instance by @MortenSchou in #29

Full Changelog: v0.3.0...v1.0.0

Contributors

MortenSchou
Assets 2
Loading