Table of Contents Previous Chapter 33 The Validator

33 The Validator

This chapter is a reference to the validator user interface and a reference for the terminology used in validation. For a guide to how to use the validator, see chapter 8, Validating a System.

The Validator Monitor

A validator generated by SDT is similar to a simulator in that it contains an interactive monitor system. The validator monitor looks and behaves very similar to the simulator monitor; the only real difference is the set of available commands.

Monitor User Interfaces

Two different user interfaces are provided for the validator monitor, a textual and a graphical. The textual interface only allows commands to be entered from the keyboard, in the same way as for the simulator monitor. The graphical interface still allows commands to be entered from the keyboard in the same way, but also provides buttons, menus and dialogs for easy access to commands and other features.

The textual interface is invoked by executing the generated validator directly from the operating system prompt. This is called running a validator in stand-alone mode. When started, the validator responds with the following text:

Welcome to SDT VALIDATOR
Command :
------------------------------------------------------------------
Note:                                                               
Before a validator can be run in stand-alone mode, a command file   
must be executed from the operating system prompt. The file is      
called telelogic.sou or telelogic.profile and is located in         
the SDT binary directory that is included in the user's path.       
------------------------------------------------------------------
The graphical interface, known as the Validator UI, runs in a separate window. It is invoked from the Organizer by selecting Validator UI from the Tools menu (see page 1129). The graphical interface is basically the same as for the simulator monitor. However, some special windows and menus have been added; see "Graphical User Interface" on page 1915 for more information.

Activating the Monitor

Commands can be issued to the interactive monitor system when it becomes active. The validator's monitor system becomes active:

  1. When the validator is started.
  2. When the last command was Next or Random-Down and the transitions initiated by this command have completed.
  3. When the last command was Bit-State-Exploration, Verify-MSC or Exhaustive-Exploration and the behavior tree down to the defined search depth has been fully explored.
  4. When the last command was Random-Walk and the defined number of repetitions have been executed.
  5. Immediately after a report with the report action Abort has been generated during automatic state space exploration.
  6. In the Validator UI, when the Break button is clicked in the Explore button module; in stand-alone mode, when <Return> is pressed during an automatic state space exploration.
    ------------------------------------------------------------------
    Note:                                                               
    No other characters may be typed before <Return> is pressed.  
    ------------------------------------------------------------------
    

Monitor Commands

This section provides an alphabetical listing of all available commands in the validator monitor. The syntax of commands and data type literals in the validator monitor is the same as for the simulator monitor. Commands may be abbreviated, as well as most command parameters. All input to the monitor is case insensitive. For more information, see "Syntax of Monitor Commands" on page 1788 and "Input and Output of Data Types" on page 1792.

? (Interactive Context Sensitive Help)

Parameters:

(None)
The monitor will respond to a `?' (question mark) by giving a list of all allowed values at the current position, or by a type name, when it is not suitable to enumerate the values. After the presentation of the list, the input can be continued.

? (Command Execution)

Parameters:

<Command name>
Executes the monitor command given as a parameter. This is a convenience function for the Validator UI. Entering `?' as parameter gives a list of all possible command names.

Bit-State-Exploration

Parameters:

(None)
Starts an automatic state space exploration from the current system state using the bit state space algorithm. When the exploration is started, the following information is printed:

The exploration will continue until either the complete state space to the defined depth is explored, <Return> is pressed from the command prompt, or the Break button is pressed in the graphical user interface. The system is then returned to the state it was in before the exploration was started.

If a bit state exploration already has been started, but has been stopped, this command asks if the exploration should continue from where it was stopped, or restart from the beginning again.

A status message is printed for every 20,000 transitions that are executed.

When the exploration is finished or stopped, the Report Viewer is by default opened (this can be changed with the command Define-Report-Viewer-AutoPopup). The following statistics are also printed:

Bottom

Parameters:

(None)
Go down in the behavior tree to the end of the current path.

Clear-Coverage-Table

Parameters:

(None)
Clears the test coverage information.

Clear-MSC

Parameters:

(None)
Clears the currently loaded MSC and sets the current state to the current root of the behavior tree.

Clear-Observer

Parameters:

<Process type>
Defines all process instances of the given type to be usual SDL processes, not observer processes.

Clear-Parameter-Test-Values

