Workcraft v3.2.5 (2019-11-21)
Show shortcuts in
dialog for quickly creating new models
Configurable font size via global preferences (
Label font size (cm)
Name font size (cm)
Contact font size (cm)
Function font size (cm)
Models→Signal Transition Graph
Transition font size (cm)
Auto-save of last edited
Menu item for combined verification of all basic properties (in Digital Circuit, Signal Transition Graph, and Dataflow Structures) is renamed to
All of the above (reuse unfolding) [MPSat]
Model and tool plugins
Digital Circuit plugin
Tool for reducing the number of zero delay inverters (available via
Transformation→Optimise zero delay of buffers and inverters (selected or all)
Verification of circuit implementation for binate functions (via
Verification→Binate consensus [MPSat]
Names and pins of gates for synthesis of reset logic (BUF, AND2, OR2, NAND2B, NOR2B) are now automatically extracted from Genlib gate library.
In global preferences use of separators to create subsections for import/export, reset, and testing.
Undo/redo functionality in
Signal Transition Graph plugin
Handshake verification wizard (
Verification→Handshake wizard [MPSat]…
Search of signal events by the signal name directly from the
of the model
eXtended Burst Mode plugin
Model capturing functionality
Auto-calculation of signal changes in input and output bursts
Verification for unique state encoding and inclusion of conditionals
Conversion into STGs and Petri nets
Export into Minimalist burst mode file format
Fixes and technical stuff
Integration of BDD library (
) for complex operations on Boolean functions (e.g. checks for functions isomorphism, implication, binatness).
Update of UnfoldingTools
Bugfix for threshold operator (not used in built-in verification properties, but could affect custom Reach properties using this operator)
Syntax sugar to refer to transition or signal enabledness in LTL-X verification in Punf
Refactoring of the properties
and improvements of
properties rendered as a buttons (can be an array of actions associated with one property).
properties that occupy both columns.
to structure properties into subsections.
Textual properties with associated action (e.g. create or search for a node with the specified name)
Rework of the build system updating Gradle and its plugins
Refactoring of Boolean formula
files recognise split
suffix. These can be produced in the intermediate .g files when calling Punf with