Module 4.7: Exercises
You will now practice what you have learned in this third module. When modeling, there is generally not one correct answer, as multiple solutions are possible. After you complete an exercise, an example solution is given, together with an explanation.
Exercise 1
Consider a system that consists of a button and a lamp. Pressing the button once turns on the lamp, and pressing it again turns off the lamp.
a. Model the plant and requirement automata for this system, synthesize a supervisor from it, and validate the result using simulation with the state visualizer.
Use a single requirement automaton and no requirement invariants.
The requirement essentially tracks whether the button is pushed an even or odd number of times. Depending on this, it decides whether the lamp may be turned on or off.
plant button:
uncontrollable u_pushed, u_released;
location Released:
initial;
marked;
edge u_pushed goto Pushed;
location Pushed:
edge u_released goto Released;
end
plant lamp:
controllable c_on, c_off;
location Off:
initial;
marked;
edge c_on goto On;
location On:
edge c_off goto Off;
end
requirement invert_by_push:
location Even:
initial;
marked;
edge lamp.c_off;
edge button.u_pushed goto Odd;
location Odd:
edge lamp.c_on;
edge button.u_pushed goto Even;
end
The synthesized supervisor does not impose any additional restrictions. The requirements are enough to ensure a proper supervisor.
b. Now replace the requirement automaton by state/event exclusion invariants. What else do you need to change? Then synthesize a supervisor and validate it using simulation with the state visualizer.
The requirement can be changed to state/event exclusion invariants, but we still need to track even/odd button pushes.
Thus, that part of the requirement automaton is changed to a plant.
It is essentially an observer, that observes the number of button pushes.
It does not limit the plant behavior.
We could make it a monitor, but since in every location the u_pushed event is already present, that is not needed.
plant button:
uncontrollable u_pushed, u_released;
location Released:
initial;
marked;
edge u_pushed goto Pushed;
location Pushed:
edge u_released goto Released;
end
plant lamp:
controllable c_on, c_off;
location Off:
initial;
marked;
edge c_on goto On;
location On:
edge c_off goto Off;
end
plant observer:
location Even:
initial;
marked;
edge button.u_pushed goto Odd;
location Odd:
edge button.u_pushed goto Even;
end
requirement lamp.c_off needs observer.Even;
requirement lamp.c_on needs observer.Odd;
c. Why should you not use state requirement invariants to model the requirements for this system?
All states of the system should remain present, and only certain transitions in certain states should be prevented. A state requirement invariant can not restrict transitions, but only prevent certain states from being reached.
Exercise 2
Consider again the system with three machines from Exercise 4 of Module 3.
a. Specify a requirement automaton without guards that ensures that at most one machine is off at any particular moment.
Model it in CIF, synthesize a supervisor for it, and validate the result.
All machines are initially on. Since at most one of them may be off at any time, turning off one machine means that it must be started again before any machine may be turned off after that.
controllable o1, s1;
controllable o2, s2;
controllable o3, s3;
plant machine1:
location On:
initial;
marked;
edge s2;
edge o1 goto Off;
location Off:
edge s1 goto On;
end
plant machine2:
location On:
initial;
marked;
edge s3;
edge o2 goto Off;
location Off:
edge s2 goto On;
end
plant machine3:
location On:
initial;
marked;
edge s1;
edge o3 goto Off;
location Off:
edge s3 goto On;
end
requirement AtMostOneOff:
location AllOn:
initial;
marked;
edge o1 goto Off1;
edge o2 goto Off2;
edge o3 goto Off3;
location Off1:
edge s1 goto AllOn;
location Off2:
edge s2 goto AllOn;
location Off3:
edge s3 goto AllOn;
end
b. Replace the requirement automaton by one or more state requirement invariants.
Model it in CIF, synthesize a supervisor for it, and validate the result. Can you think of different ways to model the state requirement invariants?
The event declarations and plant automata remain unchanged. The requirement automaton can for instance be replaced by the following state requirement invariant, which indicates that at all times at least two machines are on:
requirement (machine1.On and machine2.On)
or (machine2.On and machine3.On)
or (machine3.On and machine1.On);
We can also express that no two machines may be off at the same time:
requirement not (machine1.Off and machine2.Off);
requirement not (machine2.Off and machine3.Off);
requirement not (machine3.Off and machine1.Off);
We can also count the number of machines that are off, and specify that this must be at most one.
requirement if machine1.Off: 1 else 0 end
+ if machine2.Off: 1 else 0 end
+ if machine3.Off: 1 else 0 end
<= 1;
Here we use an if expression per machine to count 1 if it is off, and 0 if it is on.
We add them up using +.
And we express as requirement that this sum must be at most one.
c. Replace the state requirement invariants by state/event exclusion requirements.
Model it in CIF, synthesize a supervisor for it, and validate the result.
Can you think of both needs and disables variants?
An example of using needs state/event exclusion requirements could be:
requirement o1 needs machine2.On and machine3.On;
requirement o2 needs machine1.On and machine3.On;
requirement o3 needs machine1.On and machine2.On;
An example of using disables state/event exclusion requirements could be:
requirement machine1.Off disables {o2, o3};
requirement machine2.Off disables {o1, o3};
requirement machine3.Off disables {o1, o2};
Exercise 3
Consider a building with three floors. There is an elevator that connects the floors. At each floor, there is a sensor that detects that the elevator is at that floor. Initially, the elevator stands still at the bottom floor. The elevator can be told to go up a floor, or go down a floor.
a. Model the plants of this system.
Think of what states should be reachable, and what events should be possible in each state. Validate your plant model.
We define Sensor as an automaton definition, to instantiate it once for each floor.
Since the initial state is different between sensors, we use a parameter for this.
The elevator has three states, for the floors it can be on.
It can move up and down between floors.
The sensors need to go on and off when the elevator moves between floors.
The connection is made through guards in the sensor automata.
A location parameter is used to provide the location of the elevator that indicates that the particular sensor should be on.
plant def Sensor(alg bool initialOn; location isOn):
uncontrollable u_on, u_off;
location Off:
initial not initialOn;
marked not initialOn;
edge u_on when isOn goto On;
location On:
initial initialOn;
marked initialOn;
edge u_off when not isOn goto Off;
end
sensor_top: Sensor(false, elevator.Top);
sensor_middle: Sensor(false, elevator.Middle);
sensor_bottom: Sensor(true, elevator.Bottom);
plant elevator:
controllable c_up, c_down;
location Bottom:
initial;
marked;
edge c_up goto Middle;
location Middle:
edge c_down goto Bottom;
edge c_up goto Top;
location Top:
edge c_down goto Middle;
end
b. Ensure that the elevator can only go from top to bottom and bottom to top, and can not reverse direction in the middle.
Add only requirements for this. Think of how you could model this with different kinds of requirements, and what is the best way. Synthesize a supervisor and validate the result.
The restriction that is needed, is that if the elevator is in the middle, it can only continue to go in the direction it is already going. We must therefore keep track of this direction. We can easily do this using a requirement automaton.
requirement NoReverse:
location Bottom:
initial;
marked;
edge elevator.c_up goto GoingUp;
location GoingUp:
edge elevator.c_up goto Top;
location Top:
edge elevator.c_down goto GoingDown;
location GoingDown:
edge elevator.c_down goto Bottom;
end
Exercise 4
Consider a system with two buttons and a lamp. If the first button is pushed, and then the second button is pushed, the lamp may be turned on. If the second button is pushed again, and then the first button is pushed again, the lamp may be turned off again. Model this using plant automata and state/event requirement invariants.
Hint: Add an observer to the plant and make it a monitor.
Since we have two buttons, we make a plant definition and instantiate it twice. There is only one lamp, so it can be modeled as an automaton. The observer plant tracks button pushes and releases. To ensure that we don't block button pushes and releases, we make it a monitor. The state/event exclusion requirements are then expressed using the state of the observer.
plant def Button():
uncontrollable u_pushed, u_released;
location Released:
initial;
marked;
edge u_pushed goto Pushed;
location Pushed:
edge u_released goto Released;
end
button1: Button();
button2: Button();
plant lamp:
controllable c_on, c_off;
location Off:
initial;
marked;
edge c_on goto On;
location On:
edge c_off goto Off;
end
plant observer:
monitor;
location Off:
initial;
marked;
edge button1.u_pushed goto On1;
location On1:
edge button2.u_pushed goto On;
location On:
edge button2.u_released goto Off2;
location Off2:
edge button1.u_released goto Off;
end
requirement lamp.c_on needs observer.On;
requirement lamp.c_off needs observer.Off;
Exercise 5
Consider a counter, that can be incremented and decremented by one through events. The count itself is modeled as a ranged integer variable, with lower bound zero and upper bound eight (both inclusive). Let synthesis ensure that the variable stays within its range, rather than modeling this yourself. Explain the guards of the synthesized supervisor automaton.
The counter is modeled as a plant automaton.
The count itself is stored in a discrete variable with type int[0..8].
The events to increment and decrement the count are controllable events, such that synthesis can restrict them:
plant counter:
disc int[0..8] count;
controllable c_inc, c_dec;
location:
initial;
marked;
edge c_dec do count := count - 1;
edge c_inc do count := count + 1;
end
Synthesis will figure out that if count has its lowest value, zero, decrementing it is not possible.
And that if count has its highest value, eight, incrementing it is not possible.
Hence, the synthesized supervisor looks like this:
supervisor automaton sup:
alphabet counter.c_dec, counter.c_inc;
location:
initial;
marked;
edge counter.c_dec when counter.count != 0;
edge counter.c_inc when counter.count != 8;
end
Exercise 6
Consider two machines that require a shared resource to product a product. Both machines follows the same steps when producing a product:
- They start to produce the product.
- They prepare the product.
- At some point they have produced the product.
- And then they wait until the product has cooled down before they are finished.
a. Model the plant of this system (the two machines).
The supervisor may only control the first of the steps.
Since we have two identical machines, we use an automaton definition and instantiate it twice. Given the four steps, we have four locations four three events. Since the supervisor may only control the first step, only the first event is controllable, and the remaining ones are uncontrollable.
plant def Machine():
controllable c_start;
uncontrollable u_prepared, u_produced, u_cooled;
location Idle:
initial;
marked;
edge c_start goto Preparing;
location Preparing:
edge u_prepared goto Producing;
location Producing:
edge u_produced goto CoolDown;
location CoolDown:
edge u_cooled goto Idle;
end
machine1: Machine();
machine2: Machine();
b. Model the mutual-exclusion requirement and synthesize a supervisor.
Make sure that the two machines are not producing a product at the same time. Think of the best way to model this requirement, trying different requirement forms. Explain the guards of the synthesized supervisor.
The requirement can be most intuitively modeled by a state requirement invariant. It directly captures the requirement that the two machines may not be producing at the same time:
requirement not (machine1.Producing and machine2.Producing);
The supervisor that is synthesized looks like this:
supervisor automaton sup:
alphabet machine1.c_start, machine2.c_start;
location:
initial;
marked;
edge machine1.c_start when machine2.Idle or machine2.CoolDown;
edge machine2.c_start when machine1.Idle or machine1.CoolDown;
end
If one machine is producing, then the other may not produce. But, producing a product can't be prevented, and neither can preparing a product, since the supervisor only has control over starting the process. Synthesis thus prevents a machine from starting if the other machine is preparing or producing. In other words, it only allows a machine to start if the other machine is either idle or letting a produced product cool down. The latter is fine, as after cooling down the machine is idle again, and it won't start due to the supervisor restricting that. A maximally permissive supervisor therefore allows one machine to start, while the other is still cooling down the produced product.
We could also use state/event exclusion invariants to restrict the u_prepared events leading to the Producing locations:
requirement machine1.u_prepared needs not machine2.Producing;
requirement machine2.u_prepared needs not machine1.Producing;
Also in this case, as uncontrollable events may not be restricted by the supervisor, the restrictions are pushed back to the c_start events.
The controlled system then has the same behavior.
Alternatively, we can impose the exact same restrictions that the synthesized supervisors impose on the c_start events:
requirement machine1.u_prepared needs not machine2.Producing;
requirement machine2.u_prepared needs not machine1.Producing;
In this case, the requirements are enough, and the supervisor does not need to restrict anything extra:
supervisor automaton sup:
alphabet machine1.c_start, machine2.c_start;
location:
initial;
marked;
edge machine1.c_start when true;
edge machine2.c_start when true;
end
We can also model the requirement by a requirement automaton:
requirement MutualExclusive:
location NotProducing:
initial;
marked;
edge machine1.u_prepared goto Producing1;
edge machine2.u_prepared goto Producing2;
location Producing1:
edge machine1.u_produced goto NotProducing;
location Producing2:
edge machine2.u_produced goto NotProducing;
end
As soon as we're done preparing, we are producing. If one machine is producing, we must finish that and have produced the product, before another product may be in production.
The requirement automaton is obviously much longer than the requirement invariants. The state requirement invariant is the most direct in this case, and therefore is preferred over the state/event exclusion requirement invariants.
Exercise 7
Consider again the elevator from Exercise 3, and specifically the plant model given as the solution to Exercise 3a, so without the requirement and supervisor.
In the course files, you'll find in the module4 folder, an SVG file named elevator.svg:
The left side has a building, represented by the outer rectangle. Within it are three smaller rectangles, indicating the floors. The elevator is depicted by the dark-grey rectangle that is positioned at the bottom floor. To the right of each floor is an orange circle, indicating the sensor for that floor.
a. Update the image based on the plant state.
Connect the SVG image to the plant model. Add SVG output mappings to animate the image:
-
Make sure the elevator moves to the correct floor, by changing the
ycoordinate of theelevatorelement. Initially, it is atyposition110. Each floor is 50 pixels high, and SVG counts y positions from the top, so the higher you want the elevator to be, the smaller itsyvalue should be. -
Make the circle for the sensor of each floor disappear if the elevator is not at that floor, and appear if the elevator is at that floor.
The SVG element ids for the sensors are
sensor-top,sensor-middleandsensor-bottom. You can use thedisplayattribute for show or hide an element. Valuenonemeans an element is not displayed, while valueinheritcan be used to display the element.
Validate your visualization connection by simulating the adapted plant model.
An svgfile declaration is added at the top of the model.
The Sensor plant definition gets an extra parameter named floorName.
Note that we use floorName rather than just floor, since floor is a keyword in CIF.
The automaton instantiations give the correct name for the particular floor.
Within the Sensor plant definition there is a single SVG output mapping to make the sensor appear or disappear.
Because it is in the definition, each instantiation gets such a mapping.
The mapping itself selects the relevant SVG element id, by adding to the fixed name sensor- the floor name.
The value of the display is either inherit if the sensor is in its On location, or none otherwise, so when it is in its Off location.
For the elevator, the value of its y attribute is changed using an if expression.
If the elevator is at the bottom, it has value 110.
If it is at the middle, it is 50 less, so 60.
And otherwise, when being at the top floor, it has value 10.
svgfile "elevator.svg";
plant def Sensor(alg string floorName; alg bool initialOn; location isOn):
uncontrollable u_on, u_off;
location Off:
initial not initialOn;
marked not initialOn;
edge u_on when isOn goto On;
location On:
initial initialOn;
marked initialOn;
edge u_off when not isOn goto Off;
svgout id "sensor-" + floorName attr "display" value if On: "inherit" else "none" end;
end
sensor_top: Sensor("top", false, elevator.Top);
sensor_middle: Sensor("middle", false, elevator.Middle);
sensor_bottom: Sensor("bottom", true, elevator.Bottom);
plant elevator:
controllable c_up, c_down;
location Bottom:
initial;
marked;
edge c_up goto Middle;
location Middle:
edge c_down goto Bottom;
edge c_up goto Top;
location Top:
edge c_down goto Middle;
svgout id "elevator" attr "y" value if Bottom: "110" elif Middle: "60" else "10" end;
end
b. Adapt the elevator plant to represent the floor its on using a ranged integer variable.
So, instead of multiple locations, use a discrete variable. Use one for the bottom floor, two for the middle floor, and three for the top floor. Adapt the rest of the plant model, including the SVG output mappings, to fit the changed elevator plant. The SVG image does not have to be changed.
The elevator automaton gets a floorNr variable, with type int[1..3].
Its three locations get replaced by a single location, with then doesn't need a name anymore.
There are two edges, one for going up and one for going down.
They update the floor number, and are guarded to prevent the variable from going outside its range.
The SVG output mapping for the elevator's y position is also adapted, to check for values of the variable instead of being in a certain location.
Given that the elevator doesn't have locations anymore, we change the isOn parameter of the Sensor definition to an algebraic boolean parameter.
And we update the instantiations to use the floor number rather than the locations.
svgfile "elevator.svg";
plant def Sensor(alg string floorName; alg bool initialOn; alg bool isOn):
uncontrollable u_on, u_off;
location Off:
initial not initialOn;
marked not initialOn;
edge u_on when isOn goto On;
location On:
initial initialOn;
marked initialOn;
edge u_off when not isOn goto Off;
svgout id "sensor-" + floorName attr "display" value if On: "inherit" else "none" end;
end
sensor_top: Sensor("top", false, elevator.floorNr = 3);
sensor_middle: Sensor("middle", false, elevator.floorNr = 2);
sensor_bottom: Sensor("bottom", true, elevator.floorNr = 1);
plant elevator:
controllable c_up, c_down;
disc int[1..3] floorNr = 1;
location:
initial;
marked;
edge c_up when floorNr < 3 do floorNr := floorNr + 1;
edge c_down when floorNr > 1 do floorNr := floorNr - 1;
svgout id "elevator" attr "y" value if floorNr = 1: "110" elif floorNr = 2: "60" else "10" end;
end
c. Adapt the SVG output mapping for the elevator's y position to not use an if or switch expression, but a computation based on the floor number.
The floor number relates to the elevator's y position as follows:
| Floor number | Y position | Y position computation |
|---|---|---|
| 3 | 10 | 10 + 0 |
| 2 | 60 | 10 + 50 |
| 1 | 110 | 10 + 2 * 50 |
So, the top floor has y position 10.
For each floor below it, the y position increases by 50.
We can thus compute the number of times that 50 needs to be added as 3 - floorNr.
We can multiply that by 50, giving us (3 - floorNr) * 50.
We can add the base value of 10 to it, giving us 10 + ((3 - floorNr) * 50).
And we can convert the resulting number to a text by casting it to a string type, giving us <string>(10 + ((3 - floorNr) * 50)).
We then get the following SVG output mapping:
svgout id "elevator" attr "y" value <string>(10 + ((3 - floorNr) * 50));
d. Adapt the plant model with three buttons, one at each floor, allowing a user to request the elevator to move to that floor.
Add the buttons. Also add observer automata that capture that the button was pressed. Such an observer only resets to no longer being requested when the elevator is at or arrives at the particular floor. Do not yet map the buttons or observers to the SVG image. Also do not yet add any requirements to ensure the proper behavior of the button.
The model can be extended with the buttons and observers by adding the following to the model:
plant def Button():
uncontrollable u_pushed, u_released;
location Released:
initial;
marked;
edge u_pushed goto Pushed;
location Pushed:
edge u_released goto Released;
end
button_top: Button();
button_middle: Button();
button_bottom: Button();
plant def Observer(event request; alg bool atFloor):
uncontrollable u_reset;
location NotRequested:
initial;
marked;
edge request goto Requested;
location Requested:
edge u_reset when atFloor goto NotRequested;
end
observer_top: Observer(button_top.u_pushed, sensor_top.On);
observer_middle: Observer(button_middle.u_pushed, sensor_middle.On);
observer_bottom: Observer(button_bottom.u_pushed, sensor_bottom.On);
The buttons are as we've seen before. Since we have multiple of them, we use automaton definition/instantiation.
The observer tracks whether the elevator is requested to go to a specific floor.
Initially, it is not requested, as the button is not yet pushed.
By pushing the relevant button, the observer tracks that there is a request.
When the elevator is at the particular floor, the request is reset, until the button is pressed again.
The Observer definition gets an event representing the button being pushed for that floor, indicating the request.
It also gets an algebraic boolean value indicating whether the elevator is at the particular floor, and thus the request can be reset.
The instantiations provide the relevant button pushed event, and the sensor for that floor being on.
e. Adapt the visualization for the updated plants.
Use the elevator-with-buttons.svg image:
Make the button rectangle's fill color reflect the request for the elevator to go to a particular floor.
Use limegreen for requested and red for not requested.
The SVG element ids for the buttons are button-top, button-middle and button-bottom.
Only the observers need to be changed:
plant def Observer(alg string floorName; event request; alg bool atFloor):
uncontrollable u_reset;
location NotRequested:
initial;
marked;
edge request goto Requested;
location Requested:
edge u_reset when atFloor goto NotRequested;
svgout id "button-" + floorName attr "fill" value if NotRequested: "red" else "limegreen" end;
end
observer_top: Observer("top", button_top.u_pushed, sensor_top.On);
observer_middle: Observer("middle", button_middle.u_pushed, sensor_middle.On);
observer_bottom: Observer("bottom", button_bottom.u_pushed, sensor_bottom.On);
The definition gets an extra parameter for the floor name, as before. The instantiations pass the relevant name. The definition also gets an SVG output mapping.
f. Add SVG input mappings for the buttons.
Map them to the same button-... SVG elements that you used above.
The only change we need is to add an SVG input mapping to the Observer definition:
svgin id "button-" + floorName event request;
Whenever a button is clicked during simulation, the corresponding request event, so the button pushed event for that particular floor, gets enabled. The button is then thus pushed, and the observer tracks that request. Since the button release is not connected to a button click, it will happen soon afterwards.
Remember that if you want to simulate a model with SVG interaction, you need to configure the SVG input mode. Also note that if you do simulate this adapted model, the elevator's movement is not restricted by the image clicks, so it will move arbitrarily.
Final remarks
We continue with this model in the next module, adding timing for the movement of the elevator, and synthesizing a supervisor to control it based on the floor requests.