Rule Attribute
A model program consists of a set of rule methods defined by types declared in a specified namespace. The namespace can be selected by the model program construct of Cord. The most common way to mark a rule method, and at the same time attach an action binding to it, is to use the Rule attribute.
The Rule attribute has the following syntactic equivalence to more basic attributes: [Rule] is equivalent to [Rule(Action = "label")], where label is computed from the name and arguments of the associated method, as explained below.
If no argument is given for the Rule attribute, the label is derived from the declaration of the associated method, depending on the kind of the method, as follows:
Method declaration:
static void A(T1 p1,...,Tn pn). Resulting action label: "A(p1,...,pn)"Method declaration:
static T A(T1 p1,...,Tn pn). Resulting action label: "A(p1,...,pn)/result"Method declaration:
void A(T1 p1,...,Tn pn). Resulting action label: "this.A(p1,...,pn)"Method declaration:
T A(T1 p1,...,Tn pn). Resulting action label: "this.A(p1,...,pn)/result"
For each explored state (which can be determined by a composition context) each method marked as a rule is explored. A rule is considered enabled if all its condition statements evaluate to true. Thus, if one of these statements is encountered when exploring a rule and its condition evaluates to false, exploration of the rule is aborted and no steps are produced.
If no failing condition is found, the rule is enabled, and one or more steps are produced. The state result of running the method is a successor state, which is added to a list of active states. Running a single rule can produce more than one exploration step due to control-flow branching or call-return.
If the resolved action is not atomic (that is, it is neither an event, nor explicitly marked as a call or a return) the following steps are added:
Upon entering of the rule method, a call step with input parameters, as bound by the method.
Upon return from the method, a return step with the result and output values of the method, if any.
If the resolved action is atomic, the corresponding step is generated upon return from the rule method, even for call steps
When an exploration step is created for a rule, it is named after the label specified in the Rule attribute associated with the rule.
The label, given as a string, is parsed and validated like an action invocation in a Cord behavior. The context signature for the validation is provided by the configuration used in the model program construct (only rules in this configuration are allowed). Local names can be used to refer to parameters or results of the associated method. The special name this is used to refer to the implicit instance parameter of an instance method. The special name result is used to refer to the return value of the method. All method parameters, including this and result, must be bound to an action parameter.
The parameters of a method rule are initialized with symbolic values, which may be bound by parameter domains. If, at some point while running an update rule, such a symbolic value is required to have a concrete value and no domain is assigned, an exploration error may result.
Examples
Example 1
In the following example, M1 creates a sequence of six atomic steps.
call Add(1); return Add, call Add(1); return Add, call Add(1); return Add
M2 creates a sequence of three atomic steps:
event Add(1); event Add(1); event Add(1)
class C
{
static int counter;
[Rule(Action = "Add(x)")]
static void Rule(int x)
{
Condition.IsTrue(x == 1 && counter < 3);
counter += x;
}
}
The following is the Cord configuration.
config CallReturn
{
action abstract static void ModelActions.Add(int x);
}
machine M1() : CallReturn
{
construct model program
}
config Event
{
action abstract event static void ModelActions.Add(int x);
}
machine M2() : Event
{
construct model program
}