![]() |
![]() |
![]() |
![]() |
![]() |
User-Defined Rules
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.
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.
Predicates
The following types of predicates exist:
- Quantifiers over process instances and signals in input ports.
- Boolean operator predicates such as "and", "not" and "or".
- Relational operator predicates such as "=" and ">".
Parenthesis are allowed to group predicates.
Quantifiers
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>).
Boolean Operator Predicates
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.
Relational Operator Predicates
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.
Expressions
The expressions that are possible to use in relational operator predicates are of the following categories:
- Process functions: Extract values from process instances.
- Signal functions: Extract values from signals.
- Global functions: Examine global aspects of the system state.
- SDL literals: Conventional SDL constant values.
Process Functions
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.
Signal Functions
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.
Global Functions
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.
SDL Literals
<STATE ID><PROCESS TYPE><PROCESS INSTANCE>A process instance identifier of the format <PROCESS TYPE>:<INSTANCE NO>, e.g. Initiator:1.
<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>truefalse<REAL LITERAL><CHARACTER LITERAL><CHARSTRING LITERAL>
http://www.ibm.com/rational |
![]() |
![]() |
![]() |
![]() |