Parameters:

<Signal> ( <Parameter number> | "-" ) | "-"
Clears all test values for the signal parameter given as parameter to the command. If `-' is given instead of the parameter number then the test values for all parameters of the signal are cleared. If `-' is given instead of the signal name then all test values for all parameters to all signals are cleared.

Regenerates the set of signals that can be sent from the environment during state space exploration.

Clear-Reports

Parameters:

(None)
Delete the current reports from the latest state space exploration.

Clear-Rule

Parameters:

(None)
The currently defined rule is deleted.

Clear-Signal-Definitions

Parameters:

<Signal> | "-"
Clears all currently defined test values for the signal given by the parameter. If `-' is given, the test values for all signals are cleared.

------------------------------------------------------------------
Note:                                                               
The signals cleared by this command may be regenerated if any of    
the commands for defining test values for sorts or parameters are   
used.                                                               
------------------------------------------------------------------

Clear-Test-Values

Parameters:

<Sort> | "-"
Clears all test values for the sort given as parameter. If the parameter is `-', all test values for all sorts are cleared.

Regenerates the set of signals that can be sent from the environment during state space exploration.

Command-Log-Off

Parameters:

(None)
The command log facility is turned off; see the command Command-Log-On for details.

Command-Log-On

Parameters:

<Optional file name>
The command enables logging of all the commands given in the monitor. The first time the command is entered a file name for the log file has to be given as parameter. After that any further Command-Log-On commands, without a file name, will append more information to the previous log file, while a Command-Log-On command with a file name will close the old log file and start using a new file with the specified name.

Initially the command log facility is turned off. It can be turned off explicitly by using the command Command-Log-Off.

The generated log file is directly possible to use as a file in the command Include-File. It will, however, contain exactly the commands given in the session, even those that were not executed due to command errors. The concluding Command-Log-Off command will also be part of the log file.

Default-Options

Parameters:

(None)
Resets all options in the Validator to their default values and clears all reports. It also sets the current state to the current root. Compare with the command Reset.

Define-Bit-State-Depth

Parameters:

<Depth>
The parameter is the maximum depth of bit state exploration, i.e., the number of levels to be reached in the behavior tree. If this level is reached during the exploration, the current path is truncated and the exploration continues in another node of the behavior tree. The default value is 100.

Define-Bit-State-Hash-Table-Size

Parameters:

<Size in bytes>
Sets the size of the hash table used to represent the generated state space during bit state exploration. The default value is 1,000,000 bytes.

Define-Channel-Queue

Parameters:

<Channel name> ("On" | "Off")
Adds or removes a queue for the specified channel. If a queue is added for a channel, it implies that when a signal is sent that is transported on this channel, it will be put into the queue associated with the channel. By default no channels have queues.

Define-Exhaustive-Depth

Parameters:

<Depth>
The parameter defines the depth of the search when performing exhaustive exploration. The default value is 100.

Define-Max-Input-Port-Length

Parameters:

<Number>
The maximum length of the input port queues is defined. If this length is exceeded during state space exploration, a report is generated (see "Max Queue Length Exceeded" on page 1933). The default value is 3.

Define-Max-Instance

Parameters:

<Number>
Defines the maximum number of instances allowed for any particular process type. If this number is exceeded during state space exploration, a report is generated (see "Create Errors" on page 1932). The default value is 100.

Define-Max-Signal-Definitions

Parameters:

<No of signals>
This command defines the maximum no of signals that will be added to the list of signals from the environment for any particular signal. The default value is 10.

Define-Max-State-Size

Parameters:

<Size in bytes>
Sets the size of an internal array used to store each system state when computing the hash value for the system state. The default size is 100,000 bytes.

Define-Max-Test-Values

Parameters:

<No of text values>
This command defines the maximum no of test values that will be generated for a particular data type or signal parameter. The default value is 10.

Define-Max-Transition-Length

Parameters:

<Number>
The maximum number of SDL symbols allowed to be executed during the performance of a behavior tree transition is defined. If this number is exceeded during state space exploration, a report is generated (see "Transition Length Error" on page 1937). The default value is 1,000.

Define-MSC-Trace-Action

Parameters:

"On" | "Off"
This command defines whether actions like tasks, decisions, etc. are shown in the MSC trace. The default value is "Off".

