User Tools

Site Tools


supcon:pushbutton_lamp_tutorial_state_based

State-based supervisory control tooling: PushButton/Lamp tutorial

This page contains a step-by-step tutorial that can be used as an introduction to the state-based supervisory control tooling, including editing with the graphical editor (SCIDE), simulation, and verification.

The PushButton/Lamp example

We use a very simple example system, consisting of just a single button and a single lamp. The goal is to make sure that for as long as the button is pushed, the lamp stays on. That is, once the button is pushed, the lamp goes on, and once the button is released, the lamp goes off. It should (obviously) be possible to push the button again after that, to make the lamp go on, etc.

Modeling the plants

We start by making an (untimed) model of the plants (automata representing the hardware) and the control requirements (by means of logical expressions). In this case the plants are the PushButton and the Lamp. Once finished, it should look like this:

We are now going to reproduce the above figure. Follow these steps to do so:

  • Start the SCIDE (Supervisory Control IDE) application.
    • Linux: In a terminal, enter the following command:
      • scide
    • Windows: Start scide.exe.
  • Wait for the application to finish loading and click on 'File' → 'New' → 'Scim Diagram'.
  • Change the name of the file to 'PushButton_Lamp.scim' (case sensitive).
    • Linux: Leave the directory (that is, everything up-to and including the last '/') the same.
    • Windows: You can put the file anywhere you want, but remember where you put it!
  • Click 'Finish'.
  • On the left, you have a large white area, called the 'canvas'. Besides it, is the 'Palette', containing several 'tools'. On the bottom-right, you can see the 'Properties' window.
  • Left-click once on the 'Model' tool in the palette. Then left-click in the upper-left corner of the canvas and drag (while keeping the left mouse button down) the model to the bottom-right corner of the canvas. Then release the left mouse button. You just added a model to the canvas.
  • Once you added the model to the canvas, the name 'M' is automatically selected. Enter the correct name of the model (PushButton_Lamp) and press <enter>. You can also change the name in the property window. To do that, select the model, click on the 'Name' property in the property window, enter the correct name (PushButton_Lamp) and press <enter>.
    • Most names (and other texts) can be changed on the canvas as well. Just select the text you want to change and press <F2> to start editing. This way the current text is selected, and you can modify it. Alternatively, select the text and just start typing, overwriting the old text.
  • Select the 'Action' tool in the palette. Add an action declaration to your model by left clicking in the 'Declarations' area of the model. You may notice that the mouse cursor changes when you move over an area of the canvas in which you are not allowed to put an action. Once you move over the 'Declarations' area of the model, it changes into an arrow and a plus sign. Click once to add the action.
    • In Linux, the cursor changes to an 'X'.
    • In Windows, the cursor changes to some other forbidden sign, or whatever icon you configured in the Windows Control Panel.
  • Once you added the action, give it the appropriate name (PushButton1On).
  • Add three more actions (as we need four in total, see the image above). Note that if you hold the <ctrl> key on your keyboard while you add an action, you keep the tool selected, and you can immediately add another action, without having to select the 'Action' tool again from the palette. This goes for other tools as well.
    • If you ever want to remove an action, click on the 'A' icon of the action and then press the <del> key on the keyboard.
  • Select the 'PushButton1On' action, and change the 'Controllable' property (in the 'Properties' window) from 'true' to 'false'.
  • Do the same for the 'PushButton1Off' action. Notice how they are now colored red, instead of blue. Also, uncontrollable actions are displayed in italic.
  • When you added the model, an automaton was already added inside the model. Resize it to about a third of the canvas (the large empty area inside the model).
  • Change the name of the automaton to 'PushButton'. If you edit the name on the canvas, make sure you don't remove the 'Plant : ' (note the single space before the colon and the single space after the colon!) part. Obviously, you can also edit the name in the 'Properties' windows, if you like.
  • With the automaton selected, go to the 'Properties' window, and click on the 'Sync Acts' property.
  • Click on the square button with '…' in it to browse for available actions. Select the 'PushButton1On' and 'PushButton1Off' actions. There are two ways to do this:
    • Double click on the action in the left list ('Choices' list) to make it appear in the right list ('Feature' list), or
    • Left click once on the action in the left list and use the 'Add' button to make it appear in the right list.
  • Once you have added both actions to the right list, click 'OK' to close the window. Notice how the actions appear on the canvas, in the automaton, after the 'Sync:' text.
  • The atomic automaton contains locations and edges in it's canvas. One location is added automatically. This location is colored green, which makes it the initial location. Change the name of the initial location to 'Released'.
  • Add a new location using the 'Location' tool and call it 'Pushed'.
  • Note that in the figure, the 'Released' location has a thicker, blue border. This means that the location is marked. To make a location marked, change the 'Marked' property to 'true' in the 'Properties' window.
  • Select the 'Edge' tool. Left click on the 'Released' location, and drag the edge to (the middle of) the 'Pushed' location. Once there, release the left mouse button and see how you just added an edge.
  • In the Properties window, you can add the 'PushButton1On' action to edge, by changing the 'Labels' property, similar to how you added sync actions to the automaton earlier.
  • Click somewhere in the middle of the edge with the left mouse button and drag the edge a bit upwards. See how an additional point appears in the edge.
  • Add another edge from 'Pushed' to 'Released' and add the 'PushButton1Off' action (label) to it.
  • Select the 'Automaton' tool and add a second automaton to the model. You should once again cover about a third of the canvas inside of the model.
  • Complete the two plant automata ('PushButton' and 'Lamp') to make them look like the final result as shown above.
  • Using the 'LogicalExpressions' tool, add a logical expressions block to the model, and name it 'Requirements'.
  • Then edit the logical expressions, by using the 'Expressions' property in the 'Properties' window.
  • Note that once you have added some text, you can edit the text in the canvas as well. Select the logical expressions text (not the box, but the actual text) and press the <F2> key. You can move around using the arrow keys. To introduce a newline, use <ctrl> + <enter>. Press <enter> once you're done editing. Note that you can always also edit it using the 'Properties' window.
  • You're model should now look like the figure above.
  • Save the model. You can use <ctrl>+<s>, or use the button on the toolbar, or use the 'File' menu.

