PetriNetValidator

This work is being done and updated accordingly as a course project at HSE University (Moscow, Russia)

The project allows its users to validate two Workflow Petri net models' (imported from .pnml-files) behaviour by checking compliance of the second model (typically, a multi-agent system net) with the first one (the interface net) using property-preserving transformations ("Fusion of Parallel Places", "Fusion of Parallel Transitions" and "Local Transition Elimination" abstraction rules and their refinement counterparts).

The way of rules' application to the second model in general cases is deduced via the difference in the amounts of transitions and places in each respective model - it might be either strictly abstraction (reduction) or strictly refinement (extension). In case the amounts are equal to each other,the program checks whether the models are isomorphic by using a custom hash-function, applied to the arcs of each respective model.

Whenever the main.py script executes, it uses two input arguments from the terminal which represent the absolute (or relative) paths to the .pnml-files of each respective model. In the directory relative to the script execution the "Output"-subdirectory is created, which is going to store subdirectories for each pair of used files - the subdirectories names have a format "{file1}-{file2}", where "file1" and "file2" resemble the filename for each respective .pnml-file without the extension. Initially, the subdirectory will contain "interface.png" and "net.png", which represent two original models, while at the end of program's execution a file "converted.png" is also added to the subdirectory, showing the final view of the transformed initial second model.

For each executed transformation, two .png-files are created to depict the local transformation of the second net ("{i}-1.png" and "{i}-2.png", where "i" is the number of the transformation starting with 1; "-1" and "-2" suffixes represent the initial and final views on the model respectively).

Installation (requires up to 500MB of free space):

1. Download a Python3 interpreter;
2. Download (or git-clone with git clone https://github.com/Muxianesty/PetriNetValidator) and unzip this repository if needed;
3. Download and install GraphViz-executables (here);
4. Download and install a Petri net editor if needed (we recommend using WOLFGANG - here);
5. Setup a Python virtual environment in the downloaded repository by using python -m venv {env_name} , with "env_name" as your environment directory name;
6. Download dependencies with "pip" (from virtual environment): pip install -r libs.txt or just pip install pm4py as pm4py-library is the only main library being used in the project.

Execution:
{env_name}\Scripts\python main.py {f1} {f2} for Windows
{env_name}/bin/python main.py {f1} {f2} for Linux/MacOS
where "env_name" is the name of the virtual environment directory, "f1" and "f2" are absolute/relative paths to the files of the two Workflow Petri net models.