Module 4.8: Water lock case requirements and supervisor
In Module 3, you finished the plant model of the Westsluis water lock. Now you'll apply what you've learned in this module, to model the requirement of the Westsluis. And you'll synthesize a supervisor.
Assignment 1
To model the various requirements, create a new CIF file named requirements.cif.
In this new file, import the plant model.
This allows the requirements to refer to event and locations of the plant.
Since the requirements model imports the plant model, it will combine both the plants and the requirements, and will thus form the input for synthesis. For now though, only add the import, but do not yet add any requirements and do not yet perform synthesis.
The requirements.cif file now contains the following:
import "plant.cif";
Assignment 2
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. A single command may enable events of multiple components. For instance, when the operators clicks the button to open the north traffic barriers, the events to open the north-west and north-east traffic barriers should both be enabled. When a command is activated, the supervisor should ensure the proper control responses, before the plant unrequests the command.
Model the requirements for all the commands. Avoid as much as possible duplicating the requirements for the north and south side, as well as for multiple components connected to a single command.
The requirements.cif file is extended with the following:
group def CommandRequirements(Side side):
requirement side.Gate.Actuator.c_start_opening
needs side.GateOpenCommand.Requested;
requirement side.Gate.Actuator.c_start_closing
needs side.GateCloseCommand.Requested;
requirement side.Bridge.Actuator.c_start_opening
needs side.BridgeOpenCommand.Requested;
requirement side.Bridge.Actuator.c_start_closing
needs side.BridgeCloseCommand.Requested;
requirement {side.Culverts.East.Actuator.c_start_opening,
side.Culverts.West.Actuator.c_start_opening}
needs side.Culverts.OpenCommand.Requested;
requirement {side.Culverts.East.Actuator.c_start_closing,
side.Culverts.West.Actuator.c_start_closing}
needs side.Culverts.CloseCommand.Requested;
requirement {side.TrafficBarriers.East.Actuator.c_start_opening,
side.TrafficBarriers.West.Actuator.c_start_opening}
needs side.TrafficBarriers.OpenCommand.Requested;
requirement {side.TrafficBarriers.East.Actuator.c_start_closing,
side.TrafficBarriers.West.Actuator.c_start_closing}
needs side.TrafficBarriers.CloseCommand.Requested;
requirement {side.EnteringTLs.East.Actuator.c_to_red_red,
side.EnteringTLs.West.Actuator.c_to_red_red}
needs side.EnteringTLs.RedRedCommand.Requested;
requirement {side.EnteringTLs.East.Actuator.c_to_red,
side.EnteringTLs.West.Actuator.c_to_red}
needs side.EnteringTLs.RedCommand.Requested;
requirement {side.EnteringTLs.East.Actuator.c_to_red_green,
side.EnteringTLs.West.Actuator.c_to_red_green}
needs side.EnteringTLs.RedGreenCommand.Requested;
requirement {side.EnteringTLs.East.Actuator.c_to_green,
side.EnteringTLs.West.Actuator.c_to_green}
needs side.EnteringTLs.GreenCommand.Requested;
requirement {side.LeavingTLs.East.Actuator.c_to_red,
side.LeavingTLs.West.Actuator.c_to_red}
needs side.LeavingTLs.RedCommand.Requested;
requirement {side.LeavingTLs.East.Actuator.c_to_green,
side.LeavingTLs.West.Actuator.c_to_green}
needs side.LeavingTLs.GreenCommand.Requested;
requirement {side.BridgeTLs.East.Actuator.c_to_on,
side.BridgeTLs.West.Actuator.c_to_on}
needs side.BridgeTLs.OnCommand.Requested;
requirement {side.BridgeTLs.East.Actuator.c_to_off,
side.BridgeTLs.West.Actuator.c_to_off}
needs side.BridgeTLs.OffCommand.Requested;
end
NorthCommandRequirements: CommandRequirements(North);
SouthCommandRequirements: CommandRequirements(South);
We opt for a group definition for the command requirements of each side, to prevent duplication for the two sides.
The definition is parameterized with a component parameter that indicates the side to which the requirements are to be applied.
The definition is instantiated twice, once for the North side and once for the South side.
The requirements for the commands are given as state/event exclusion requirements, enabling certain actuator events only if the corresponding command is requested. In case a single command enables multiple actuator events for multiple components, a single state/event exclusion requirement is used that restricts these events. Empty lines are used to separate the requirements for the gate, bridge, culverts, traffic barriers, and so on, to increase readability.
The supervisor will enable the right controllable events immediately upon a request. There is no need to handle the unrequesting of commands in the requirements.
Assignment 3
In the first module, you simulated the Westsluis water lock, using models provided as part of the course files. The model did not yet contain a proper controller to ensure safe behavior, allowing you to discover the potential unsafe behaviors of the system through simulation. The model that you simulated, did however already contain a supervisor synthesized from the plant model and command requirements. By including the connection between the commands and their effect on the system, you were able to manually control the system, and identify its unsafe behavior.
Let's recreate that simulation, step by step.
a. Synthesize a partially-supervised supervisor from the plant and requirement models you've created so far.
To prevent having to click through various menus and configure all settings every time again, you can use a ToolDef script.
ToolDef is a cross-platform scripting language, and among others allows you to easily script CIF tools.
Create a file named synthesize.tooldef that contains a script to automatically synthesize the supervisor:
from "lib:cif" import *;
cifdatasynth(
"requirements.cif",
"--output=lock.cif",
);
This script first imports all CIF tools, from the library of CIF tools.
It then starts data-based synthesis, using requirements.cif as input model.
Remember that this file contains the plants and the requirements.
The output of synthesis is written to a file named lock.cif.
Remember that you can execute a ToolDef script by right-clicking it and choosing Execute ToolDef, or by pressing F10 while the ToolDef file is selected in the Project Explorer.
b. Copy the simulation files from the Module 1 course files.
Copy lock.svg, the SVG image of the Westsluis water lock.
Also copy the simulation.cif file, the file that contains the simulation model.
Inspect the simulation model, to see whether you understand it.
You may see some continuous variables (keyword cont) and equations (keyword equation), that will be explained in the next module.
Finally, copy the simulate.tooldef file, the script to start the simulation.
Inspect the file, and make sure you understand it.
If needed, start the simulator to show its option dialog, by right-clicking the simulation.cif file and choosing the appropriate menu items.
In the option dialog, select Command line options from the Help category.
It lists the various options that can be used on the command line, as well as in ToolDef scripts, as well as their syntax.
Don't actually start the simulation, but instead press Cancel to close the option dialog.
c. Simulate the partially-controlled system.
Start the simulation by running the simulation ToolDef script. Check that the behavior is still the same as it was in Module 1.
Assignment 4
The partially-controlled Westsluis is not yet safe. Before modeling safety requirements, it is good to first think of what the desired behavior of the system is, and which requirements are needed to ensure that only this desired behavior is possible.
Draw on paper an operation cycle for one side of the lock, that ensures that the lock operates safely. This cycle should ensure that the lock transitions safely from a state where the road traffic can drive over the bridge to a state where the water traffic can leave or enter the lock, and can safely transition back. Which sequences of actions should be taken to achieve this? Leave out the culverts for now. And for the entering traffic lights, consider only the red and green lights, leaving out red/red and red/green for now. Also, remember that in the initial state of the plant model, road traffic is allowed to cross the bridge and water traffic is not permitted to enter or exit the lock.
As usual, when designing a controller there is not one correct behavior of the system. Choices can be made, and the following is just one of the options:
Initially, road traffic is allowed over the bridge. The bridge traffic lights at both sides the bridge are turned on, to indicate that bridge traffic should stop using the bridge. The traffic barriers on both sides of the bridge are then closed, the bridge is then opened, the gate is opened, and the entering or leaving traffic lights are turned green. Water traffic is then allowed to enter or exit the lock. This completes the downward path of the cycle.
The upward path of the cycle is similar, but in reverse, and turns the entering or leaving traffic lights to red instead of green, closes the gate instead of opening it, and so on.
Assignment 5
We add the requirements step by step, following at the same time both paths of the operation cycle, from top to bottom. We thus consider the left path from start to finish, and the right path in reverse order. We start at the top, so with the bridge traffic lights.
Simulate again the partially-controlled system, and check what behavior is possible for the bridge traffic lights. And then think of what the desired behavior is. In which states is it allowed and desired to turn the bridge lights on or off, and in which states is it not allowed?
Model these safety requirements as state/event exclusion requirements.
Turning on the bridge traffic lights is the start of the left path, and does not any restrictions. Turning off the bridge traffic lights should only be allowed if the traffic barriers are open. This can be modeled with state/event exclusion invariants as follows:
group BridgeTLRequirements:
requirement {North.BridgeTLs.East.Actuator.c_to_off,
North.BridgeTLs.West.Actuator.c_to_off}
needs North.TrafficBarriers.IsOpen;
requirement {South.BridgeTLs.East.Actuator.c_to_off,
South.BridgeTLs.West.Actuator.c_to_off}
needs South.TrafficBarriers.IsOpen;
end
We again combine requirements with the same conditions. We do not use component definition/instantiation, since the overhead would be bigger than the gain, as the definition would only contain a single state/event exclusion requirement. We do add a named group around the requirements, for readability of the model.
Assignment 6
The next step is to add safety requirements for the traffic barriers. Think again about the states in which they should and may not be opened and closed. And then model the requirements.
Closing the traffic barriers should only be done once the traffic bridge lights are on. Opening the traffic barriers should only be done once the bridge is closed. This can be modeled with state/event exclusion invariants as follows:
group TrafficBarrierRequirements:
requirement {North.TrafficBarriers.East.Actuator.c_start_closing,
North.TrafficBarriers.West.Actuator.c_start_closing}
needs North.BridgeTLs.IsOn;
requirement {South.TrafficBarriers.East.Actuator.c_start_closing,
South.TrafficBarriers.West.Actuator.c_start_closing}
needs South.BridgeTLs.IsOn;
requirement {North.TrafficBarriers.East.Actuator.c_start_opening,
North.TrafficBarriers.West.Actuator.c_start_opening}
needs North.Bridge.IsClosed;
requirement {South.TrafficBarriers.East.Actuator.c_start_opening,
South.TrafficBarriers.West.Actuator.c_start_opening}
needs South.Bridge.IsClosed;
end
Assignment 7
Add the safety requirements for the bridge.
Opening the bridge should only be done once the traffic barriers are closed. Closing the bridge should only be done once the gate is closed. This can be modeled with state/event exclusion invariants as follows:
group BridgeRequirements:
requirement North.Bridge.Actuator.c_start_opening needs North.TrafficBarriers.IsClosed;
requirement South.Bridge.Actuator.c_start_opening needs South.TrafficBarriers.IsClosed;
requirement North.Bridge.Actuator.c_start_closing needs North.Gate.IsClosed;
requirement South.Bridge.Actuator.c_start_closing needs South.Gate.IsClosed;
end
Assignment 8
Add the safety requirements for the gate. Consider for this also the states of the culverts, entering traffic lights and leaving traffic lights.
Opening a gate should only be done once the bridge is closed. To prevent floods, we also require that the gate and culverts at the other side are closed.
Closing a gate should only be done once the entering and leaving traffic lights have been turned to red. For the entering traffic lights, out of service (red/red) should be taken into account as well.
group GateRequirements:
requirement North.Gate.Actuator.c_start_opening
needs North.Bridge.IsOpen and South.Gate.IsClosed and South.Culverts.IsClosed;
requirement South.Gate.Actuator.c_start_opening
needs South.Bridge.IsOpen and North.Gate.IsClosed and North.Culverts.IsClosed;
requirement North.Gate.Actuator.c_start_closing
needs (North.EnteringTLs.IsRed or North.EnteringTLs.IsRedRed)
and North.LeavingTLs.IsRed;
requirement South.Gate.Actuator.c_start_closing
needs (South.EnteringTLs.IsRed or South.EnteringTLs.IsRedRed)
and South.LeavingTLs.IsRed;
end
Assignment 9
Add the safety requirements for the culverts.
The culverts may only be opened if on the other side the culverts and gate are closed.
group CulvertRequirements:
requirement {North.Culverts.East.Actuator.c_start_opening,
North.Culverts.West.Actuator.c_start_opening}
needs South.Culverts.IsClosed and South.Gate.IsClosed;
requirement {South.Culverts.East.Actuator.c_start_opening,
South.Culverts.West.Actuator.c_start_opening}
needs North.Culverts.IsClosed and North.Gate.IsClosed;
end
Assignment 10
Add the safety requirements for the leaving traffic lights.
The leaving traffic lights may only be set to green if the gate is open and the entering traffic lights are either red or red/red.
group LeavingTLRequirements:
requirement {North.LeavingTLs.East.Actuator.c_to_green,
North.LeavingTLs.West.Actuator.c_to_green}
needs North.Gate.IsOpen
and (North.EnteringTLs.IsRed or North.EnteringTLs.IsRedRed);
requirement {South.LeavingTLs.East.Actuator.c_to_green,
South.LeavingTLs.West.Actuator.c_to_green}
needs South.Gate.IsOpen
and (South.EnteringTLs.IsRed or South.EnteringTLs.IsRedRed);
end
Assignment 11
And finally, add the safety requirements for the entering traffic lights. Carefully consider the order in which the lights change color, and from what color they may change to what other color. Hint: Besides state/event exclusion requirements, also use requirement automata.
The requirement automaton definition indicates the allowed order of color changes. We instantiate it once for each of the four leaving traffic lights.
The entering traffic lights are initially red. To become green, they should first become red/green for a bit. Once they are green, they can become red again. Only if they are red, may they become red/red. It is always possible to become red.
Leaving traffic lights may only be turned to green once the gate is open and the leaving traffic lights are red.
requirement def EnteringTLOrder(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;
location RedRed:
marked;
edge c_to_red goto Red;
location RedGreen:
edge c_to_red goto Red;
edge c_to_green goto Green;
location Green:
edge c_to_red goto Red;
end
group EnteringTLRequirements:
NorthEastOrder: EnteringTLOrder(
North.EnteringTLs.East.Actuator.c_to_red_red,
North.EnteringTLs.East.Actuator.c_to_red,
North.EnteringTLs.East.Actuator.c_to_red_green,
North.EnteringTLs.East.Actuator.c_to_green);
NorthWestOrder: EnteringTLOrder(
North.EnteringTLs.West.Actuator.c_to_red_red,
North.EnteringTLs.West.Actuator.c_to_red,
North.EnteringTLs.West.Actuator.c_to_red_green,
North.EnteringTLs.West.Actuator.c_to_green);
SouthEastOrder: EnteringTLOrder(
South.EnteringTLs.East.Actuator.c_to_red_red,
South.EnteringTLs.East.Actuator.c_to_red,
South.EnteringTLs.East.Actuator.c_to_red_green,
South.EnteringTLs.East.Actuator.c_to_green);
SouthWestOrder: EnteringTLOrder(
South.EnteringTLs.West.Actuator.c_to_red_red,
South.EnteringTLs.West.Actuator.c_to_red,
South.EnteringTLs.West.Actuator.c_to_red_green,
South.EnteringTLs.West.Actuator.c_to_green);
requirement {North.EnteringTLs.East.Actuator.c_to_green,
North.EnteringTLs.West.Actuator.c_to_green}
needs North.Gate.IsOpen and North.LeavingTLs.IsRed;
requirement {South.EnteringTLs.East.Actuator.c_to_green,
South.EnteringTLs.West.Actuator.c_to_green}
needs South.Gate.IsOpen and South.LeavingTLs.IsRed;
end
Reflection on the requirements
The various requirements fulfill different purposes:
- The command requirements ensure the connection between the commands and their effects on the system.
- The bridge traffic light, traffic barrier, bridge, gate, culvert, leaving traffic light and entering traffic light requirements ensure the proper safe cycle of the system.
- The gate and culvert requirements additionally ensure that no floods can occur.
- The entering and leaving traffic light requirements additionally ensure that they are not simultaneously green.
- The entering traffic light requirements additionally ensure that the entering traffic lights change their color in the right order.
Assignment 12
Now that the requirements are complete, it is time to synthesize a supervisor.
Execute the synthesize.tooldef script and wait for it to finish.
Depending on how fast your computer is, this should take only one or a few seconds.
Then simulate the fully controlled system using the simulate.tooldef script.
Check that it is indeed safe in all situations.
Assuming you did everything correctly, you should observe that the system is now safe. For instance, you cannot open two opposite gates, nor can you close the traffic barriers when the bridge lights are not on.
Final remarks
You've completed the plants and requirements for the Westsluis water lock, and you've synthesized a supervisor for it. Congratulations!
In the next module, we will add timing to the simulation model. That way, opening a gate is not instantaneous, but takes some time, like in the real system.