About CPNUnf

CPNUnf is an unfolder for Contextual Petri Nets (also called c-nets) that implements the theoretical concepts presented in (1) and is written in Scala. Its simple design and straightforward implementation allows to study the algorithm and easily implement extensions to the core library. Yet this tool keeps an eye on performance, and allows to run 93% of the test suite.

CPNUnf also allows generation of logic programs in ASP form that can be run by Clingo to check for deadlocks in c-nets.

Prerequisites

In order to compile and execute the unfolder you need to have Java SDK 1.6 and Scala 2.9 installed. Make sure they are available on your system and configured as defaults. Ant is also required to build the software.

Download

You can find the latest version here: cpnunf-latest.zip. After downloading and decompressing the archive, the source code is inside the src/ directory.

To compile the software simply run ant on the project folder.

Known Usage

• Cpunf-ModelCheck, by Alberto Franco, is a model checker for interference properties of atomic, a thread-based programming language with atomic sections.

Reporting Issues

If you encounter a problem using this project, please don't hesitate to report a bug in the Issues section. I'm also open to receive any feedback that you might have, and suggestions for improvement, so you are very welcome to file those as well.

See Also

1. Cunf, a fast c-net unfolder by César Rodríguez.
2. Mole, a Petri net unfolder by Stefan Schwoon.

References

1. Paolo Baldan, Alessandro Bruni, Andrea Corradini, Barbara König, César Rodríguez, and Stefan Schwoon. Efficient Unfolding of Contextual Petri Nets. Theoretical Computer Science 449, 2 – 22 (2012)