Module 5.7: Water lock case hybrid model
In the first three modules, you modeled the plant for the Westsluis water lock. In the fourth module, you added the requirements and synthesized a supervisor. And you validated the supervisor using interactive simulation. However, the simulation model that you used was untimed. Now you'll apply what you've learned in this module, to add timing to the simulation model, making it a hybrid model. That way, for instance, opening a gate no longer instantaneous, but takes some time, like in the real system.
In the course files, in the folder module5 folder, there is a water-lock folder.
This folder contains the plant, requirements and simulation models as obtained during the previous modules.
It also contains the scripts to synthesize the supervisor an perform a simulation.
Use these files as the starting point for this module.
Assignment 1
Synthesize the supervisor from the plants and requirements. Then simulate the system with the untimed model once more, to refamiliarize yourself with it.
Execute the synthesize.tooldef script to synthesize the supervisor.
This results in a file named lock.cif.
Then execute the simulate.tooldef script to simulate the controlled system.
Read again the water lock case information from the introduction to the water lock case in the first module, if you need more information on the operation of the water lock and how to use the SVG image to control the lock.
Assignment 2
The plant model specifies the behavior of the various components of the water lock. To add timing, we need to adapt this plant model. However, we still want to be able to synthesize a supervisor, and hybrid plant models are not supported by synthesis. Hence, we will have both an untimed and a hybrid plant model.
a. Make the required changes.
Execute the following changes, one by one:
- Copy
plant.ciftohybrid_plant.cif. - Copy
plant_definitions.ciftohybrid_plant_definitions.cif. - Adapt the import in
hybrid_plant.cifto import the hybrid plant definitions instead of the untimed plant definitions. - Adapt the import in
simulation.cifto import the hybrid plant instead of the synthesizedlock.cif. - Adapt the
synthesize.tooldefscript to write the synthesis result, the controlled system, tocontrolled_system.cifinstead oflock.cif. - Adapt the
synthesize.tooldefscript to additionally supply the--sup-namespace=supoption to the synthesis tool. -
Adapt the
simulate.tooldefscript to the following content:from "lib:cif" import *; cifmerge( "controlled_system.cif", "simulation.cif", "--output=simulation_merged.cif", ); cifsim( "simulation_merged.cif", "--input-mode=svg", "--auto-algo=first", "--frame-rate=10", "--option-dialog=no", );
We then get the following setup:
The plant definitions and plant are copied, to allow us to change them to add timing, while preserving the untimed plant. We import the hybrid plant in the simulation model, to make sure we can animate the visualization based on the state of the hybrid plant.
We put the synthesis result, the controlled system, in controlled_system.cif instead of lock.cif.
We have many files for different parts of the lock model, and this new name better indicates what part of the model is in that file.
Since the simulation model then only imports the hybrid plant, and not the synthesized controlled system model (controlled_system.cif) anymore, we need a different solution to get them both in the same model.
We adapt the simulation script for that, to merge the synthesis result in controlled_system.cif with the simulation model in simulation.cif, and save the merge result to simulation_merged.cif.
We use the CIF merger tool for this.
After the merge, we simulate the merged CIF model instead of simulation.cif.
The synthesized controlled system includes both the plant and the supervisor.
The hybrid plant model also includes the plant.
They untimed plant and hybrid plant have groups and automata with the same names.
We then can't merge them, as that would lead to name clashes.
Hence, we adapt the synthesis script to put the result of synthesis in a namespace named sup.
This adds a group named sup around the synthesis result.
That way, the plant and supervisor components in the synthesis result no longer clash with the components in the hybrid plant model, and they can be merged using the CIF merger tool without issues.
To ensure that the untimed plants and supervisor still synchronize with the hybrid plant through shared events, the plants and supervisor components are placed in the sup group, but the events are still in their original places.
When merging, the events that are thus in the same places in both plant models are merged to single events, such that all automata synchronize over the same events again.
b. Try out the new setup.
Resynthesize the supervisor using the synthesize.tooldef script.
Then simulate the controlled system together with the hybrid simulation model using the simulate.tooldef script.
Assignment 3
In the next assignments, you will change some of the components of the water lock model, by adding timing behavior for them and adjusting the visualization in the simulation model to match those changes. Which of the following components of the water lock model do you think should be adjusted?
- The gates.
- The bridges.
- The culverts.
- The traffic barriers.
- The entering traffic lights.
- The leaving traffic lights.
- The bridge traffic lights.
Also explain your answer.
Opening and closing the gates takes time, so timing will be added to it. Similarly, timing will be added to the opening and closing of the bridges, culverts and traffic barriers. They are all open/closed components.
Since the bridge traffic lights have two red lights that alternatingly blink on and off while the bridge traffic lights are on, timing is needed for the alternation. Note however that this timing is actually already present in the simulation model. The simulation model is thus already partially a hybrid model.
The other traffic lights do not exhibit such alternating behavior. They change color practically instantly, and therefore there is no need to add timing to them.
Assignment 4
First, we'll adapt the open/closed components, so the bridges, gates, culverts and traffic barriers. So far, the sensors of the open/closed components changed their state based on the state of the corresponding actuators. We need to change this to be dependent on the position of the component, which gradually moves from one place to another.
Change the OpenClosedSensor.
Since different open/closed components may move to and from different positions, adapt the definition to have extra parameters for the open, closed and current positions.
Adapt the edges as well, to ensure the correct state changes.
For now, don't update the instantiations of the definition just yet. The model will thus temporarily be invalid after this assignment.
Note that we'll later use smaller values for the closed position than for the open position of the various open/closed components.
The OpenClosedSensor definition in hybrid_plant_definitions.cif can be adapted as follows:
plant def OpenClosedSensor(
alg bool initial_closed;
alg real closed_position, open_position, current_position
):
uncontrollable u_closed, u_not_closed, u_open, u_not_open;
location Closed:
initial initial_closed;
marked initial_closed;
edge u_not_closed when current_position > closed_position goto Intermediate;
location Intermediate:
edge u_closed when current_position <= closed_position goto Closed;
edge u_open when current_position >= open_position goto Open;
location Open:
initial not initial_closed;
marked not initial_closed;
edge u_not_open when current_position < open_position goto Intermediate;
end
We add three parameters of type real to represent the open, closed and current positions.
We put closed_position first, as it will have lower values than open_position.
The actuator parameter will no longer be used, so we remove it.
We adapt the guards of the edges.
An open/closed component is no longer closed when its position starts to rise above the closed position.
Similarly, such a component is no longer open when its position starts to drop below the open position.
In the Intermediate location, a component can be closed or opened (again) once it reaches the corresponding limit position.
Assignment 5
Adapt the OpenClosedComponent definition, to ensure the open/closed sensor instantiation is valid again.
The actual limits may differ for different open/closed components, so their values are not defined here just yet.
However, do define the current position using a continuous variable.
The speed by which different open/closed components move also differs, so those values can also not be defined here.
Also account for the fact that some open/closed components start opened, while others start closed.
The OpenClosedComponent definition in hybrid_plant_definitions.cif can be adapted as follows:
group def OpenClosedComponent(
alg bool initial_closed;
alg real closed_position, open_position, speed
):
Actuator: OpenClosedActuator(Sensor);
Sensor: OpenClosedSensor(initial_closed, closed_position, open_position, position);
cont position = if initial_closed: closed_position else open_position end
der if Actuator.Opening and position < open_position: +speed
elif Actuator.Closing and position > closed_position: -speed
else 0.0
end;
alg bool IsMoving = not Actuator.Idle;
alg bool IsOpen = Sensor.Open;
alg bool IsClosed = Sensor.Closed;
end
For Sensor, we remove the second argument of instantiation of OpenClosedSensor.
We add closed_position, open_position and position as arguments.
The first two come from new parameters of this definition, and are thus not decided locally.
We opt to name the third argument position rather than current_position, as it is the position of the component and it is defined locally.
We define position a continuous variable.
Initially, it is either at the closed_position or at the open_position, depending on the value of existing parameter initial_closed.
The derivative of the continuous variable indicates how the open/closed component moves as time progresses.
If the Actuator is Opening and has not yet reached the open position, then the component will move according to its speed.
We opt for + before the variable name to explicitly contrast it from the - sign for the movement in the opposite direction, but we could also leave out the + sign.
For the movement in the other direction, if the Actuator is Closing and has not yet reached the closed position, then the component will move according to its negative speed.
The speed differs between components, so it is added as a parameter.
If the actuator is not Opening or Closing, or it has already reached the corresponding limit position, then the component stands still, and thus its derivative is zero.
Assignment 6
Now that we've adapted the open/closed component's definitions, we should also adapt the instantiations in the hybrid plant model. Adapt the instantiations, using the following values:
| Component | Closed position | Open position | Speed |
|---|---|---|---|
| Gate | 0 | 40 | 14 |
| Bridge | 0 | 40 | 10 |
| Culvert | 0 | 20 | 10 |
| Traffic barrier | 0 | 90 | 30 |
The gates and bridges both move 40 meters. The gate does so in just under 3 seconds, while the bridge takes 4 seconds for the movement. The culverts fill and drain in 2 seconds. The traffic barriers open from zero to 90 degrees, with 30 degrees per second, for a total of 3 seconds per movement.
Note that in reality, opening and closing takes considerably longer. We set these relatively short times in order to not have to wait to long during simulations.
The Side definition in hybrid_plant.cif can be adapted as follows (only the relevant parts are shown, and the omitted parts are indicated by ...):
...
group def Side():
Gate: OpenClosedComponent(true, 0, 40, 14);
GateOpenCommand: Command();
GateCloseCommand: Command();
Bridge: OpenClosedComponent(true, 0, 40, 10);
BridgeOpenCommand: Command();
BridgeCloseCommand: Command();
group Culverts:
East: OpenClosedComponent(true, 0, 20, 10);
West: OpenClosedComponent(true, 0, 20, 10);
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, 0, 90, 30);
West: OpenClosedComponent(false, 0, 90, 30);
OpenCommand: Command();
CloseCommand: Command();
alg bool IsOpen = East.IsOpen and West.IsOpen;
alg bool IsClosed = East.IsClosed and West.IsClosed;
end
...
The values from the table are directly used as arguments of the instantiations.
Assignment 7
Now that the hybrid plant model has been adapted, the visualization model is next. We start with the traffic barriers. Adapt the existing SVG output mappings for the traffic barriers.
To help you to get the rotations correct, here is a sketch of the new mappings.
Adapt them by filling in the ... parts, and put them in the simulation model.
The ... parts may be empty, depending on how to plan to fill in the rotation angles.
svgout id "TBNWred" attr "transform" value ... "rotate(..., 154.92546, 87.100967)" ...;
svgout id "TBNWwhite" attr "transform" value ... "rotate(..., 154.92546, 87.100967)" ...;
svgout id "TBNEred" attr "transform" value ... "rotate(..., 154.92546, 87.100967)" ...;
svgout id "TBNEwhite" attr "transform" value ... "rotate(..., 154.92546, 87.100967)" ...;
svgout id "TBSWred" attr "transform" value ... "rotate(..., 154.92546, 87.100967)" ...;
svgout id "TBSWwhite" attr "transform" value ... "rotate(..., 154.92546, 87.100967)" ...;
svgout id "TBSEred" attr "transform" value ... "rotate(..., 154.92546, 87.100967)" ...;
svgout id "TBSEwhite" attr "transform" value ... "rotate(..., 154.92546, 87.100967)" ...;
The SVG elements that need to be adapted have ids that start with TB.
What follows is NW for North-West, NE for North-East, SW for South-West, or SE for South-East.
The traffic barrier visualization consists of overlapping red and white parts.
These parts need to be rotated in the same way.
Each element is given a transformation using the transform attribute.
The transformation that is to be performed is a rotate.
The first argument of the rotate is the number of degrees to rotate.
The second and third argument, which are already given, are the x and y position around which to rotate.
Check whether your changes work, by using simulation.
We can fill in the number of degrees to rotate by using string casting to convert the real value to a string, and then string concatenation (+) to join the multiple parts of the string:
svgout id "TBNWred" attr "transform" value "rotate(" + <string>(-North.TrafficBarriers.West.position) + ", 154.92546, 87.100967)";
svgout id "TBNWwhite" attr "transform" value "rotate(" + <string>(-North.TrafficBarriers.West.position) + ", 154.92546, 87.100967)";
svgout id "TBNEred" attr "transform" value "rotate(" + <string>(-North.TrafficBarriers.East.position) + ", 154.92546, 87.100967)";
svgout id "TBNEwhite" attr "transform" value "rotate(" + <string>(-North.TrafficBarriers.East.position) + ", 154.92546, 87.100967)";
svgout id "TBSWred" attr "transform" value "rotate(" + <string>(-South.TrafficBarriers.West.position) + ", 154.92546, 87.100967)";
svgout id "TBSWwhite" attr "transform" value "rotate(" + <string>(-South.TrafficBarriers.West.position) + ", 154.92546, 87.100967)";
svgout id "TBSEred" attr "transform" value "rotate(" + <string>(-South.TrafficBarriers.East.position) + ", 154.92546, 87.100967)";
svgout id "TBSEwhite" attr "transform" value "rotate(" + <string>(-South.TrafficBarriers.East.position) + ", 154.92546, 87.100967)";
Alternatively, we can use the fmt function:
svgout id "TBNWred" attr "transform" value fmt("rotate(%s, 154.92546, 87.100967)", -North.TrafficBarriers.West.position);
svgout id "TBNWwhite" attr "transform" value fmt("rotate(%s, 154.92546, 87.100967)", -North.TrafficBarriers.West.position);
svgout id "TBNEred" attr "transform" value fmt("rotate(%s, 154.92546, 87.100967)", -North.TrafficBarriers.East.position);
svgout id "TBNEwhite" attr "transform" value fmt("rotate(%s, 154.92546, 87.100967)", -North.TrafficBarriers.East.position);
svgout id "TBSWred" attr "transform" value fmt("rotate(%s, 154.92546, 87.100967)", -South.TrafficBarriers.West.position);
svgout id "TBSWwhite" attr "transform" value fmt("rotate(%s, 154.92546, 87.100967)", -South.TrafficBarriers.West.position);
svgout id "TBSEred" attr "transform" value fmt("rotate(%s, 154.92546, 87.100967)", -South.TrafficBarriers.East.position);
svgout id "TBSEwhite" attr "transform" value fmt("rotate(%s, 154.92546, 87.100967)", -South.TrafficBarriers.East.position);
This function is given a pattern as first argument.
The pattern contains %s, which represents a placeholder for the number of degrees to rotate.
The value to be filled in is given as the second argument of the fmt function.
You can read more about the fmt function in the CIF tutorial lesson on text formatting.
Assignment 8
Adapt the SVG output mappings for the gates.
Look at the existing mapping, and take inspiration from the previous assignment.
Make use of the fmt function.
When you're done, use simulation to validate your changes.
The existing mappings use a translate to move the elements.
The first argument is the x direction movement, and the second argument is the y direction movement.
The y direction movement goes from 40 when closed to 0 when open.
We thus subtract the current position from 40:
svgout id "gateN" attr "transform" value fmt("translate(0,%s)", 40 - North.Gate.position);
svgout id "gateS" attr "transform" value fmt("translate(0,%s)", 40 - South.Gate.position);
Assignment 9
Adapt the SVG output mappings for the bridges.
Use the following sketch, which again contains some ... parts.
When you're done, use simulation to validate your changes.
svgout id "bridgeNclosed" attr "transform" value fmt("scale(1, %s) translate( 0, 40)", 1 - North.Bridge.position / 130);
svgout id "bridgeSclosed" attr "transform" value fmt("scale(1, %s) translate(-116, 40)", 1 - North.Bridge.position / 130);
svgout id "bridgeNopen" attr "display" value if ...: "block" else "none" end;
svgout id "bridgeNclosed" attr "display" value if ...: "none" else "block" end;
svgout id "bridgeSopen" attr "display" value if ...: "block" else "none" end;
svgout id "bridgeSclosed" attr "display" value if ...: "none" else "block" end;
For the bridge, two transformations are applied: one to scale and subsequently one to move by a translation.
The first argument for the scale is 1, indicating no scaling in the x direction.
The second argument is the scaling in the y direction.
Being closed is no longer the inverse of being closed, as a bridge can also be in the intermediate position.
The if conditions are updated to account for this:
svgout id "bridgeNclosed" attr "transform" value fmt("scale(1, %s) translate( 0, 40)", 1 - North.Bridge.position / 130);
svgout id "bridgeSclosed" attr "transform" value fmt("scale(1, %s) translate(-116, 40)", 1 - South.Bridge.position / 130);
svgout id "bridgeNopen" attr "display" value if North.Bridge.IsOpen: "block" else "none" end;
svgout id "bridgeNclosed" attr "display" value if North.Bridge.IsOpen: "none" else "block" end;
svgout id "bridgeSopen" attr "display" value if South.Bridge.IsOpen: "block" else "none" end;
svgout id "bridgeSclosed" attr "display" value if South.Bridge.IsOpen: "none" else "block" end;
Assignment 10
Next up are the culverts. They should not immediately change color when they're filled with water, or when they are drained. Adapt the SVG output mappings of the culverts as follows:
svgout id "culvertNW" attr "fill" value if North.Culverts.IsClosed: "#4094ff"
elif North.Culverts.IsOpen: "#0058f1"
else "#4088ff"
end;
svgout id "culvertNE" attr "fill" value if North.Culverts.IsClosed: "#4094ff"
elif North.Culverts.IsOpen: "#0058f1"
else "#4088ff"
end;
svgout id "culvertSW" attr "fill" value if South.Culverts.IsClosed: "#4094ff"
elif South.Culverts.IsOpen: "#0058f1"
else "#4088ff"
end;
svgout id "culvertSE" attr "fill" value if South.Culverts.IsClosed: "#4094ff"
elif South.Culverts.IsOpen: "#0058f1"
else "#4088ff"
end;
Assignment 11
Currently, when opening the gates, the water level in the chamber between the gates rises or drops instantly.
The simulation model has an automaton named WaterLevel.
Make the water level, represented by H_Chamber, time-dependent by making it a continuous variables instead of a discrete variable.
Use a speed of 0.4 meters per second.
Adapt the rest of the automaton as necessary.
Do not yet update the visualization.
The WaterLevel automaton can be adapted as follows:
automaton WaterLevel:
disc real H_North = 2, H_South = 1, speed = 0.4;
cont H_Chamber = H_South
der if (OCCC or COCC or OOCC) and (H_Chamber < H_North): +speed
elif (CCCO or CCOC or CCOO) and (H_Chamber > H_South): -speed
else 0.0
end;
location CCCC:
initial;
edge when North.Gate.IsOpen goto OCCC;
edge when North.Culverts.IsOpen goto COCC;
edge when South.Gate.IsOpen goto CCOC;
edge when South.Culverts.IsOpen goto CCCO;
location OCCC:
edge when North.Gate.IsClosed and H_Chamber >= H_North goto CCCC;
edge when North.Culverts.IsOpen and H_Chamber >= H_North goto OOCC;
edge when South.Gate.IsOpen and H_Chamber >= H_North goto OCOC;
edge when South.Culverts.IsOpen and H_Chamber >= H_North goto OCCO;
location COCC:
edge when North.Gate.IsOpen and H_Chamber >= H_North goto OOCC;
edge when North.Culverts.IsClosed and H_Chamber >= H_North goto CCCC;
edge when South.Gate.IsOpen and H_Chamber >= H_North goto COOC;
edge when South.Culverts.IsOpen and H_Chamber >= H_North goto COCO;
location CCOC:
edge when North.Gate.IsOpen and H_Chamber <= H_South goto OCOC;
edge when North.Culverts.IsOpen and H_Chamber <= H_South goto COOC;
edge when South.Gate.IsClosed and H_Chamber <= H_South goto CCCC;
edge when South.Culverts.IsOpen and H_Chamber <= H_South goto CCOO;
location CCCO:
edge when North.Gate.IsOpen and H_Chamber <= H_South goto OCCO;
edge when North.Culverts.IsOpen and H_Chamber <= H_South goto COCO;
edge when South.Gate.IsOpen and H_Chamber <= H_South goto CCOO;
edge when South.Culverts.IsClosed and H_Chamber <= H_South goto CCCC;
location OOCC:
edge when North.Gate.IsClosed and H_Chamber >= H_North goto COCC;
edge when North.Culverts.IsClosed and H_Chamber >= H_North goto OCCC;
edge when South.Gate.IsOpen and H_Chamber >= H_North goto OOOC;
edge when South.Culverts.IsOpen and H_Chamber >= H_North goto OOCO;
location OCOC:
edge when North.Gate.IsClosed goto CCOC;
edge when North.Culverts.IsOpen goto OOOC;
edge when South.Gate.IsClosed goto OCCC;
edge when South.Culverts.IsOpen goto OCOO;
location OCCO:
edge when North.Gate.IsClosed goto CCCO;
edge when North.Culverts.IsOpen goto OOCO;
edge when South.Gate.IsOpen goto OCOO;
edge when South.Culverts.IsClosed goto OCCC;
location COOC:
edge when North.Gate.IsOpen goto OOOC;
edge when North.Culverts.IsClosed goto CCOC;
edge when South.Gate.IsClosed goto COCC;
edge when South.Culverts.IsOpen goto COOO;
location COCO:
edge when North.Gate.IsOpen goto OOCO;
edge when North.Culverts.IsClosed goto CCCO;
edge when South.Gate.IsOpen goto COOO;
edge when South.Culverts.IsClosed goto COCC;
location CCOO:
edge when North.Gate.IsOpen and H_Chamber <= H_South goto OCOO;
edge when North.Culverts.IsOpen and H_Chamber <= H_South goto COOO;
edge when South.Gate.IsClosed and H_Chamber <= H_South goto CCCO;
edge when South.Culverts.IsClosed and H_Chamber <= H_South goto CCOC;
location OOOC:
edge when North.Gate.IsClosed goto COOC;
edge when North.Culverts.IsClosed goto OCOC;
edge when South.Gate.IsClosed goto OOCC;
edge when South.Culverts.IsOpen goto OOOO;
location OOCO:
edge when North.Gate.IsClosed goto COCO;
edge when North.Culverts.IsClosed goto OCCO;
edge when South.Gate.IsOpen goto OOOO;
edge when South.Culverts.IsClosed goto OOCC;
location OCOO:
edge when North.Gate.IsClosed goto CCOO;
edge when North.Culverts.IsOpen goto OOOO;
edge when South.Gate.IsClosed goto OCCO;
edge when South.Culverts.IsClosed goto OCOC;
location COOO:
edge when North.Gate.IsOpen goto OOOO;
edge when North.Culverts.IsClosed goto CCOO;
edge when South.Gate.IsClosed goto COCO;
edge when South.Culverts.IsClosed goto COOC;
location OOOO:
edge when North.Gate.IsClosed goto COOO;
edge when North.Culverts.IsClosed goto OCOO;
edge when South.Gate.IsClosed goto OOCO;
edge when South.Culverts.IsClosed goto OOOC;
end
The type of the discrete variables is changed to real.
Variable H_Chamber becomes a continuous variable.
It is still initialized to H_South.
For the locations where the water level can change, a speed it set, unless the final height is already reached.
This is similar to the position of open/closed components.
The assignments to H_Chamber are removed.
Some edges get additional guards to ensure the correct time-dependent behavior of the transitions between the locations.
Assignment 12
And finally, we visualize the water level.
Change the color of the water chamber (SVG element with id waterchamber) and the two inlets near the culverts into which the gates close (SVG elements with ids culvertNinlet and culvertSinlet).
Use the same three colors as for the culverts.
svgout id "waterchamber" attr "fill" value if WaterLevel.H_Chamber <= 1: "#4094ff"
elif WaterLevel.H_Chamber >= 2: "#0058f1"
else "#4088ff"
end;
svgout id "culvertNinlet" attr "fill" value if WaterLevel.H_Chamber <= 1: "#4094ff"
elif WaterLevel.H_Chamber >= 2: "#0058f1"
else "#4088ff"
end;
svgout id "culvertSinlet" attr "fill" value if WaterLevel.H_Chamber <= 1: "#4094ff"
elif WaterLevel.H_Chamber >= 2: "#0058f1"
else "#4088ff"
end;
Final remarks
And with that, we've come to the end of the water lock case. You have made plants, requirements, a supervisor and a hybrid simulation model of the Westsluis water lock. You can now simulate its correct and safe behavior. Congratulations!