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

Exercise 1

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

Quiz 2

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.

                                        
                                            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