# linking the jurisdiction and the system

So far we modeled the traffic light system as follows:

Given our choices of the various jurisdictions:

we can use `constraints`

to restrict parts of the
system.

In Clafer, constraints are formulas of type Boolean and they can be
arbitrary first-order logic formulas containing Boolean operators (and:
`&&`

, or: `||`

, not: `!`

,
implication: `=>`

, equivalence: `<=>`

),
set operators (equality `=`

, union: `++`

or
`,`

, subtraction: `--`

, intersection:
`&`

) and quantifiers (not exists: `no`

,
exactly one: `one`

, exists: `some`

, for all:
`all`

) extended with a few relational logic operators
(relational join: `.`

, domain restriction:
`<:`

, range restriction: `:>`

). The
constraint language also supports integers and integer formulas
(operators: `+ - * / ^`

and comparisons:
`> >= < <= =`

) and string literals
(`"some text"`

). Finally there is a set cardinality operator
`#`

to compute the size of the set and a ternary operator
`if then else`

. For details, see the grammar.

Similarly to OCL, constraints are always declared in the
**context** of some clafer, meaning that the constraint
must hold for every instance of that clafer.

Unlike in OCL but similarly to Alloy, constraints always work on sets
and relations, never on scalars—a scalar is a singleton set.

In our model, we’d like to say that certain jurisdictions require the presence of certain clafers in the instance. For example, in Europe, the green arrow lamps are used and the lights are mounted in front of intersections. We add the constraints as follows:

The constraints are expressed using square brackets `[ ]`

.
Each clafer is interpreted as a set and the default quantifier is
`some`

, which means `exists`

. The first
constraint, illustrates an implication
`if there's an instance of Europe then there must be an instance of leftGreenArrow and an instance of rightGreenArrow`

.
The quantifier `some`

can be omitted, as shown in the next
two constraints.

The second constraint, illustrates full qualification using the
relational `join`

oprerator `.`

:
`Jurisdiction.Europe`

is a set of instances of the clafer
`Jurisdiction`

joined with the relation `Europe`

(a clafer semantically really is a relation but the join produces a set
as in Alloy be ignoring the column on which the join is performed). The
Clafer compiler automatically adds the necessary qualification as long
as a given clafer can be referenced unambiguously. This is why, in the
first and the third constraint, the explicit qualification was
dropped.

More information: Tutorial: Constraints

Let’s see what instances we will get now, assuming that we want to
restrict the system to UK only. We therefore add another constraint to
require the presence of an instance of `UK`

as our
jurisdiction.

After generating the instances, you can edit the model directly in the configurator.

- Enlarge the view
`Input Clafer Model and Options`

using window size buttons . - Change the constraint
`[UK]`

to`[Canada]`

.

After each change, the model must be recompiled.

- Close the instance generator by pressing the button
`Quit`

. - Press the button
`Compile`

right above the text editor. - Generate the instances again by pressing
`Run`

.

The fact that we see only one instance for UK is good—it means the
system is fully configured. However, for Canada, we get four instances
which means that the system is only partially specified—we still need to
make decisions about the green arrows (e.g.,
`[ leftGreenArrow ]`

and
`[ no rightGreenArrow ]`

). An easy way to make and save
decisions is to select or eliminate clafers in the matrix view and copy
the corresponding constraints from the view
`Constraints`

.

Let’s look at some more differences across the jurisdictions: nested constraints.

**Previous**