====== 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 =====

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.

[[https://github.com/tuura/process-mining/|PGMiner on GitHub]]


===== ScEnco =====

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

[[https://github.com/tuura/scenco/|ScEnco on GitHub]]


===== GraphViz =====

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.

[[http://www.graphviz.org/|GraphViz homepage]]


===== Spot =====

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

[[https://spot.lrde.epita.fr/|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.

[[unfoldingtools:start|Unfolding Tools - download page for the current version]]

[[http://homepages.cs.ncl.ac.uk/victor.khomenko/home.formal/tools/UnfoldingTools/|Unfolding Tools - download page for older versions]]


===== Petrify =====

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.

[[http://www.lsi.upc.edu/~jordicf/petrify/|Petrify homepage]]