This page provides a detailed description of the set of declarations from the CPN for the Distributed database which is one of the example nets. The Declarations

## Explanation

• `val n = 4;`: Declares a value (i.e., a constant). In this case the constant `n` is bound to the value `4`.
• `colset DBM = index d with 1..n;`: Declares an index color set named `DBM`. The color set consists of the set of elements {`d(i)` | i = 1..`n`}, i.e. the set {`d(1)`,`d(2)`,`d(3)`,`d(4)`}.
• `colset PR = product DBM * DBM;`: Declares a product color set named `PR`. Each value (i.e. color) in `PR` is a pair, where each element of the pair is of type `DBM`. The values in `PR` have the form `(d(i), d(j))` where `i` and `j` are integers between 1 and 4. For example, the value `(d(1),d(4))` is an element in `PR`, but the value `(d(1),d(10))` is not an element in `PR`.
• `fun diff(x,y) = (x<>y);`: Declares a function named `diff` which has two formal parameters `x` and `y`. The function returns `true` if the values bound to `x` and `y` are not equal, otherwise returns `false`.
• `colset MES = subset PR by diff;`: Declares a subset color set named `MES` which is a subset of the color set `PR`. The color set `MES` consists of the values of `PR` that are mapped to `true` by the function `diff`. For example, the value `(d(1),d(2))` is in `MES`, but the value `(d(3),d(3))` is not in `MES`.
• `colset E = with e;`: Declares an enumerated color set named `E`. The only element in `E` is the value `e`.
• `fun Mes(s) = PR.mult(1`s, DBM.all()--1`s);`: Declares a function named `Mes` which has one formal parameter `s`. The function `Mes` returns a multiset of elements from the color set `PR`.
The multiset that is returned by `Mes` is generated using the function `PR.mult`. The function `mult` is one of the color set functions that is available for product color sets. The two arguments for the function `PR.mult` are multisets of elements from the color set `DBM`. The first argument consists of the multiset `1`s`, i.e. the multiset consists of a single element, and the value of the element is determined by the binding of the parameter `s`.
The second multiset is generated using the `DBM.all` function and multiset subtraction. Evaluating the color set function `DBM.all()` will result in the multiset with one of each element from the color set `DBM`.
Suppose `Mes(d(2))` is called, in which case, the formal parameter `s` is bound to the value `d(2)`. The results of evaluating subexpressions in the body of the function `Mes` are described below:
Expression Evaluates to
1`s1`d(2)
DBM.all()1`d(1)++1`d(2)++1`d(3)++1`d(4)
DBM.all()--1`s1`d(1)++1`d(3)++1`d(4)
PR.mult(1`s,DBM.all()--1`s)1`(d(2),d(1))++1`(d(2),d(3))++1`(d(2),d(4))
Mes(d(2))1`(d(2),d(1))++1`(d(2),d(3))++1`(d(2),d(4))
• `var s,r : DBM;'`‘: Declares two variables, `s` and `r`, which have type `DBM`.

## Size of color sets

All of the color sets in this example are small, i.e. they contain a finite number of elements. More information is available about the size and complexity of color sets.