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 :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.------------------------------------------------------------------ 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. ------------------------------------------------------------------
------------------------------------------------------------------ Note: No other characters may be typed before <Return> is pressed. ------------------------------------------------------------------
(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 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.
(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:
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:
(None)Go down in the behavior tree to the end of the current path.
(None)Clears the test coverage information.
(None)Clears the currently loaded MSC and sets the current state to the current root of the behavior tree.
<Process type>Defines all process instances of the given type to be usual SDL processes, not observer processes.
<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.
(None)Delete the current reports from the latest state space exploration.
(None)The currently defined rule is deleted.
<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. ------------------------------------------------------------------
<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.
(None)The command log facility is turned off; see the command Command-Log-On for details.
<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.
(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.
<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.
<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.
<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.
<Depth>The parameter defines the depth of the search when performing exhaustive exploration. The default value is 100.
<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.
<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.
<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.
<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.
<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.
<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.
"On" | "Off"This command defines whether actions like tasks, decisions, etc. are shown in the MSC trace. The default value is "Off".
"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".
"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".
<Depth>The parameter defines the depth of the search when performing MSC verification using the Verify-MSC command. The default value is 1,000.
<Process type>Defines all process instances of the given type to be observer processes.
<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.
<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:
<Depth>The parameter defines the depth of the search when performing random walk exploration. The default value is 100.
<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.
<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.
<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.
<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.
<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.
"On" | "Off"This command defines whether the Report Viewer automatically will pop up when an automatic exploration is finished. The default is "On".
"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. -------------------------------------------------------------------
<User-defined rule>A new rule is defined that will be checked during state space exploration.
"All" | "First"Defines which process instances in the ready queue are allowed to execute at each state. The parameter defines the scheduling as follows:
<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. -----------------------------------------------------------------------
"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.
<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. --------------------------------------------------------------------
<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:
"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.
"SDL" | "Symbol-Sequence"Defines the semantics and length of the transitions in the behavior tree. The parameter defines the transitions as follows:
<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.
(None)The currently defined rule is evaluated with respect to the current system state. The command prints whether or not the rule is satisfied.
<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.
<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.
<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.
<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.
<PId value> <Optional variable name>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.
<Optional component selection>
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.
(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.
(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.
<Path>Go to the system state specified by the path. For details about paths, see the command Print-Path.
<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.
<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.
<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.
<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.
<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.
(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. -----------------------------------------------------------------
(None)Lists all currently defined test values for signal 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.
(None)A list of process instances in the ready queue is printed. For more information, see the Simulator command "ListReadyQueue" on page 1805.
(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.
(None)A list of all currently defined signals is printed.
(None)Lists all test values that currently are defined.
(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.
<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.
<File name>A command file with Define-Signal commands is loaded and the signals are defined. This command exists for backward compatibility reasons only.
(None)The command Log-Off turns off the interaction log facility, which is described in the command Log-On.
<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.
<File name>An existing report file is opened and the reports in it are added to the current reports.
<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.
(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.
<File name>A new report file for report storage is created. The current reports are deleted.
<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.
<File name>An existing report file is opened and the reports in it are loaded. The current reports are deleted.
(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.
<File name>The content of the named text file is displayed on the screen.
(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.
(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.
(None)The name of the current report file is printed.
(None)The currently defined rule is printed.
<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.
(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.
<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.
(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:
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.
(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.
<File name>The current reports are saved in a new file. The name of the current report file is set to the new file.
<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.
<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.
<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. --------------------------------------------------------------
<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.
(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.
(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
(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
(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
(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
(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.
(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.
(None)The values of all options defined for the Validator are printed, including the report action defined for each report type.
(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.
(None)The versions of the C Code Generator and the runtime kernel that generated the currently executing program are presented.
(None)Go up in the behavior tree to the start of the current path (the root system state).
<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.
<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