Explanation of the model

Our model has four actions. The 'PushButton1On' and 'PushButton1Off' actions represent the physical behavior of the button. The Lamp1On and Lamp1Off actions represent the physical behavior of the lamp. All actions must be declared before they can be used. Actions are also called events.

The 'PushButton' automaton shows all the physical behavior of the button (hardware). Initially, the button is released (as stated by the initial location called 'Released'). You should always give locations a meaningful name. All locations within a single atomic automaton must have a unique name. Locations are also called states. Once the user pushes the button ('PushButton1On' action), the button is in a pushed state. This is why that location is called 'Pushed'. Once the user releases the button ('PushButton1Off' action), the button is in a released state.

The lamp is similar to the button.

The requirements state that if event 'Lamp1Off' is enabled, the state 'Released' must be active. In other words, if the state is not 'Released', then action 'Lamp1Off' must be disabled. Again in yet other words, if the state is 'Pushed', then action 'Lamp1Off' must be disabled. The requirement for 'Lamp1On' is similar.

For the syntax of the logical expressions, see here.

Running the script

To run the script, you need to get it first. You need to do this only once (unless the script changes). Follow these steps:

  • From a terminal, enter (notice that -O is a captical letter o):
    • wget http://devel.se.wtb.tue.nl/trac/svctools/export/HEAD/trunk/sewiki/supcon/state_based_button_led_tutorial/synscript -O synscript
    • chmod u+x synscript

Next you can run the script. You need to make sure you are in a Linux terminal, and that you are in the same directory as where you put the PushButton_Lamp.scim file. If you created it using the Linux version of SCIDE, and you followed the instructions above, you should find it in your home directory, which is the same directory as where a new terminal usually opens in. If you used the Windows version of SCIDE, you need to upload the .scim file to make it available from your Linux account. Once you are in the correct directory and have the PushButton_Lamp.scim file in that directory, execute the following command:

  • ./synscript -s PushButton_Lamp

This executes the script on PushButton_Lamp.scim. It performs conversions, does supervisory synthesis, creates a CIF model of the plants and supervisor (for simulation), generates the state space, and creates logical expressions for the controller. Each time you change your .scim file, you should rerun the script to generate the new files. It should end with 'INFO: Script finished without fatal errors.'. If not, something went wrong. In such a case, read the output on the screen. Look for warning and error messages.

