![]() |
![]() |
![]() |
![]() |
![]() |
Using User-Defined Rules
In the Explorer, you may define a user-defined rule to be used during state space exploration to check for properties of the encountered system states. If a system state is found for which the user-defined rule is true, a report will be generated. Note that only one user-defined rule may be defined at a time.
Different Usages
There are three different situations in which a user-defined rule is useful:
- To verify properties of the SDL system.
- A user-defined rule describes properties of system states. By using an automatic state space exploration, it is thus possible to verify the existence of system states that satisfy the specified properties. If the state space is small enough to allow a complete exploration it is also possible to verify that the state space does not contain any system state with the specified property.
- To search for specific system states.
- A user-defined rule makes it possible to go to a specific system state in the state space without the need to use the navigating commands of the explorer monitor. By describing the desired state with a rule and using an automatic state space exploration, you can go directly to the report that satisfied the rule. In this case, the report action for the user-defined rule report should be set to Abort.
- To reduce the state space to be explored.
- For many SDL systems, the state space can be very large or even infinite, which makes it difficult to perform a state space exploration effectively. However, in many cases the state space contains large subspaces that for some reason are not interesting to explore. For instance, they may be equivalent to other parts of the state space except for the value of one particular variable. In such cases, a user-defined rule can be used to restrict the exploration by defining system states that are considered to be uninteresting. When such a state is encountered, the exploration is truncated and continued in another node.
Examples of Rules
An example of a rule that checks a system property is:
exists P:Proc | P->var=12;which is true for all system states where there exists a process of type "Proc" with a variable "var" that is equal to 12.
A simple example of a rule that searches for a system state is:
state(initiator:1)=disconnected;which is true for all system states where the process instance
"initiator:1" is in the state "disconnected".A more complex example of such a rule is:
state(Game:1)=Winning and sitype(signal(Game:1))=Probewhich is true for all system states where the state of the process instance "Game:1" is equal to "Winning" and the type of signal to be consumed by the same process instance is "Probe".
An example of a rule that reduces the state space is:
(Game:1->Count > 2) or (Game:1->Count < -2)which is true for all system states where the absolute value of the variable "Count" in the process instance "Game:1" is greater than 2.
For a full description of the features and syntax of user-defined rules, see User-Defined Rules.
Managing User-Defined Rules
To define the user-defined rule, select Define Rule from the Commands menu, or enter the command Define-Rule, followed by the definition of the rule.
To clear the user-defined rule, enter the command Clear-Rule.
To print the definition of the current user-defined rule, enter the command Print-Rule.
To evaluate the user-defined rule in the current system state, i.e. to check whether the rule is satisfied, enter the command Evaluate-Rule.
http://www.ibm.com/rational |
![]() |
![]() |
![]() |
![]() |