CPN Tools 4: Declare Constraints

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 its own tool, also named Declare. Everything herein can be done with CPN Tools pre-releases starting from 3.9.2; get your copy here.

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:

  1. If you are bored, you should go to a concert.
  2. You can go to different concerts.
  3. Never, can you go to both a concert with Britney and a concert with Xtina.
  4. Only persons going to a Britney concert can ever be truly happy.

A CPN model mostly satisfying this, can be seen below.

Screen Shot 2013-08-14 at 17.31.53

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:

Screen Shot 2013-08-14 at 17.42.20

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:

Screen Shot 2013-08-14 at 17.45.44

Now all three concerts are enabled (there are tokens on the place).  Executing Britney Concert leads to:

Screen Shot 2013-08-14 at 17.47.20

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.

Intelligent Prediction

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:

Screen Shot 2013-08-14 at 17.50.46

The existence constraint above True Happiness forces execution of this transition. Executing Bored now leads to this state:

Screen Shot 2013-08-14 at 17.52.04

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.

Screen Shot 2013-08-14 at 17.57.22

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 Tools, but are always applied between two transitions. Neither of the transitions can be a substitution transition. If we start a constraint from one transition and click on the background, we add a bend-point, and if we double-click on the background, a new transition is created and the constraint attached. Unary constraint are just applied to existing transitions.

The constraints are separated into 5 groups:

Screen Shot 2013-08-14 at 17.58.05
  • 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:

Screen Shot 2013-08-14 at 18.17.02

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:

Screen Shot 2013-08-14 at 18.18.22

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:

Screen Shot 2013-08-14 at 18.19.51

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:

Screen Shot 2013-08-14 at 18.30.12

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).

Screen Shot 2013-08-14 at 18.49.12

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):

Screen Shot 2013-08-14 at 18.52.16

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).

Incremental Check

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:

Screen Shot 2013-08-14 at 19.07.41

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:

Screen Shot 2013-08-14 at 19.09.30

And then we can go to our concert:

Screen Shot 2013-08-14 at 19.11.04

Of course, the data choices impact what we can do in Declare; now we go to the Xtine Concert and get a decent ticket:

Screen Shot 2013-08-14 at 19.12.21

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.

Mixing Paradigms

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!

Screen Shot 2013-08-14 at 19.20.29
Screen Shot 2013-08-14 at 19.21.55

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.

8 thoughts on “CPN Tools 4: Declare Constraints

  1. Hi Michael, this is really a detailed description of Delare. It helped me so much! In addtion, I am confused about the ‘exp’ on binary constraints. I mean, when I click a binary constraint which has already connected two transitions, a default ‘exp’ would show up on the constraint. I would like to know what it is used for.
    Thank you!

    1. Hi Carina,

      Glad you found it useful. I was planning on sending you the link directly, but forgot.

      The expression is currently not used, but I’m planning on making an extension also allowing values on Declare constraints as well as time stamps. More about timed Declare in this presentation: https://westergaard.eu/2012/08/looking-into-the-future-a-priori-advice-about-timed-declare-process-models/ and more about colored Declare here: https://westergaard.eu/2013/03/modeling-is-not-just-for-supermodels/

      I’ll just disable it for the release to not confuse anybody.

  2. Hi Michael, I am confused about the green triangle on the bottom left of transition “Get Ticket”. I would like to know How to add “ticket=? B G X” to the transition. Thank you!

  3. Hello
    I am working with version 4.0 of CPN TOOLS because I want to create a process model and from these generate event logs associated, I have been studying their publications and are very good and instructive, but priate want to try different types of statements you used does not leave me, as if he were locked in the program, that you think might be this.
    My other question I have not found in any of their publications on the blog is in generating event logs designed models, if you have any materials or help I would appreciate.

    1. There’s two suggested ways of creating logs. One is using the CPN-XES library (see https://westergaard.eu/2011/07/prom-package-documentation-keyvalue/); it is basically the same library as the old ProM CPN library, so most of the documentation applies.

      Alternatively, just import the simulation log created in CPN Tools into ProM. This is also covered in the KeyValue documentation. Any information you need in the log needs to be in the simulation log, so make sure it is available in the trantiion name or in variables around the transition.

  4. Hi Michael,
    I have modeled a process model where i use this declare constraint, it is working fine but when ever i m entering to state space analysis is shows error as “Declare Constraints not supported with state space generation”. I would like to know how to generate state space analysis report with declare constraints. Thank you.

Leave a Reply

Your email address will not be published. Required fields are marked *

This site uses Akismet to reduce spam. Learn how your comment data is processed.