Module 2.9: More detailed models for the water lock case
In the first module, you made a start on the water lock case. We identified seven different types of components, and you made a start on modeling them. In this module, you additionally learned how to model synchronizing automata, shared variables, constants and algebraic variables. Now it is time to adapt the water lock models to use these new concepts.
When you modeled the seven types of components in CIF, in the previous module, you made simple models. You modeled each component as a single automaton, describing its basic behavior. However, in real life, these components again consist of subcomponents. The subcomponents of a component can be modeled as multiple synchronizing automata, that together capture the behavior of the larger component. In this module, you will therefore extend each component by modeling its subcomponents.
Traffic lights
As you know, a leaving traffic light has two states: green and red. In the previous module, you modeled this as follows:
automaton LeavingTrafficLight:
event to_green, to_red;
location Red:
initial;
marked;
edge to_green goto Green;
location Green:
edge to_red goto Red;
end
This is an oversimplification of the component's behavior. This automaton only models the actuator that turns the red and green lights on and off. What is not yet modeled, are the sensors that indicate whether the light has actually turned green or red.
For example, imagine that the actuator of the traffic light is an electronic button that activates a switch to close an electrical circuit, and that the sensor simply measures whether the electrical circuit is closed and thus whether the light is on. You can turn on the green light with the button, and a very short moment later, the green light will be on. Note that, for now, we ignore that actuators and sensors can also physically break down, and thus malfunction.
In general, a physical component has actuators that change the component's state. While an actuator can physically have many forms, such as being electrical, electronic, hydraulic or pneumatic, this does not necessarily always matter for their control. Often, they can be modeled similarly, when considering them as discrete event components. A component should be modeled in sufficient detail, to allow a supervisory controller to control it, without modeling unnecessary details. To be informed of the effect of the actuators on the component, sensors are present that indicate changes to the component's state. That is, actuators change the component's state and sensors give feedback on the component's state. This understanding of physical components is key in modeling them.
The automaton above thus only models the leaving traffic light's actuator, which changes the traffic light's state. To complete this model, the sensors that indicate when the state actually changes, should be added.
Assignment 1
Complete the model of the leaving traffic light by adding two automata, one for the green light sensor and one for the red light sensor.
Both automata have two locations named On and Off.
Also introduce two variables that indicate whether the light is green or red.
Check the behavior using simulation, or by computing and visualizing the state space.
Hints: The green light sensor goes on when the traffic light actuator is turned to green, and similarly for the red light sensor. The traffic light is a certain color when the actuator and sensors are in certain locations.
The LeavingTLActuator is the same as the LeavingTrafficLight above, but with a different name.
SensorGreen goes on when the light is turned to green, and goes off when it is turned to red.
Contrarily, SensorRed goes on when the light is turned to red, and goes off when it is turned to green.
Algebraic variables IsGreen and IsRed update automatically to reflect whether the green and red lights, respectively, are on or not.
automaton LeavingTLActuator:
event to_green, to_red;
location Red:
initial;
marked;
edge to_green goto Green;
location Green:
edge to_red goto Red;
end
automaton SensorGreen:
event go_on, go_off;
location Off:
initial;
marked;
edge go_on when LeavingTLActuator.Green goto On;
location On:
edge go_off when LeavingTLActuator.Red goto Off;
end
automaton SensorRed:
event go_on, go_off;
location On:
initial;
marked;
edge go_off when LeavingTLActuator.Green goto Off;
location Off:
edge go_on when LeavingTLActuator.Red goto On;
end
alg bool IsRed = LeavingTLActuator.Red and SensorGreen.Off and SensorRed.On;
alg bool IsGreen = LeavingTLActuator.Green and SensorGreen.On and SensorRed.Off;
Assignment 2
Similarly as in assignment 1, now also update the model of the bridge traffic light. Is it much different? Check the behavior using simulation, or by computing and visualizing the state space.
Hint: Consider whether it is necessary to model the detailed blinking behavior, or not.
The structure is the same as for assignment one, and only some names are different. This makes sense, as both actuators have two states: the leaving traffic light is green or red, and the bridge traffic light is on or off.
However, if the bridge traffic light is on, then in reality, its two red lights are blinking. But, here we only model whether the light is on and thus blinking, or is off. We assume the detailed control of the blinking behavior is taken care of by a lower-level resource controller. For controlling the water lock, the detailed blinking behavior is not relevant, and we are only concerned with when to turn the blinking on or off. The bridge traffic light is therefore modeled similarly to the leaving traffic light.
There is however another difference. For the leaving traffic light, each of the two states of the actuator is connected to a separate light. That is, when the leaving traffic light is green, the lower light is green, and when the leaving traffic light is red, the upper light is red. The two sensors are connected to the two different lights. For the bridge traffic light however, this is not the case. The on sensor checks whether the lights are blinking, and the off sensor checks that both lights are off.
automaton BridgeTLActuator:
event to_on, to_off;
location Off:
initial;
marked;
edge to_on goto On;
location On:
edge to_off goto Off;
end
automaton SensorOn:
event go_on, go_off;
location Off:
initial;
marked;
edge go_on when BridgeTLActuator.On goto On;
location On:
edge go_off when BridgeTLActuator.Off goto Off;
end
automaton SensorOff:
event go_on, go_off;
location On:
initial;
marked;
edge go_off when BridgeTLActuator.On goto Off;
location Off:
edge go_on when BridgeTLActuator.Off goto On;
end
alg bool IsOn = BridgeTLActuator.On and SensorOn.On and SensorOff.Off;
alg bool IsOff = BridgeTLActuator.Off and SensorOn.Off and SensorOff.On;
Assignment 3
Similarly as in assignments 1 and 2, now also update the model of the entering traffic light. Check the behavior using simulation, or by computing and visualizing the state space.
Hints: Every single light of an entering traffic light has its own sensor that indicates whether it is on or off, just like in the leaving traffic light. Also add four boolean algebraic variables that indicate whether the traffic light displays a certain signal.
automaton EnteringTLActuator:
event to_red_red, to_red, to_red_green, to_green;
location Red:
initial;
marked;
edge to_red_red goto RedRed;
edge to_red_green goto RedGreen;
edge to_green goto Green;
location RedRed:
marked;
edge to_red goto Red;
edge to_red_green goto RedGreen;
edge to_green goto Green;
location RedGreen:
edge to_red goto Red;
edge to_red_red goto RedRed;
edge to_green goto Green;
location Green:
edge to_red goto Red;
edge to_red_red goto RedRed;
edge to_red_green goto RedGreen;
end
automaton SensorTopRed:
event go_on, go_off;
location On:
initial;
marked;
edge go_off when EnteringTLActuator.Green goto Off;
location Off:
edge go_on when not EnteringTLActuator.Green goto On;
end
automaton SensorGreen:
event go_on, go_off;
location Off:
initial;
marked;
edge go_on when EnteringTLActuator.RedGreen or EnteringTLActuator.Green goto On;
location On:
edge go_off when EnteringTLActuator.Red or EnteringTLActuator.RedRed goto Off;
end
automaton SensorBottomRed:
event go_on, go_off;
location Off:
initial;
marked;
edge go_on when EnteringTLActuator.RedRed goto On;
location On:
edge go_off when not EnteringTLActuator.RedRed goto Off;
end
alg bool IsRed = EnteringTLActuator.Red and SensorTopRed.On and SensorGreen.Off and SensorBottomRed.Off;
alg bool IsRedRed = EnteringTLActuator.RedRed and SensorTopRed.On and SensorGreen.Off and SensorBottomRed.On;
alg bool IsRedGreen = EnteringTLActuator.RedGreen and SensorTopRed.On and SensorGreen.On and SensorBottomRed.Off;
alg bool IsGreen = EnteringTLActuator.Green and SensorTopRed.Off and SensorGreen.On and SensorBottomRed.Off;
Open/closed components
In module 1, we concluded that gates, culverts, traffic barriers and bridges are all similar components. They can all be opened and closed by an actuator. We modeled it there as follows:
automaton OpenClosedComponent:
event to_open, to_closed;
location Closed:
marked; initial;
edge to_open goto Open;
location Open:
edge to_closed goto Closed;
end
This is again an oversimplification of the component's behavior. Consider a bridge that is closed. When an operator wants to open it, they press a button, and the actuator causes the bridge to start opening. The bridge then goes from a state in which it is closed to an intermediate state, because the actuator is not infinitely fast such that it is immediately open after the button is pressed. Only after some time, the bridge reaches its open position.
The actuator that is responsible for the movement of an OpenCloseComponent is not infinitely fast due to physical constraints.
Initially, when the bridge is still closed, it is at rest, doing nothing.
Then, when the button is pressed to open the bridge, the actuator moves to open the bridge, and when the bridge needs to be closed, the actuator moves to close the bridge.
The actuator can thus either be in an opening, closing or idle state.
Note that this is different from the traffic lights, where there is no intermediate state. The actuators of those lights turn them on and off practically instantaneously, as they don't need to warm up first, or anything like that.
As mentioned above, components have actuators to change the components's state and sensors that give feedback on the component's state.
For the OpenClosedComponent, another type of sensor is used.
This sensor can detect whether the component is in the open, closed or intermediate partially open state.
Assignment 4
Update the model of the OpenClosedComponent.
When modeling the actuator, use the locations Opening, Closing and Idle, and the events start_opening, stop_opening, start_closing and stop_closing.
Take the following physical constraints into account:
- The actuator can only start opening when it is not already open.
- The actuator can only start closing when it is not already closed.
- The actuator should stop opening when it is open.
- The actuator should stop closing when it is closed.
When modeling the sensor use the locations Closed, Intermediate and Open, and the events closed, not_closed, open and not_open.
closed means that the component is closed, while not_closed means that the component is not closed anymore.
Note that not_closed is not the same as open.
Furthermore, add three boolean algebraic variables, Moving, Open and Closed, that indicate whether the component is moving, open or closed, respectively.
Check the behavior of your model using simulation, or by computing and visualizing its state space.
The actuator is pretty straightforward.
The sensor has a single Intermediate location.
From the sensor location alone, we can't see which direction it is moving.
We thus use guards based on the actuator state, to go to the right next location.
For the algebraic variable, note that it is not relevant what the sensor indicates for the component to be moving, as this is entirely determined by the actuator. Similarly, for the component to be open or closed, it is not relevant whether the component is moving, as the sensor will update once the component starts moving. The sensor state is thus sufficient.
automaton Actuator:
event start_opening, stop_opening, start_closing, stop_closing;
location Idle:
initial;
marked;
edge start_opening when not Sensor.Open goto Opening;
edge start_closing when not Sensor.Closed goto Closing;
location Opening:
edge stop_opening when Sensor.Open goto Idle;
location Closing:
edge stop_closing when Sensor.Closed goto Idle;
end
automaton Sensor:
event closed, not_closed, open, not_open;
location Closed:
initial;
marked;
edge not_closed when Actuator.Opening goto Intermediate;
location Intermediate:
edge closed when Actuator.Closing goto Closed;
edge open when Actuator.Opening goto Open;
location Open:
edge not_open when Actuator.Closing goto Intermediate;
end
alg bool IsMoving = not Actuator.Idle;
alg bool IsOpen = Sensor.Open;
alg bool IsClosed = Sensor.Closed;
Final remarks
In extending the water lock component models, you wrote a lot of the same code. The three types of traffic lights, for example, already have seven sensors that only differ in name. Multiple gates, culverts, traffic barriers and bridges need to be modeled when modeling the entire system in the next module. This would be labor intensive, even when using a copy-paste-modify approach. And mistakes are easily made. Therefore, in the next module, you will learn how to model such similar components in a better, more scalable way.