This post has 2110 words. Reading it will take approximately 11 minutes.
CPN Tools 4 merges the colored Petri net language with the Declare language. Declare was previously supported
In colored Petri nets, the control flow is either dependent on data or on explicit passing of a control flow token. Declare instead specifies relations between actions, but does not support flow of data. By combining the two, it is possible to specify control flow either explicitly or implicitly, and to specify data flow.
Declarative Modeling from Abstract Description
Consider if we have to model:
- If you are bored, you should go to a concert.
- You can go to different concerts.
- Never, can you go to both a concert with Britney and a concert with
- Only persons going to a Britney concert can ever be truly happy.
A CPN model mostly satisfying this, can be seen below.
While this model mostly satisfies our constraints, it does have some problems. For example, nothing says we cannot be bored more than once (but our model does not specify that). We introduce an unmentaioned activity, Go Back, which is necessary to allow the choice between True Happiness and going to more concerts. We never exclude going to both Britney and Xtina concerts. Also, we can only be truly happy immediately after going to a Britney Concert (and not, e.g., after going the Britney and then Gaga).
We can fix these problems, but this requires adding more and more detail. Our abstract description simply allows too much, making the resulting restricted a more or less arbitrary simplification thereof. This may be useful in some cases, but maybe we just want to directly model the abstract description.
Declare allows just such abstract descriptions. Instead of explicitly describing the flow, Declare allows us to instead specify relations between the constraints. A more accurate model of the above can be seen below:
Here, we have replaced the book-keeping around the Britney Concert with Declare constraints. The not-coexistence constraint between Britney and Xtina Concert means that no execution can allow both of them (satisfying requirement 3). The precedence constraint from Britney Concert to True Happiness exactly models requirement 4. The requirement states that True Happiness can only be executed after executing Britney Concert, but we do not have to do so immediately; we can easily go to any other allowed concert. This also means that True Happiness is not enabled in the initial state above as Britney Concert has not yet been executed.
This is the state after executing Bored:
Now all three concerts are enabled (there are tokens on the place). Executing Britney Concert leads to:
Now, the Xtina Concert becomes disabled (due to the not-coexistence constraint) and True Happiness becomes enabled. True Happiness remains enabled regardless of which other transitions we execute.
The Declare component enables and disables transitions as needed to ensure no constraints are violated. This also means avoiding future conflicts. Consider this slightly altered example:
The existence constraint above True Happiness forces execution of this transition. Executing Bored now leads to this state:
The tool realizes that even though Xtina Concert could be executed without immediately breaking any constraints, executing it would eventually lead to a conflict. The reason is that executing Xtina Concert prevents us from ever executing Britney Concert (due to not-coexistence). We can only ever execute True Happiness if we first execute Britney Concert, so if we execute Xtina Concert, we can never simultaneously satisfy the not-coexistence between Britney and Xtina Concert, the precedence from Britney Concert to True Happiness, and the existence on True Happiness. The tool recognizes and avoids this conflict automatically.
Using the Declare Language
CPN Tools now has a new Declare tool palette, which contains all the various constraints:
We see 16 (19 in some versions) binary constraints and 11 unary constraints. Binary constraints work exactly like regular arcs in CPN
The constraints are separated into 5 groups:
- green and red: constraints concerned with ordering of tasks
- red: constraints specifying if-then like orderings
- green minus red: constraints specifying if-then-not like orderings
- purple: specifying unordered existence/choices
- yellow: specifying first and last events (positions)
- blue: specifying existence of events
The existence constraints (blue) specify, from left to right and top to bottom, that a transition has to be executed at least once (twice, three times), at most zero times (once, twice), and exactly once (twice, three times). We also call these existence, absence and exactly (existence of one execution, absence of one execution, and exactly one execution). The absence of one execution (0) is useful in conjunction with the predictive analysis to avoid error states.
The position constraints (yellow) simply specifies that the initial and last transitions to execute. When one transition has the init constraint, no other transition can be executed until it has been executed. Two transitions with this constraint immediately yields a conflict, which is why the below model has no enabled transitions:
The last constraint indicates that when the execution terminates, it must be with this transition. It is perfectly legal to execute the transition earlier as well, as seen here:
We can use last in conjunction with a constraint limiting the number of times we can execute a transition to terminate an execution as soon as a transition is executed:
The unordered constraints (purple) specify that if one end of the constraint is executed, the other end is impacted, regardless of the order of the execution of the two. From the top-left, we have responded existence, co-existence, choice, and exclusive choice.
The responded existence means that if the end with the circle is executed, so must the other end as well, either before or after (it corresponds to logical implication: if the circle-side is executed, the other must be executed; if the circle-side is not executed, the other can be executed or not as desired). The co-existence can be thought of as a responded existence in both direction. If one of the two is executed, the other must be as well. It is also legal not to execute any of them (it corresponds to logical bi-implication; each side is executed if an only if the other is).
The choice constraint indicates that at least one of the ends have to be executed and exclusive choice that exactly one must be executed (they correspond to disjunction and exclusive or in logic respectively; either one side is executed or the other, and either one side is executed or the other but not both).
The ordered constraints (green and red) strengthen this further, and require that execution takes place in a specific order. They extend the use of the circle to mean that "if this end is executed," and also introduce an order of execution. The first column contains the response, precedence, and succession constraints:
The response constraint means that if the side with the circle is executed, the other side must be executed at some time afterwards. Hence, if we execute A1, we must at some time afterwards execute B1. We can execute B1 whenever we want; only A1 imposes an obligation. One B1 can satisfy as many A1 as required, so A1, A1, A1; B1, B1, B1; and B1, A1, A1, B1 are perfectly valid executions, while A1, A1, A1 and A1, A1, B1, A1 are not (the first never satisfies any of the A1s and the second doesn't satisfy the last A1).
The precedence imposes the same order, but reverses the proof obligation. Thus, we can only execute B2 after executing A2. We can execute A2 as many times as we want without ever executing B2, and after executing the first A2, we can execute B2 as often as we want (it still occurs after the first A2). This is why B2 is not enabled in the initial state shown: we have not yet executed and A2.
The succession is the conjunction of the two; both A3 and B3 impose an obligation. Thus, we cannot execute B3 before executing A3 first, and after executing A3, we must execute B3. Thus, A3, A3, A3, B3, A3, B3, B3 is a valid execution, while B3, A3, A3, B3 and A3, A3, A3 are not.
The next column are the alternate response, alternate precedence, and alternate succession constraints. They strengthen the regular response, precedence, and succession constraints by forcing a certain alternation. Hence, the alternate response requires that each A1 is followed by one or more B1 before we can execute another A1. The alternate precedence requires that each B2 is preceeded by one or more A2a, and does not allow executing B2 more than once before a fresh A2 is required. The alternate succession requires that we alternate between A3 and B3, starting with A3. We can of course at all times add any other action in-between.
The final column of positive ordered constraints include the chain response, chain precedence, and chain succession. This column is discouraged and only included because it is useful when using time (not yet supported). This further strengthens the requirements, so we are not allowed to execute anything else between the As and Bs. Chain response means that executing an A1 forces the next transition to be a B1. Chain precedence means that B2 is only enabled immediately after executing A2. Chain succession combines the two.
The negative constraints comprise three constraints: not co-existence, not succession, and not chain succession. The not co-existence is not actually ordered, but says that at most one of the ends can be executed (it corresponds to a logical nand withou order; if one is executed the other cannot, but it is ok to execute neither).
The not succession means that if A1 is executed, B1 is permanently disabled: it is not allowed to execute it after A1. It is perfectly ok to execute B1 until A1 has been executed, and A1 can be executed at leisure whenever desired.
The not chained succession slightly weakens this, and just says that B2 can never immediately follow A2. We can execute A2 at leisure, and if we execute anything but A2, we can execute B2 as much as we want again.
Note that Declare uses a finite semantics. This means that the below model is inconsistent (and hence no transition is enabled):
This model effectively states that any A must be followed by a B, and any B must be followed by an A. Any execution satisfying this and containing either of these cannot be finite (it will have a last execution of either of A and B, which is not followed by the other).
Declare constraints integrate completely with CPN Tools' incremental syntax check. As you add/remove constraints, the enabling of transitions is updated. This even happens if you add/remove constraints during simulation:
Declare and CP-nets
We have already seen that Declare can cooperate with CP-nets, though not explicitly. Assume we want to add tickets to our above example. We could end with a model looking like this:
Here, we require an appropriate ticket to go to each concert (B, X, or G). Even though, we have been bored, we cannot immediately go to a concert. We need to first pick our ticket:
And then we can go to our concert:
Of course, the data choices impact what we can do in Declare; now we go to the Xtine Concert and get a decent ticket:
We see that even though we have a Britney ticket, we cannot go to the Britney Concert due to the Declare constraint. CPN Tools cannot currently prevent such conflicts as this requires a full state-space analysis.
Aside from adding a data perspective to Declare, the union of the two languages has another advantage: they each have their own domains of comfort. Declare is good for very abstract processes, or processes where a lot of freedom, whereas CPN models are good for providing guidance. Basically, any part of a model requiring an xor-split (choice), should be done with a CPN fragment. Consider what the difference is between the following two models. First see if you can spot the difference, then try building the models in CPN Tools and try it out!
I hope you have fun with Declare in CPN Tools 4 and find it useful!
Time person of the year 2006, Nobel Peace Prize winner 2012.