Define-MSC-Trace-Autopopup

Parameters:

"On" | "Off"
This command defines whether an MSC Editor automatically will pop up and show an MSC trace when going to a report. The default value is "On".

Define-MSC-Trace-State

Parameters:

"On" | "Off"
This command defines if the SDL process graph states are shown in the MSC trace. If "On", a condition symbol will be shown in the MSC trace each time a process performs a nextstate. The default value is "On".

Define-MSC-Verification-Depth

Parameters:

<Depth>
The parameter defines the depth of the search when performing MSC verification using the Verify-MSC command. The default value is 1,000.

Define-Observer

Parameters:

<Process type>
Defines all process instances of the given type to be observer processes.

Define-Parameter-Test-Value

Parameters:

<Signal> <Parameter number> <Value>
The parameter test value described by the command parameters is added to the current set of test values. The list of signals that can be sent from the environment is regenerated based on the new set of test values.

Define-Priorities

Parameters:

<Internal events> <Input from ENV> <Timeout events> 
<Channel output> <Spontaneous transitions>
Defines the priorities for the different event classes. The priorities can be set individually to 1, 2, 3, 4 or 5. For more information about event classes and priorities, see "Event Priorities" on page 438.

The default priorities are:

Define-Random-Walk-Depth

Parameters:

<Depth>
The parameter defines the depth of the search when performing random walk exploration. The default value is 100.

Define-Random-Walk-Repetitions

Parameters:

<No of repetitions>
The parameter defines the number of times the search is performed from the start state when performing random walk exploration. The default is 100.

Define-Report-Abort

Parameters:

<Report type> | "-"
Defines that the state space exploration will be aborted whenever a report of the specified type is generated.

The available report types are listed with the command Show-Options. They are also described in "Rules Checked During Exploration" on page 1931. If the parameter is specified as `-', all report types will be defined in the same way.

Define-Report-Continue

Parameters:

<Report type> | "-"
Defines that a state space exploration will continue past a state where a report of the specified type is generated. With this definition, the exploration of the behavior tree is not affected by a report being generated.

The available report types are listed with the command Show-Options. They are also described in "Rules Checked During Exploration" on page 1931. If the parameter is specified as `-', all report types will be defined in the same way.

Define-Report-Log

Parameters:

<Report type> ("On" | "Off")
Defines if reports of a specified type will be stored in the list of found reports when they are encountered during state space exploration. Default for all report types is "On".

If "Off" is specified for a report type, reports of this type will not be stored, which implies for example that they will not be listed by the List-Reports command. However, the reports will be generated and the appropriate action taken as specified by the commands Define-Report-Abort, Define-Report-Continue and Define-Report-Prune.

The available report types are listed with the command Show-Options. They are also described in "Rules Checked During Exploration" on page 1931. If the parameter is specified as `-', all report types will be defined in the same way.

Define-Report-Prune

Parameters:

<Report type> | "-"
Defines that a state space exploration will not continue past a state where a report of the specified type is generated. Thus, the part of the behavior tree beneath the state will not be explored. Instead, the exploration will continue in the siblings or parents of the state. This is also known as "pruning" the behavior tree at the state. This is the default behavior for all report types.

The available report types are listed with the command Show-Options. They are also described in "Rules Checked During Exploration" on page 1931. If the parameter is specified as `-', all report types will be defined in the same way.

Define-Report-Viewer-AutoPopup

Parameters:

"On" | "Off"
This command defines whether the Report Viewer automatically will pop up when an automatic exploration is finished. The default is "On".

Define-Root

Parameters:

"Original" | "Current"
Defines the root of the behavior tree to be either the current system state or the original start state of the SDL system.

-------------------------------------------------------------------
Note:                                                                
When the root is redefined, all paths, e.g. MSC traces or report     
paths, will start in the new root, not in the original start state.  
-------------------------------------------------------------------

Define-Rule

Parameters:

<User-defined rule>
A new rule is defined that will be checked during state space exploration.

Define-Scheduling

Parameters:

"All" | "First"
Defines which process instances in the ready queue are allowed to execute at each state. The parameter defines the scheduling as follows:

The default is First.

Define-Signal

Parameters:

