Example declarations

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`s	1`d(2)
  DBM.all()	1`d(1)++1`d(2)++1`d(3)++1`d(4)
  DBM.all()--1`s	1`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.