CIF 3

Exercise 1: getting familiar with the toolchain

The goal of the first exercise is to get familiar with the toolchain for the design of a supervisory controller, as well as the CIF 3 tooling that plays a role in the toolchain. The exercise also demonstrates why a controller is needed. The goal is to go through the entire process and use all the available tools, just as you would do when developing your own controller, for your own system. This exercise will guide you through the entire process, step by step. After this exercise, you should be able to do this by yourself.

Preparation

Make sure you installed the tooling, and made the 4K420 course files for one of four workstations available. If you follow the 4K420 course, choose the workstation you’re assigned. If you don’t follow the course, choose an arbitrary station.

In the remainder of this page, # will be used to refer to the name of the workstation, as part of for instance file names. That is, # will refer to input_station, test_station, process_station, or storage_station, depending on the workstation you’re using.

If you already previously installed the tooling, make sure to update it. Also update the 4K420 course files, if you previously made them available in your workspace.

The Button/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 untimed plants

We start by making an (untimed) model of the plants (automata representing the physical hardware). In this case the plants are Button1 and Lamp1. Follow these steps:

  • Right click the project for your workstation, and choose New ‣ File.

  • In the New File dialog, enter the file name of the new file. Use #_plants_reqs1.eventbased.cif as file name, where # is the name of your workstation. That is, if you use the input station, name the file input_station_plants_reqs1.eventbased.cif, etc.

  • Click Finish to actually create the file.

  • A text editor opens for the new file.

  • Add the following content to the file:

     1
     2
     3
     4
     5
     6
     7
     8
     9
    10
    11
    12
    13
    14
    15
    16
    17
    18
    19
    20
    21
    plant Button1:
      uncontrollable u_pushed, u_released;
    
      location Released:
        initial;
        edge u_pushed goto Pushed;
    
      location Pushed:
        edge u_released goto Released;
    end
    
    plant Lamp1:
      controllable c_on, c_off;
    
      location Off:
        initial;
        edge c_on goto On;
    
      location On:
        edge c_off goto Off;
    end
    
  • Save the file, by clicking File ‣ Save, by using the corresponding toolbar item, or by pressing Ctrl+S.

Explanation of the model

../../_images/exercise1_button1.png

The Button1 plant automaton (lines 1-10) shows all the physical behavior of the button (hardware). The button declares two uncontrollable events (line 2), u_pushed and u_released. These events respectively indicate the button being pushed and released, by the user. Initially, the button is released, as stated by the initial keyword (line 5), of location Released (lines 4-6). Once the user pushes the button (u_pushed event), the button is in a pushed state (location Pushed, lines 8-9). Hence, the edge (line 6) with that event to location Pushed (as indicated by the goto keyword). Once the user releases the button (u_released event), the button is once again in a released state, and thus in location Released.

The lamp is similar to the button: it can be turned on and off, in alternating sequences, and is initially off.

For more information on the terminology used, and the link between the graphical representation of automata and the textual CIF 3 syntax, see the Terminology overview page.

Simulation of the untimed plants

Follow these steps to simulate your untimed plants using the CIF 3 simulator:

  • Right click the #_plants_reqs1.eventbased.cif file, and choose Simulate CIF 3 specification....
  • Once the options dialog appears, go to the Output category, then the State visualization subcategory, and enable state visualization, by checking the checkbox labeled Visualize the state.
  • Click OK to continue, accepting the other default settings.

You are now simulating the model. In the GUI, you’ll see the following:

../../_images/exercise1_plants_sim.png

It shows two things (you may have to rearrange the GUI to get them to appear side by side), the current state, and the possible transitions that can be taken.

The State Visualizer shows the current state. The Button1 automaton is initially in its Released location, and the Lamp1 automaton is initially in its Off location. You may ignore the time variable for now.

The GUI input shows two possible transitions. You can choose a transitions by clicking on the corresponding button.

The two transitions that are possible are event u_pushed of Button1 (indicated as Button1.u_pushed), and event c_on of Lamp1 (indicated as Lamp1.c_on). Let’s choose the Button1.u_pushed event by clicking the button with that label. You’ll see in the state visualizer that automaton Button1 is now in location Pushed.

The possible transitions are now event Button1.u_released, and event Lamp1.c_on. Let’s choose the transition for event Button1.u_released. Since this transition is the first transition listed, it is the default transition. Therefore, just pressing ENTER is enough, if the button still has the focus. As you can see, both automata are back in the initial state.

You can choose some more transitions, undo some transitions, or reset the entire simulation back to the initial state. Feel free to simulate some more. To quit the simulation, simply close the GUI input.

While the state visualizer output is useful, later on we’ll use visualizations that give much more insight and provide a better overview of the entire system.

Once you’ve had enough, you should have realized something: it is possible to turn on the lamp, without ever even pushing the button. Since we only modeled the hardware (the plants), this is to be expected. We specified the possible behavior of the individual hardware components (the button and lamp), but there is no coupling between them. Next, we will add a supervisor.