<Signal> <Optional parameter values>
A signal that is to be sent to the SDL system from the environment is defined. The signal is defined by its name and optionally the values of its parameters. Multiple Define-Signal commands may be used to define the same signal, but with different values for the parameters.

-----------------------------------------------------------------------
Note:                                                                    
The signals defined by this command will be destroyed if the signals     
are regenerated, i.e., if any of the commands defining test values for   
sorts or signal parameters are used.                                     
-----------------------------------------------------------------------

Define-Spontaneous-Transition-Progress

Parameters:

"On" | "Off"
Defines whether a spontaneous transition (input none) is considered as progress when performing non-progress loop check. Default is that spontaneous transition is considered to be progress, i.e. "On". See "Non Progress Loop Error" on page 1937.

Define-Test-Value

Parameters:

<Sort> <Value>
The test value described by the parameters is added to the current set of test values. The list of signals that can be sent from the environment is regenerated based on the new set of test values.

--------------------------------------------------------------------
Note:                                                                 
When regenerating the set of signals, all signals that have been man  
ually defined using the Define-Signal command will be lost.           
--------------------------------------------------------------------

Define-Timer-Check-Level

Parameters:

<Number>
The action taken during MSC verification when checking timer statements (set, reset and timeout) is defined. The possible values for the specified number are:

The default value is 1.

Define-Timer-Progress

Parameters:

"On" | "Off"
Defines if the expiration of a timer is considered as progress when performing non-progress loop check. Default is that timer expiration is considered to be progress, i.e. "On". See "Non Progress Loop Error" on page 1937.

Define-Transition

Parameters:

"SDL" | "Symbol-Sequence"
Defines the semantics and length of the transitions in the behavior tree. The parameter defines the transitions as follows:

The default is SDL.

Down

Parameters:

<Number of levels>
Go down the specified number of levels in the behavior tree, each time selecting the child of the current system state that is part of the current path. If the parameter is too large, Down will stop at the end of the current path.

Evaluate-Rule

Parameters:

(None)
The currently defined rule is evaluated with respect to the current system state. The command prints whether or not the rule is satisfied.

Examine-Channel-Signal

Parameters:

<Channel name> <Entry number>
The parameters of the signal instance at the position equal to the entry number in the queue of the specified channel are printed. The entry number is the number associated with the signal instance when the command List-Channel-Queue is used.

Examine-PId

Parameters:

<PId value>
Information about the specified process instance is printed. This information contains the current values of Parent, Offspring, Sender and a list of all currently active procedure calls made by the process instance. The list starts with the latest procedure call and ends with the process instance itself.

If the process instance contains service(s), information about all services is also printed.

Examine-Signal-Instance

Parameters:

<PId value> <Entry number>
The parameters of the signal instance at the specified position in the input port of the specified process instance are printed. The entry number is the number associated with the signal instance when the command List-Input-Port is used.

Examine-Timer-Instance

Parameters:

<Entry number>
The parameters of the specified timer instance are printed. The entry number is the number associated with the timer when the List-Timer command is used.

Examine-Variable

Parameters:

<PId value> <Optional variable name>
<Optional component selection>
The value of the specified variable or formal parameter of the specified process instance is printed. If no variable name is specified, all variables are printed. If the process instance contains service(s) and/or has called procedure(s), all variables in the process, services and procedures with the specified name are printed.

If the variable is an array or a struct, the optional component selection can be used to select only one of the components in the array/struct. To select a specific component of an array the index is given as an optional component selection and to select a specific field in a structure the field name is given. More that one optional component selection can be specified to for example print the value of a specific field in a struct that is a component of an array.

Exhaustive-Exploration

Parameters:

(None)
Starts an automatic state space exploration from the current system state, where the entire generated state space is stored in primary memory. This is only recommended for SDL systems with small state spaces.

The exploration will continue until either the complete state space to the defined depth is explored, <Return> is pressed from the command prompt, or the Break button is pressed in the graphical user interface. The system is then returned to its initial system state. The maximum depth of the exploration can be set with the command Define-Exhaustive-Depth.

If an exhaustive exploration already has been started, but has been stopped, this command asks if the exploration should continue from where it was stopped, or restart from the beginning again.

A status message is printed every 50,000 states that are generated. When the exploration is finished or stopped, the same information as for a bit state exploration is printed.

Exit

Parameters:

