# Using Formulas for Rules

In addition to purely tabular rules, like those we've seen so far, Statestep provides the option of using a formula to help define a rule. Rule formulas can be helpful where the only alternative is to define many very similar tabular rules.

*This is a relatively advanced topic.
As it's never strictly necessary to use a rule formula,
you may prefer to
skip this section
for now.
*

## An example

The easiest way to learn about rule formulas is by
looking at some examples.
Open up "harelsWatch.s2" once more and, in
the rules window, select the event `c_pressed`.
If you now look at any of the rules from `_6` to
`_14`, you'll notice that they're rather
repetitive.
In fact, all these rules differ only in the values of
the variable `Update`.

Using a formula, it's possible to replace all these rules
with just one rule.
We'll do this by editing rule `_6`
so that it models the behaviour of rules
`_7` to `_14` as well.
First, in the top row of the table for rule `_6`
select all the values for `Update` except
`none` and `pending`.
Notice that rule `_6` now conflicts
with rules `_7` to `_14`.

Next, in the bottom row, select all the
values except `time-sec` and `pending` -
that is, all the values to which `Update` changes
in rules `_7` to `_14`.
At this point, we have a non-deterministic rule: it
allows `Update` to change to any of several values.

Notice that the conflicts have changed back to overlaps.
Like violations, conflicts are not reported if
non-determinism means a way can be found to make the
rules agree.
For example, our modified rule `_6` agrees with
rule `_10` in that it allows `Update`
to change from `cal-mon` to `cal-date`.
It doesn't matter that it also allows it to change to, say,
`time-hour` instead.

Rule `_6` is non-deterministic because it is
missing some information: how to choose the next value of
`Update`.
We can now provide this information as a formula.
To do this, enlarge the rule window by clicking and
dragging the top or bottom edge with your mouse.
Double-click in the empty region that appears at the
bottom of the rule and enter the following formula in
the window that appears:

This formula describes exactly what the value of the
variable `Update` is in the next
state, given its current value: if it is
`time-sec`, it changes to `time-_1min`;
if it is `time-_1min`, it becomes
`time-_10min`, and so on.
When you've finished editing the formula, it is
incorporated into the rule:

The difference between this formula and the comments we saw earlier is that Statestep understands and checks it. To verify this, edit the formula so that, instead of ending with "... {mode} -> {none}", it ends with (say) "... {mode} -> {cal-day}". You will find that one of the overlaps has changed to a conflict. Open the conflicting rule to see the contradiction.

When you have restored the formula to the correct version,
you can delete rules `_7` to `_14`
- since all the information that was in these rules is
now contained in rule `_6`.
Using a formula has thus allowed us to replace nine rules
with just one.

## Another example

For a more advanced example of what's possible with
a rule formula, take a look at the first
three rules for the event `a_pressed`:
Rule `_1` specifies what happens if
`Alarm1` and `Alarm2` are both
beeping;
rules `_2` and `_3` give the
response when only one of the two alarms is beeping.
In all three rules, the response is simply to
silence the beeping alarm(s), leaving the other
variables unchanged.

Again, with the help of a formula, this behaviour
could be expressed in just one rule.
Modify rule `_1` so that it applies regardless
of the values of the two alarms, that is, select
"don't care" in the top row of the table
for each of these variables.
On the bottom row, let the value in the next state
for these variables be either of the sub-values
of `quiet` (if either alarm starts with
the value `quiet-disabled` we want to allow
it to remain unchanged, as currently happens in
rules `_2` and `_3`).

At this point, you'll notice quite a few conflicts. That's because the rule now also covers cases where neither alarm is beeping. We want the rule to apply only when at least one of the alarms is beeping. To limit the rule to these cases, add this formula:

However, this still leaves us with a non-deterministic
rule since in the table we've only limited the alarms
in the next state to one of two values
(`quiet-enabled` or `quiet-disabled`);
we haven't specified exactly how it is decided which
of these is chosen.
To do this, the formula can be amended so that
the completed rule looks like this:

If this looks obscure, don't worry; the main goal here is
to get a feeling for what can be done with formulas.
Here's what it means:
There are now three parts to the formula, separated by
logical "and" operators ("&&").
The first part is as before.
The two additional parts tell us how to derive the
new values of `Alarm1` and `Alarm2`
respectively.
In each case, either the alarm is `beeping`,
in which case it changes to `quiet-enabled`,
or it is `quiet-*`, in which case it stays
the same (that is, `quiet-enabled` if it was
`quiet-enabled` or `quiet-disabled`
if it was `quiet-disabled`).

Rules `_2` and `_3` can now be
deleted.
Although this last formula has allowed us to reduce
the number of rules by two, it's worth reflecting on
whether this actually improves the model.
The formula is a good deal more difficult to
understand than the one in the previous example.
Even for programmers and those used to this kind of
representation, it takes longer to parse
and understand than a purely tabular rule and is
more likely to be the source of a mistake.

In any case, if you use a formula like this, it's a good idea to at least include a comment before it for those who won't understand the notation. In this case, for example, something like "One or both alarms are beeping; any beeping alarm is silenced but remains enabled," might suit.

If you wish, you can define rules using only formulas, leaving the table cells empty. The colours of the (unselected) values shown in the table should still help in editing the formulas and finding uncovered cases.

*Exercise: If you feel comfortable with what you've
seen so far, find out what happens when a formula
contradicts the tabular part of a rule.
*

These are introductory examples; for a fuller description of rule formulas, you can look at the help page on the subject later.

Next: Autodeletion of Rules