![]() |
![]() |
![]() |
![]() |
![]() |
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: DeadlockDeadlockAll 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: ImplSigConsWarning: 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: CreateError 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: OutputError 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
there is no possible process instance that can provide the remote procedure.Max Queue Length Exceeded
Report Type: MaxQueuelengthError 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
Channel Output Errors
Report Type: ChannelOutputIn 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.
Operator Errors
Report Type: OperatorThe 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 boundsError in SDL Operator: Extract! in sort Charstring, Index out of boundsError in SDL Operator: MkString in sort Charstring, character NUL not allowedError in SDL Operator: First in sort Charstring, Charstring length is zeroError in SDL Operator: Last in sort Charstring, Charstring length is zeroError in SDL Operator: Substring in sort Charstring, Charstring length is 0Error in SDL Operator: Substring in sort Charstring, Sublength is less than or equal to zeroError in SDL Operator: Substring in sort Charstring, Start is less than or equal to zeroError 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 IntegerInteger overflowSecond operand is 0Error in SDL Operator: Mod in sort IntegerSecond operand is 0Error in SDL Operator: Rem in sort IntegerSecond operand is 0Range Errors
Report Type: SubrangeError in assignment in sort <sort>:<value> out of rangeA variable of a restricted syntype is assigned a value out of its range.
Index Error
Report Type: IndexError in SDL array index in sort <sort>:<value> out of rangeAn array index is out of range.
Decision Error
Report Type: DecisionError 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).
Import Errors
Report Type: ImportError 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 environmentError in SDL Import. Attempt to import from NULLError in SDL Import. Attempt to import from stopped process instanceError in SDL Import. Several processes exporting this variableError in SDL Import. The specified process does not export this variableError in SDL Import. No process exports this variableError in SDL Import. More than one process exports this variableView Errors
Report Type: ViewError 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 environmentError in SDL View. Attempt to view from NULLError in SDL View. Attempt to view from stopped process instanceError in SDL View. More than one process instance reveals the variableError in SDL View. The specified process does not reveal the variable.Error in SDL View. No process instance reveals this variableTransition Length Error
Report Type: MaxTransLenMax 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.
Non Progress Loop Error
Report Type: LoopLoop 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:
- contains communication with the environment
- contains an assignment of the variable xProgress to 1 in user-defined C code
- includes a timer expiration (see Timer Progress)
- includes a spontaneous transition (see Spontaneous Transition Progress)
Assertion Errors
Report Type: AssertionAssertion 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: UserRuleUser-defined rule satisfiedA user-defined rule is evaluated to true.
Observer Errors
Report Type: ObserverObserver violationA process defined as an observer process has not been able to execute a transition.
MSC Verification Errors
Report Type: MSCVerification Report Type: MSCViolationMSC <MSC name> verifiedMSC sequence: <MSC name list>MSC <MSC name> violatedEvent: <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:
- The execution trace must include all events that exist in the MSC.
- The execution trace must not contain any observable event that is not part of the MSC.
- The sequence of observable events in the execution trace must be consistent with the partial ordering of the events that is defined by the MSC.
An event on the execution trace is considered to be "observable" if it is either
- an input or output of a signal that is sent between process instances that correspond to different MSC instances, or
- a create of a process instance that corresponds to a different MSC instance than the creating process instance, or
- a set, reset or input of a timer, depending on the value set by the command Define-Timer-Check-Level.
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:
- includes an observable event that is not part of the loaded MSC, or
- contains a sequence of observable events that is not consistent with the partial ordering of events defined by the MSC.
REF Errors
Report Type: RefErrorNo 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 memoryThe 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 NULLCalling UserFree with parameter NULLThe UserMalloc or UserFree functions has been called with NULL as a parameter which is illegal.
Calling UserFree without dynamically allocated memoryUserFree 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 |
![]() |
![]() |
![]() |
![]() |