IBM
Contents Index Previous Next



Rules Checked During Exploration


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 SDL Explorer are the same ones as checked and reported by the SDL Simulator, with a few additions and differences.

Apart from the predefined rules, an additional rule can be defined by the user of the explorer 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 Explorer. The names of the report types listed below are the ones to be used in the monitor commands that define the report actions.

Deadlock

Report Type:  Deadlock



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.

Implicit Signal Consumption

Report Type:  ImplSigCons



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.

Create Errors

Report Type:  Create



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.

Output and Remote Procedure Call Errors

Report Type:  Output



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.

Max Queue Length Exceeded

Report Type:  MaxQueuelength



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

Channel Output Errors

Report Type:  ChannelOutput

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.

Operator Errors

Report Type:  Operator

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

Range Errors

Report Type:  Subrange



Error in assignment in sort <sort>:
<value> out of range

A variable of a restricted syntype is assigned a value out of its range.

Index Error

Report Type:  Index



Error in SDL array index in sort <sort>:
<value> out of range

An array index is out of range.

Decision Error

Report Type:  Decision



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).

Import Errors

Report Type:  Import

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

View Errors

Report Type:  View

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

Transition Length Error

Report Type:  MaxTransLen



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.

Non Progress Loop Error

Report Type:  Loop



Loop Detected.

The Explorer includes a mechanism for non-progress loop detection. A report will be generated if the Explorer 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 Errors

Report Type:  Assertion



Assertion is false: <user-defined string>

A user-defined action in the SDL system has called the function
xAssertError
. See Using Assertions for more information.

User Defined Rule

Report Type:  UserRule



User-defined rule satisfied

A user-defined rule is evaluated to true.

Observer Errors

Report Type:  Observer



Observer violation

A process defined as an observer process has not been able to execute a transition.

MSC Verification Errors

Report Type:  MSCVerification

Report Type:  MSCViolation



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:

REF Errors

Report Type:  RefError



No reference to dynamically allocated memory of 
sort: <Sort Name>

The list of dynamically allocated data areas that is maintained by the Explorer 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 Explorer 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.


http://www.ibm.com/rational
Contents Index Previous Next