Statestep Tutorial

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:

Update = {time-sec} -> {time-_1min} -> {time-_10min} -> {time-hour} -> {cal-mon} -> {cal-date} -> {cal-day} -> {cal-year} -> {mode} -> {none}

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:

Rule with formula for toggling

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:

(Alarm1 = {beeping} || Alarm2 = {beeping})

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:

Rule with silence alarms formula

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