Reuse of open workspace entries when loading models – this makes unsaved changes in environment/refinement models visible to verification commands
Restore highlights in Output tab after applying global preferences
Model and tool plugins
Digital Circuit plugin
Enhanced support two Mutex protocols: Late (previously Strict) and Early (previously Relaxed)
Add user-defined suffix for MUTEX cells with Late and Early protocols
Include two flavours of MUTEX cell into the library presets
Distinguish Late and Early MUTEX cell on Verilog import
Refresh set/reset functions on contact inversion
Refactor Scan and Reset insertion so they change the model only if needed
Fix conformation check for mutex whose outputs are not exposed
Fix simulation tool for highlighting suggested components
Signal Transition Graph plugin
Improvements for N-way conformation check
Composition trace for N-way conformation is extended with component violation events
Use projected composition events in Table and List views
Enhanced verification of mutex place implementability
Add Mutex protocol property to enable fine-grain tuning of mutex places
When syntactically detecting mutex requests, exclude grants from the set of triggers
Fix detection of place redundancy in presence of read arcs
Fix handling of replica (i.e. proxy) places in transition contraction
Fix undo/redo functionality when changing signal type via model-level property
Fixes and technical stuff
Update of UnfoldingTools backend
MPSat can now build unfolding prefix and supports LTL-X verification
MPSat's command line parameters have changed significantly to enable the above
Punf is phased out, as all its functionality is now available in MPSat
Fix technology mapping into libraries without C-elements
Fix PComp's storing of place and transition correspondence in XML formal when one of signal phases is absent in the composition and so a transition in a component STG has no corresponding transitions in the composition.
Update toolchain to Gradle v7.0.2, PMD v6.34, Checkstyle v8.42