The results of net synthesis for Petri Net and FSM model are interpreted as Petri nets (implicitly converted from STGs).
Support for scalable SVGs is added to user documentation and tutorials (dimensions can be specified in % of the original size, similar to LaTeX).
Fit model to screen on opening and for automated layout.
Ignore saved selection on opening a work file (it is only useful for copy-paste).
Allow modification actions in Connection tool while not creating a connection.
Pass a work file as a parameter, so Workcraft can be assigned as a default application to open .work files.
Empty verification trace is emphasised by grey [empty trace] text.
Converter of Petri Net models into Policy Net models.
Model and tool plugins
Digital Circuit plugin
Improved formulation of circuit conformation property.
Compact Reach expression (does not depend on the size of system STG).
Additional checks for the device STG (has places, free of dummies, no disconnected transitions).
Internal signals in the environment STG are substituted by dummies.
Support for renaming gates and pins on Verilog export; a file of substitution rules can be specified under Digital Circuit preferences (accessible via Edit→Preferences… menu).
Empty model title is replaces with “.model Untitled” in .g file to enforce correct name of Verilog module synthesised by Petrify.
Corrected the parent of self-loop net in automatically generated circuits.
Warning on import of incorrect zero delay components.
Support for relative path to circuit environment files in Windows.
Module name (title) of a synthesised circuit is copied from the STG model title.
Signal Transition Graph plugin
Combined verification of STG for deadlock, consistency and output persistency reusing the same unfolding.
Dual producing-consuming arcs are converted into read arcs on import of .g files.
Two options for converting STGs to FSTs: basic and binary-encoded.
Proper positioning of Petri net/STG places generated from FSM/FST models.
Tokens of implicit places are drown on top of the arc now (not under the arc).
xMAS Circuit plugin
Perform all VXM calculations in a temporary directory, so the master copy of the tools/vxm/ directory is not modified.
Correct visualisation of contacts after rotation/flipping/resizing of a Queue component.
User documentation and tutorial for xMAS circuits.
Structured Occurrence Net plugin
Safeness checking in structural verification.
Structural property checking for ASON.
Error tracing support for ASON.
Fixes and technical stuff
Functionality of PetrifyPlugin related to write_sg and draw_astg tools is moved to PetrifyExtraPlugin.
MPSat is updated (backend tool for synthesis and verification of speed-independent circuits).
Punf, MPSat and PComp tools are packaged as UnfoldingTools.
VXM is updated (a backend tool for verification of xMAS circuits).
Extra arguments to backend tools are added after the built-in arguments but before the file parameters.
New default paths to all the backend tools for Windows (e.g. tools\PetrifyTools\petrify.exe) and Linux (e.g. tools/PetrifyTools/petrify).
Refactoring of the way external tools are called in order to overcome the “command line too long” in
Refuse to run ScEnco if the number of scenarios is too big (depending on the OS).