User Tools

Site Tools


changelog:v3.0.7

Workcraft v3.0.7 (2016-01-04)

Usability improvements

  • 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).