If the state space calculation takes to long, or the results are too large to be meaningful, you can disable state space calculation. In that case, execute the following command (thus leaving out the -s option):

  • ./synscript PushButton_Lamp

Simulation of the model

Follow these steps:

  • From a terminal, enter:
    • ./synscript -s PushButton_Lamp
    • simcif PushButton_Lamp_bdd.core.cifx

You are now simulating the model. First the simulator shows a textual representation of the model. You see the 'PushButton' and 'Lamp' automata. The 'PushButton' automaton is in the 'Released' location and the 'Lamp' automaton is in the 'Off' location. Two possible transitions are shown. Each transition has a number associated with it, so that you choose a transition, just by entering the number.

The two transitions that are possible are action 'PushButton1On' and a time transition. You can just ignore time transitions for now. Let's choose the 'PushButton1On' action by entering the number corresponding to this action (transition), followed by pressing <enter>. You see that automaton 'PushButton' is now in location 'Pushed'. You may need to scroll up in the terminal. Note that making the terminal window larger (or just full screen) can be very helpful.

The possible transitions are now action 'PushButton1Off', action 'Lamp1On', and a time transition. Let's choose the action 'PushButton1Off'. When this action corresponds to the default transition (Transition 0), you don't need to enter the number, you can just press <enter>. As you can see, both automata are back in the initial state.

You can choose some more transitions. Feel free to simulate some more. Press 'q', followed by <enter>, to quit the simulation. You can restart it using the same 'simcif' command you used the first time. Alternatively, press 'r', followed by <enter>, to reset the simulation.

Note that you can also start the simulator as follows:

simcif --visualize-automata=* PushButton_Lamp_bdd.core.cifx

This gives you the same simulator, but with automata visualization. Green locations show the current location and red edges are enabled at that time. You should experiment with this visualization. Note that you need to click 'Ludicrous speed' in the 'viz-timing-gui' window once it pops up.

There is another visualization available:

simcif --visualize-msc=* PushButton_Lamp_bdd.core.cifx

This visualization gives you an overview of the transitions that you have chosen and the automata that play a role in it. For this simple model it is not very interesting, but for larger ones it is invaluable for debugging. Play with this visualization a bit as well.

Note that you can combine both visualization options.

Once you've had enough, you should have realized something: Only the wanted behavior is possible during the simulation. It is not possible to turn on the lamp if the button is released, and it is not possible to release the lamp if the button is pushed. This is exactly what we wanted.

Visualization of the state space

Follow these steps:

  • From a terminal, enter:
    • ./synscript -s PushButton_Lamp
    • gv PushButton_Lamp_statespace.ps

This shows you a graphical representation of the state-space of the controlled system. You should observe that only the wanted behavior is present. The states shown are the same states that are reachable using the simulator.

Visualization of the controller

Follow these steps:

  • From a terminal, enter:
    • ./synscript -s PushButton_Lamp
    • cat PushButton_Lamp_simpcont.txt

This shows a textual representation of the controller, using logical expressions for each controllable event. It looks something like this:

# STS file: PushButton_Lamp.sts
# STS mapping file: PushButton_Lamp.stsmap
# BDD directory: .
# Logical expressions file: PushButton_Lamp.le
# Requested result expression: simpcont = (sup & elig)[cb]
# MVSIS command used: "set cost 2;fullsimp;fxu"
# Post-processing: enabled

# Event "Lamp1Off" ((supen & elig)[?cb?]):
Lamp.On & PushButton.Released

# Event "Lamp1On" ((supen & elig)[?cb?]):
Lamp.Off & PushButton.Pushed

From this you can see that in the controlled system (plants in parallel with the generated supervisor), controllable event 'Lamp1Off' is only enabled if automaton 'Lamp' is in location 'On' and automaton 'PushButton' is in location 'Released'. So only if the lamp is on, and the button is released, may the lamp be turned off. This is exactly what we want. Similarly for event 'Lamp1On'.

supcon/pushbutton_lamp_tutorial_state_based.txt · Last modified: Tuesday, 30 November 2010 : 12:57:48 by dhendriks