Petri Net Reachability & Analysis Tool

This repository contains a Petri Net analyzer implemented in C++. It parses PNML (Petri Net Markup Language) files and performs several analyses including explicit reachability (BFS), symbolic reachability using Binary Decision Diagrams (BDD via CUDD), deadlock detection, and reachable marking optimization.

---

Features

• Task 1: Parsing PNML (Petri Net Markup Language) files using TinyXML2.
• Task 2: Explicit Reachability Graph generation (BFS).
• Task 3: Symbolic Reachability analysis using Binary Decision Diagrams (BDD) with CUDD.
• Task 4: Deadlock detection using BDDs, with Gurobi ILP to find the minimal deadlock marking.
• Task 5: Reachable marking optimization (maximizing token weight) using BDD cube enumeration.

---

Dependencies

Make sure you have the following installed before building the project:

• C++ compiler: GCC (MSYS2 / MinGW recommended on Windows).
• TinyXML2: TinyXML2 sources are included in the repository (tinyxml2.cpp/.h).
• CUDD: Colorado University Decision Diagram package (source included in cudd/).
• Gurobi Optimizer: Required for ILP computations used in Task 4.

Note: On Windows we recommend using MSYS2 UCRT64 (or a compatible environment) for building CUDD and the project.

---

Setup & Installation

1. Build and install CUDD (example: MSYS2 UCRT64)

The CUDD source code is included in the cudd/ directory. You must compile it as a static library and install it into a local installed/ folder.

Example commands (run from the project root directory in MSYS2):

cd cudd
./configure --enable-obj --enable-static --disable-shared --prefix="$PWD/installed"
make -j4
make install
cd ..

After this step you should have cudd/installed/include and cudd/installed/lib available for the main project.

---

2. Gurobi setup

Install Gurobi on your system (for example C:/gurobi1300/win64). Make sure you have a valid academic or commercial license and the Gurobi C++ API available. You will need to reference Gurobi's include and lib directories during compilation.

---

Compilation

Option 1: MSYS2 Terminal

From your MSYS2 terminal (adjust paths to your local installation of cudd and gurobi):

g++ main.cpp task1.cpp task2.cpp task3.cpp task4.cpp task5.cpp tinyxml2.cpp "C:/gurobi1300/win64/src/cpp/*.cpp" \
-o main \
-I"cudd/installed/include" \
-I"C:/gurobi1300/win64/include" \
-L"cudd/installed/lib" \
-L"C:/gurobi1300/win64/lib" \
-lcudd \
-lgurobi130

Option 2: VS Code Terminal

After performing the setup steps above (specifically configuring and building CUDD via MSYS2), you can compile the project directly in the VS Code terminal using this single line:

g++ main.cpp task1.cpp task2.cpp task3.cpp task4.cpp task5.cpp tinyxml2.cpp "C:/gurobi1300/win64/src/cpp/*.cpp" -o main -I"cudd/installed/include" -I"C:/gurobi1300/win64/include" -L"cudd/installed/lib" -L"C:/gurobi1300/win64/lib" -lcudd -lgurobi130

Notes

• Gurobi Paths: Ensure C:/gurobi1300/win64 matches your actual Gurobi installation version and path.
• Gurobi Library: If your version differs, change -lgurobi130 to match your installed library name (e.g., -lgurobi100 for version 10.0).
• Linking Errors: If linking fails, verify that the cudd/installed/lib directory was created successfully during the Setup phase.

---

Usage

Place your Petri net PNML/XML file in the project directory (e.g. Net_1.xml).

Open main.cpp and verify the inputFileName string points to your file:

string inputFileName = "Net_1.xml";

Run the compiled executable:

./main
# or on Windows cmd: main.exe

Output: the program writes a text file named <input>_output.txt (e.g. Net_1_output.txt) containing results from tasks/analyses.

---

File Structure

• main.h — Shared header: definitions for Place, Transition, and function prototypes.
• main.cpp — Program entry point, file I/O, and orchestration of tasks.
• task1.cpp — PNML parsing using TinyXML2.
• task2.cpp — Explicit state-space exploration (BFS) implementation.
• task3.cpp — Symbolic reachability using BDDs (CUDD wrapper logic).
• task4.cpp — Deadlock detection using BDDs + Gurobi ILP for minimization.
• task5.cpp — Reachable marking optimization using BDD cube iteration.
• tinyxml2.cpp, tinyxml2.h — TinyXML2 XML parsing library (included).
• cudd/ — Source code for the CUDD library. Requires local configuration and building (see Setup).

---

Troubleshooting & Tips

• Linker errors for CUDD/Gurobi: Double-check -L library paths and -I include paths. Make sure you built CUDD with --enable-static and installed it to the specified prefix.
• Gurobi library name: The -lgurobiXXX name depends on the Gurobi minor version; inspect the C:/gurobi*/win64/lib folder to find the correct .a/.lib name.
• Running on native Windows (cmd/PowerShell): If you compile using MinGW/MSYS2, use the MSYS2 terminal to avoid path and toolchain mismatches. The produced binary may be runnable from cmd as main.exe, but debugging build files is easier inside MSYS2.
• CUDD build errors: Ensure you have required build tools installed in MSYS2 (autoconf/automake, gcc, make). If ./configure fails, check config.log in cudd for hints.

---

Example

Put Net_1.xml in the project root.

Ensure main.cpp has string inputFileName = "Net_1.xml";.

Build and run the program.

Inspect Net_1_output.txt for task outputs: parsed net description, reachability results, deadlock detection outcome, and optimized marking.