Cardinality

Cardinality is a way of expressing variability among concepts. In the first car example we said that a car has a radio. In the real world, however, this is not necessarily the case. Some cars have radios, others do not. To represent different car variants in a single Clafer model we use cardinalities. Cardinality is as single number or an interval that follows clafer’s name. It specifies how many instances of a given clafer can appear as children of the instance of the parent clafer. Let us refine the car model:

car
  engine
  radio ?
    cdPlayer

The question mark following radio indicates that radio is an optional element of a car. The question mark is a shorthand for 0..1. The first number gives minimal bound, the second maximal bound. We did not explicitly specify cardinalities of other elements. What are their cardinalities? Clafer assumes that by default clafers are mandatory and their cardinality is equal to 1..1. It allows us to write Clafer models more concisely. The same model, but with explicit cardinalities is shown below. Please note that 1 has the same meaning as 1..1.

car 1
  engine 1..1
  radio 0..1
    cdPlayer 1

As in the first example, a car must have an engine. It may have a radio; if it has a radio, then the radio plays CD’s, otherwise it does not. The example of a car with optional radio represents two valid car configurations:

1. A car with a radio (and a CD player)
   

   car
     engine
     radio
       cdPlayer

2. A car without a radio (and without a CD player)
   

   car
     engine
     radio 0
       cdPlayer 0

Any other configuration is invalid. For example, let us look at:

car
  engine
  radio 0
    cdPlayer 1

The radio clafer is followed by 0, which means that car has no radio. Under radio, however, we specified that cdPlayer ’s cardinality is 1. Although the above example is syntactically correct, it represents an invalid configuration. Such a model is inconsistent, because it makes not sense to have a CD player if the radio is not installed. Clafer comes with tool support (e.g., Clafer-to-Alloy translator) that automates checking consistency of models.

FAQ

What is the syntax for specifying cardinalities?

The are for ways of specifying cardinalities:

1. Using the default cardinality, e.g. car
2. As a single number, e.g., car 5.
3. As an interval, e.g., car 2..7, car 1..*. The latter means that there is at least one car.
4. Using one of the symbols: car ? (optional, i.e., 0..1), car + (some, i.e., 1..*), car * (any, i.e., 0..*).

---

What does it mean that cardinality specifies how many instances of a given clafer can appear as children of the instance of the parent clafer?

It means that cardinality is not a number of all possible instances under all parents, but a number of clafer instances under a given instance of the parent. Let us look at the the example:

car 10
  door 4

In the example we have 10 cars, and each car has 4 doors. So in total we have 40 instances of door. If the door cardinality constraint specified the number of doors under all parents, then we would have 4 doors in total.