Adding the supervisor

Next, we will manually add a supervisor, or supervisory controller. Open the text editor again, and add the following text, keeping the plants intact:

supervisor Supervisor:
  location ReleasedOff:
    initial;
    edge Button1.u_pushed goto PushedOff;

  location PushedOff:
    edge Button1.u_released goto ReleasedOff;
    edge Lamp1.c_on goto PushedOn;

  location ReleasedOn:
    edge Button1.u_pushed goto PushedOn;
    edge Lamp1.c_off goto ReleasedOff;

  location PushedOn:
    edge Button1.u_released goto ReleasedOn;
end

Do some simulations, to confirm that we now only get the expected behavior.

Note

Questions

  1. Do you understand why the supervisor looks the way it does, that is, why it is modeled this way?
  2. Why is it necessary for the button to be allowed to be released, before the lamp is turned on (location PushedOff)?

Make sure you know the answer to both questions, before you continue. If you follow the 4K420 course, check your answers with one of the teachers.

Modeling the requirements

We will once again change the CIF file. Switch to the text editor again. Remove the manually added supervisor, and add an (event-based) requirement instead. The result should look like this:

plant Button1:
  uncontrollable u_pushed, u_released;

  location Released:
    initial; marked;
    edge u_pushed goto Pushed;

  location Pushed:
    edge u_released goto Released;
end

plant Lamp1:
  controllable c_on, c_off;

  location Off:
    initial; marked;
    edge c_on goto On;

  location On:
    edge c_off goto Off;
end

requirement LampOnWhileButtonPushed:
  location Released:
    initial; marked;
    edge Button1.u_pushed goto Pushed;
    edge Lamp1.c_off;

  location Pushed:
    edge Button1.u_released goto Released;
    edge Lamp1.c_on;
end

Note that besides the added requirement, the initial locations of the plants are now also marked locations. Each automaton requires at least one marked location. Usually, the initial locations are also the marked locations.

Explanation of the model

The plants are still the same, except for the added marking. The requirement is very simple and specifies that initially the button can be pushed, as there is an edge with event Button1.u_pushed going to location Pushed. Then the lamp can go on (self loop with event Lamp1.c_on). But once the button is released, the lamp can only go off (another self loop). That is, until the button is pushed again, at which point the lamp can go on again, etc.

Synthesizing the supervisor

We are now ready to synthesize the supervisor. In the directory that contains your CIF file, locate the script file named 1a_synthesize1.tooldef2. Right click that file, and choose Execute ToolDef. In the Console view, you’ll see the output of the synthesis. The actual output depends on the tooling version you use, and the workstation you chose, but it should look somewhat like this:

File "generated_files/input_station_sup1.eventbased.cif": synthesizing...
Loading CIF specification "input_station_plants_reqs1.eventbased.cif"...
Converting to internal representation...
Computing supervisor...
Starting synthesis...
Pruning non-coreachables (4 locations, 6 edges)...
Pruning non-reachables (4 locations, 6 edges)...
Synthesis finished (4 locations, 6 edges).
Converting from internal representation...
Writing result to "generated_files/input_station_sup1.eventbased.cif"...
File "generated_files/input_station_sup1.eventbased.cif": synthesized.
File "generated_files/input_station_sup1.databased.cif": skipped ("input_station_plants_reqs1.databased.cif" was not found).

The Synthesis finished (4 locations, 6 edges). line indicates that synthesis completed successfully, and that a supervisor was synthesized that has four locations, and six edges. The Writing result to "generated_files/input_station_sup1.eventbased.cif"... line indicates that the synthesized supervisor is written to a file named input_station_sup1.eventbased.cif, in the newly created generated_files directory. The remaining details are of little interest at the moment.

You just synthesized your first supervisor!

Viewing the supervisor

Now that we have generated the supervisor, we would like to see what it looks like. To this end, we’ll open it in a text editor. Simple double click the file that contains the synthesized supervisor (in the generated_files directory), to open it.

Alternatively, you can generate a visual model diagram from the generated supervisor, using the CIF to yEd transformer.

Inspect the synthesized supervisor and make sure you understand it, and that it is correct. If the supervisor is wrong, you will need to go back to the original plants and requirements and change them. In this case, that is not necessary, so we continue with simulation.

Note

Questions

  1. Compare the manually created supervisor from before, with the newly synthesized supervisor. What do you observe?

Simulation of the hybrid plants and supervisor

Next, we will simulate the plants and supervisor to gain further understanding of the supervisor and to validate that it is indeed correct. We’ll use hybrid plant models, that include not only the discrete behavior, but also the timing of movements, etc. For the current exercise, the timing of the behavior is of little interest, but for later exercises, the hybrid simulation model will provide significant benefits. For now, the visualization that is coupled to the hybrid simulation model, will already make it easier to test our supervisor.

