Rules

Article
05/15/2013

In Spec Explorer, rules are represented by methods in the model program that have been marked with the Rule Attribute. The Rule attribute has an optional Action argument that specifies an action invocation associated with the rule.

Rules determine what steps can be taken from the current state in the model program. All rules are tried out by exploration from each state. Because rules exist to specify what steps the model program allows from a given state, the output of a rule is zero or more step labels representing possible next actions from that state. Because of advanced features in Spec Explorer, such as domains and parameter generation, it is quite possible for a single rule to yield multiple instances of step labels for a given state. A particular rule method always produces the same kind of step label, in keeping with the Cord action declaration that matches the action invocation of its Rule attribute; however, each step label will have a different combination of parameter values.

When a rule method is explored to generate step labels, the action invocation contained in its Rule attribute is used to map the exploration-supplied input values to the rule method, and to map back out/result values after the rule method has executed. A step label that cannot be produced by a rule due to violating a constraint in a Condition class method (for example, Condition.IsTrue) is simply discarded and will not appear in the exploration graph.

The action invocation in the Rule attribute is used to establish the correspondence between the Cord action declaration signature and the potentially different rule method signature, in a way that is quite unique to Spec Explorer. Here are details.

If the Action keyword is not specified in the Rule annotation (for example, the attribute is simply [Rule]), Spec Explorer will automatically construct an invocation based on the rule method signature. The method name of the rule will be used as the action name (which must then match an action declaration in the corresponding Cord config), and the method's parameter names will be used as the action invocation parameters. For example, if the method signature is int MyMethod(string name, float age), the constructed action invocation will be Action ="this.MyMethod(name,age)/result".
The name of the action invocation annotating a rule does not need to match the name of the rule method. It must match the name of an action declaration in the Cord config that the model program is constructed from in Cord, using the ModelProgramConstruct. For example, construct model program from MyActionsConfig.
Action invocation arguments must always match in position and type with the corresponding action declaration signature in Cord.
If an action invocation argument is a literal value (for example, a number) it is not mapped at all to the rule method parameters. The rule method may simply assume anything when the action invocation parameter has that value, without having to explicitly test for it.
If an action invocation argument is a variable rather than a literal value, it is mapped by name only, not by position, to the corresponding rule method parameter. If no such mapping is possible, a validation error occurs. The type of the rule method parameter must agree with the corresponding type in the Cord definition. This includes the special names that can be used as action invocation arguments: this represents the receiver of an instance-based rule method and result represents the return value of a non-void rule method. The apparent return value of a C# rule method simply maps to a result output parameter. See Rule Attribute for more details.
All parameters of a rule method must appear in the action invocation annotating it. If one or more of the rule method parameters do not appear in the corresponding action invocation, a validation error will result. This applies to the special parameters this for instance-based rule methods and result for non-void rule methods.

Here is a code example showing an action declaration in Cord and its corresponding action invocation in the C# model program.

// In Cord
action abstract Sum(int x);

// In the C# Model Program
static int stateTotal;

[Rule(Action = "this.Sum(op) / result")]
int AddtoTotal(int op)
{
    return stateTotal += op;
}

In summary, the action invocation in the Rule attribute must match in type and position (but not necessarily in name) the signature of the Cord action declaration. Rule method parameters must match the action invocation in the Rule attribute in name and type (but not necessarily in position).

Rules

See Also

Reference

Concepts

Additional resources