Return to User manual

Extract CTL rules from process model(s)

Authors: Heerko Groefsema, Nick van Beest, Abel Armas Cervantes

This plugin extracts a set of business rules in CTL (Computation Tree Logic) from a set of business process variants, expressed as Petri nets. It takes as input one or more process models in PNML format and returns a CTL specification as XML file. This CTL specification describes the constraints capturing the behavior of all process models used as input, as well as all behavior between these models. In other words, this CTL specification declaratively describes a generic business process based on the input models, while allowing for variability within those constraints.

To launch this plugin, hit “Discover>Extract CTL rules”. Once the plugin is launched, it asks for the types of CTL constraints to be included. By default, all sets are selected.

Extract Variability Specification select sets

By clicking “Accept”, the plugin will show the generated CTL specification, which can be downloaded as an XML file.

Extract Variability Specification plugin output

The extracted CTL specification can be used as input to the Check compliance against CTL rules plugin.

A screencast of this plugin is available here.