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.
ScEnco (short for Scenario Encoder) is a collection of encoding algorithms for Conditional Partial Order Graphs.
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.
Spot is a platform for LTL and ω-automata manipulation.
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.
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.