(None)
The executing validator is terminated. If the command is abbreviated, the monitor asks for confirmation. If any of the Validator options have been changed, the monitor will ask if the changed options should be saved. If so, the changed options are saved in a file .valinit in the directory from where SDT was started. This file is automatically loaded the next time a Validator is started from the same directory, thus restoring the previously saved options.

This is the same command as Quit.

Goto-Path

Parameters:

<Path>
Go to the system state specified by the path. For details about paths, see the command Print-Path.

Goto-Report

Parameters:

<Report number>
Go to the state in the behavior tree where the report with the corresponding number has been found. The last behavior tree transition that was executed before the reported situation is printed, with the same information as for a full trace during simulation. The report number is the number associated with the report when the command List-Reports is used. If only one report exists, the report number is optional.

Help

Parameters:

<Optional command name>
Issuing the Help command without a parameter will print all the available commands. If a command name is given as parameter, this command will be explained.

Include-File

Parameters:

<File name>
This command provides the possibility to execute a sequence of monitor commands stored in a text file. The Include-File facility can be useful for including, for example, an initialization sequence or a complete test case. It is allowed to use Include-File in an included sequence of commands; up to five nested levels of include files can be handled.

List-Channel-Queue

Parameters:

<Channel name>
A list of all signal instances in the specified channel queue is printed. For each signal instance an entry number, the signal type, and the sending process instance is given. The entry number can be used in the command Examine-Channel-Signal.

List-Input-Port

Parameters:

