Table of ContentsTable of Contents 
Previous Chapter 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" on page 1940 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.
DeadlockAll 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 foundAn attempt was made to output a signal to an invalid PId expression.
Error in SDL Output of signal <signal> No path to receiverAn 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 foundAn 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 foundAn 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 instanceAn 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 NULLAn 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 TRANSFERAn 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 procedureAn 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 procedureAn attempt was made to call a remote procedure in a system state where
Error in SDL Output of signal <signal> Max input port length exceededThe 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 exceededThe 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 exceededThe 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 exceededThe 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 foundAn attempt was made to output a signal to an invalid PId expression.
Error in channel output. No path to receiverAn 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 foundAn 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 foundAn 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 instanceAn 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 NULLAn 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 rangeA variable of a restricted syntype is assigned a value out of its range.
Error in SDL array index in sort <sort>: <value> out of rangeAn array index is out of range.
Error in SDL Decision: Value is <value>: Fatal error. Analysis is not continued below this nodeThe 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 exceededThe 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:
Assertion is false: <user-defined string>A user-defined action in the SDL system has called the function
User-defined rule satisfiedA user-defined rule is evaluated to true.
Observer violationA process defined as an observer process has not been able to execute a transition.
MSC <MSC name> verified 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:
----------------------------------------------------------------- Note: Two process instances can correspond to the same MSC instance if the MSC is a system or block level MSC. -----------------------------------------------------------------
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 opera tors described below. ------------------------------------------------------------------
exists <RULE VARIABLE> [: <PROCESS TYPE>]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.
[ | <PREDICATE>]
all <RULE VARIABLE> [ : <PROCESS TYPE>]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.
[ | <PREDICATE>]
siexists <RULE VARIABLE> [ : <SIGNAL TYPE>]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>).
[ - <PROCESS INSTANCE>] [ | <PREDICATE>]
siall <RULE VARIABLE> [ : <SIGNAL TYPE>]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>).
[ - <PROCESS INSTANCE>] [ | <PREDICATE>]
not <PREDICATE> <PREDICATE> and <PREDICATE> <PREDICATE> or <PREDICATE>The operators are listed in priority order, but the priority can be changed by using parenthesis.
<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.
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.
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.
Gives the length of the longest input port queue in the system.
maxlen( )
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.
The name of an SDL state.
<STATE ID>
<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.
nullSDL null process instance value
envReturns 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>
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)* `)'
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.
Example 56 : A Generated LTSA 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:{ }
In addition to these general restrictions, the following restrictions are specific to the SDT Validator:
Table of Contents 
Next Chapter