Sym Parikh

Implementation of Parikh image computation for symbolic automata.

Dependencies

• Catch2 -- assumed 3.12 or compatible. For unit testing.
• z3 -- assumed 4.12.1 or compatible.

Building

Build is using CMake. Recommended routine, from the root folder of the implementation

$ mkdir build
$ cd build
$ cmake ../
$ make

Alternatively, a Docker environment is provided in the docker folder. See the README in that folder for more information.

Running

After compiling as above

$ ./sym_parikh --help

For example

$ ./sym_parikh --file mysmtfile.smt2

Tests can be run with

$ ./tests

Debugging

If there are errors, it can be helpful to recompile with debugging symbols.

$ cmake ../ -DCMAKE_BUILD_TYPE=Debug
$ make

Benchmark Results

The complete results used in the POPL 2024 submission are available in benchmark-scripts/results-2023-07-05. See the artifact for a way to recreate these data.