Statestep Tutorial

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:

These constraints have to be expressed as formulas.

Constraints with more than two variables

Consider the constraint

Weather = {fog} => Temperature = {cold} && Wind = {calm}

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

Weather = {fog} => Temperature = {cold}

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

Suppose, however, we have the constraint

Temperature = {cold} => Weather = {fog | snow} || Wind = {gale}

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 Model menu and select Constraints. In the window that appears, click the New 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:

Constraint: dubious

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 Explore 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.

Effect of constraint in rule

Right-click in the table cell for Wind and select the Explain 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 Event tab at the top. Now, click on the field at the top of the panel and select 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.

Alarm1 = {beeping} || Alarm2 = {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