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.
10 thoughts on “CPN Tools 4: Declare Constraints”
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.
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.
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!
This is not something you add – it’s the result of using manual binding (see http://cpntools.org/documentation/gui/palettes/simulation_tools/bind_manually) The green triangle is a shortcut for opening this. You only see variables if they exist around the transition (like in the example).
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.
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.
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.
You don’t. As the message says that is not supported. Declare constraints have a implicit notion of state not supported by the state space tool.
i want to know how to use OR operator in cpn tools?
As i want to execute different processes one by one.
CPN Tools is not a BPM system, so it does not have a notion of an OR operator. you can simulate the behavior of an OR operator, though. How to do that depends on the exact OR semantics you are going for.
For a simple XOR semantics, create a place with a shared black token and allow any subprocess to consume that. You can make a join by having all processes produce a black token on another place.
For more complex semantics, you can use a single place with a shared token and double arcs to all subprocesses if subprocesses can be executed more than once. Join by consuming the shared token.
Another semantics would only allow each subprocess to be executed once by creating a separate place with a black token for each subprocess and let each consume this token. Produce a token on each place in the split and consume them all using reset arcs in the join.
A third semantics would force each subprocess to be executed exactly once but in any order, and could be created by again creating a place for each subprocess and have them consume a single black token from this place. Now, have each process also produce a token on a shared output place, and in the join consume the exact number of black tokens corresponding to the number of subprocesses.
If it is possible to enter the OR component more then once simultaneously, you need to use identifiers instead of black tokens to keep the two invocations separate (this will not work with reset arcs).
Hope this helps!