User Tools

Site Tools


Back-end tools

A number of plug-ins included in Workcraft depend on third-party tools and some of the plugins act as a user friendly front-end for such tools. In order to obtain complete functionality from Workcraft these back-end tools have to be present on your system (note that the Workcraft distribution comes bundled with these tools, so you do not have to install them separately). Download locations for those tools are linked below.


PGminer is a tool for extracting concurrency from event logs. It takes a set of event traces, detects potentially concurrent events, and produces a set of partial orders, to be further compressed into a Conditional Partial Order Graph.

PGMiner on GitHub


ScEnco (short for Scenario Encoder) is a collection of encoding algorithms for Conditional Partial Order Graphs.

ScEnco on GitHub


Graphviz (short for Graph Visualization Software) is a package of open-source tools initiated by AT&T Labs Research for drawing graphs specified in DOT language scripts. Workcraft can use GraphViz Dot to automatically layout interpreted graph models.

GraphViz homepage


Spot is a platform for LTL and ω-automata manipulation.

Spot homepage

Unfolding Tools

Unfolding Tools (PUNF, MPSAT, and PCOMP) by Victor Khomenko provide an extensive set of functions for composition and verification of Petri nets and STGs, and for synthesis of electronic circuits from STGs. They serve as the primary verification back-end of Workcraft and also parallel the synthesis capabilities of Petrify, but are based on Petri net unfoldings rather than BDDs and so often more efficient.

Unfolding Tools - download page for the current version

Unfolding Tools - download page for older versions


Petrify is a tool for synthesis of Petri nets and asynchronous controllers by Jordi Cortadella. Petrify reads a Petri net and generates another bisimilar Petri net which is simpler than the original description. Initially, petrify performs a token flow analysis of the initial Petri net and produces a transition system (TS). In the initial TS, all transitions with the same label are considered as one event. The TS is then transformed and transitions relabeled to fulfil the conditions required to obtain a Petri net. Petrify is able to obtain Petri nets with some specific properties: pure, free choice, unique choice, place irredundant, etc.

Petrify homepage

Copyright © 2014-2024

Donate Powered by PHP Valid HTML5 Valid CSS Driven by DokuWiki