Module 3.6: Water lock case plant models
In the first module, we made a start on the water lock case. We identified seven different types of components, and we made a start on modeling them. In the second module, we adapted the models to be more realistic, using among others synchronizing automata and algebraic variables.
In the second module, we also noted that several components have quite similar automata. And we concluded that it was burdensome and error-prone to make and adapt each one individually. In this module, you learned about parameterized component definitions and instantiations, which can be used to reduce the duplication.
In this module, you also learned about groups, that can be used to add structure to models. And you learned about imports, that can be used to divide models into separate files, which is useful for larger models and for reuse. And finally, you learned about plant models, controllable and uncontrollable events, as well various properties to which a proper supervisor should adhere.
You will now improve the models for the water lock case, by making use of these new modeling features. At the end of this module, you will have the complete plant model for the water lock case.
Two CIF files
We will divide the CIF model for the water lock case over two CIF files:
- File
plant_definitions.cif, containing all the automaton and group definitions for the different components of the water lock (bridges, gates, lights, etc). - File
plant.cif, containing the instantiations that define the form the actual plant.
The definitions file is imported into the plant file. This approach gives a clear structure, makes it easier to find the different parts of the model and reduces duplication. The different kinds of components are defined once in the definitions file, and the actual plant is easily built in the plant file through instantiations. The resulting model can be easily adapted and extended.
Assignment 1
Look at your answers to the water lock case assignments of the second module. There, you modeled all components of the water lock, such as the bridges, gates, and so on, as well as their sub-components, the sensors and actuators. As mentioned before, you will adapt these models to make use of component definitions and instantiations.
Identify how many automaton definitions you need to make, for each sub-component type. Does, for example, one definition suffice to model all sensors or do you need multiple definitions for different kinds of sensors? Also, think of how definitions should be made for the components. For example, do you need group/automaton definitions and instantiations for them?
Looking at the solutions provided for the assignments in the second module, all sensors of the traffic lights are similar in structure. However, the sensors of the open/closed components are structurally different. Two different definitions should thus be modeled, one for the sensors of the traffic lights, and one for the the sensors of the open/closed components.
The actuators of the entering, leaving, and bridge traffic lights, as well as those of the open/closed components, are all different in structure. Their definitions need to be modeled separate. You thus need to model two sensor definitions and four actuator definitions.
Components contain sub-components. For instance, the entering traffic lights consist of three sensors and one actuator. It is thus best to model the components of the water lock as group definitions. Within the group definitions, there are then automaton instantiations for the sub-components.
Assignment 2
Model the automaton and group definitions of the entering, leaving and bridge traffic light actuators. Don't forget to define the events as being either controllable or uncontrollable.
The automata are now defined as automaton definitions.
Since they are part of the plant, they are defined as plant automata definitions.
All the events are controllable, and the supervisor is allowed to enable or disable the actuators of the system.
The event names are prefixed with c_.
plant def EnteringTLActuator():
controllable c_to_red_red, c_to_red, c_to_red_green, c_to_green;
location Red:
initial;
marked;
edge c_to_red_red goto RedRed;
edge c_to_red_green goto RedGreen;
edge c_to_green goto Green;
location RedRed:
marked;
edge c_to_red goto Red;
edge c_to_red_green goto RedGreen;
edge c_to_green goto Green;
location RedGreen:
edge c_to_red goto Red;
edge c_to_red_red goto RedRed;
edge c_to_green goto Green;
location Green:
edge c_to_red goto Red;
edge c_to_red_red goto RedRed;
edge c_to_red_green goto RedGreen;
end
plant def LeavingTLActuator():
controllable c_to_green, c_to_red;
location Red:
initial;
marked;
edge c_to_green goto Green;
location Green:
edge c_to_red goto Red;
end
plant def BridgeTLActuator():
controllable c_to_on, c_to_off;
location Off:
initial;
marked;
edge c_to_on goto On;
location On:
edge c_to_off goto Off;
end
Assignment 3
Now consider the definitions for the traffic light sensors.
Looking at the models from the second module, for some traffic light sensors the On location is the initial and marked location, while for others it is the Off location.
To allow for this flexibility, add a boolean parameter to the sensor definition.
initial keywords.
If the predicate evaluates to true, the location is initial, otherwise it is not.
Similarly, a location can be conditionally marked.
Furthermore, not all sensors have the same guards for their edges. For instance, some sensors will go on when the corresponding light is green and others when it is red. Parameterize the definition by adding two more parameters, one representing the guard for going on, and one for going off.
With the above considerations in mind, model a single definition that can be used for all traffic light sensors. And also here, don't forget to define the events as being either controllable or uncontrollable.
As with the actuators, the automata are now defined as plant automaton definitions.
The events are all uncontrollable, since the supervisor is not allowed to disable sensor events.
The event names are prefixed with u_.
The definition has three boolean algebraic parameters. Since they are of the same type, the type needs to be specified only once.
The initial_on parameter indicates whether the sensor is initially on.
The On location is made conditionally initial and marked, based on this variable being true.
Note that we simply use condition initial_on, instead of condition initial_on = true, as they are functionally identical and the former is shorter.
The Off location is similarly made conditionally initial and marked, but with the negated condition.
The guard_go_on and guard_go_off parameters indicate when the sensor goes on and off, respectively.
They are used as guards of the edges.
plant def Sensor(alg bool initial_on, guard_go_on, guard_go_off):
uncontrollable u_go_on, u_go_off;
location On:
initial initial_on;
marked initial_on;
edge u_go_off when guard_go_off goto Off;
location Off:
initial not initial_on;
marked not initial_on;
edge u_go_on when guard_go_on goto On;
end
Assignment 4
Having completed the definitions of the traffic light actuators and sensors, now you are going to model a definition for an entire leaving traffic light. Look again at the solutions in the second module, to see what which components are part of the leaving traffic lights and how they behave.
Model the entire leaving traffic light as a group definition that combines the sub-components. When defining the automaton instantiations, think of the right argument values to use for the parameters of the automaton definitions. Also, add algebraic boolean variables that indicate whether the light is green or red, as in the second module.
We name the group definition LeavingTL, to match LeavingTLActuator.
We use Actuator as name for the instantiation of LeavingTLActuator, since it is the only actuator of the leaving traffic light.
Also, since it is part of the group definition, there is no need to repeat LeavingTL.
We keep the names of the two sensors.
The leaving traffic light is initially red.
We therefore provide true for the initial_on parameter of the Sensor definition, for SensorRed.
It is then not initially green, so we provide false for SensorGreen.
We also provide the guard predicates for the sensors going on and off.
The algebraic variables are kept as they were in the second module, but have been updated to account for the change in the actuator name.
group def LeavingTL():
Actuator: LeavingTLActuator();
SensorGreen: Sensor(false, Actuator.Green, Actuator.Red);
SensorRed: Sensor(true, Actuator.Red, Actuator.Green);
alg bool IsRed = Actuator.Red and SensorGreen.Off and SensorRed.On;
alg bool IsGreen = Actuator.Green and SensorGreen.On and SensorRed.Off;
end
Assignment 5
Model the definition for the entering and bridge traffic lights, just as you did in Assignment 4 for the leaving traffic lights. Do not forget the algebraic variables indicating the state of the lights.
group def BridgeTL():
Actuator: BridgeTLActuator();
SensorOn: Sensor(false, Actuator.On, Actuator.Off);
SensorOff: Sensor(true, Actuator.Off, Actuator.On);
alg bool IsOn = Actuator.On and SensorOn.On and SensorOff.Off;
alg bool IsOff = Actuator.Off and SensorOn.Off and SensorOff.On;
end
group def EnteringTL():
Actuator: EnteringTLActuator();
SensorTopRed: Sensor(true, not Actuator.Green, Actuator.Green);
SensorGreen: Sensor(false, Actuator.RedGreen or Actuator.Green, Actuator.Red or Actuator.RedRed);
SensorBottomRed: Sensor(false, Actuator.RedRed, not Actuator.RedRed);
alg bool IsRed = Actuator.Red and SensorTopRed.On and SensorGreen.Off and SensorBottomRed.Off;
alg bool IsRedRed = Actuator.RedRed and SensorTopRed.On and SensorGreen.Off and SensorBottomRed.On;
alg bool IsRedGreen = Actuator.RedGreen and SensorTopRed.On and SensorGreen.On and SensorBottomRed.Off;
alg bool IsGreen = Actuator.Green and SensorTopRed.Off and SensorGreen.On and SensorBottomRed.Off;
end
Assignment 6
Looking again at the second module, an open/closed component has different sensors and actuators than the other components. In the second module, you already modeled this. Now, make definitions for its sub-components. Use component parameters for allow the sensor and actuator to use information about each other's state. Also parameterize the sensor with a parameter that indicates whether the open/closed component is initially closed.
plant def OpenClosedActuator(OpenClosedSensor sensor):
controllable c_start_opening, c_stop_opening, c_start_closing, c_stop_closing;
location Idle:
initial;
marked;
edge c_start_opening when not sensor.Open goto Opening;
edge c_start_closing when not sensor.Closed goto Closing;
location Opening:
edge c_stop_opening when sensor.Open goto Idle;
location Closing:
edge c_stop_closing when sensor.Closed goto Idle;
end
plant def OpenClosedSensor(alg bool initial_closed; OpenClosedActuator actuator):
uncontrollable u_closed, u_not_closed, u_open, u_not_open;
location Closed:
initial initial_closed;
marked initial_closed;
edge u_not_closed when actuator.Opening goto Intermediate;
location Intermediate:
edge u_closed when actuator.Closing goto Closed;
edge u_open when actuator.Opening goto Open;
location Open:
initial not initial_closed;
marked not initial_closed;
edge u_not_open when actuator.Closing goto Intermediate;
end
Assignment 7
Make a definition for an entire open/closed component, with its two sub-components and three algebraic variables. Use again a group definition and parameterize it to allow an open/closed component to be initially open or closed.
group def OpenClosedComponent(alg bool initial_closed):
Actuator: OpenClosedActuator(Sensor);
Sensor: OpenClosedSensor(initial_closed, Actuator);
alg bool IsMoving = not Actuator.Idle;
alg bool IsOpen = Sensor.Open;
alg bool IsClosed = Sensor.Closed;
end
Assignment 8
Having completed the plant definitions of the water lock case in plant_definitions.cif, it is now time to model the actual plant in plant.cif.
The Westsluis water lock is symmetric: the north and south sides of the lock contain the same components. Model one side of the lock using instantiations. Group components of the same type, like multiple culverts. Model the traffic barriers as being initially open, and the other open/closed components as being initially closed.
Gate: OpenClosedComponent(true);
Bridge: OpenClosedComponent(true);
group Culverts:
East: OpenClosedComponent(true);
West: OpenClosedComponent(true);
end
group TrafficBarriers:
East: OpenClosedComponent(false);
West: OpenClosedComponent(false);
end
group EnteringTLs:
East: EnteringTL();
West: EnteringTL();
end
group LeavingTLs:
East: LeavingTL();
West: LeavingTL();
end
group BridgeTLs:
East: BridgeTL();
West: BridgeTL();
end
Assignment 9
Since the north and south side of the lock are the same, turn the solution to Assignment 8 into a definition. Then, instantiate it for each side, to complete the plant model.
For components of the same type that you grouped, add algebraic variables indicating the state of both the east and west components.
For instance, define an algebraic variable Open for the culverts, which is true when both the east and west culvert are open.
We will use these algebraic variables in the next module.
group def Side():
Gate: OpenClosedComponent(true);
Bridge: OpenClosedComponent(true);
group Culverts:
East: OpenClosedComponent(true);
West: OpenClosedComponent(true);
alg bool IsOpen = East.IsOpen and West.IsOpen;
alg bool IsClosed = East.IsClosed and West.IsClosed;
end
group TrafficBarriers:
East: OpenClosedComponent(false);
West: OpenClosedComponent(false);
alg bool IsOpen = East.IsOpen and West.IsOpen;
alg bool IsClosed = East.IsClosed and West.IsClosed;
end
group EnteringTLs:
East: EnteringTL();
West: EnteringTL();
alg bool IsRed = East.IsRed and West.IsRed;
alg bool IsRedRed = East.IsRedRed and West.IsRedRed;
alg bool IsRedGreen = East.IsRedGreen and West.IsRedGreen;
alg bool IsGreen = East.IsGreen and West.IsGreen;
end
group LeavingTLs:
East: LeavingTL();
West: LeavingTL();
alg bool IsRed = East.IsRed and West.IsRed;
alg bool IsGreen = East.IsGreen and West.IsGreen;
end
group BridgeTLs:
East: BridgeTL();
West: BridgeTL();
alg bool IsOn = East.IsOn and West.IsOn;
alg bool IsOff = East.IsOff and West.IsOff;
end
end
North: Side();
South: Side();
Assignment 10
The lock has various commands that allow the operator to control the it. For instance, the north gate may only be opened after the operator requests it to be opened. So far, in modeling the plants, we have ignored these commands.
You did see these commands in the first module, when you simulated the lock to find undesired behavior. Simulate it again, as you did in the first module, if you don't remember what commands an operator can give to the system. Note that some commands control multiple components of the system.
Model a plant definition for a command. A command can be requested by the operator. The system will then give the supervisor the opportunity to process the command. However, the supervisor may have disabled the command, if it is unsafe. After a brief time, the system will, by itself, unrequest the command.
Instantiate the definition it as many times as needed for the various components of the lock that can be controlled.
The plant_definitions.cif file is extended with one extra definition:
plant def Command():
uncontrollable u_request, u_unrequest;
location NotRequested:
initial;
marked;
edge u_request goto Requested;
location Requested:
edge u_unrequest goto NotRequested;
end
A command can be requested and unrequested. The request is uncontrollable, since the operator does the request and the supervisor can't prevent it. After some time, the system unrequests the command. The supervisor can't prevent this either, so that is also modeled as an uncontrollable event.
The plant.cif file is updated as follows:
import "plant_definitions.cif";
group def Side():
Gate: OpenClosedComponent(true);
GateOpenCommand: Command();
GateCloseCommand: Command();
Bridge: OpenClosedComponent(true);
BridgeOpenCommand: Command();
BridgeCloseCommand: Command();
group Culverts:
East: OpenClosedComponent(true);
West: OpenClosedComponent(true);
OpenCommand: Command();
CloseCommand: Command();
alg bool IsOpen = East.IsOpen and West.IsOpen;
alg bool IsClosed = East.IsClosed and West.IsClosed;
end
group TrafficBarriers:
East: OpenClosedComponent(false);
West: OpenClosedComponent(false);
OpenCommand: Command();
CloseCommand: Command();
alg bool IsOpen = East.IsOpen and West.IsOpen;
alg bool IsClosed = East.IsClosed and West.IsClosed;
end
group EnteringTLs:
East: EnteringTL();
West: EnteringTL();
RedCommand: Command();
RedRedCommand: Command();
RedGreenCommand: Command();
GreenCommand: Command();
alg bool IsRed = East.IsRed and West.IsRed;
alg bool IsRedRed = East.IsRedRed and West.IsRedRed;
alg bool IsRedGreen = East.IsRedGreen and West.IsRedGreen;
alg bool IsGreen = East.IsGreen and West.IsGreen;
end
group LeavingTLs:
East: LeavingTL();
West: LeavingTL();
RedCommand: Command();
GreenCommand: Command();
alg bool IsRed = East.IsRed and West.IsRed;
alg bool IsGreen = East.IsGreen and West.IsGreen;
end
group BridgeTLs:
East: BridgeTL();
West: BridgeTL();
OnCommand: Command();
OffCommand: Command();
alg bool IsOn = East.IsOn and West.IsOn;
alg bool IsOff = East.IsOff and West.IsOff;
end
end
North: Side();
South: Side();
The gate and bridge get open and close commands, as do the culverts and traffic barriers. The entering traffic lights get commands to switch the lights, as do the leaving traffic lights and bridge traffic lights.
Final remarks
Congratulations, you have completely modeled the plant of the Westsluis water lock case. Hopefully, you have realized that the use of component definitions/instantiations, groups and imports can greatly improve the structure of a plant model, making it more readable and adaptable. However, this plant model still has dangerous behavior, as we saw in the first module. In the next module, we will add requirements and synthesize a supervisor to prevent this unsafe behavior.