Table of Contents 
Previous Chapter 3 Tutorial: A First Example
In addition to simulating a system, it is also possible to validate the system using the SDT Validator. A validator can be used to automatically find errors and inconsistencies in a system, or to verify the system against requirements.
In the same way as for a simulator, you must generate an executable validator and start it with a suitable user interface.
-----------------------------------------------------------------------
Note:
In order to generate a validator that behaves as stated in the exercis
es, you should copy all SDL diagrams that are included in the distri
bution to your work directory (~/demon_game). These diagrams are
by default stored in a subdirectory to the SDT installation directory.
The name of the directory should be
$sdtrelease/examples/demongame
If you generate a validator from the diagrams that you have created,
the scheduling of processes (i.e. the execution order) may differ.
-----------------------------------------------------------------------
- To quickly generate and start an executable validator.
A validator can be generated and started in the same way as described earlier for the simulator, i.e., by using the Make dialog and the Tools menu in the Organizer. However, we will now show a quicker way.
- Make sure the system diagram icon is selected in the Organizer.
- Click the Validate quick button. The following things will now happen, in rapid succession:
- An executable validator is generated. Messages similar to when generating a simulator are displayed in the Status Bar, ending with "Compiler done." This is the same action as manually using the Make dialog and selecting a validator kernel. If you like, you can verify that a validator kernel has been used by looking at the tail of the Organizer log.
- A graphical user interface to the validator is started. The Status Bar of the Organizer will read "Validator UI started." This is the same action as manually selecting Validator UI from the Tools menu.
- The generated validator is started. The Validator UI shows the message "Welcome to SDT VALIDATOR." This is the same action as manually using the Open quick button and selecting the executable validator (named demongame_vla.val).
The Validator UI looks like this:
Figure\x11 124 : The Main Window of the Validator UI.
-----
(fig)
-----
As you can see, the graphical user interface of a validator is very similar to a simulator GUI, which you have learned to use in the previous exercises. However, the button modules to the left are different and a few extra menus are available.
A validator contains the same type of monitor system as a simulator. The only difference is the set of available commands.
When a validator is started, the static process instances in the system are created (in this case Main and Demon), but their initial transitions are not executed. The process in turn to be executed is the Main process. You can check this by viewing the process ready queue:
- In the button module View, click the Ready Q button. The first entry in the ready queue is Main, waiting to execute its start transition.
- If required, resize the Validator UI window so that all button modules are visible. You may also reduce the width of the text area. In the exercises to come, you will have a number of windows open at the same time.
Before you start working with the validator exercises, you should have an understanding about the basic concepts of the SDT Validator.
- When examining an SDL system using the validator, the SDL system is represented by a structure called a behavior tree. In this tree structure, a node represents a state of the complete SDL system. The collection of all such system states is known as the state space of the system.
- By moving around in the behavior tree, you can explore the behavior of the SDL system and examine each system state that is encountered. This is called state space exploration, and it can be performed either manually or automatically.
- The size and structure of the behavior tree is determined by a number of state space options in the validator. These options affect the number of system states generated for a transition in an SDL process graph, and the number of possible branches from a state in the behavior tree.
In this first exercise, we will explore the state space of the Demongame system by manually navigating in the behavior tree. The validator will then behave in a way similar to when running a simulator. However, there are also important differences, which will be pointed out.
By default, the validator is set up in a way that results in a state space as small as possible. In this set-up, a transition between two states in the behavior tree always corresponds to a complete transition in the SDL process graphs. Also, the number of possible branches from a state is limited to a minimum.
- To use the Navigator tool
- To get printed trace and GR trace.
When interactively exploring the behavior tree, a validator tool called the Navigator is used.
- Start the Navigator by clicking the Navigator button in the Explore module. The Navigator window is opened:
Figure\x11 126 : The Navigator Tool.
-----
(fig)
-----
The Navigator shows part of the behavior tree around the current system state. In general, the upper box represents the behavior tree transition leading to the current state, i.e., the transition that just has been executed. The boxes below represent the possible tree transitions from the current state. They are labelled Next 1, Next 2, etc. and have not yet been executed.
Since the system now is in its start state, there is no up node. The only next node is the start transition of Main.
- To be able to see the printed trace familiar from simulation, open the Command Window from the View menu. (The trace is not printed in the main window of the validator.)
- To switch on GR trace of SDL symbols, select Toggle SDL Trace from the Commands menu in the Validator window; SDL trace is now enabled. However, an SDL Editor will not be opened until the first transition is executed.
- In the Navigator, execute the next transition by double-clicking on the Next 1 node. The following happens, in order:
- If needed, move and resize all opened windows to make them completely visible and still fit on the screen together.
- Double-click the Next 1 node to execute the next transition. The start transition of Demon is traced in the Command window and in the SDL Editor.
At this stage, neither of the two active processes can continue without signal input; Main awaits the signal Newgame from the environment, and Demon awaits the sending of the timer signal T. These are the two transitions from the current state now shown in the Navigator as Next 1 and Next 2. As you can see, the transitions in the boxes are described by the same type of information as in a printed trace.
Figure\x11 129 : Transition Descriptions in the Navigator.
-----
(fig)
-----
This means that the validator gives information of all possible transitions from the current system state, even though they have not been executed yet. (This information cannot easily be obtained when running a simulator.)
- Send the timer signal by double-clicking the Next 2 node. The Command window tells us that the timer signal is sent and the Navigator shows that the next transition is the input of the timer T.
- Execute the next transition by double-clicking the Next 1 node. This is where the dynamic error in the Demongame system occurs, as explained in the simulator tutorial earlier (see "Dynamic Errors" on page 143). Instead of showing the next transition, the Navigator displays the error message in the next box.
Figure\x11 130 : The Dynamic Error.
-----
(fig)
-----
- Double-click the Up 1 node to go back to the previous state. Repeat this action again to go to the state we were in after step 3 above. This way of backing up in the execution is not possible when running a simulator, as you may have noticed when running the Simulator tutorial.
You should also note that the Next 2 node is marked with three asterisks "***." This is used to indicate that this is the transition we have been backing up through:
Figure\x11 132 : Marking a Transition that has been Backed Through.
-----
(fig)
-----
- Execute the Next 1 transition instead with a double click. The printed trace shows that the signal Newgame was sent from the environment. The Main process is ready to receive the signal. Note that you do not have to send the signal yourself; this is taken care of automatically by the validator.
- Execute the next transition. The printed trace and the SDL trace show that Main now is in the state Game_On. The Navigator displays the start transition of the newly created Game process.
- Execute the start transition of Game. The Navigator will now show the different signal inputs that are required to continue execution: Endgame, Probe, Result, and the timer T.
Figure\x11 133 : Signal Inputs Required for Continued Execution.
-----
(fig)
-----
If the number of transitions from a state is large, it may be difficult to see them all in the Navigator when a tree structure is used. To overcome this problem, the display can be changed to a list structure.
- Click the Structure quick button to see how the list structure looks like. Now it is easier to see the possible signals.
Figure\x11 134 : The List Structure.
-----
(fig)
-----
- Change back to the tree structure.
We will not continue further down in the behavior tree in this exercise. Figure 135 on page 188 shows the part of the behavior tree we have explored so far. The nodes in the figure represent states of the complete SDL system. Each node lists the active process instances that have changed since the previous system state, what process state they are in and the content of their input queues. The arrows between the nodes represent the possible tree transitions. They are tagged with a number and the SDL action that causes the transition. The arrow numbers are the same numbers as printed in the Next nodes in the Navigator.
Note that this is a somewhat different view of the behavior tree compared to the Navigator. In the Navigator, the nodes represent the tree transitions and the process states are not shown.
Figure\x11 135 : A Demongame Behavior Tree.
-----
(fig)
-----
In this exercise, we will take a look at some of the additional tracing and viewing possibilities of the validator.
- To print a complete trace from the start state
- To use the view commands
- To use the MSC trace facility
- To go to a state by using the path commands.
- Make sure you are still in the same state as after the last step in the previous exercise.
To see a complete printed trace from the start state to the current state, you can use the Print-Trace command. As parameter, it takes the number of levels back to print the trace from.
- On the input line of the Validator UI, enter the command pr-tr 9 (you can use any large number). The trace is printed in the text area of the main window. This trace gives an overview of what has happened in the SDL system so far.
- The validator supports the same viewing commands as the SDT simulator. Click the Timer List button in the View module to list the active timer set by the Demon process.
- Examine the GameP variable in the Main process by clicking the Variable button and making selections in the dialogs.
--------------------------------------------------------------------
Note:
The first dialog asks for a process, which the corresponding simula
tor command does not. The reason is that the validator has no con
cept of process scope, so you have to select the process explicitly.
--------------------------------------------------------------------
- You may also use the Watch window in the validator to continuously monitor the values of variables.
In addition to textual and graphical traces, the validator can also perform an MSC trace.
- First, turn off SDL trace by selecting Toggle SDL Trace from the Commands menu. Then, turn on MSC trace from the same menu. An MSC Editor is opened, showing a Message Sequence Chart for the trace from the start state to the current state.
Figure\x11 136 : The Current MSC Trace.
-----
(fig)
-----
- When the MSC appears, execute, with a double-click, one of the signal transitions in the Navigator, e.g. Probe. The message is appended to the MSC.
Figure\x11 137 : Appending Probe to the MSC.
-----
(fig)
-----
- Go up a few levels in the Navigator.
Note how the selection in the MSC Editor changes to reflect the MSC event corresponding to the current state!
- Go down again, but select a different path than before, i.e., send one of the other signals.
Note how the MSC diagram is redrawn to show the new behavior of the system!
- Toggle MSC trace off in the Commands menu. Unless other MSC diagrams were opened, the MSC Editor is closed.
You can use the commands Print-Path and Goto-Path to return to a state where you have been before.
- Execute the command Print-Path from the input line. The output represents the path taken in the behavior tree from the start state to the current state.
Command : print-path
1 1 1 1 1 3 0
- The numbers in the path are the same as the transition numbers in the Navigator, and the arrow numbers shown in Figure 135 on page 188.
- Go up a few levels in the Navigator.
- In the text area, locate the path printed by the Print-Path command above (you may have to scroll the text area). With the mouse, select the numbers in the path by dragging the mouse to the end of the line. Make sure you select the final zero.
- In the input line, enter goto-path and a space character. Paste in the path numbers by positioning the mouse pointer at the end of the entered text and clicking the middle mouse button. Hit <Return> to execute the command. You now end up in the previous state.
- If you make an error while copying or pasting the path numbers, simply clear the input line by using the <Down> arrow key and try again.
In the previous exercises, we have navigated manually in the behavior tree. We have also found an error situation by studying the Navigator and the printed trace in the Command window.
In this exercise, we will show how to find errors and possible problems by automatically exploring the state space of the Demongame system. This is referred to as validating an SDL system.
- To perform an automatic state space exploration
- To examine reported errors using the Report Viewer
- To change state space and exploration options
- To check the system coverage of an exploration
- To use user-defined rules
- To perform a random walk exploration.
Automatic state space exploration can be performed using different algorithms. The algorithm called bit state exploration can be used to efficiently validate reasonably large SDL systems. It uses a data structure called a hash table to represent the system states that are generated during the exploration.
An automatic state space exploration always starts from the current system state. Since we want to explore the complete Demongame system, we must first go back to the start state of the behavior tree.
- Go to the top of the tree by clicking the Top button in the Explore module.
- Start a bit state exploration by clicking the Bit-State button. After a few seconds, a tool called the Report Viewer is opened. We will soon describe this window; in the meantime, just move it away from the main window.
- For a small system such as Demongame, the exploration is finished almost immediately and some statistics are printed in the text area. They should look something like:
** Starting bit state exploration **
Search depth : 100
Hash table size : 1000000 bytes
** Bit state exploration statistics **
No of reports: 1.
Generated states: 2569.
Truncated paths: 156.
Unique system states: 1887.
Size of hash table: 8000000 (1000000 bytes)
No of bits set in hash table: 3642
Collision risk: 0 %
Max depth: 100
Current depth: -1
Min state size: 68
Max state size: 124
Symbol coverage : 100.00
Of the printed information, you should note the following:
- Search depth : 100
The search depth limits the exploration; it is the maximum depth, or level, of the behavior tree. If this level is reached during the exploration, the current path in the tree is truncated and the exploration continues in another branch of the tree. It is possible to change the search depth by setting an option in the Validator UI.
- No of reports: 1.
The exploration found one error situation. This error will be examined in the next exercise.
- Truncated paths: 156.
The maximum depth was reached 156 times, i.e., there are parts of the behavior tree that were not explored. This is a normal situation for SDL systems with infinite state spaces. Demongame is such a system, since the game can go on forever.
- Collision risk: 0 %
The risk for collisions was very small in the hash table that is used to represent the generated system states. If this value is greater than zero, the size of the hash table may have to be increased by setting an option; otherwise, some paths may be truncated by mistake. This situation will not occur in this tutorial.
- Symbol coverage : 100.00
All SDL symbols in the system were executed during the exploration. If the symbol coverage is not 100%, the validation cannot be considered finished. This situation will occur in a later exercise.
The error situations reported from a state space exploration can be examined in the Report Viewer. The Report Viewer window displays the reports in the form of boxes in a tree structure.
Figure\x11 138 : The Report Viewer.
-----
(fig)
-----
- The top box shows how many reports there are (in this case only one).
- On the next level in the report tree, there is one box for each type of report, stating the number of reports of that type.
- On the next level, it is possible to see the actual reports. However, this level of the tree is by default collapsed, indicated by the small triangle icon below the report type boxes.
- To expand the report, double-click on the report type box Output. You will now see a box reporting the error we have found manually earlier. In addition, the tree depth of the error situation is shown.
Figure\x11 139 : An Expanded Report.
-----
(fig)
-----
If you look in the Navigator and Command windows, you can see that the validator is still in the start state of the system, even though a state space exploration has been performed. We will now go to the state where the error has occurred.
- Double-click the report box in the Report Viewer. The following things will now happen:
- The printed trace of the error situation is displayed in the text area of the Validator UI and in the Command window.
- The Navigator moves to the error state and displays the error.
- An MSC Editor is opened, showing the MSC trace to the current state. You can see that the signal Bump was not received by any process, since the Game process has not yet been created.
Once you have used the Report Viewer to go to a reported situation, you can easily move up and down the path to this state. Simply use the Up and Down buttons in the Explore module, instead of double-clicking a node in the Navigator:
- Move up two steps by using the Up button. Of the two transitions possible from this state, the one that is part of the path leading to the error is indicated by three asterisks "***" (see Figure 132 on page 186). This is the transition chosen when using the Down button.
- Move up to the top of the tree (click the Top button in the Explore module). Move down again to the error by using the Down button repeatedly.
Note that you do not have to chose which way to go when the tree branches. The path to the error is remembered by the validator until you manually chose another transition.
We will now run a more advanced bit state exploration, with a different setting of the state space options. This will make the state space much larger, so that more error situations can be found.
- Go back to the top of the behavior tree (use the Top button).
- In the Explore module, click the Advanced button. This sets a number of the available state space options in one step, as you can see by the commands executed in the text area:
Command : def-sched all
Command : def-prio 1 1 1 1 1
Command : def-max-input-port 2
Max input port length is set to 2.
Command : def-rep-log maxq off
No log for MaxQueueLength reports
Note that the Navigator now shows two possible transitions from the start state; this is an immediate effect of the larger state space.
- In addition, we will increase the search depth of the exploration from 100 (the default) to 200. From the Options2 menu, select Bit-State: Depth. In the dialog, enter 200 and click OK.
Figure\x11 140 : Specifying Depth = 200.
-----
(fig)
-----
Since the behavior tree becomes much larger with these option settings, the exploration will take longer to finish. We will therefore show how to stop the exploration manually.
- Start a new bit state exploration. In the text area, a status message is printed every 20,000 transitions that are executed. Stop the exploration after one of the first status messages by pushing the Break button in the Explore module. The text area should now display something like this:
*** Break at user input ***
** Bit state exploration statistics **
No of reports: 2.
Generated states: 72000.
Truncated paths: 2472.
Unique system states: 25905.
Size of hash table: 8000000 (1000000 bytes)
No of bits set in hash table: 50554
Collision risk: 0 %
Max depth: 200
Current depth: 161
Min state size: 68
Max state size: 168
Symbol coverage : 100.00
Command :
Note the following differences in the printed information compared to the previous exploration:
- No of reports: 2.
The exploration found an additional error situation. This is an effect of more transitions being able to execute from each state in the behavior tree.
- Max depth: 200
Current depth: <number>
The exploration was at the printed depth in the behavior tree at the moment it was stopped. However, since the exploration uses a depth-first algorithm, the maximum depth of 200 was reached at an earlier stage. The exploration may be continued from the current depth if you wish to explore the remaining parts of the behavior tree.
- In the Report Viewer, open the two report type boxes to see both reports with a double-click on each. The Report Viewer window should now look something like:
Figure\x11 141 : The Two Reports as Displayed in the Window.
-----
(fig)
-----
- For now, just note on which depth each of the reported situations occurred; do not double-click any of the reports.
- Continue the exploration by clicking the Bit-State button again. A dialog is opened, asking if you would like to continue the interrupted exploration or restart it from the beginning.
Figure\x11 142 : Continuing the Exploration.
-----
(fig)
-----
- In the dialog, select Continue and click OK. Wait for the exploration to finish by itself.
- In the Report Viewer, open the two reports again. Note that the depth values have changed. This is because only one occurrence of each report is printed; the one found at the lowest depth so far.
- Go to the state where an unsuccessful create of the Game process was reported (double-click the Create report).
Figure\x11 143 : The Report about an Unsuccessful Process Create.
-----
(fig)
-----
- To see what caused the unsuccessful create, look at the MSC trace.
At the receipt of the last Newgame signal, the Main process attempts to create a Game process. However, the already active Game process has not yet consumed the previous GameOver signal, and has therefore not been terminated. Since you cannot have more than one instance of the Game process in the Demongame system, the process create could not be executed!
If the symbol coverage after an automatic state space exploration is less than 100%, the Coverage Viewer can be used to check what parts of the system that have not been executed. To attain a symbol coverage less than 100% for the Demongame system, we will set up the exploration in a special way.
- Go to the top of the tree.
- First, we need to restore the smaller, default state space. Click the Default button in the Explore module. Note that the Navigator changes back to display only a single possible transition from the top node.
- To avoid reaching all system states, we will reduce the search depth of the exploration from 100 to just 10. Use the Bit-State: Depth menu choice from the Options2 menu and specify a maximum depth of 10.
- Start a bit state exploration. The printed statistics should now inform you that the symbol coverage is about 82%.
- If the symbol coverage still is 100%, click Reset in the Explore module and repeat steps 3 and 4 above.
- To find out which parts of the Demongame system that have not been reached, open the Coverage Viewer from the Commands menu.
A symbol coverage tree is displayed, showing all symbols which have not been executed yet.
- Change to a transition coverage tree by clicking the Coverage Type quick button.
Figure\x11 144 : The Transition Coverage Tree.
-----
(fig)
-----
You can now see that none of the transitions from the state Winning in the Game process has been executed. To explore this part of the system in the validator, you can go to the state Winning and start a new exploration from there. How to do this is explained in the following exercises.
To go to a particular system state, you could use the Navigator to manually find the state by studying the transition descriptions and the printed trace in the Command window. This can be both tedious and difficult, especially for larger systems than Demongame. Instead, we will show an easier way: by using a user-defined rule.
When performing state space exploration, the validator checks a number of predefined rules in each system state that is reached. It is when such a rule is satisfied that a report is generated.
In this exercise, we will show how to define a new rule to be checked during state space exploration. The rule will be used to find the state Winning in the Game process.
- Make sure you still are at the top of the behavior tree.
- Define a new rule by selecting Define Rule from the Commands menu. In the dialog that appears, enter the rule definition
state(Game:1)=Winning
Figure\x11 145 : Specifying a New Rule.
-----
(fig)
-----
This very simple rule says that the state of the process instance Game:1 must be equal to Winning. By defining the rule, a report will be generated when a state space exploration reaches a state that satisfies the rule.
- Start a bit state exploration. Since we have not changed any of the options since the last exploration the same statistics will be printed, with the exception that an additional report is generated.
- From the Report Viewer, go to the reported situation where the user-defined rule was satisfied. You have now reached the first place in the behavior tree where the Game process is in the state Winning. We will now start another type of state space exploration from this state; a random walk.
Apart from bit state exploration, there is another exploration method known as random walk. A random walk simply explores the behavior tree by repeatedly choosing a random path down the tree. This is mainly useful for SDL systems where the state space can be very large. For a small system like Demongame, it can be as effective as other exploration methods.
- First, we have to clear the user-defined rule and the current reports. Enter the commands clear-rule and clear-reports on the input line.
- Start a random walk exploration from the current state by clicking the Random walk button. From the printed statistics, you can see that the symbol coverage now has become 100%.
- Open the Coverage Viewer from the Commands menu. Note that all symbols have been executed at least 4 times.
To see that a random walk for the whole Demongame system gives a full coverage of all symbols, do as follows:
- Reset the system by clicking the Reset button in the Explore module. You are now back at the top of the tree.
- Perform a random walk. The symbol coverage should be 100%.
- Open the Coverage Viewer from the Commands menu. Change to transition coverage and display the whole tree. Note that all transitions have executed a large number of times. When the exploration selects a random path down the tree, there is no mechanism to avoid that already explored paths are explored once more. Therefore, the same transition may be executed any number of times.
- Exit the Coverage Viewer from the File menu.
Another main area of use for a validator is to verify a Message Sequence Chart. To verify an MSC is to check if there is a possible execution path for the SDL system that satisfies the MSC. This is done by loading the MSC and performing a state space exploration set up in a way suitable for verifying MSCs.
In this exercise, we will verify one MSC made on the system level, i.e., an MSC that only defines signals to and from the environment. The MSC is included in the SDT distribution and is shown in the figure below. The name of the MSC file is systemlevel.msc and is located in the same directory as the remaining files for the DemonGame example.
Figure\x11 146 : A System Level MSC.
-----
(fig)
-----
- From the operating system prompt, make sure you can locate the MSC mentioned above (systemlevel.msc). Make a copy of the MSC and put it in your tutorial directory.
- If you cannot find the MSC, ask your system manager or the person responsible for the SDT environment at your site.
- Reset the system by clicking the Reset button in the Explore module.
- Start an MSC verification by clicking the Verify MSC button. A file selection dialog is opened, in which you select the MSC to verify.
- Select systemlevel.msc and click OK. A state space exploration is immediately started, which is guided by the loaded MSC.
In the printed statistics, note that the exploration is completed without any truncated paths. This is because the loaded MSC restricts the size of the behavior tree; only the parts dealing with the events in the MSC are executed. The maximum depth of it is not more than 13.
The last line printed tells if the MSC was verified or violated:
** MSC SystemLevel verified **
The MSC was verified, i.e., the behavior described in the MSC was indeed possible. In the Report Viewer, however, one of the reports is a violation of the loaded MSC, while the other one is a verification of the MSC. The exploration may very well find states that violate the MSC; it is the existence of states that verify the MSC that determines the result of the verification.
Figure\x11 147 : One Violation and one Verification of the MSC.
-----
(fig)
-----
- Go to the state where the MSC was verified. The printed trace in the Command window shows that the Main process has received the Endgame signal, and sent the GameOver signal to the Game process:
* OUTPUT of GameOver. Receiver: Game:1
* Signal GameOver received by Game:1
- Take a look at the MSC trace and compare it with the loaded MSC in Figure 146 on page 204. Note that the loaded MSC only defines signals to and from the environment and therefore is less detailed than the MSC trace. An MSC trace in the validator is always made on the process level.
Figure\x11 148 : The MSC Trace.
-----
(fig)
-----
The validator tutorial is now finished. Close the validator windows in the following way:
- To close the Navigator and the Report Viewer, click the Close quick button in these windows.
- To close the Command window, select Close from the File menu.
- Exit the Validator UI from the File menu. Since you have changed some of the options, you are asked in a dialog whether to save the changes.
Figure\x11 149 : Saving Changed Options.
-----
(fig)
-----
- If you select Yes and click OK, the option settings are saved in a file called .valinit. This file is read each time the Validator UI is started from the same directory, or when the validator is restarted or reset from the Validator UI. You should select No and click OK.
You have now learned the basics of SDT; we hope you have enjoyed the "tour". The example you have been practising on, the system DemonGame, is however rather simple. To deepen your knowledge about SDT, you may practise on a number of exercises that illustrate the advantages of SDL-92 when adopting an object-oriented design methodology. These exercises are described in chapter 4, Tutorial: An SDL-92 Example.
Table of Contents 
Next Chapter