In the directory that contains your CIF file with the plants and requirements, locate the script file named 2_simulate.tooldef2. Right click that file, and choose Execute ToolDef. The script will perform various tasks, which includes (re)synthesizing the supervisor if necessary, and merging the supervisor with the simulation model. Once it starts the simulator, you’ll be presented with an options dialog. Simply click OK to confirm the default settings.

After closing the dialog, the simulator will start. This may take a few seconds. Once the simulator is initialized, the visualization of the workstation will be shown. A part of the visualization shows the buttons and lamps (your actual visualization may be different, if you chose a different workstation):

../../_images/exercise1_sshot_viz_ui1.png

Here, the buttons all have red circles, to indicate that they are released. That is, the sensors that detect whether the buttons are pushed are all off. The lamps are all off as well, as indicated by the gray circles.

You can now interactively push a button, by clicking on the red circle just beneath the Button1 text. Clicking that circle will change the visualization:

../../_images/exercise1_sshot_viz_ui2.png

Since clicking the button results in the corresponding button sensor going on, the circle for that button sensor is now green. Quickly after clicking the button, the supervisor will turn on the lamp:

../../_images/exercise1_sshot_viz_ui3.png

Clicking the green circle will release the button. You may experiment a bit more, by pressing and releasing the button. Note that by clicking the button in the user interface, the button is pushed, and by clicking it again, the button is released. That is, to push and release the button, you need to click twice. If all is well, you should see that the supervisor correctly controls the system.

To stop the simulation, you’ll need to terminate the simulator.

This visualization-based simulation approach makes it much easier to test the supervisor, as we no longer need to choose transitions from the console. Instead, we can just click on the visualization, and immediately observe the result of the supervisor that controls the system.

Controlling the actual hardware

Once you have validated your supervisor, it is time to move on to controlling the actual hardware.

Controlling the hardware involves the use of one of the four workstations, and is only possible if you have access to the lab where these workstations are located. You’ll need to turn on the computer next to the workstation, if it is not already on. Also, make sure you’ve turned on the power supplies (three in total for all four workstations), and the compressed air valve (one valve for all stations) is opened (handle in the vertical position). Then, you need to follow some steps on the computer next to the workstation, taking into account the following:

  • When asked to provide a name for the TwinCAT project and solution, choose #_plc (where # is replaced by the name of your workstation). Create the solution in the directory that contains the CIF file with your plants and requirements, on your G drive (network share).
  • When instructed to run the script, execute the 3_gen_plc_code.tooldef2 script.
  • When instructed to load TwinCAT I/O mappings, use the #_twincat_io_mapping.xml file provided by the 4K420 course files.

The steps further describe all you need to be able to do in TwinCAT, to control the physical hardware setup, and can be found in the TwinCAT usage section of the TwinCAT PLC output page. That page also provides further information on the use of TwinCAT. In particular, if you run into problems using TwinCAT, read the Frequently Asked Questions (FAQ) section of that page.

You should be able to press the button on the hardware labeled PushButton1 and the lamp with name Lamp1 should go on. Verify that your supervisor enforces the correct behavior.

Using data-based synthesis

So far, we’ve used event-based synthesis. To use data-based synthesis, simply rename the #_plants_reqs1.eventbased.cif file to #_plants_reqs1.databased.cif. You can then use the simulation script (2_simulate.tooldef2) to automatically re-synthesize the supervisor using data-based synthesis, merge the result with the simulation model, and simulate it again. You should try this now.

The event-based requirement that we used, can be used for data-based synthesis as well. However, for data-based synthesis, we may also use state-based or data-based models. State-based models are similar to event-based models, but additionally allow referring to plant locations in requirements. Data-based models allow even more language features, including variables, guards, updates, and invariants.

We can replace the event-based LampOnWhileButtonPushed requirement automaton by the following state-based requirement invariants:

// Lamp on only while button is pushed.
requirement Lamp1.c_off needs Button1.Released;
requirement Lamp1.c_on  needs Button1.Pushed;

The first requirement indicates that for the lamp to be turned off, the button needs to be released. That is, the lamp can only be turned off while the button is released. In other words, as long as the button is pushed, the lamp can not be turned off. Similarly, the second requirement relates turning the lamp on to the button being pushed.

Then, using the simulation script (2_simulate.tooldef2), we can automatically re-synthesize the supervisor using data-based synthesis, merge the result with the simulation model, and simulate it again. You should try this now.

Reading material

Before you continue with the next exercise, you may want to read the may want to read some of the reference information provided as part of this documentation. Of particular interest is the Toolchain section, which contains an overview of the entire toolchain, as well as detailed descriptions of each phase and the step required in each phase. You should read that section at least once, in its entirety. Also of interest may be the 4K420 workstations section, which explains the four workstations, their sensors and actuators, etc.