====== CPOG plugin ======
Familiarise yourself with [[..:core:start|Workcraft interface]] to learn its common features that are available for all plugins.
The CPOG plugin provides support for the specification of a collection of behavioural scenarios, e.g., microprocessor instructions, and interfaces with the tools for their further analysis using [[help:cpog:encoding_plugin|CPOG encoding]] and verification techniques((See the following two papers for more details:
* A. Mokhov, A. Yakovlev. //“Conditional Partial Order Graphs: Model, Synthesis and Application”//, IEEE Transactions on Computers, 2010, vol. 59, no. 11, pp. 1480-1493.
* A. Mokhov, A. Alekseyev, A. Yakovlev. //“Encoding of Processor Instruction Sets with Explicit Concurrency Control”//, Special Issue on Best Papers from ACSD'2010 conference, IET Computers & Digital Techniques, 2011, vol. 5, no. 6, pp. 427-439.
)).
===== Getting started =====
The plugin is currently only available for documents using the Conditional Partial Order Graph model. To create a new document of this kind click //File -> Create work...// then select //Conditional Partial Order Graph// in the opened window and click //OK//.
===== Specification of scenarios =====
There are two different ways of creating scenarios: by drawing their graphical representations and by entering their algebraic descriptions. In practice a combination of both works best.
==== Drawing scenarios ====
To create a scenario, first add the events (vertices) by activating the **Vertex** tool {{..:core:editor_tools-vertex.png?nolink|Vertex tool icon}} and clicking on the places where you want to place them. Then add the dependencies (arcs) between the events using the **Connection** tool {{..:core:editor_tools-connect.png?nolink|Connection tool icon}}. You can move the elements of the graph and edit their properties using the **Selection** tool {{..:core:editor_tools-select.png?nolink|Selection tool icon}}. Finally, select the graph representing the scenario and click {{..:core:tool_controls-select-group.png?nolink|Group icon}} to create a box (group) encapsulating the vertices and arcs of the scenario inside. You will then be able to label the scenario. If you wish to edit the scenario later click {{..:core:tool_controls-select-level_down.png?nolink|Level down icon}} and {{..:core:tool_controls-select-level_up.png?nolink|Level up icon}} to go inside/outside the group.
Repeat the above steps to add more scenarios into the document.
==== Algebraic scenario specification ====
Drawing scenarios graphically may be a tedious process, so we implemented an alternative way to create them. The **Selection** tool has a text box which can be used for specifying an algebraic representation of a graph((See the following paper for more details: A. Mokhov, V. Khomenko, A. Alekseyev, A. Yakovlev. //“Algebra of Parameterised Graphs”//, International Conference on Application of Concurrency to System Design (ACSD’12), nominated for Best Paper Award, p. 22-31, June 2012.)), which can then be added into the document by clicking the Insert button below it, as shown on this screenshot:
{{ tool_controls-select.png?nolink |}}
The following examples show simple algebraic expressions and describe the corresponding graphs:
* **''a + b + c''** -- this will insert a graph with three vertices labelled 'a', 'b' and 'c' and no arcs.
* **''a -****> b + c''** -- this will insert a graph with three vertices a, b and c and an arc going from vertex a to vertex b.
* **''a + (b + c) -****> d''** -- this will insert a graph with four vertices a, b, c and d and two arcs going from vertices b and c to vertex d.
* Note that the **+** operator can be omitted for clarity, hence inserting the expression shown in the above screenshot will produce the following graph (after manual layout):
{{ inserted_graph.png?nolink |}}
We plan to implement more sophisticated automated graph layout options in future versions of the plugin.
===== Scenario encoding =====
Once you have created all scenarios it is possible to automatically generate an optimal encoding for them and combine the scenarios into a Conditional Partial Order Graph. Several encoding algorithms are available; here we only look at one of them, called SAT-based optimal encoding. See the [[help:cpog:encoding_plugin|CPOG encoding]] plugin for a comprehensive overview of all currently supported algorithms.
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.
==== SAT-based optimal encoding settings ====
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:
* The number of encoding variables (note that you need at least log2(N) variables to encode N scenarios).
* The maximum number of 2-input gates in the combinational circuit computing all the conditions in the resulting Conditional Partial Order Graph.
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:
* Paths to supported SAT solvers; currently **minisat**((Can be downloaded from http://minisat.se/)) and **clasp**((Can be downloaded from http://www.cs.uni-potsdam.de/clasp/)) are supported. One of them needs to be installed.
* The preferred SAT solver.