# Using Formulas for Constraints

Previously, we saw how to use the constraint table to define constraints and see their effects. However, there are two kinds of constraint which can't be expressed in the constraint table:

- certain constraints involving more than two variables
- constraints which relate to an event

These constraints have to be expressed as formulas.

## Constraints with more than two variables

Consider the constraint

- where "&&" is read "and". This is equivalent to two separate constraints, each of which could be put in the constraint table:

Weather = {fog} => Wind = {calm}

Suppose, however, we have the constraint

meaning, "If it's cold then either it's foggy or snowing or there's a gale blowing" (that is, '|' and "||" both mean "or"). Unfortunately, this can't be broken up into simpler constraints - and, because it involves more than two variables, there is no way to express it in the constraint table. Instead, we just have to use the formula itself to define the constraint.

To do this, first load "activities.s2" once more. Next, go to the

menu and select . In the window that appears, click the button, enter an identifier for the constraint ("dubious", say) and then enter the formula into the box that appears. The constraints window should then look like this:

Open the constraint table window and set the
display options to show derived inferences.
The new constraint seems to have no effect.
In fact, the constraint table does take the
new constraint into account;
it's just that it's not possible to derive anything
from it that can be shown in the table.
For example, if `Temperature` is `cold`
then `Wind` can still have any value.

However, we can see the effect of the constraint in
another way.
Using the menu,
open a rule navigator window.
A rule navigator is a kind of temporary or scratchpad rule.
You can read more about rule navigators and their uses
later in the appropriate Help page.
For now, just edit the cells on the top row of the table
for `Temperature` and `Weather`,
selecting `cold` in the first and
`fine` in the second.
You should then see that `Wind` can have only
the value `gale`.

Right-click in the table cell for `Wind` and
select the function.
The explanation, of course, is simply the constraint
defined above, given the values already selected for
`Temperature` and `Weather`.

What happens to the formula if a variable or variable
value mentioned in it is renamed?
Open the variables window, select the
`Temperature` variable and give it a new name,
say, "Temp".
As you can see, the formula is updated automatically.

What if a variable or value is deleted?
In the variables window, select `Weather`
and delete the value `fog`.
Now look at the constraint again:
the '#'s that are added turn each of the
lines of the formula into comments.
Comment text is ignored by Statestep and so
the constraint no longer has any effect.
It is up to you to fix a "commented out" formula
and remove the leading '#'s - or to delete the
constraint, if it's no longer relevant.
Statestep could try to update formulas automatically
as it does after a variable renaming but, in general,
it's not possible for it to do this reliably.

## Event constraints

All of the constraints we've seen so far were global constraints, that is, facts that must always be true. There is another kind of constraint, called an event constraint. An event constraint is something that can be assumed to be true whenever a particular event occurs. In other words, we know the event cannot occur except when the constraint is satisfied.

For an example of this, open
"harelsWatch.s2" again.
Go to the constraints window and click on the
`alarm_beep_timeout`
from the list of events that appears.
You should see one constraint listed, expressing the
fact that a beep timeout can occur only
if one of the alarms is beeping.

This event constraint tells the tool that the rules
for the beep timeout event don't need to cover cases
where neither of the alarms is beeping.
To see what would happen without it,
open the rules window and make sure the
`alarm_beep_timeout` event is visible in it.
Now, go back to the constraints window, select the
constraint (click once on it) and delete it.
Notice that a
'U'
appears beside `alarm_beep_timeout`
in the rules window.
This is a warning that there are now uncovered cases
for this event (the cases which the constraint said
were impossible).

We haven't quite covered the full constraint formula syntax in the tutorial; you can do this later by going to the help page for the constraints window.

Next: Formulas for Rules