Declare adheres to the declarative workflow modeling paradigm, where, instead of modeling allowed behavior and explicit choices, users model disallowed behavior. This makes it easier to model loosely structured processes. Without appropriate precautions, however, users are less supported in choosing which actions lead to the desired endresult. The goal of Declare is to ensure flexibility when modeling loosely structured processes and, at the same time, to provide support for decision making during the execution. Declare consists of a Designer component for creating and verifying models, a framework which acts as a server for enacting models, and a Worklist, which allows users to see and pick tasks to perform. Declare can act as a client of the operational support service in ProM, which makes it possible to guide users towards desired goals, to obtain statistics about an executed process, and to monitor a running case. In addition to this, a ProM plug-in has been also implemented that allows for the discovery of Declare models from logs.
is forbidden, declarative models are “open” and tend to offer more possibilities for execution.
Declare [
In the screenshot in Fig. 1, we see the Declare Designer with a loaded model consisting of a number of tasks and constraints. Here, tasks are shown as rectangles (e.g., Money) and constraints as arcs between them (e.g., response between Low Risk and Bonds).
The model in Fig. 1 models a simple stock investment strategy and contains tasks related to that, such as getting Money, purchasing Stocks or Bonds, and a desire for Low Risk and High Yield. The constraints restrict the allowed behavior. The constraint alternate response from Money to Bonds and Stocks reflects that if you get money, you should invest it (in Bonds or Stocks). The precedence constraint between Stocks and High Yield models that only if you invest in stocks can you subsequently get high yield (but there is no guarantee). The not coexistence between Bonds and High Yield states that you can never get high yield if you invest in bonds. Finally, the response constraint between Low Risk and Bonds states that if you want low risk, you must invest in bonds.
Declare supports constructing such models using a graphical editor, the Declare Designer. The Designer can also verify that a model is consistent. Suppose, for instance, we add to the model in Fig. 1 a constraint saying that if we want Low Risk we must subsequently obtain High Yield. Declare can then detect that in the resulting model Low Risk can never be executed (as we subsequently have to execute both Bonds and High Yield, which is not allowed by the not co-existence constraint). Declare is also able to pinpoint the exact reason of the inconsistency as shown in Fig. 2. This is possible as Declare has a formal semantics, realized by associating with each constraint an LTL formula, which can be used to translate a Declare model to a finite automaton for analysis.
We can also use that automaton to enact the model, ensuring that we never execute events that would violate constraints. Enactment is done using the Declare Framework as the backend server and the Declare Worklist as the user client. When enacting a Declare model, one or more constraints may be temporarily violated. This is reported to the user, who can take appropriate actions. For instance, in Fig. 3, we see an execution where we have just obtained money. The constraint alternate response is temporarily violated, shown using orange color instead of green (used for satisfied constraints). To satisfy the temporarily violated constraint, the user can execute Bonds or Stocks. Note also that all tasks except High Yield can be executed. High Yield is disabled because its execution would violate the constraint precedence.
Due to the declarative nature of the Declare models, it is not always easy
to foresee the effects of choices during the execution of a process. To guide
users in the decision-making task, it is possible to integrate Declare with the
operational support service in ProM [
Using the operational support service, it is also possible to monitor a running process w.r.t. a given Declare model and get health information about it. This is completely orthogonal to the Declare Worklist application. In this case, the Monitor only observes the behavior of a process which executes independently and detect possible violations. In Fig. 5, we see the Declare Monitor in action. Here, 4 instances of our example process are being executed (as shown by instances Smith, Westergaard, Brown, and Maggi). The Monitor provides at-aglance information about the health of all instances, by adding the text Warning in red after an instance if it has violated constraints. In the example in Fig. 5, the instance Brown violates the precedence constraint after executing High Yield. The status of each constraint is updated after each executed event (displayed on the horizontal axis). We additionally get a measure of the overall health of the instance at the top. We see that violating the precedence constraint lowers the health to 0.69. Furthermore, the Diagnostics panel provides users with additional information about violated constraints.
As well as manually creating a Declare model using the Designer, users can
also discover models from logs using the Declare Miner [
Declare is an advanced prototype, which supports models of real-life size.
The Declare Miner and the Monitor have been used in the Poseidon project 1 to
monitor sea vessels. In particular, in [
Declare models from real-life historical data and monitor live data w.r.t. to the mined model. We consider Declare stable enough for evaluating declarative approaches. Declare is open source (licensed under the GNU Public License). Binaries and source code can be obtained from its homepage at declare.sf.net.