Version:
v12.0-M1
[release notes]

# Module 2.7: Constants and algebraic variables

So far, in our models, we have only used discrete variables. Discrete variables hold a value, which can be used in for instance guards, and can be updated by assignments on edges. We will now introduce constants, that hold a fixed value, and algebraic variables, that hold a value that is computed from other values, such as those of constants and discrete variables. We will introduce these new concepts through an example.

## Example

Consider the following model of a bridge, with a bridge deck, a bridge light and a car:

                                automaton bridge_deck:
                                    disc int angle = 0;
                                    event open_further, close_further;

                                    const int step = 10;

                                    alg bool is_open   = angle >= 90;
                                    alg bool is_closed = angle <= 0;

                                    location:
                                        initial;
                                        edge open_further  when angle < 90 do angle := angle + step;
                                        edge close_further when angle >  0 do angle := angle - step;
                                end

                                automaton bridge_light:
                                    event turn_on, turn_off;

                                    alg bool is_on = On;
                                    alg bool is_off = Off;

                                    location On:
                                        initial;
                                        edge turn_off goto Off;

                                    location Off:
                                        edge turn_on goto On;
                                end

                                alg bool car_may_drive     =     bridge_deck.is_closed and bridge_light.is_off;
                                alg bool car_may_not_drive = not bridge_deck.is_closed or  bridge_light.is_on;

The `bridge_deck` automaton models the bridge deck. The bridge deck can open or close. If the deck is closed, and thus horizontal, cars can drive over it. As it opens, its angle compared to the road increases from 0 to 90, and cars can not drive over it. Since the automaton has only a single location, its name is left out. There are two edges, one to open the deck a bit further, and one to close it a bit further. Each occurrence of one of these events opens or closes the bridge deck a bit, changing its angle by a number of degrees. Since opening and closing the deck is done in increments of ten degrees, a constant `step` is defined to hold this value.

Constants are declared using the `const` keyword. Like variables, constants have a name, a type and a value. In this case, a constant named `step` is defined of type `int` and with value `10`. Like variables, constants can also have a different type, such `bool` or `real`. Constants hold a fixed value that can not be changed by assignments. Still, constants can be useful. By giving a value a name, the name can be used instead of the value. This can make models more readable, as you don't have to guess what the value represents. Furthermore, if the constant is used in multiple places, then changing the value of the constant has an affect in all places where it is used. This makes it easier to change values that are used multiple times in the model, and thus to keep the model consistent after such changes.

The bridge deck is open at 90 degrees and closed at 0 degrees. The bridge deck automaton has two algebraic variables `is_open` and `is_closed`, that model sensors that indicate whether the bridge deck is open or closed, respectively. An algebraic variable are declared using the `alg` keyword and have a name, a type and a defining expression. The expression represents a computation that produces the value of the algebraic variable, and this computation may make use of constants and other variables. For instance, algebraic variable `is_open` has a `bool` type. Its value is thus either `true` or `false`. Its defining expression is `angle >= 90`, which indicates that if the bridge deck's angle is at least 90 degrees, then the bridge deck is open. The `angle` refers to the discrete variable named `angle`. The value of the algebraic variable `is_open` thus depends on the value of the discrete variable `angle`. If `angle` is at least 90, then `is_open` is `true`, and otherwise, if `angle` is less than 90, then `is_open` is `false`. The algebraic variable can't be assigned a new value. Instead, its value is at all times determined by its defining expression. But, assigning a different value to discrete variable `angle` may lead to `is_open` getting a different value as well. That is, if `angle` is `80` and the `open_further` edge is taken, then `angle` becomes `90` and the value of `is_open` automatically changes from `false` to `true`. Similarly, the value of algebraic variable `is_closed` also changes based on the value of discrete variable `angle`, and is only true if the `angle` is at most zero.

If the values of the sensors would instead be modeled as discrete variables, they would need to be updated on every edge where the value of variable `angle` is updated. That is, if the angle is increased, `is_open` would need to be assigned value `false` if the `angle` was `0` before the edge is taken, and `is_closed` would need to be assigned value `true` if the `angle` becomes `90` after the edge is taken. And similarly for the edge where the angle is decreased. A benefit of algebraic variables is that they don't have to be updated on every edge. Instead, they are defined once and automatically change value as needed. This benefit increases when there are more edges where the variable would have otherwise been needed to be updated. And when a new edge is added to the automaton that also updates the `angle`, the algebraic variable does not need to be changed. If the variables would instead be modeled as discrete variables, the new edge would also need to update them. If this would be forgotten, the variables would no longer hold the right value. Algebraic variables can thus reduce modeling effort and improve consistency.

The `bridge_light` automaton models the bridge light. When the light is on, cars may not drive over the bridge. Cars may only drive over the bridge when the light is off. This automaton also has two algebraic variables, `is_on` and `is_off`, that indicate whether the light is on or off, respectively. The `is_on` is `true` when the automaton is in its `On` location, and is `false` otherwise. Similarly, `is_off` is defined by the automaton being in its `Off` location.