<PId value>
A list of all signal instances in the input port of the specified process instance is printed. For each signal instance an entry number, the signal type, and the sending process instance is given. A `*' before the entry number indicates that the corresponding signal instance is the signal instance that will be consumed in the next transition performed by the process instance. The entry number can be used in the command Examine-Signal-Instance.

List-Next

Parameters:

(None)
A list of the possible behavior tree transitions that can follow from the current system state is printed.

-----------------------------------------------------------------
Note:                                                              
The number of possible transitions depends on the selected state   
space options.                                                     
-----------------------------------------------------------------

List-Parameter-Test-Values

Parameters:

(None)
Lists all currently defined test values for signal parameters.

List-Process

Parameters:

<Optional process name>
A list of all process instances with the specified process name is printed. If no process name is specified all process instances in the system are listed. The list will contain the same details as described for the List-Ready-Queue command.

If the process contains services, information about the currently active service is also printed. To get information about all services use the Examine-PId command.

List-Ready-Queue

Parameters:

(None)
A list of process instances in the ready queue is printed. For more information, see the Simulator command "ListReadyQueue" on page 1805.

List-Reports

Parameters:

(None)
All situations that have been reported during state space exploration are printed. For each report, the error or warning message describing the situation is printed, together with the depth in the behavior tree where it first occurred. Only one occurrence of each reported situation is printed; the one with the shortest path from the root of the behavior tree. The report numbers printed can be used in the command Goto-Report.

List-Signal-Definitions

Parameters:

(None)
A list of all currently defined signals is printed.

List-Test-Values

Parameters:

(None)
Lists all test values that currently are defined.

List-Timer

Parameters:

(None)
A list of all currently active timers is printed. For each timer, its corresponding process instance and associated time is given. An entry number will also be part of the list, which can be used in the command Examine-Timer-Instance.

Load-MSC

Parameters:

<MSC file name>
The specified Message Sequence Chart is loaded into the Validator. Loading an MSC always resets the state space and sets the current state to the root of the behavior tree.

Load-Signal-Definitions

Parameters:

<File name>
A command file with Define-Signal commands is loaded and the signals are defined. This command exists for backward compatibility reasons only.

Log-Off

Parameters:

(None)
The command Log-Off turns off the interaction log facility, which is described in the command Log-On.

Log-On

Parameters:

<Optional file name>
The command Log-On takes an optional file name as a parameter and enables logging of all the interaction between the Validator and the user that is visible on the screen. The first time the command is entered, a file name for the log file has to be given as parameter. After that any further Log-On commands, without a file name, will append more information to the previous log file, while a Log-On with a file name will close the old log file and start using a new file with the specified file name.

Initially the interaction log facility is turned off. It can be turned off explicitly by using the command Log-Off.

Merge-Report-File

Parameters:

<File name>
An existing report file is opened and the reports in it are added to the current reports.

MSC-Log-File

Parameters:

<File name>
A log file is produced containing information about the Message Sequence Chart for the trace from the root of the behavior tree to the current system state. This file can be opened in an MSC Editor; we recommend using a filename with the suffix .mpr, since that suffix is used as default.

MSC-Trace

Parameters:

(None)
An MSC Editor is opened, showing the Message Sequence Chart for the current execution path. The current state is shown in the MSC by the selection of some of the symbols. Whenever the current state and/or current path changes in the Validator, the MSC will be updated.

If the MSC trace is already on, this command will turn it off.

New-Report-File

Parameters:

<File name>
A new report file for report storage is created. The current reports are deleted.

Next

Parameters:

<Transition number>
Go to a system state in the next level of the behavior tree, i.e. a child to the current system state. The parameter is the transition number given by the List-Next command.

Open-Report-File

Parameters:

<File name>
An existing report file is opened and the reports in it are loaded. The current reports are deleted.

Print-Evaluated-Rule

Parameters:

(None)
The currently defined rule is printed with the values obtained from the last evaluation of the rule. The printed information is in the form of a so-called parse tree, and may require some knowledge of such structures to be interpreted correctly.

Print-File

Parameters:

<File name>
The content of the named text file is displayed on the screen.

Print-MSC

Parameters:

(None)
A textual version of the currently loaded MSC is printed. The format is similar to the textual MSC format defined in CCITT recommendation Z.120.

Print-Path

Parameters:

(None)
The path to the current system state is printed. A path is a sequence of integer numbers, terminated with a 0, describing how to get to the current system state. The first number indicates what transition to select from the root, the second number what transition to choose from this state, etc. To go to the state specified by a path, use the command Goto-Path.

Print-Report-File-Name

Parameters:

(None)
The name of the current report file is printed.

Print-Rule

Parameters:

(None)
The currently defined rule is printed.

Print-Trace

Parameters:

<Number of levels>
The textual trace leading to the current system state is printed. The same information as for a full trace during simulation is printed for each behavior tree transition. The parameter determines how many levels up the trace should start. For example, Print-Trace 10 will print the ten last transitions.

Quit

Parameters:

(None)
The executing validator is terminated. If the command is abbreviated, the monitor asks for confirmation. If any of the Validator options have been changed, the monitor will ask if the changed options should be saved. If so, the changed options are saved in the file .valinit in the directory from where SDT was started. This file is automatically loaded the next time a Validator is started from the same directory, thus restoring the previously saved options.

This is the same command as Exit.

Random-Down

Parameters:

<Number of levels>
Go down the specified number of levels in the behavior tree, each time selecting a random child of the current system state.

Random-Walk

Parameters:

(None)
This command will perform an automatic exploration of the state space from the current system state. Random walk is based on the idea that if more than one transition is possible in a particular system state, one of them will be chosen at random. When the exploration is started, the following information is printed:

The exploration will continue until either it is finished, <Return> is pressed from the command prompt, or the Break button is pressed in the graphical user interface. The system is then returned to the state it was in before the exploration was started.

When the exploration is finished or stopped, the Report Viewer is by default opened (this can be changed with the command Define-Report-Viewer-AutoPopup). A few statistics are also printed; see the command Bit-State-Exploration for an explanation of these.

Reset

Parameters:

(None)
Resets the state of the Validator to its initial state. This command resets all options and test values in the Validator to their initial values and clears all reports, MSCs, and user-defined rules. It also sets the current state and the current root to the original start system state.

This command reads the .valinit file (see the command Exit). It is equivalent to closing the Validator and starting it again. Compare with the command Default-Options.

Save-As-Report-File

Parameters:

<File name>
The current reports are saved in a new file. The name of the current report file is set to the new file.

Save-Coverage-Table

Parameters:

<File name>
Test coverage information is saved in the specified file. The test coverage table consists of two parts, a Profiling Information section, and a Coverage Table Details section. This is the same type of file as generated by the Simulator; for more detailed information about the file, see "PrintCoverageTable" on page 1811.

Save-Options

Parameters:

<File name>
Creates a Validator command file with the name given as parameter. The file contains commands defining the options of the Validator. If this file is loaded (using the command Include-File) the options will be restored to their saved values.

Save-State-Space

Parameters:

<File name>
A Labelled Transition System (LTS) representing the generated state space is saved to a file. For a description of the file syntax, see section "State Space Files" on page 1946.

--------------------------------------------------------------
Note:                                                           
It is necessary to have executed an Exhaustive-Exploration com  
mand before the state space can be saved on a file.             
--------------------------------------------------------------

Save-Test-Values

Parameters:

<File name>
A command file is generated containing Validator commands that, if loaded with the Include-File command, will recreate the current test value definitions.

SDL-Trace

Parameters:

(None)
This command opens an SDL Editor that will show the transition leading to the current system state. Whenever the current system state changes in the Validator, the Editor will be updated.

If the SDL trace already is on, the command will turn it off.

Set-Application-All

Parameters:

(None)
The state space options of the Validator are set to perform state space exploration according to the semantics of an application generated by the SDT Code Generator. No assumptions are made about the performance of the SDL system compared to timeout values or the performance of the environment.

This command sets the exploration mode factors by executing the following commands:

Define-Transition SDL
Define-Scheduling First
Define-Priorities 1 1 1 1 1

Set-Application-Internal

Parameters:

(None)
The state space options of the Validator are set to perform state space exploration according to the semantics of an application generated by the SDT Code Generator. The assumption is made that the time it takes for the SDL system to perform internal actions is very small compared to timeout values and the response time of the environment.

This command sets the exploration mode factors by executing the following commands:

Define-Transition SDL
Define-Scheduling First
Define-Priorities 1 2 2 1 2

Set-Specification-All

Parameters:

(None)
The state space options of the Validator are set to perform state space exploration according to the CCITT semantics for SDL. No assumptions are made about the performance of the SDL system compared to timeout values, or the performance of the environment.

This command sets the exploration mode factors by executing the following commands:

Define-Transition Symbol-Sequence
Define-Scheduling All
Define-Priorities 1 1 1 1 1

Set-Specification-Internal

Parameters:

(None)
The state space options of the Validator are set to perform state space exploration according to the CCITT semantics for SDL. The assumption is made that the time it takes for the SDL system to perform internal actions is very small compared to timeout values and the response time of the environment.

This command sets the exploration mode factors by executing the following commands:

Define-Transition Symbol-Sequence
Define-Scheduling All
Define-Priorities 1 2 2 1 2

Show-Coverage-Viewer

Parameters:

(None)
This command starts the Coverage Viewer. The current test coverage is automatically loaded and a symbol coverage tree is presented. See chapter 28, The Coverage Viewer for further description of the Coverage Viewer.

Show-Navigator

Parameters:

(None)
This command starts the Navigator tool to simplify interactive navigation in the behavior tree of the SDL system. See "The Navigator Tool" on page 1924 for more details.

Show-Options

Parameters:

(None)
The values of all options defined for the Validator are printed, including the report action defined for each report type.

Show-Report-Viewer

Parameters:

(None)
This command starts the Report Viewer that presents a hierarchical view of all reports generated during state space explorations. See "The Report Viewer" on page 1927 for more details.

Show-Versions

Parameters:

(None)
The versions of the C Code Generator and the runtime kernel that generated the currently executing program are presented.

Top

Parameters:

(None)
Go up in the behavior tree to the start of the current path (the root system state).

Up

Parameters:

<Number of levels>
Go up the specified number of levels in the behavior tree. Up 1 goes to the parent state of the current system state. Up will stop at the root of the behavior tree (the start state) if the parameter is too large.

Verify-MSC

Parameters:

<MSC file>
This command will perform an automatic exploration from the current system state to search for an execution trace that is consistent with the MSC that is given as a parameter. The search algorithm is a variant of the bit state algorithm that is adapted to suite MSC verification. Before the exploration is started, the root of the behavior tree is set to the current system state.

When the exploration is finished, the same information as for a bit state exploration is printed. In addition, a message is printed stating whether or not the MSC was verified, i.e., if an execution path was found that satisfied the MSC. For more information on criteria for MSC verification, see "MSC Verification Errors" on page 1938.

If the search was successful and the MSC was verified, the system state of the Validator will be set up to the last system state in the path that satisfied the MSC. Otherwise, the system is returned to its initial state.

This page intentionally left blank

 
Table of Contents Next Chapter