All algorithms: {pre*, post*, dual*} x {shortest, longest} trace

This release implements shortest and longest trace versions for both pre* and post* algorithms and the combination 'dual*'. Using dual* (-e 3) gives overall the best performance in our benchmarks.
Parsing now supports wildcard rules and vector weights.
Various bug-fixes and algorithmic improvements.

What's Changed

• CMake improvement by @MortenSchou in #30
• Wildcard rules by @MortenSchou in #31
• GitHub Actions build and test workflow by @MortenSchou in #33
• Upload artifacts in GitHub Actions by @MortenSchou in #34
• Add option to include dependencies in the binary by @MortenSchou in #35
• Parse vector weights by @MortenSchou in #36
• Structured json output by @MortenSchou in #37
• Fix bug in post* shortest trace by @MortenSchou in #38
• Fix bug in P-automaton JSON parser by @MortenSchou in #39
• Improve data structure use + various simplification and clean up by @MortenSchou in #40
• Fix PAutomaton to_dot with vector_printer by @MortenSchou in #41
• Add longest trace post* engine + interleaved pre*/post* fixed-point by @MortenSchou in #42
• Fix post* shortest trace (Dijkstra version) by @MortenSchou in #43
• Add file format examples to readme by @MortenSchou in #44
• Add pre* and dual* for shortest trace by @petergjoel in #48
• Lazy pop longest prestar by @MortenSchou and @petergjoel in #47

Full Changelog: v1.0.0...v1.1.0

Stand-alone tool + longest trace

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

General early termination | Dual search | CEGAR

This release contains several upgrades:

• On-the-fly intersection of P-automata allowing early termination in the general case.
• Dual search algorithm (interleaving pre* and post*).
• CEGAR (counter-example guided abstraction refinement) of the pushdown reachability analysis.

Also featuring:

• ptrie_interface, which makes it easier to work with heterogeneous types in the ptrie data structures.

Deprecation:
The Reducer class (implementing top-of-stack reductions of PDA) only works with PDAs with one initial and final state and empty initial/final stack, which the new workflow is no longer restricted to. Since Reducer is no longer compatible with the reachability analysis, it may be removed in a later release, unless it is generalized (which should be possible, but requires some labor).

v0.2.5: Merge pull request #17 from DEIS-Tools/fifo-poststar

Use FIFO-queue for transitions in post*

v0.2.4: Merge pull request #14 from DEIS-Tools/bug-fix-dummy-label

More bugfixing

Performance and bugfix

Various updates and fixes

v0.2.2 Journal Release

Release for repeatability of journal.

Performance improvements

Improves the performance of PDAFactory and PAutomaton.

Weighted PDAAAL

Implements weighted pushdown systems and shortest trace post* reachability analysis.
Still supports 'any trace' post* and pre* for both weighted and unweighted pushdown systems.

Initial PDAAAL

Initial implementation, taken out from AalWiNes.