The car is modeled by two algebraic variables that model the whether it may or may not drive over the bridge. The car may only drive over the bridge if the bridge deck is closed, and the bridge light is off. Both conditions must hold. This is the case when the algebraic variable `is_closed` of the `bridge_deck` automaton and the algebraic variable `is_off` of the `bridge_light` automaton are both `true`. Hence, `car_may_drive` is defined by expression `bridge_deck.is_closed and bridge_light.is_off`. In all other situations, thus when the bridge deck is not closed, or the bridge light is off, or both, the car may not drive. Hence, `car_may_not_drive` is defined by expression `bridge_deck.is_open or bridge_light.is_on`. Similar to discrete variables, algebraic variables can be read globally, and if defined inside an automaton, and read outside of it, their name must be prefixed with the name of the defining automaton and a period. Note that instead of the boolean algebraic variable `bridge_light.is_on`, also the `On` location of the `bridge_light` could have been used directly. That is, the defining expression of `car_may_not_drive` could instead have also been defined by expression `bridge_deck.is_open or bridge_light.On`.

In general, algebraic variables can be used to give names to expressions (computations), similar to how constants can be used to give names to fixed values. This brings similar benefits, in terms of readability and making it easier to change the model consistently. Boolean algebraic variables can often be used instead of locations, or vice versa. For instance, the above model could also be modeled using only locations and no algebraic variables. However, using algebraic variables can often make it easier to read and work with the model.

Besides that, algebraic variables offer a means of abstraction. The car can refer to the algebraic variables like `is_closed`. It does not have to know how this algebraic variable is defined. It does not have to that the bridge deck has an `angle`, nor at which exact angle the it is closed. As the bridge deck automaton is changed, and even the defining expression of `is_closed`, this does not matter to the car. It can still use the algebraic variable as before, assuming its name and type have not changed. Algebraic variables thus offer a form of abstraction, making it easier to adapt the part of the model that it abstracts.

## Quiz 1

[ { type: 'single-choice', question: ` The above example is also part of the course files (folder `module2`, file `constants-and-algebraic-variables.cif`). Simulate it and check with the state visualizer whether the model, and especially the algebraic variables, show the desired behavior. What do you think?`, answers: [ "Yes, the model has the desired behavior.", "No, the model does not have the desired behavior." ], correctAnswer: '1' } ]

## Exercise 1

Check the model from the quiz above for unreachable and blocking states. Does the result of the trim check make sense? If not, why not, and how can you fix it?

Hint: Remember from the previous sub-module, that to run tools from CIF's event-based toolset on models with variables, you need to first compute the state space of the model using the CIF explorer.

##

The trim check indicates that all locations are blocking. This is to be expected, since none of the locations are marked. Therefore, no location can reach a marked location. To resolve this for this example, the initial locations can be marked.

## Quiz 2

[ { type: 'single-choice', question: "How can the value of an algebraic variable be changed?", answers: [ "By assigning it a new value in an update.", "The value changes automatically according to the expression of the variable.", "By assigning it a new value in an expression." ], correctAnswer: '2' }, { type: 'single-choice', question: "Can an algebraic variable be read by another algebraic variable in another automaton?", answers: [ "Yes, that is possible because of the 'global read' concept.", "No, that is not possible because of the 'local write' concept.", "It depends on whether it is a boolean, integer or real-valued algebraic variable." ], correctAnswer: '1' }, { type: 'single-choice', question: "Is `bridge_deck.is_open or bridge_light.is_on` a good alternative defining expression for algebraic variable `car_may_not_drive`?", answers: [ "Yes, because when the bridge is not closed, it is open.", "No, because when the bridge is not closed, it may not be fully open." ], correctAnswer: '2' }, { type: 'single-choice', question: "Is `not car_may_drive` a good alternative defining expression for algebraic variable `car_may_not_drive`?", answers: [ "Yes, it is completely equivalent.", "No, it is not always equivalent." ], correctAnswer: '1' } ]

## Exercise 2

Model the bridge deck and bridge light example without algebraic variables. When you are done, check with the state visualizer whether the behavior is the same as before.

##

The example model can be modeled without algebraic variables, making use of more locations, as follows:

                                                automaton bridge_deck:
                                                    disc int angle = 0;
                                                    event open_further, close_further;

                                                    const int step = 10;

                                                    location Closed:
                                                        initial;
                                                        edge open_further do angle := angle + step goto InBetween;

                                                    location InBetween:
                                                        edge open_further when angle < 90 - step do angle := angle + step;
                                                        edge open_further when angle = 90 - step do angle := angle + step goto Opened;
                                                        edge close_further when angle > 0 + step do angle := angle - step;
                                                        edge close_further when angle = 0 + step do angle := angle - step goto Closed;

                                                    location Opened:
                                                        edge close_further do angle := angle - step goto InBetween;
                                                end

                                                automaton bridge_light:
                                                    event turn_on, turn_off;

                                                    location On:
                                                        initial;
                                                        edge turn_off goto Off;

                                                    location Off:
                                                        edge turn_on goto On;
                                                end

                                                automaton car:
                                                    event may_drive_now, may_not_drive_anymore;

                                                    location MayNotDrive:
                                                        initial;
                                                        edge may_drive_now when bridge_deck.Closed and bridge_light.Off goto MayDrive;

                                                    location MayDrive:
                                                        edge may_not_drive_anymore when not bridge_deck.Closed or bridge_light.On goto MayNotDrive;
                                                end

This is just one possible answer. Hopefully, you see that the version of the model with algebraic variables is simpler.