Algebraic variables and equations

Consider the following CIF specification:

``````automaton car:
event start, stop, breakdown, start_repair, repaired;

alg bool can_drive = idle or moving;

location idle:
initial;
edge start goto moving;

location moving:
edge stop goto idle;
edge breakdown goto broken;

location broken:
edge start_repair goto repairing;

location repairing:
edge repaired goto idle;
end``````

The `car` is initially `idle`. Once you `start` driving, the car is `moving`. Once you `stop` driving, the car is `idle` again. While `moving` it is possible for a `breakdown` to occur, meaning the car is `broken`. Once a mechanic starts the repair (`start_repair`), the mechanic is `repairing` the car. Once it is `repaired`, the car is `idle`, and you can `start` driving it again, etc.

Algebraic variable `can_drive` indicates whether you can currently drive the car. As the value calculation indicates, the car can be driven whenever it is `idle` or `moving`. That is, it can’t be driven if the car is `broken` or a mechanic is `repairing` it.

In the example above, the value of the algebraic variable is defined with the declaration, as was already explained in the lesson that introduced algebraic variables. However, it also possible to specify the value separately, using an equation:

``````automaton car:
event start, stop, breakdown, start_repair, repaired;

alg bool can_drive;

equation can_drive = idle or moving;

// Locations omitted for brevity.
end``````

This allows for separation of variable declarations and equations. Both variants have the same algebraic variable with the same value. An equation of an algebraic variable must be placed in the same component as where the algebraic variable is declared. In the example above, the equation for algebraic variable `can_drive` must be placed in automaton `car`, as that is where the algebraic variable is declared.

For algebraic variables declared in automata, it is also possible to specify the value using an equation per location of the automaton:

``````automaton car:
event start, stop, breakdown, start_repair, repaired;

alg bool can_drive;

location idle:
initial;
equation can_drive = true;

edge start goto moving;

location moving:
equation can_drive = true;

edge stop goto idle;
edge breakdown goto broken;

location broken:
equation can_drive = false;

edge start_repair goto repairing;

location repairing:
equation can_drive = false;

edge repaired goto idle;
end``````

Every algebraic variable must have a unique value in every situation. Algebraic variables must thus have a value with their declaration, a single equation in the same component, or an equation in every location of the automaton. For every algebraic variable, one of the three variants must be chosen. It is allowed to choose a different variant for different algebraic variables, but it is not allowed to use multiple variants for the same algebraic variable.

Which variant fits best for a specific algebraic variable, depends on the situation. One of the benefits of using an equation per location, is that the equations are checked for completeness. If you add a new location, you must add an equation to that location as well, as otherwise the model is invalid (incomplete). This means you can’t forget to specify the value of the algebraic variable for that new location. If you use a value with the declaration or a single equation in the component, you might forget to update the value for the changes you made to the automaton.