Alpyne is a package designed for the construction and verification of Algebraic Petri Nets with Python.

Algebraic Petri Nets (APNs) are a high order variant of Petri Nets, a class of models typically used in the verification of concurrent software. The objective of Alpyne is to provide a framework to build models of concurrent programs with APNs and to automatically check properties on them.

To install Alpyne, simply clone this repository and run the command pip3 install --upgrade . at its root (and preferably inside of a virtual environment). Once this is done, the package can be used like any other Python library.

Algebraic Petri Nets are built on top of the concept of Algebraic Data Types (a.k.a. ADTs -- mathematically formalised data structures described with the help of many-sorted algebrae, axioms and rewrite rules -- see the book by Sannella and Tarlecki for an in-depth discussion on the subject).

Before an Algebraic Petri Net can be built, the sorts of the terms it uses as tokens need to be defined. This can be done with the adt module of this package. Examples of definitions of ADTs can be found in the /alpyne/adts folder of this repository, where the ADTs of base sorts such as booleans or naturals are defined.

To define and use APNs, the apn module of this package can be used. An example of script that builds and executes an APN to compute the Fibonacci sequence is provided in the /examples folder of this repository.