![]() |
![]() |
![]() |
![]() |
![]() |
Configuring the SDL Explorer
This section describe the various possibilities available to control the behavior of the Explorer using the options that can be defined for different features. The available options are grouped into a number of categories; each category and option will be described later in this section.
Managing Options
Each option can be set using a monitor command, usually named something similar to "Define-<option>". Most options can also be set from the menus Options1 and Options2 in the Explorer UI. The monitor command and menu choice associated with an option is listed together with the description of the option.
If the options are changed during a session with the Explorer, you will be asked whether to save the options when you exit or restart the currently executing explorer. If you save the options, the new values will be stored in a file named .valinit (on UNIX), or valinit.com (in Windows), in the directory from where the SDL Suite was started. This file will automatically be loaded the next time the Explorer is started from the same directory, thus restoring the previous options.
Some monitor commands operate on all the options:
- To print a list of all options and their current values, select
Show Options from either the Options1 or Options2 menu, or enter the command Show-Options. (A few of the options described here are not listed.)- To set all options to their predefined default values, click the
Default button in the Explore module, or enter the command
Default-Options. Note that this also clears all reports.- To set all options to their initial values, i.e. the values set when the explorer was started, click the Reset button in the Explore module, or enter the command Reset.
This command also resets the explorer completely and is equivalent to restarting the explorer from scratch. To just set the options to their initial values without resetting the explorer:
- Set the options to their default values. See above.
- Read in the file .valinit (on UNIX), or valinit.com (in Windows); see above. Select Include Command Script from the Commands menu, or enter the command Include-File.
Affecting the State Space
Some of the options affect, directly or indirectly, the size of the state space and the structure of the behavior tree. This can only be done while being in the current root of the behavior tree, since the whole structure of the tree may be affected. If such an option is changed when the explorer is not in the current root of the behavior tree, you have two choices: either to change the current system state back to the current root, or to redefine the current root to the current system state.
In this case, the following dialog is opened:
To change the root to the current system state, select yes and click OK. (In stand-alone mode, enter yes)
To keep the current root and move back to it, select no and click OK. (In stand-alone mode, enter no)
It is not possible to cancel this operation, i.e. you have to either change the current root or the current system state.
Bit State Exploration Options
Bit state exploration is an efficient automatic state space exploration algorithm for reasonably large SDL systems (for a reference, see [17]). It performs a depth-first search through the state space and uses a bit array to store the states that has been traversed during the search.
Every time a new system state is generated during the search, two hash values are computed from the system state. The bit array is checked:
- If both of the positions indicated by the hash values are already set, the state is considered to have been previously visited. The search of this particular path in the state space is pruned, and the search backs up to a previous system state and continues elsewhere.
- If both of the positions are not set, the state is a new state that has not been previously visited. Both position in the bit array are then set and the search continues with the successor states.
Search Depth
The search depth is the maximum depth the Explorer will explore a particular execution path in the state space. When this depth is reached, the search is truncated and the search backs up to a previous system state.
- Default value: 100
- Command: Define-Bit-State-Depth
- Menu choice: Options2: Bit-State: Depth
Hash Table Size
The size of the bit array used as hash table is an important factor defining the behavior of the bit state exploration. The reason is that each time a new state is checked by comparing its hash values with previous hash values there is a risk for collision. The bigger the hash table is, the smaller the collision risk is.
- Default value: 1,000,000 (bytes)
- Command: Define-Bit-State-Hash-Table-Size
- Menu choice: Options2: Bit-State: Hash Size
Random Walk Options
Random walk is an automatic state space exploration algorithm that can be useful for very large SDL systems. It performs a depth-first search through the state space by selecting transitions to execute at random.
When the maximum search depth is reached during such a "random walk," the search is restarted from the original state again and a new random walk is performed. However, there is no mechanism to avoid that already explored paths are explored once more, i.e. a system state may be visited a large number of times.
Search Depth
The search depth determines how many transitions will be executed before the search is pruned and restarted from the beginning again.
- Default value: 100
- Command: Define-Random-Walk-Depth
- Menu choice: Options2: Random: Depth
Repetitions
The number of times the random walk search will be repeated from the start state before the exploration is finished.
- Default value: 100
- Command: Define-Random-Walk-Repetitions
- Menu choice: Options2: Random: Repetitions
Exhaustive Exploration Options
Exhaustive exploration is an automatic state space exploration algorithm intended for small SDL systems where the requirements on correctness are very high.
The algorithm is a depth-first search through the state space similar to the bit state search, but there is no collision risk involved. The reason is that all traversed system states are stored in primary memory, so it is always possible to determine whether a newly generated system state has already been visited during the search.
The drawback with the algorithm is that very much primary memory is needed to be able to store all traversed states. This limits the complexity of the SDL systems the algorithm is applicable to.
Search Depth
The search depth is the maximum depth the Explorer will explore a particular execution path in the state space. When this depth is reached, the search is truncated and the search backs up to a previous system state.
- Default value: 100
- Command: Define-Exhaustive-Depth
- Menu choice: Options2: Exhaustive: Depth
MSC Verification Options
The MSC verification algorithm is a bit state exploration that is adapted to suit the needs of MSC verification:
- An MSC is always loaded to guide the search
- The search depth is different from the depth used during usual bit state exploration
- The search is aborted as soon as the MSC has been verified.
Search Depth
The maximum depth searched by the algorithm. The intention is that this depth always should be enough. If the MSC verification fails and the number of truncations is more than 0, this depth should be increased.
- Default value: 1,000
- Command: Define-MSC-Verification-Depth
- Menu choice: Not available
Timer Check Level
When verifying an MSC where there are timers in the MSC and/or in the SDL system, there is a choice of how to perform the matching between the timer events in the MSC and in the SDL system. The timer check level determines how this matching should be done:
- 0: No checking of timer events is performed.
- 1: If a timer event exists in the MSC a matching timer event must exist in the explored SDL path, but a timer event in the explored SDL path is accepted even if there is no corresponding MSC timer event.
- 2: All timer events in the MSC must match a corresponding timer event in the explored SDL path, and vice versa.
The choice must be determined by the style of MSC that is used.
This option affects the state space; see Affecting the State Space.
- Default value: 1
- Command: Define-Timer-Check-Level
- Menu choice: Options2: MSC: Timer check level
Report Options
For each report type, you can define the action performed when the report is found and whether it should be reported to the user.
Report Action
The report action determines what action should be performed when a report situation is encountered while performing state space exploration. There are three possibilities:
- Continue: The search continues past the reported situation as if it never happened.
- Prune: The search is pruned and depending on the algorithm some appropriate action is taken. For example, when using bit state exploration, the search will back up one state and continue with the next alternative transition, as if max search depth was reached and the search truncated.
- Abort: The search is aborted and the command prompt displayed.
Note that for some report types, like Deadlock, the continue choice is impossible.
This option affects the state space; see Affecting the State Space.
- Default value: Prune for all report types
- Commands: Define-Report-Continue, Define-Report-Prune and Define-Report-Abort
- Menu choices: Options2: Report: Continue, Options2: Report: Prune and Options2: Report: Abort
Report Log
The report log setting defines whether the report should be recorded in the list of generated reports. If the report log is set to Off for a particular report type, these reports will never show up in the report list. Note however that the report action still is performed, even though the report is not logged.
This option affects the state space; see Affecting the State Space.
- Default value: On for all report types
- Command: Define-Report-Log
- Menu choice: Options2: Report: Report log
Report Viewer Autopopup
When an automatic state space exploration is finished, the Report Viewer is normally started automatically to present the found reports. In some cases this may be inconvenient, so there is a possibility to turn this feature off.
- Default value: On
- Command: Define-Report-Viewer-Autopopup
- Menu choice: Options1: Report Viewer Auto Popup
MSC Trace Options
When the Explorer performs an MSC trace, you can define what types of events that are traced.
Action Trace
By default, actions like tasks, decisions, etc. are not shown in the MSC trace. You may change this by setting action trace to On.
- Default value: Off
- Command: Define-MSC-Trace-Action
- Menu choice: Not available
State Trace
By default, changes in process states are shown in the MSC trace by adding a condition symbol. You may change this by setting state trace to Off.
- Default value: On
- Command: Define-MSC-Trace-State
- Menu choice: Not available
MSC Trace Autopopup
When you go to a report, an MSC Editor is normally started automatically to present the trace from the current root to the state where the report was generated. In some cases this may be inconvenient, so there is a possibility to turn this feature off.
- Default value: On
- Command: Define-MSC-Trace-Autopopup
- Menu choice: Options1: MSC Trace Auto Popup
State Space Options
The structure and size of the state space that can be generated for any given SDL system can be modified in a number of ways using the state space options. The default values are defined to make the state space as small as possible to make the Explorer immediately useful for as many applications as possible. This, however, also means that the search performed by the Explorer is fairly scarce compared to what is possible. Some error situations may thus be overlooked during the search if they only occur in a part of the state space that never is reached.
Since these options affect the state space, note the information in Affecting the State Space.
Transition Type
There are two alternatives possible for the type of a behavior tree transition during state space exploration:
- It can be equal to a complete SDL process graph transition (the value "SDL" in the command)
- It can be a part of such an SDL transition (the value
"Symbol-Sequence" in the command).If it is equal to an SDL process graph transition, whenever such a transition is started, it is completed before anything else is allowed to happen. This implies that all process instances in all system states in the behavior tree will always be in an SDL process graph state.
If it is only a part of an SDL process graph transition, a transition in the behavior tree is considered to be a sequence of events that are local to the process instance, followed by a non-local event. Examples of local events are tasks and decisions; examples of non-local events are creates and inputs/outputs of signals from/to other process instances. The idea of this alternative is to model the ITU semantics for SDL as closely as possible while still allowing optimized performance during state space exploration.
- Default value: SDL
- Command: Define-Transition
- Menu choice: Options1: State Space: Transition
Scheduling Algorithm
The scheduling algorithm defines which of the process instances in a system state will be allowed to execute. There are two possible alternatives:
- All of the process instances in the ready queue are allowed to execute (the value "All" in the command)
- Only the first process instance in the ready queue is allowed to execute (the value "First" in the command).
The ready queue is a queue containing all process instances that have received a signal that can cause an immediate transition, but that have not yet had the opportunity to execute this transition to its end.
If all process instances are allowed to execute, the semantics of ITU recommendation Z.100 are modeled. There will be one child node to the current node in the behavior tree for each process instance in the ready queue.
If only the first process instance is allowed to execute, the semantics of an application that has been generated by the SDL to C Compiler are modeled. There will only be one child node to the current node in the behavior tree, the first process instance in the ready queue.
- Default value: First
- Command: Define-Scheduling
- Menu choice: Options1: State Space: Scheduling
Event Priorities
The events that are represented in a behavior tree can be divided into five classes:
- Internal events: Events local to the processes in the system, e.g., tasks, decisions, inputs, outputs.
- Input from ENV: Reception of signals from the environment. The signal is put in the input port of a process instance or on a channel queue.
- Timeout events: Expiration of SDL timers. The timer signal is put in the input port of a process instance.
- Channel outputs: A signal is removed from a channel queue and put into another channel queue or the input port of a process instance
- Spontaneous transitions: A transition in a process caused by input of none.
To each of these event classes a priority of 1, 2, 3, 4 or 5 is assigned. These priorities are used during state space exploration to determine which transitions should be generated from each system state. The events with priority 1 are first considered. Only if no events with priority 1 are possible in the current state, the events with priority 2 are considered. Only if no events with priority 1 or 2 are possible in the current state are events with priority 3 considered, etc.
Note that also the setting of the symbol time option will have an impact on the events that will can be executed in each system state; see section Transition Time.
The two most common ways of assigning priorities to event classes are:
- All event classes are assigned priority 1.
- Internal events and channel outputs are assigned priority 1, and external, timeout and spontaneous transition events are assigned priority 2 (the default).
The first alternative represents the situation where no assumptions can be made about the time scale for the different types of events. The second alternative represents a situation where the internal delays are very short compared to the timeout durations and execution speed of the environment.
- Default value: Priorities 1, 2, 2, 1, 2
- Command: Define-Priorities
- Menu choice: Options1: State Space: Priorities
Transition Time
A common simplification made in the analysis of SDL systems is to consider the time it takes for a process to execute a symbol, e.g. an action or output, to be zero. This time is of course never zero in a real system, but in many cases the time is very small compared to the timer durations in the system, and can be neglected when analyzing the system.
Consider for example a situation where a process sets a timer with a duration 5 and then executes something that may take a long time, e.g. a long loop, and then sets a timer with duration 1. If symbol time is assumed to be zero, the second timer will always expire first. If considered to be non-zero, any one of the timers can potentially expire first.
The explorer allows the user to choose whether to assume that the execution time for SDL symbols is zero or undefined using the Define-Symbol-Time command.
- Default value: Zero
- Command: Define-Symbol-Time
- Menu choice: Options1: State Space: Symbol time
Channel Queues
The Explorer allows queues to be attached to and removed from all channels in the SDL system. If a queue is added for a channel, it implies that when a signal is sent transported on this channel it will be put into the queue associated with the channel. Then there will be a separate transition in the state space that represents the forwarding of the signal to the receiver (or the next channel queue).
- Default: No channels have queues
- Command: Define-Channel-Queue
- Menu choice: Options1: State Space: Channel queues
Maximum Input Port Length
The length of the input port queues is not infinite in the Explorer, since in practice it is likely to be a design error if the queues grow forever. If the length of a queue exceeds the defined max length during state space exploration, a "MaxQueuelength" report is generated.
- Default value: 3
- Command: Define-Max-Input-Port-Length
- Menu choice: Options1: State Space: Input port length
Maximum Transition Length
To make it possible to detect infinite loops within a transition in the state space, the maximum number of SDL symbols allowed to be executed in one transition is defined. If this number is exceeded during state space exploration, a "MaxTransLen" report is generated.
- Default value: 1,000
- Command: Define-Max-Transition-Length
- Menu choice: Options1: State Space: Transition length
Maximum Number of Instances
To avoid infinite chains of create actions in the state space, the Explorer uses a max number of allowed process instances for any type. If this number is exceeded during state space exploration, a "Create" report is generated.
- Default value: 100
- Command: Define-Max-Instance
- Menu choice: Options1: State Space: Max instance
Maximum State Size
When the Explorer is exploring the state space, an internal buffer is used to store the system states. The size of this buffer defines the maximum size of the system states that the Explorer can handle.
- Default value: 100,000 (bytes)
- Command: Define-Max-State-Size
- Menu choice: Options1: State Space: Max state size
Timer Progress
One test that can be made with the Explorer is to look for non-progress loops, i.e. loops in the state space without any progress being made. The intention with this test is to look for situations where the SDL system is busy doing internal communication but to an outside observer looks dead.
This option defines if the expiration of a timer is considered as progress when performing non-progress loop checking. See also Non Progress Loop Error.
- Default: On (timer expiration is considered to be progress)
- Command: Define-Timer-Progress
- Menu choice: Options1: State Space: Timer progress
Spontaneous Transition Progress
One test that can be made with the Explorer is to look for non-progress loops, i.e. loops in the state space without any progress being made. The intention with this test is to look for situations where the SDL system is busy doing internal communication but to an outside observer looks dead.
This option defines if a spontaneous transition is considered as progress when performing non-progress loop checking. See also Non Progress Loop Error.
- Default: On (spontaneous transition is considered to be progress)
- Command: Define-Spontaneous-Transition-Progress
- Menu choice: Not available
Autolink Options
See section Computing Test Cases for a discussion of the Autolink options.
Setting Advanced Options
Advanced options can be set for state space explorations to achieve a much larger state space than the default, thus allowing for special kind of errors to be detected. See Using Advanced Validation for more information.
To set advanced options, click the Advanced button in the Explore module. This executes the following set of commands:
Define-Scheduling AllDefine-Priorities 1 1 1 1 1Define-Max-Input-Port-Length 2Define-Report-Log MaxQueuelength OffThe reasoning behind these settings are:
- The scheduling should be set to All, since we in this case are looking for signal races and a characteristic property of signal race conditions is that they are depending on the ordering of internal events.
- The priorities should be set to 1 for all types of events.
- To reduce the size of the state space, the maximum queue length should be set to a very small number. The reason is that when the environment is allowed to send signals to the system at any time, the queues that can receive signals from the environment will grow very rapidly.
- Since a lot of maximum queue length reports will be generated with these options, the report log for this report should be set to Off. Note also that the report action for this report should be Prune (which is the default).
http://www.ibm.com/rational |
![]() |
![]() |
![]() |
![]() |