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 Validating a System.
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.
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 textual mode. When started, the validator responds with the following text:
Welcome to SDT VALIDATOR Command :
Another prompt may appear if the SDL system contains external synonyms. For more information, see Supplying Values of External Synonyms.
The graphical interface, known as the Validator UI, runs in a separate window. It is started from the Organizer by selecting SDL > Validator UI from the Tools menu. 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 for more information.
Commands can be issued to the interactive monitor system when it becomes active. The validator's monitor system becomes active:
<Return> is pressed during an automatic state space exploration.
|
Note: No other characters may be typed before |
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 and Input and Output of Data Types.
(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.
[ `(' <PId value> `)' ]
<Variable name> <Optional component selection>
<New value>
The new value is assigned to the specified variable in the process instance, service instance, or procedure given by the current scope. Sender, Offspring, and Parent may also be changed in this way, but their names may not be abbreviated.
After the command is given, the root of the behavior tree is set to the current system state.
It is, in a similar way as for the command Examine-Variable, possible to handle components in structured variables (struct, strings, array, and Ref) by appending the struct component name or a valid array index before the value to be assigned. Nested structs and arrays can be handled by entering a list of index values and struct component names.
If a PId is given within parenthesis, the scope is temporarily changed to this process instance instead.
(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:
(None)
Go down in the behavior tree to the end of the current path.
<Directory>
Change the current working directory to the specified directory.
<Directory>
Clears the current Autolink configuration.
<Constraint name> | `-'
Removes the constraint specified by the parameter. If `-' is given instead of a constraint name, all constraints are cleared.
Note: Only constraints that are not used by any generated test case can be cleared. Constraints used by one or more test cases are cleared automatically if the corresponding test cases are cleared.
(None)
Clears the test coverage information.
<Test case name> | `-'
Removes the generated test case specified by the parameter from memory. However, the corresponding MSC test case on disk is preserved. If `-' is given instead of a test case name, all generated test cases are cleared.
(None)
Clears all defined instance conversions. See also the command Define-Instance-Conversion.
Note that this command will not change an already loaded MSC.
(None)
Clears the currently loaded MSC and sets the current state to the current root of the behavior tree.
<File name> | `-'
Removes the MSC test case specified by the parameter from disk. If `-' is given instead of a file name, all test cases are cleared.
<File name> | `-'
Removes the MSC test case specified by the parameter from disk. If `-' is given instead of a file name, all test steps are cleared.
<Process type>
Defines all process instances of the given type to be usual SDL processes, not observer processes.
( <Signal> | `-' ) ( <Parameter number> | `-' ) ( <Value> | `-' )
The test value described by the value parameter is cleared for the signal parameter given as the parameter to the command. If the specified value parameter is `-', clears all test values for the signal parameter given as the 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> | `-' ) ( <Value> | `-' )
Clears all test values for the sort given as parameter. If the specified sort parameter is `-', all test values for all sorts will be cleared. If the value parameter is `-', all test values for the specified sort will be 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.
<Optional node number>
First go to the system state node which is the child with the specified number to the current system state. Same as the Next command. Then go down as long as there is only one child, i.e. a branch is found.
(None)
Go up in the behavior tree as long as there is only one child, i.e. a branch is found.
(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.
<Configuration>
Defines an Autolink configuration which might consist of:
If any rule or function is already defined, Autolink prompts the user to decide whether to add the new rules or to clear the existing Autolink configuration. If Define-Autolink-Configuration is part of a command file, the existing configuration is always replaced.
Rules beginning with TRANSLATE are evaluated when a constraint is created during test case generation. A translation rule specifies the name and the parameters of a constraint for a given SDL signal. In addition, it allows to replace signal parameter values by wildcards in a constraint declaration table (TTCN matching mechanism). Translation rules can also be used to introduce test suite parameters and constants.
Test suite structure rules are evaluated when a test suite is saved. A test suite structure rule specifies a test group reference for test cases and/or test steps.
An Autolink configuration has to obey the syntax rules described in Autolink Configuration Syntax.
For a detailed description of the semantics, see Syntax and Semantics of the Autolink Configuration.
<Depth>
Sets the maximum depth of the state space exploration for test case generation to the given value. The default value is 1000.
<Size>
Sets the size of the hash table used for test case generation to <Size> bytes. The default value is 1,000,000 bytes.
"On" | "Off"
Determines whether Autolink sets its own default state space options before generating test cases. If "On', the state space options are automatically set when Generate-Test-Case is invoked and reset to the previous options when the command is completed. The default value is"On".
Note that in general, the Validator's default options are too strict to find all inconclusive events. Also be aware that for Autolink to work correctly, the priority of "Input from ENV" has to be higher than the priority of all other event classes, and the queues for all channels to the environment have to be activated.
<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 is8 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.
<Step>
The Bit-State-Exploration algorithm includes a feature to automatically make a number of explorations with an increased depth for each exploration. The iteration continues until the search depth is greater than the maximum depth search as defined by Define-Bit-State-Depth command or one exploration terminates without any truncations.
This command activates the feature and defines how much the depth is increased for each iteration. If <Step> is set to 0 the iterative exploration is deactivated, otherwise <Step> defines how much the maximum depth is increased for each exploration.
The default value is 0, i.e. the feature is not activated.
<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.
<Constraint name> <Signal definition>
Defines a new constraint, which is automatically written to the test suite if the user enters the Save-Test-Suite command later.
<Depth>
The parameter defines the depth of the search when performing exhaustive exploration. The default value is 100.
<From string> <To string>
Adds an entry into an instance conversion table. If a string contains spaces, it must be quoted.
When reading instances in an MSC diagram and the name textually match a <From string> in the conversion table, it will be replaced by the <To string>. This is useful if you want to verify some, but not all, instances in an MSC, in which case you can convert the unwanted instances to be considered as environment.
Note that this command will not change an already loaded MSC.
"dec" | "hex" | "oct"
Defines whether integer values are printed in decimal, hexadecimal or octal format. In hexadecimal format the output is prepended with "0x", in octal format the output is prepended with `0' (a zero).
On input: if the format is set to hexadecimal or octal, the string determines the base as follows: After an optional leading sign a leading zero indicates octal conversion, and a leading "0x" hexadecimal conversion. Otherwise, decimal conversion is used.
The default is "dec", and no input conversion is performed.
<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). 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). 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). The default value is 1,000.
"On" | "Off"
Defines whether the parameters of signals (and timers) will be ignored (i.e. set to default values) when reading MSC diagrams. The default is "Off".
Note that this command will not change an already loaded MSC.
"Verification" | "Violation"
Defines options for MSC verification depending on the purpose of the exploration. "Verification" mode should be used if the intention with the exploration is to verify all MSC alternatives. "Violation" mode should be used if the intention is to check if the SDL system can violate the MSC.
The difference between "Verification" and "Violation" mode is that in "Verification" mode the validator will:
The synchronization in "Verification" mode implies that the validator will try to execute all events in one MSC before continuing with the events in a subsequent MSC. The special MSC action is executed when all events in one MSC has been executed and it is time to start with the subsequent MSC. Note that if there are more than one subsequent MSC (e.g. due to an HMSC alternative or an inline expression) each MSC action will select one of the MSCs. In the trace output (and in the Navigator) the MSC actions will be presented as "Enter MSC XXX" where XXX is the name of the MSC that the validator will try to execute next.
A simple way to get hands-on experience with the difference between "Verification" and "Violation" mode is to load an MSC that includes alternatives (either an HMSC or an MSC with inline expressions) using the Load-MSC command. Then set up the MSC search mode and use the Navigator to manually explore the state space.
Note that in "Verification" mode the par operator is not supported.
The default search mode is "Violation" mode.
<Directory name> | `-'
Defines the directory in which the MSC test cases are stored. If `-' is provided instead of a directory name, the test cases directory becomes undefined.
<Directory name> | `-'
Defines the directory in which the MSC test steps are stored. If `-' is provided instead of a directory name, the test steps directory becomes undefined.
"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".
"On" | "Off"
Defines whether the env instance should be split into one instance for each channel connected to env in the MSC trace. The default is "Off".
"TreeSearch" | "BitState"
Defines the search algorithm that is used for MSC verification. Two options are available, the tree search algorithm and the bit state algorithm. The default is "BitState".
Note that this command only defines what search algorithms that is used by the Verify-MSC command. It is possible to use other search algorithms, like Power-Walk and Exhaustive-Exploration, by manually loading the MSC with the Load-MSC command and then starting the desired search algorithm.
<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.
( <Repetitions> | `-' ) ( <Timeout> | `-' ) ( <Coverage> | `-' )
Sets the thresholds for the three termination criteria of the Power-Walk command. Each parameter has to be specified as a natural number with the following meaning:
Repetitions: The maximum number of times the search algorithm is performed without a new PowerWalk report being created. The default value is 50.Timeout: The maximum amount of computation time in minutes. The default value is 10,000 (about a week).Coverage: The target coverage in percent. The default value is 100.If `-' is given instead of a parameter value, the corresponding threshold remains unchanged. The thresholds are checked after each separate state space exploration. If any of them is exceeded, the Power-Walk command is stopped.
<Depth>
Sets the maximum number of transitions which the power walk algorithm performs randomly in the behavior tree in order to increase the symbol coverage (see the command Power-Walk). The default value is 100.
<Depth>
Sets the total maximum depth of the power walk exploration to the value given by the parameter. The default value for max depth is 500.
<Depth>
Sets the depth up to which the power walk algorithm performs a full tree search in order to find a transition increasing the symbol coverage (see the command Power-Walk). The default value is 3.
<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.
The default priorities are:
Note that the priorities of events processed in the validator also is affected by the command Define-Symbol-Time.
<Seed>
Defines the seed for a sequence of pseudo-random numbers, which is used by the commands Random-Walk and Power-Walk. If a seed value is reused, then the resulting sequence of pseudo-random numbers is identical. The default value is 1.
<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. 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. If the parameter is specified as `-', all report types will be defined in the same way.
<Report type> ( "Off" | "One" | "All" )
Defines how many 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 "One".
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.
If "One" is specified only one occurrence of each reported situation is stored.
If "All" is specified then all occurrences of a reported situation that have different execution paths is stored in the list.
The available report types are listed with the command Show-Options. They are also described in Rules Checked During Exploration. 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. 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:
All
All process instances in the ready queue are allowed to execute at each state. First
Only the first process instance in the ready queue is allowed to execute at each state. The default is "First".
<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.
"Zero" | "Undefined"
The time it takes to execute one symbol, e.g. an input, task or decision, in an SDL process is defined either to be zero or undefined. If it is set to zero, it is assumed that all actions performed by process instances take are infinitely fast compared to the timer values that are used in the system. If the symbol time is set to undefined, no assumption is made about how long time it takes for processes to execute symbols. 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 the sets a timer with duration 1. If symbol time is set to zero then the second timer will always expire first. If symbol timer is set to undefined then both timers can potentially expire first.
Note that when symbol time is set to zero, no timer will expire if an internal action is possible, even if internal and timer events have the same priority as set by the command Define-Priorities.
The default value of the symbol time options is "Zero".
<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 manually 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:
The default value is 1.
"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.
"SDL" | "Symbol-Sequence"
Defines the semantics and length of the transitions in the behavior tree. The parameter defines the transitions as follows:
SDL
The behavior tree transitions correspond to complete SDL process graph transitions. Symbol-Sequence
The behavior tree transitions correspond to the longest sequence of SDL symbols that can be executed without any interaction with other process instances. The default is "SDL".
<Depth>
Defines the maximum search depth for tree search.
The default value is 100.
"Standard" | "ITEX"
Determines whether Autolink generates the declarations part of a TTCN test suite. If set to "Standard", Autolink creates declarations with ASN.1 data field names being constructed of the form "data type+parameter number" (e.g. "Integer2"). If set to "ITEX", no declarations are created. In this case, ASN.1 data field names used in constraint definitions are represented by `#' characters. This allows to merge the test suite with declarations generated by Link in ITEX. The default value is "Standard".
This command exists for backward compatibility reasons only.
"ASP" | "PDU"
Determines whether the constraints are stored as ASN.1 ASP constraints or ASN.1 PDU constraints. By default, signals are mapped onto ASPs.
"Global" | "Local" | "Inline"
Defines how test steps are written in a TTCN test suite. "Global" is the default value.
If set to "Global", each test step is saved in a separate behaviour description table. If a test step is used in more than one test case, then only one behaviour description table is generated.
If set to "Local", each test step is saved as a local tree in the behaviour table of the corresponding test case. If a test step is used several times in a single test case, then only one behaviour description is generated.
If set to "Inline", all test step trees are directly inserted into the test case descriptions.
Note that a test step which is used in several places may lead to trees with different inconclusive events or different verdicts. In this case, the test steps are stored in separate tables with unique names.
<Process or Process Type> [ <Variable name> | "Parent" | "Offspring" | "Sender" ] [ "Compare" | "Skip" ]
This command defines how a specific variable is treated when comparing two system states during state space exploration. If the value for a variable is "Compare", this variable will be taken into account when comparing two system states. If the value is "Skip", this variable will not be taken into account, i.e. if the only difference between two system states is that values of variables in "Skip" mode differs, then the system states will be considered equal.
The purpose of the "Skip" mode for variables is to optimize the state space search. There are two different situations where this command can be used:
The benefit with constant variables in "Skip" mode is that the Validator will ignore these variables when computing hash values. This can for large data structures like arrays mean that the performance of the validator can be considerably improved.
<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.
(None)
Information about the process instance given by the current scope is printed (see the Set-Scope command for an explanation of scope). 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.
<Entry number>
The parameters of the signal instance at the specified position in the input port of the process instance given by the current scope are printed (see the Set-Scope command for an explanation of scope). 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>
<Optional component selection>
The value of the specified variable or formal parameter in the current scope is printed (see the Set-Scope command for an explanation of scope). Variable names may be abbreviated. If no variable name is given, all variable and formal parameter values of the process instance given by the current scope are printed. Sender, Offspring, and Parent may also be examined in this way. Their names, however, may not be abbreviated and they are not included in the list of all variables.
|
Note: If a variable is exported, both its current value and its exported value are printed. |
It is possible to examine only a component of a struct, string or array variable, by appending the struct component name or a valid array index value as an additional parameter. The component selection can handle structs and arrays within structs and arrays to any depth by giving a list component selection parameters. SDL syntax with `!' and "( )" as well as just spaces, can be used to separate the names and the index values.
It is also possible to print a range of an array by giving "FromIndex : ToIndex" after an array name. Note that the space before the `:' is required if FromIndex is a name (enumeration literal), and that no further component selection is possible after a range specification.
To see the possible components that are available in the variable, the variable name must be appended by a space and a `?' on input. A list of components or a type name is then given, after which the input can be continued. After a component name, it is possible to append a `?' again to list possible sub components.
To print the value of the data referenced by a Ref pointer it is possible to use the SDL syntax, i.e. the "*>" notation. If, for example, Iref is a Ref(Integer) variable, then Iref*> is the integer referenced by this pointer. If Sref is a Ref of a struct, then Sref*> ! Comp1 is the Comp1 component in the referenced struct. The sequence *> ! can in the monitor be replaced by -> (as for example in C).
If a PId is given within parenthesis, the scope is temporarily changed to
this process instance instead.
(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 (on UNIX), or valinit.com (in Windows), 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.
<Directory name> ( <File name> | `-' )
Extracts all signals from an MSC which are to be sent from the environment into the SDL system and adds them to the list of active signals. This command is only applicable to basic MSCs in textual format, i.e. to those MSCs stored with file extension .mpr. If `-' is given instead of a file name, signal definitions from all MSCs in the specified directory are extracted.
<File name> | `-'
Starts the state space search algorithm which constructs an internal data structure for the MSC test case specified by the parameter. Additionally, constraints for all signals occurring in the test case are generated. At the end all constraints with identical signal definitions are merged. If the command parameter is specified as `-', test cases are generated for all MSC test cases in the current test cases directory. If the previous generation of a test case has been interrupted, Autolink prompts the user to decide whether to continue the interrupted generation or to abort it. No file name is needed if the test case generation is to be continued.
Note that this command requires a TTCN Link license in addition to the Validator license.
<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.
(None)
Lists all currently defined constraints.
(None)
Lists all test cases which have been generated either by Generate-Test-Case or Translate-MSC-Into-Test-Case, or which have been loaded with the Load-Generated-Test-Cases command.
[ `(' <PId value> `)' ]
A list of all signal instances in the input port of the process instance given by the current scope is printed (see the Set-Scope command for an explanation of scope). 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.
If a PId is given within parenthesis information about this process instance is printed instead.
(None)
Lists all defined instance conversions. See also the command Define-Instance-Conversion.
(None)
Lists all MSC test cases and test steps currently stored in the test cases and test steps directories.
(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)
List all process types which are defined to be observer processes.
(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 List-Ready-Queue.
(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.
<File name>
Loads all constraints stored in the file specified by the parameter. The suggested file extension is .con.
<File name>
Loads all generated test cases stored in the file specified by the parameter. The suggested file extension is .gen.
<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.
<First name> <Second name>
Merges the two constraints specified by the parameters. The resulting constraint has at least the formal parameters of the original constraints. If additional constraint parameters are necessary (e.g. when merging two constraints with signals S(1,1) and S(1,2)), Autolink prompts the user to enter a name for each new formal parameter. Merge-Constraints can only be applied to constraints with the same signal. The new constraint gets the name of the second constraint.
<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.
<Constraint name> <Replacement definition>
Replaces concrete values in a constraint with formal parameters. The replacement is defined by a sequence of pairs of a signal parameter number followed by the corresponding formal parameter name. The definition must be terminated with a 0.
(None)
Performs a sequence of automatic explorations of the state space starting from the root system state. Power walk is a combination of a tree search and a random walk. It can be used for the generation of test cases based on the symbol coverage criteria. If the symbol coverage table is not empty when the command is started, Autolink prompts the user to decide whether to clear the table or not. The power walk search algorithm performs the following steps:
Tree-Depth-bounded tree search with `root' as starting state. After the computation of each new state, check whether the current depth is less than Max-Depth or symbol coverage has increased. If the current depth equals Max-Depth then drive the system into a stable state and go to 3. If symbol coverage has increased, set `root' to the new state and go to 1. If no state with increased coverage can be found, continue with 2.Continuation-Depth-bounded random walk. After the computation of each new state, check whether the current depth is less than Max-Depth or symbol coverage has increased. If the current depth equals Max-Depth, then drive the system into a stable state and go to 3. If symbol coverage has increased, set `root' to the new state and go to 1. If no state with increased coverage can be found, continue with 2.The exploration can be interrupted at any time by pressing <Return> at the command prompt or by pressing the Break button if the graphical user interface is used. Furthermore, Define-Power-Walk-Abort-Conditions allows to set values for several criteria to control the number of state space explorations.
(None)
Displays the current Autolink configuration on the screen.
(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.
<Test case name> | `-'
Displays the internal representation of the generated test case specified by the parameter on the screen. If `-' is given instead of a test case name, all generated test cases are shown.
(None)
A textual version of the currently loaded MSC is printed. The format is similar to the textual MSC format defined in ITU 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 (on UNIX), or valinit.com (in Windows),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:
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.
<Old name> <New name>
Renames a constraint. If a constraint with the same "new" name but a different signal definition already exists, the user is prompted to choose between one of the following operations (which can be abbreviated):
Rename: A different name can be chosen for the constraint.Keep_old: The definition of the renamed constraint is cleared. Any references from previously generated test cases to the renamed constraint are redirected to the old constraint.Overwrite_old: The definition of the old constraint is cleared. Any references from previously generated test cases to the old constraint are redirected to the renamed constraint.Restriction: If one of the constraints contains formal parameters, then a different name must always be chosen for the renamed constraint. Rename-Constraint in combination with its options Keep_old and Overwrite_old allows to merge two constraints, e.g. if some signal parameters are irrelevant (see also the command Merge-Constraints and consider the use of CONSTRAINT MATCH ... statements in an Autolink configuration).
(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 (on UNIX), or valinit.com (in Windows), 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>
Saves the current Autolink configuration in a command file. The command name Define-Autolink-Configuration and the terminating End are written at the beginning and the end of the file in order to allow to reload the configuration with Include-File. The suggested file extension is .com.
( <Constraint name> | `-' ) <File name>
Saves the constraint in a file identified by <File name>.If `-' is given instead of a constraint name, all currently defined constraints are saved. The suggested file extension is .con.
<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 Print-Coverage-Table.
(None)
Saves all reports (except those indicating an MSC verification) as MSCs in the target directory. The reports are stored as complete MSCs with file extension .mpr.
For each MSC a generic name consisting of the name of the currently loaded MSC (or "ErrorReport", if none is loaded), a four letter abbreviation of the error type and a sequence number is generated.
Save-Error-Reports-As-MSCs helps to find out what went wrong when running a batch job with a large number of MSC verifications.
Note: This command does not generate MSCs for MSC violation reports if the current MSC could be verified.
( <Test case name> | `-' ) <File name>
Saves the generated test case in a file. If `-' is given instead of a test case name, all generated test cases which are currently stored in memory are saved. The suggested file extension is .gen.
This command allows to compute test cases in parallel on different machines and to merge them afterwards by using Load-Generated-Test-Cases.
( <Test case name> | `*' )
Saves a test case as a system level Message Sequence Chart in the test cases directory (with file extension .mpr). The MSC contains a separate instance axis for each channel to the environment and another axis for the system. It comprises all signals sent to and from the environment for the trace from the root of the behavior tree to the current system state. If `*' is given instead of a test case name, a generic test case name is generated.
( <Test step name> | `*' )
Saves a test step as a system level Message Sequence Chart in the test steps directory (with file extension .mpr). The MSC contains a separate instance axis for each channel to the environment and another axis for the system. It comprises all signals sent to and from the environment for the trace from the root of the behavior tree to the current system state. If `*' is given instead of a test step name, a generic test step name is generated.
<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.
( <Report type> | `-' )
Saves all reports of a specified type as MSC test cases in the test cases directory (in system level MSC format; with file extension .mpr). The MSCs contain a separate instance axis for each channel to the environment and another axis for the system. For each MSC test case a generic name consisting of the report type and a five digit number is generated. If `-' is provided instead of a report type, all current reports are saved.
<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.
|
Note: It is necessary to have executed an Exhaustive-Exploration command before the state space can be saved on a file. |
<Test suite name> <File name>
Saves the generated test cases and all constraints in a test suite file in TTCN MP format. In addition, it generates the declarations part of the TTCN test suite. If the generation of a test case has been interrupted, Autolink prompts the user to decide whether to cancel the command or to abort the test case generation. The suggested file extension for the second parameter is .mp.
Note that this command requires a TTCN Link license in addition to the Validator license.
<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 prints the current scope. See the command Set-Scope for a description of scope.
<Optional service name>
Moves the scope one step down in the procedure call stack. If the current scope is a process containing services, one of the services should be specified. See also the commands Stack, Set-Scope and Scope-Up.
(None)
Moves the scope one step up in the procedure call stack. Up from a service leads to the process containing the service. See also the commands Set-Scope, Stack and Scope-Down.
(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 SDL 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
<PId value> <Optional service name>
This command sets the scope to the specified process, at the bottom procedure call. If the process contains services, one of the services can be given as parameter to the command. A scope is a reference to a process instance, a reference to a service instance if the process contains services, and possibly a reference to a procedure instance called from this process/service. The scope is used for a number of other commands for examining the local properties of a process instance. The scope is automatically set to the process that executed in the transition leading to the current system state.
See also the commands Scope, Stack, Scope-Down and Scope-Up.
(None)
The state space options of the Validator are set to perform state space exploration according to the ITU 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 ITU 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 The Coverage Viewer for further description of the Coverage Viewer.
(None)
This command displays a summary of the current execution mode and some other information about the current state of the SDT Validator.
(None)
This command starts the Navigator tool to simplify interactive navigation in the behavior tree of the SDL system. See The Navigator Tool 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 for more details.
(None)
The versions of the C Code Generator and the runtime kernel that generated the currently executing program are presented.
(None)
The procedure call stack for the PId/service defined by the scope is printed. For each entry in the stack, the type of instance (procedure/process/service), the instance name and the current state is printed. See also the commands Set-Scope, Scope-Down and Scope-Up.
(None)
Go up in the behavior tree to the start of the current path (the root system state).
( <File name> | `-' )
Translates an MSC into an internal test case data structure without performing a state space search. Additionally, constraints for all signals occurring in the test case are generated. At the end, all constraints with identical signal definitions are merged. If the command parameter is specified as `-', all MSCs in the current test cases directory are transformed into test cases.
Translate-MSC-Into-Test-Case does not require a fully specified SDL system. However, the signals used in the MSC must be defined in the SDL specification. Additionally, the channels between the SDL system and its environment have to be specified in order to find out which MSC instances relate to PCOs and which relate to the SDL system. Therefore, a direct translation cannot be applied to MSCs which consist of only a single instance axis for the environment.
Since the translation is done statically, it is not checked whether the MSC can in fact be verified. In addition, no inconclusive events are computed.
Note that this command requires a TTCN Link license in addition to the Validator license.
(None)
Performs a tree search of the state space from the current system state. A tree search is an exploration where all possible combinations of actions are executed. The tree that is explored is exactly the same tree that can manually be inspected using the Navigator feature (or manual exploration using the Next / List-Next commands).
The depth of the tree search is bounded and is defined by the Define-Tree-Search-Depth command. The default depth is 100.
The command can be aborted by the user by pressing the Break button in the Validator UI or any key if running the validator from the command prompt.
<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 all execution traces that are 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.
The file can either be an basic MSC file (.msc), a textual MSC file (.mpr) or a high-level MSC file (.mrm).
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, and reports for MSC verification and MSC violation are generated.
If the MSC is a high-level MSC or it contains MSC reference expressions more that one MSC verification report can be generated. There will be one report for each sequence of `leaf' MSCs that can be verified. For more information on criteria for MSC verification, see MSC Verification Errors.
If the MSC was verified and exactly one MSC verification report was generated, 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.
If the MSC contains MSC references the Validator needs to match the logical MSC names in the MSC references with MSC file names. This is done according to the following algorithm:
.msc, .mpr or .mrm. .msc, .mpr or .mrm. If this is the case this MSC file is used.This section describes the appearance and functionality of the graphical user interface to the validator monitor (ValUI). Some user interface descriptions general to all tools in Telelogic Tau can be found in User Interface and Basic Operations. These general descriptions are not repeated in this chapter.
For an explanation of the Validator main window, depicted in Figure 467, see Graphical User Interface.
|
|
A new ValUI is started by selecting SDL > Validator UI from the Tools menu in the Organizer. When the ValUI is started, a number of definition files are read, controlling the contents of the main window and some status windows. See Definition Files for more information.
No validator is started automatically by the ValUI in this way. The user must start a validator by selecting Open from the File menu, as stated in the text area of the main window, or by using the Open quick button.
|
|
A simple way to generate a validator, start the ValUI and open the validator is to click the Validate quick button in the Organizer. |
When a simulator is started, a file selection dialog may be opened if the SDL system contains external synonyms. For more information, see Supplying Values of External Synonyms.
The following tables list the default buttons in the button modules and the corresponding monitor command. See Monitor Commands for more information.
|
Note: The buttons in the button modules are specified in the button definition file. If the default button file is not used, the button modules may be different than described here. See Button and Menu Definitions for more information. |
| Button | Monitor command |
|---|---|
|
Bit-State |
|
|
Exhaustive |
|
|
Top |
|
|
Bottom |
|
|
Random Walk |
|
|
Tree Search |
|
|
Up |
Up 1 |
|
Down |
Down 1 |
|
Power Walk |
|
|
Verify MSC |
|
|
Navigator |
|
|
Break |
Pressing |
| Button | Monitor command |
|---|---|
|
Scope |
|
|
Set Scope |
|
|
Scope Up |
|
|
Scope Down |
|
|
Call Stack |
|
|
Ready Q |
|
|
Process List |
|
|
Process |
|
|
Input Port |
|
|
Signal |
|
|
Timer List |
|
|
Timer |
|
|
Variable |
| Button | Monitor command |
|---|---|
|
List Value |
|
|
List Par |
|
|
List Signal |
|
|
Clear Signal |
|
|
Def Value |
|
|
Def Par |
|
|
Def Signal |
|
|
Extract Sigs |
|
|
Clear Value |
|
|
Clear Par |
This section describes the additional menus of the ValUI's menu bar in comparison with the SimUI. The menus common to both the ValUI and the SimUI is described in The Menu Bar.
The menu bar contains the following menus:
In addition to the standard SimUI menus, a few special validator menus are included in the menu bar. The menu choices in these menus simply execute a monitor command, i.e. they are functionally equivalent to buttons in the button modules. If the monitor command requires parameters, they are prompted for using dialogs in the same way as the command buttons.
The following tables list the default menu choices and the corresponding monitor command. See Monitor Commands for more information.
|
Note: The additional menus in the ValUI are specified in the button definition file. If the default button file is not used, the additional menus may be different than described here. See Button and Menu Definitions for more information. |
| Menu choice | Monitor command |
|---|---|
|
Toggle MSC Trace |
|
|
Toggle SDL Trace |
|
|
Show Coverage Viewer |
|
|
Define Rule |
|
|
Include Command Script |
| Menu choice | Monitor command |
|---|---|
|
Show Options |
|
|
Reset |
|
|
Default |
|
|
Advanced |
Define-Scheduling All ; Define-Priorities 1 1 1 1 1 ; Define-Max-Input-Port-Length 2 ; Define-Report-Log MaxQueuelength Off |
|
State Space : Transition |
|
|
- : Scheduling |
|
|
- : Priorities |
|
|
- : Input Port Length |
|
|
- : Transition Length |
|
|
- : Max Instance |
|
|
- : Timer Progress |
|
|
- : Channel Queues |
|
|
- : Max State Size |
|
|
- : Symbol Time |
|
|
Report : Continue |
|
|
- : Prune |
|
|
- : Abort |
|
|
- : Report Log |
|
|
MSC Trace Auto Popup |
|
|
Report Viewer Auto Popup |
| Menu choice | Monitor command |
|---|---|
|
Configuration : Define |
|
|
|
|
|
- : Clear |
|
|
- : Save |
|
|
- : Load |
|
|
Constraint : Define |
|
|
- : List |
|
|
- : Rename |
|
|
- : Merge |
|
|
- : Parameterize |
|
|
- : Clear |
|
|
- : Save |
|
|
- : Load |
The Command window of the ValUI is identical to the SimUI (see Command Window). The only difference is that the default commands to execute are " List-Process -" and " Print-Trace 1". The set of commands to execute are stored in a command definition file (see Definition Files). The default command definition file can be changed with the Preference Manager.
The Watch window of the ValUI is identical to the SimUI (see Watch Window).
The Navigator is a separate tool in the ValUI that is used for navigating in the behavior tree. It can be opened in the following ways:
Figure 468 : The Navigator window
|
|
The Navigator window consists of the tree area and the tool bar. There is no menu bar or status bar in the Navigator window.
The tree area of the Navigator window shows the structure of the behavior tree around the current system state. Each box, or node, represents a tree transition from one system state to another.
The text in the boxes contains the textual trace describing the tree transition. This may represent a complete or partial SDL process graph transition, depending on how the behavior tree is set up. The number of down nodes also depends on the structure of the behavior tree. This is determined by the state space options; see State Space Options.
Double-clicking a node in the Navigator executes the corresponding tree transition and moves one level up or down in the behavior tree. The current system state is changed and the Navigator window is updated to show the situation around the new system state.
|
Note: Double-clicking a collapsed node (see below) does not expand the node; it always executes the corresponding transition. |
The Navigator window is also updated whenever a monitor command is executed that changes the current system state.
Each node in the node area has an associated popup menu.
|
Up 1 |
On the up node: Go up one level in the tree. This is the same as double-clicking the up node. |
|
Up to top |
On the up node: Go to the top of the behavior tree. |
|
Continue Up |
On the up nodes: Go up in the tree until more than one transition is possible (see Continue-Up-Until-Branch command). |
|
Goto |
On the down nodes: Go down this branch of the tree. This is the same as double-clicking the down node. |
|
Continue |
On the down nodes: Go down this branch of the tree until more than one transition is possible (see Continue-Until-Branch command). |
|
Expand |
Expand the collapsed node to show the down nodes. |
|
Expand Substructure |
The same as Expand. |
|
Collapse |
Collapse the node to hide the down nodes. A small triangle below the node shows that it is collapsed. |
The following quick buttons are special to the Navigator tool. The general quick buttons are described in General Quick-Buttons.
|
|
Close
Closes the Navigator tool. |
|
|
Structure
Switches between a tree structure and a list structure in the node area. |
|
|
Show Validator UI
Raises the Validator UI window. |
The Report Viewer is a separate tool in the ValUI that is used for examining the reports generated during an automatic state space exploration. It is opened in one of the following ways:
Figure 469 : The Report Viewer
|
|
The Report Viewer window consists of the Report Area, containing Popup Menus, and the tool bar, containing Quick Buttons. There is no menu bar or status bar in the Report Viewer window.
The report area of the Report Viewer shows the current reports from the latest state space exploration in the form of a report tree. The report tree contains three levels of nodes (see Figure 469):
Double-clicking a report node at the bottom level causes the Validator to "go to" the report, i.e., go to the system state where the report was generated. The following things happen:
Double-clicking the top node or a report type node will expand or collapse the node, depending on its state. A collapsed node hides its underlying nodes and is indicated by a small triangle below the node.
The following quick buttons are special to the Report Viewer. The general quick buttons are described in General Quick-Buttons.
|
|
Close
Closes the Report Viewer. |
|
|
Structure
Switches between a tree structure and a list structure in the report area. |
|
|
Show Validator UI
Raises the Validator UI window. |
In the ValUI, the syntax and contents of the definition files are the same as for the SimUI; see Definition Files. The default file names for the definition files are val_def.btns, val_def.cmds and val_def.vars, respectively.
For each system state encountered during state space exploration, a number of rules are checked to detect errors or possible problems in the SDL system. If a rule is satisfied, a report is generated to the user.
The rules that are checked by the SDT Validator are the same ones as checked and reported by the SDT Simulator, with a few additions and differences.
Apart from the predefined rules, an additional rule can be defined by the user of the validator to check for other properties of the system states encountered. See User-Defined Rules for more information.
The rules are listed below, together with the reported error messages. The rules are grouped according to the corresponding report type, used in the Report Viewer in the Validator. The names of the report types listed below are the ones to be used in the monitor commands that define the report actions.
Deadlock
All processes instances are waiting for some other process instance to act, implying that none of the processes will execute. This is referred to as a deadlock.
Warning: Implicit signal consumption of signal <signal>
A signal was sent to a process that was not able to handle (or save) the signal in the current state, so it was implicitly consumed.
Error in SDL Create: Processtype <type> More static instances than maximum number of instances.
There are more static instances defined than the maximum allowed number of instances.
Warning in SDL Create: Processtype <type> Unsuccessful create. Number of instances has reached maximum number.
An attempt has been made to create a new instance of a process type of which there is already the maximum number of allowed instances active. The maximum number is either the value defined by the command Define-Max-Instance, or the value defined in the SDL diagram, whichever is smallest.
Error in SDL Output of signal <signal> No valid receiver found
An attempt was made to output a signal to an invalid PId expression.
Error in SDL Output of signal <signal> No path to receiver
An attempt was made to output a signal to a PId expression. There exists, however, no path of channels and signal routes between the sender and the receiver that can convey the signal.
Error in SDL Output of signal <signal> No possible receiver found
An attempt was made to output a signal without specifying a PId expression. When all paths or all paths mentioned in a via clause had been examined no possible receiver was found.
Error in SDL Output of signal <signal> Several possible receivers found
An attempt was made to output a signal without specifying a PId expression. When all paths or all paths mentioned in a via clause had been examined several possible receivers were found.
Error in SDL Output of signal <signal> Signal sent to stopped process instance
An attempt was made to output a signal to a PId expression that referred to a process instance which has performed a stop action.
Error in SDL Output of signal <signal> Signal sent to NULL
An attempt was made to output a signal to a PId expression that was null.
Error in SDL Output of signal <signal> Illegal signal type in output TRANSFER
An attempt was made to output a signal with the TRANSFER directive that was not the same signal as in the preceding input.
Error in remote procedure call: <name> More than one process provides the remote procedure
An attempt was made to call a remote procedure in a system state where there are more than one possible process instance that can provide the remote procedure.
Error in remote procedure call: <name> No process provides the remote procedure
An attempt was made to call a remote procedure in a system state where
there is no possible process instance that can provide the remote procedure.
Error in SDL Output of signal <signal> Max input port length exceeded
The length of the input port of the receiving process has exceeded the value defined by the monitor command Define-Max-Input-Port-Length.
Error in SDL Output of signal <signal> Max channel queue length exceeded
The length of the queue of the receiving channel has exceeded the value defined by the monitor command Define-Max-Input-Port-Length.
Error in channel output. Max input port length exceeded
The length of the input port of the receiving process has exceeded the value defined by the monitor command Define-Max-Input-Port-Length.
Error in channel output. Max channel queue length exceeded
The length of the queue of the receiving channel has exceeded the value defined by the monitor command Define-Max-Input-Port-Length
In addition to the following messages, information about the channel, signal, sender and receiver is also displayed.
Error in channel output. No valid receiver found
An attempt was made to output a signal to an invalid PId expression.
Error in channel output. No path to receiver
An attempt was made to output a signal to a PId expression. There exists, however, no path of channels and signal routes between the sender and the receiver that can convey the signal.
Error in channel output. No possible receiver found
An attempt was made to output a signal without specifying a PId expression. When all paths or all paths mentioned in a via clause had been examined no possible receiver was found.
Error in channel output. Several possible receivers found
An attempt was made to output a signal without specifying a PId expression. When all paths or all paths mentioned in a via clause had been examined several possible receivers were found.
Error in channel output. Signal sent to stopped process instance
An attempt was made to output a signal to a PId expression that referred to a process instance which has performed a stop action.
Error in channel output. Signal sent to NULL
An attempt was made to output a signal to a PId expression that was null.
The errors that can be found in operators defined in the predefined data types are listed below.
Error in SDL Operator: Modify! in sort Charstring, Index out of bounds Error in SDL Operator: Extract! in sort Charstring, Index out of bounds Error in SDL Operator: MkString in sort Charstring, character NUL not allowed Error in SDL Operator: First in sort Charstring, Charstring length is zero Error in SDL Operator: Last in sort Charstring, Charstring length is zero Error in SDL Operator: Substring in sort Charstring, Charstring length is 0 Error in SDL Operator: Substring in sort Charstring, Sublength is less than or equal to zero Error in SDL Operator: Substring in sort Charstring, Start is less than or equal to zero Error in SDL Operator: Substring in sort Charstring, Start + Substring length is greater than string length. Error in SDL Operator: Division in sort Integer, Integer division by 0. Error in SDL Operator: Division in sort Real, Real division by 0. Error in SDL Operator: Fix in sort Integer Integer overflow Second operand is 0 Error in SDL Operator: Mod in sort Integer Second operand is 0 Error in SDL Operator: Rem in sort Integer Second operand is 0
Error in assignment in sort <sort>: <value> out of range
A variable of a restricted syntype is assigned a value out of its range.
Error in SDL array index in sort <sort>: <value> out of range
An array index is out of range.
Error in SDL Decision: Value is <value>: Fatal error. Analysis is not continued below this node
The value of the expression in the SDL decision did not match any of the possibilities (answers).
Error during execution of an import statement. Supplementary information about remote variables and exporting processes is also given.
Error in SDL Import. Attempt to import from the environment Error in SDL Import. Attempt to import from NULL Error in SDL Import. Attempt to import from stopped process instance Error in SDL Import. Several processes exporting this variable Error in SDL Import. The specified process does not export this variable Error in SDL Import. No process exports this variable Error in SDL Import. More than one process exports this variable
Error during execution of view statement. Supplementary information about viewed variables and revealing processes is also given.
Error in SDL View. Attempt to view from the environment Error in SDL View. Attempt to view from NULL Error in SDL View. Attempt to view from stopped process instance Error in SDL View. More than one process instance reveals the variable Error in SDL View. The specified process does not reveal the variable. Error in SDL View. No process instance reveals this variable
Max transition length exceeded
The maximum number of SDL symbols executed in one behavior tree transition is more than the value defined by the monitor command Define-Max-Transition-Length.
Loop Detected.
The Validator includes a mechanism for non-progress loop detection. A report will be generated if the Validator during state space exploration finds a loop in the state space which does not contain any progress transition. A progress transition is defined as a transition that either:
xProgress() in user-defined C codeAssertion is false: <user-defined string>
A user-defined action in the SDL system has called the function . See Using Assertions for more information.
xAssertError
User-defined rule satisfied
A user-defined rule is evaluated to true.
Observer violation
A process defined as an observer process has not been able to execute a transition.
MSC <MSC name> verified MSC sequence: <MSC name list> MSC <MSC name> violated Event: <SDL Event>
The MSC verification report is given when a state space exploration has reached a state where the execution trace from the root of the behavior tree to the current state satisfies the loaded MSC. In this case, "satisfies" means that:
An event on the execution trace is considered to be "observable" if it is either
|
Note: Two process instances can correspond to the same MSC instance if the MSC is a system or block level MSC. |
The MSC violation report is given during state space exploration for each generated execution trace that either:
No reference to dynamically allocated memory of sort: <Sort Name>
The list of dynamically allocated data areas that is maintained by the Validator contains a data area that no SDL entity (like a variable, signal parameter etc.) references. This indicates a memory leak in the system.
No reference to dynamically allocated memory
The list of dynamically allocated data areas that is maintained by the Validator contains a data area that no SDL entity (like a variable, signal parameter etc.) references. This indicates a memory leak in the system. The lack of <Sort Name> in this report indicates that this is a newly allocated data area and there has been no previous system state with a reference to this data area.
Referenced data area not found: Variable <Variable name> in process <Process name>
A REF variable (or signal parameter, structure field etc.) has been found that references a data area that is not allocated. To avoid this report always set the REF variables to NULL after the data area has been released.
Dereferencing a NULL pointer of sort: <Sort Name>.
An expression XX*> has been evaluated where XX was NULL.
Calling UserMalloc with parameter NULL Calling UserFree with parameter NULL
The UserMalloc or UserFree functions has been called with NULL as a parameter which is illegal.
Calling UserFree without dynamically allocated memory
UserFree has been called with a parameter that is not a pointer to one of the data areas in the list of the dynamically allocated data areas.
User-defined rules are used during state space exploration to check for properties of the system states encountered. If a system state is found for which a user-defined rule is true, this will be listed among the other reports when giving the List-Reports command. During an exploration more that one user defined rule report can be generated. There will be one report for each value assignment that can be made to a rule. The value assignments are the values printed by the Print-Evaluated-Rule command.
A rule essentially gives the possibility to define predicates that describe properties of one particular system state. A rule consists of a predicate (as described below) followed by a semicolon (`;'). In a rule, all identifiers and reserved words can be abbreviated as long as they are unique.
|
Note: Only one rule can be used at any moment. If more than one rule is needed, reformulate the rules as one rule, using the boolean operators described below. |
The following types of predicates exist:
Parenthesis are allowed to group predicates.
The quantifiers listed below are used to define rule variables denoting process instances or signals. The rule variables can be used in process or signal functions described later in this section.
exists <RULE VARIABLE> [: <PROCESS TYPE>] [ | <PREDICATE>]
This predicate is true if there exists a process instance (of the specified type) for which the specified predicate is true. Both the process type and the predicate can be excluded. If the process type is excluded all process instances are checked. If the predicate is excluded it is considered to be true.
all <RULE VARIABLE> [ : <PROCESS TYPE>] [ | <PREDICATE>]
This predicate is true for all process instances (of the specified type) for which the specified predicate is true. Both the process type and the predicate can be excluded. If the process type is excluded all process instances are checked. If the predicate is excluded it is considered to be true.
siexists <RULE VARIABLE> [ : <SIGNAL TYPE>] [ - <PROCESS INSTANCE>] [ | <PREDICATE>]
This predicate is true if there exists a signal (of the specified type) in the input port of the specified process for which the specified predicate is true. If no signal type is specified, all signals are considered. If no process instance is specified the input ports of all process instances are considered. If no predicate is specified it is considered to be true. The specified process can be either a rule variable that has previously been defined in an exists or all predicate, or a process instance identifier (<PROCESS TYPE>:<INSTANCE NO>).
siall <RULE VARIABLE> [ : <SIGNAL TYPE>] [ - <PROCESS INSTANCE>] [ | <PREDICATE>]
This predicate is true for all signals (of the specified type) in the input port of the specified process for which the specified predicate is true. If no signal type is specified all signals are considered. If no process is specified the input ports of all process instances are considered. If no predicate is specified it is considered to be true. The specified process can be either a rule variable that has previously been defined in an exists or all predicate, or a process instance identifier (<PROCESS TYPE>:<INSTANCE NO>).
The following boolean operators are included (with the conventional interpretation):
not <PREDICATE> <PREDICATE> and <PREDICATE> <PREDICATE> or <PREDICATE>
The operators are listed in priority order, but the priority can be changed by using parenthesis.
The following relational operator predicates exist:
<EXPRESSION> = <EXPRESSION> <EXPRESSION> != <EXPRESSION> <EXPRESSION> < <EXPRESSION> <EXPRESSION> > <EXPRESSION> <EXPRESSION> <= <EXPRESSION> <EXPRESSION> >= <EXPRESSION>
The interpretation of these predicates is conventional. The operators are only applicable to data types for which they are defined.
The expressions that are possible to use in relational operator predicates are of the following categories:
Most of the process functions must have a process instance as a parameter. This process instance can be either a rule variable that has previously been defined in an exists or all predicate, a process instance identifier (<PROCESS TYPE>:<INSTANCE NO>), or a function that returns a process instance, e.g. sender or from.
state( <PROCESS INSTANCE> )
Returns the current SDL state of the process instance.
type( <PROCESS INSTANCE> )
Returns the type of the process instance.
iplen( <PROCESS INSTANCE> )
Returns the length of the input port queue of the process instance.
sender( <PROCESS INSTANCE> )
Returns the value of the imperative operator sender (a process instance) for the process instance.
parent( <PROCESS INSTANCE> )
Returns the value of the imperative operator parent (a process instance) for the process instance.
offspring( <PROCESS INSTANCE> )
Returns the value of the imperative operator offspring (a process instance) for the process instance.
self( <PROCESS INSTANCE> )
Returns the value of the imperative operator self (a process instance) for the process instance.
signal( <PROCESS INSTANCE> )
Returns the signal that is to be consumed if the process instance is in an SDL state. Otherwise, if the process instance is in the middle of an SDL process graph transition, it returns the signal that was consumed in the last input statement.
<PROCESS INSTANCE> -> <VARIABLE NAME>
Returns the value of the specified variable. If <PROCESS INSTANCE> is a previously defined rule variable, the exists or all predicate that defined the rule variable must also include a process type specification.
<RULE VARIABLE>
Returns the process instance value of <RULE VARIABLE>, which must be a rule variable bound to a process instance in an exists or all predicate.
Most of the signal functions must have a signal as a parameter. This signal can be either a rule variable that has previously been defined in an siexists or siall predicate, or a function that returns a signal, e.g. signal.
sitype( <SIGNAL> )
Returns the type of the signal.
to( <SIGNAL> )
Returns the process instance value of the receiver of the signal.
from( <SIGNAL> )
Gives the process instance value of the sender of the signal.
<RULE VARIABLE> -> <PARAMETER NUMBER>
Returns the value of the specified signal parameter. The siexists or siall predicate that defined the rule variable must also include a signal type specification.
<RULE VARIABLE>
Returns the signal value of <RULE VARIABLE>, which must be a rule variable bound to a signal in a siexists or siall predicate.
maxlen( )
Gives the length of the longest input port queue in the system.
instno( [<PROCESS TYPE>] )
Returns the number of instances of type <PROCESS TYPE>. If <PROCESS TYPE> is excluded the total number of process instances is returned.
depth( )
Gives the depth of the current system state in the behavior tree/state space.
<STATE ID>
The name of an SDL state.
<PROCESS TYPE>
The name of a process type.
<PROCESS INSTANCE>
A process instance identifier of the format <PROCESS TYPE>:<INSTANCE NO>, e.g. Initiator:1.
<SIGNAL TYPE>
The name of a signal type.
null
SDL null process instance value
env
Returns the value of the process instance in the environment that is the sender of all signals sent from the environment of the SDL system.
<INTEGER LITERAL> true false <REAL LITERAL> <CHARACTER LITERAL> <CHARSTRING LITERAL>
An Autolink configuration is created with the command Define-Autolink-Configuration. The syntax of an Autolink configuration is expressed below in EBNF format.
<Start> ::= "Define-Autolink-Configuration"
<Configuration>
"End"
<Configuration> ::= { <TransRule> | <TSStructureRule> |
<Function> }*
<TransRule> ::= "TRANSLATE"
[ "SIGNAL" ] <AlternativeListOfTerms>
<TransRuleIf>* [ <TransRuleNoIf> ]
"END"
<TransRuleIf> ::= "IF" <Conditions> "THEN"
<TransRuleNoIf> "END"
<TransRuleNoIf> ::= { "CONSTRAINT"
<TransRuleConstraint> |
"TESTSUITE"
<TransRuleTestSuite> }*
<TransRuleConstraint> ::= { "NAME" <Term> |
"PARS" <ParameterList1> |
"MATCH" <ParameterList1> }*
<TransRuleTestSuite> ::= { "CONSTS" <ParameterList1> |
"PARS" <ParameterList2> }*
<ParameterList1> ::= <Parameter1> { "," <Parameter1> }*
<Parameter1> ::= "$" <Number> [ "=" <Term> ]
<ParameterList2> ::= <Parameter2> { "," <Parameter2> }*
<Parameter2> ::= "$" <Number> [ "=" <Term> ]
[ "/" <Term> ]
<TSStructureRule> ::= "PLACE" <AlternativeListOfTerms>
<TSStructureRuleIf>*
[ <TSStructureRuleNoIf> ]
"END"
<TSStructureRuleIf> ::= "IF" <Conditions> "THEN"
<TSStructureRuleNoIf> "END"
<TSStructureRuleNoIf> ::= "IN" <Term> { "/" <Term> }*
<Function> ::= "FUNCTION" <Identifier>
<Mappings> "END"
<Mappings> ::= <Mapping> { "|" <Mapping> }*
<Mapping> ::= <Conditions> ":" <Term>
<Term> ::= <Atom> { "+" <Atom> }*
<Atom> ::= "$" <Number> | "@" <Number> |
<Text> | <Identifier> |
<FunctionCall>
<FunctionCall> ::= <Identifier>
"(" <SequentialListOfTerms> ")"
<SequentialListOfTerms> ::= <Term> { "," <Term> }*
<AlternativeListOfTerms> ::= <Term> { "|" <Term> }*
<Conditions> ::= <Condition> { "AND" <Condition> }*
<Condition> ::= <Term> { "==" | "!=" } <Term> |
"TRUE"
For a detailed description of the semantics, see Syntax and Semantics of the Autolink Configuration.
Using the command Save-State-Space, a Labelled Transition System (LTS) representing the state space generated during exhaustive exploration is saved to a file.
The syntax of the generated LTS is (using BNF notation):
LTS ::= `START:' StateId `LTS:' TransList*
`STATES:' State*
TransList ::= StateId `:' Event `-' [StateId] (`,' Event
`-' [StateId])* `;'
Event ::= (Output | Input | Timeout | Internal)
Output ::= `o(' Signal `,' `"' GraphRef `"' `)'
Input ::= `i(' Signal `,' `"' GraphRef `"' `)'
Timeout ::= `t(' Timer `)'
Internal ::= `x'
State ::= `*****' StateId `*****' Process*
Process ::= ProcessName `:' InstanceNo `State:' StateName (VariableName `:' Value)* `Input port:[' Signal (`,' Signal)* `]' `Timers:{' Timer (`,' Timer)* `}' Procedure*
Procedure ::= `Procedure' ProcedureName `:' `State:'
StateName (VariableName `:' Value)*
Signal ::= SignalName `(' ParameterName (`,'
ParameterName)* `)'
Timer ::= TimerName `(' ParameterName (`,'
ParameterName)* `)'
The lexical elements used above are:
StateId An integer denoting a system state. GraphRef A string denoting a graphical reference to an SDL diagram. ProcessName An id denoting a process type. InstanceNo An integer denoting a process instance. StateName An id denoting a state in an SDL process graph. VariableName An id denoting a process variable. Value A string denoting a value for a variable of any defined SDL type. ProcedureName An id denoting a procedure. ParameterName An id denoting a signal or timer parameter.
A simple example of a generated LTS:
START:121
LTS:
2456:o(sig1(true,3),"5 P1 1 80 100")-43567;
43567:i(sig2(1),"5 P1 1 80 120")-2467,
i(sig2(2),"5 P1 1 100 120")-98567;
121:x-2456;
2467:x-27645;
98567:x-27645;
27645:i(sig2(1),"5 P1 1 80 120")-2467,
i(sig2(2),"5 P1 1 100 120")-98567;
STATES:
***** 121 *****
P1:1 State:idle Parent:null Offspring:null Sender:null i:0 Input port:[ ] Timers:{ }
***** 2456 *****
P1:1 State:idle Parent:null Offspring:null Sender:null i:5 Input port:[ ] Timers:{ }
***** 43567 *****
P1:1 State:s1 Parent:null Offspring:null Sender:null i:5 Input port:[ ] Timers:{ }
***** 2467 *****
P1:1 State:s1 Parent:null Offspring:null Sender:null i:1 Input port:[ ] Timers:{ }
***** 98567 *****
P1:1 State:s1 Parent:null Offspring:null Sender:null i:2 Input port:[ ] Timers:{ }
***** 27645 *****
P1:1 State:s1 Parent:null Offspring:null Sender:ENV i:5 Input port:[ ] Timers:{ }
The restrictions on the SDL system that can be validated with the SDT Validator are basically the restrictions imposed by the C Code Generator. See Restrictions for more information.
In addition to these general restrictions, the following restrictions are specific to the SDT Validator:
There following restrictions apply to monitor input:
<Ctrl+C>, <Ctrl+D>, and <Ctrl+Z> are typical characters that might terminate a validation program.There are a number of dynamic checks that are not performed at all or performed at the C level by the C runtime system. A C runtime error will of course lead to the validation program being terminated. The following check is not made at the SDL level.