## Data Constraints

Data constraints impose conditions on the parameter values in observed events. The intuition behind data constraints is: if a sequence of events is observed then a condition over the observed parameters is satisfied.

Events have the same syntax as the events in timing constraints. In addition, event parameters can be variables that are bound to actual values when the event is observed.

Below is the general structure of data constraints specifications:

    data constraints

    variables

    //Variable declarations
    Type1 VariableName1
    Type2 VariableName2
    ...

    //Constraints with the following general structure

    constraintName step1; step2; ... ; step_n where condition_boolean_expression

A step can be one of the following:

- event, e.g. notification Done

- no[event]: a negation of event, e.g. no[command putMoney]
  matches an observed event if it is different than the negated event

- body (event or negation of event) until stop condition (event or negation of event): repetition of events until a given event is observed
  matches a sequence of observed events in which the last one matches the stop condition and the preceding (possibly none) events match the body

This is an example of a data constraint that checks if the reply to a command has the same parameter value as the first command parameter:

`command A(X, *); any event until reply(Y) where X == Y`

For a more complex example, consider a component that provides communication channels to its clients. Channels have a given bandwidth. Clients can request a communication channel by sending asynchronously the signal openChannel with the desired bandwidth as a parameter. The component tries to open the channel and notifies the client by sending a notification channelStatus with two parameters: a boolean value that indicates the success/failure of the channel opening action and the actual bandwidth. A requirement on this protocol is that in case of success, the reported bandwidth must be the same as the requested bandwidth. In addition, while trying to open the channel, the component may continue receiving commands and signals and sending notifications.

The stated requirement can be formulated as the following data constraint rule:

    data constraints

    variables

    int requestedBandwidth //variable to be bound to the value of the requested bandwidth
    int confirmedBandwidth //variable to be bound to the value of the confirmed bandwidth
    bool status //variable to be bound to the status of the request

    bandwidthEquality //name of the data constraint
    signal openChannel(requestedBandwidth); //if the signal is observed
                                            //the parameter value is assigned to variable requestedBandwidth
    any event                               //any event may occur while waiting for confirmation
    until
    channelStatus(status, confirmedBandwidth) //this event marks the end of the searched sequence of events
    where

    //the condition is equivalent to: if status is true then the bandwidth values are equal
    //stated more formally: status => (requestedBandwidth == confirmedBadwidth)
    //since the CommaSuite framework does not support implication, we use the well known equivalence:
    //(G => F) <=> (NOT G OR F)

    (NOT status)
    OR
    (requestedBandwidth == confirmedBandwidth)

Similarly to time constraints, an optional when condition can be used in the events provided that the data constraint is defined in an interface definition. Note that interface variables that are allowed in the when condition cannot be used in the where condition.

During monitoring, data constraints may generate statistical information written in the statistics files. This information is in the form of name/value pairs and is visualized in the dashboard page (see the help pages on monitoring and monitoring results).

Users need to specify explicitly the name and the expression used to calculate the value. For example, consider the following data constraint:

    DR1 command sum(X, Y); reply(Z) where X + Y == Z
    observe
    expected := X + Y
    received := Z

Every time this constraint is evaluated, the values of variables expected and received will be stored in a file. The optional observe section defines at least one variable and its expression. If no observe section is given then no statistical information will be saved.