v1.1 Added DPN soundness repair

Added an algorithm to repair unsound DPNs. To use it, go to Model -> Transform model -> Transform model to repaired. The algorithm restricts DPN transitions thereby forbidding traces leading to deadlocks and livelocks. The algorithm also allows fixing DPN unboundedness in rather simple cases.

v1.0.1

Hotfix of DPN refinement execution.

First Release

First version of soundness verification algorithm. The soundness verification procedure consists of five main steps:

1. Checking boundedness of a DPN,
2. Splitting DPN transitions occurring in cycles,
3. Adding $\tau$-transitions whose guards are negations of guards of the existing DPN transitions,
4. Constructing a Labeled Transition System (LTS) for the resultant DPN,
5. Analyzing the LTS for data-aware soundness properties.
   Two algorithms for soundness verification are implemented. The direct algorithm follows the described above schema. The improved algorithm postpones the DPN refinement and performs the preliminary checks on the LTS of the source DPN and the LTS of the tau-DPN.

Process model files are imported in the extended PNML-based format. Examples are presented in Samples_For_Import directory.