N-way conformation for several STGs – check that each STG is conformant to a composition of the others. This can be verified via Verification → N-way conformation (without dummies) [MPSat].

When doing technology mapping, the user can save the final STG with all the newly inserted CSC and decomposition signals, e.g. for future analysis and optimisation. This feature can be enabled in global preferences for Petrify and MPSat synthesis separately via Open resulting STG if new signals are inserted.

Redundancy check for places of Petri net and STG models, either for all selected places via Verification→Redundancy of selected places [MPSat] menu or for a single place via Check place redundancy in the popup menu.

Promote mutex implementability check to the core properties (consistency, deadlock freeness, input properness, and output persistency).

New icons for Open and Save actions.

Export isolated trans as 1-element line of '.g' file.

Allow cancellation of the dialog for expansion of handshake transitions.

Bugfix for verification of mutex place implementability with hierarchical grant signals (inside a page).

Refactored interface to the backend tools Petrify, PComp, Punf and MPSat, so it is more type-safe.

Diagnostics of PComp failure in MPSat toolchain.