changelog:v3.2.5
Workcraft v3.2.5 (2019-11-21)
Usability improvements
- Show shortcuts in Create work dialog for quickly creating new models
- Configurable font size via global preferences (Edit→Preferences…):
- In Common→Visual the properties Label font size (cm) and Name font size (cm).
- In Models→Digital Circuit the properties Contact font size (cm) and Function font size (cm)
- In Models→Signal Transition Graph the property Transition font size (cm)
- Auto-save of last edited Custom properties and Custom assertions
- 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 Initialisation analyser and Cycle analyser tools
- Signal Transition Graph plugin
- Handshake verification wizard (Verification→Handshake wizard [MPSat]…)
- Search of signal events by the signal name directly from the Property editor 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
- Simulation tool
Fixes and technical stuff
- Integration of BDD library (https://bitbucket.org/vahidi/jdd) 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 API and improvements of Property editor
- Action properties rendered as a buttons (can be an array of actions associated with one property).
- Span properties that occupy both columns.
- Separator 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 API
- When reading .g files recognise split STG places with
@NUMBERsuffix. These can be produced in the intermediate .g files when calling Punf with-roption.
Copyright © 2014-2021 workcraft.org
