IBM
Contents Index Previous Next



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:

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))=Probe

which 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
Contents Index Previous Next