The CPOG encoding plugin is used for deriving a compact representation for a collection of partial orders. The result is expressed as a Conditional Partial Order Graph (CPOG), which contains all partial orders in a compact form. Each partial order can then be highlighted and activated by setting Boolean parameters to appropriate values (according to the codes that are derived for each partial order).
The plugin uses ABC – a software for the sequential synthesis and verification. This is used to synthesise the final controller, meant for managing the sequentiality of the operation to be performed real time. For more information about this program, please take a look at the original website: http://www.eecs.berkeley.edu/~alanmi/abc/.
Several approaches to derive the final CPOG are incorporated. Each of them has its own advantages and drawbacks and might be potentially exploited. Below the description of each technique is present with few figures, which might be helpful for a better understanding of the tool and process in general.
The plugin handles 5 out of the 6 techniques available to derive the final CPOG. The only technique which is handled separately is the so called “SAT-based optimal encoding”. It works with SAT-based programs (Clasp, Minisat). They are not included in the Workcraft package directly, but they might be downloaded and used by users interested on them.
All the techniques that are described below can be accessed via Encoding menu. It becomes visible for CPOG models. This menu contains six different approaches.
The dialogue displayed for these three approaches is the same and depicted below.
This is accessible by the corresponding buttons. Before discussing about each features which these methods allow, it is worthwhile listing what each approach is about.
In order to use one of the technique described in this tutorial, the user must make sure to first have selected at least two partial orders composed and displayed in the dedicated workspace. After that, one may choose which approach to apply for the derivation of the CPOG.
Go to Encoding → SAT-based optimal encoding. This will create a new group with the synthesised Conditional Partial Order Graph and will show the computed encodings below each scenario.
It is important to tune the encoding tool in order to produce results of desired quality. The tool window will allow you to set the following encoding parameters:
Furthermore, you can control which SAT-solver is used for optimal encoding by navigating to Edit → Preferences… and locating the section related to the SCENCO plugin. You will be able to set the following parameters there:
This encoding algorithm produces a CPOG with simple conditions (each condition is a single positive or negated literal).
The sequential encoding produces a CPOG with trivially encoded partial orders: they are given binary codes equal to their order.