Actions, Step and Rules

  • Article

These are key concepts in Spec Explorer. Unfortunately sometimes they are used almost interchangeably. For now, let's clear up what they are and how they differ. To be fair, our documentation does a good job of using the correct terms but even so it pays to keep in mind their particular meaning.

Actions

In the most general notion, an action describes an interaction with the System Under Test (SUT) as seen from the tester's (or test system's) perspective. Spec Explorer recognizes three kinds of atomic actions that are discrete and indivisible: events, call actions, and return actions. Events represent autonomous messages coming from the SUT. A call action represents a stimulus from the test system to the SUT (as originally decided in the model). A return action must always follow after a call action without any intervening actions. The return actions capture the response (if any) from the SUT.

For further reference see Actions in the on-line documentation.

Action Declarations

Actions are declared in Cord configs using definitions that are like C# signatures preceded by the keyword "action". Cord expects the target SUT assemblies, or the adapter assemblies that wrap access to the SUT, to provide the .Net code that corresponds to each action. Put another way, the code to implement actions ultimately belongs not to the model but rather to the implementation to be invoked at test run time only.

An action declaration in Cord is always one of two kinds: a synchronous action declaration, which is the default, or an explicitly stated event action declaration. A synchronous action declaration actually forms the indivisible pair of an atomic call action followed by the corresponding atomic return action. The target of a call/return pair is implemented by a single method in the SUT, or the adapter to the SUT. Tests generated from Spec Explorer models invoke these methods on the SUT, and block waiting for them to return.

Event action declarations describe a single atomic action that indicates the SUT has sent a message on its own in keeping with the .Net event model. Events are implemented as standard C# events in the SUT (or adapter). Tests generated from Spec Explorer models subscribe to these events and add them to a queue as they arrive. Events from this queue are consumed when the test reaches a point where one or more events are expected.

Action Invocations

In Cord the use of an action in a behavioral (regular) expression is called an invocation, e.g. Add(1,2)/3.  The arguments of an invocation can be variables or literals. Action invocation arguments, if specified, must always match in type and position with the signature provided by the action declaration in the applicable Cord config. Cord allows for polymorphic overloading of action declarations and Spec Explorer will chose the correct action declaration accordingly.

Note: action invocations do not directly call the implementation because they belong to the modeling. The implementation only becomes available at test execution time. Action invocations are also used to annotate rules, which are the other major part of modeling.

For further reference see Invocation in the on-line documentation.

Steps

Steps are the transitions in the graph. Step labels are action invocations that appear as transition (edge) labels in the exploration result graph.

At test run time, these step labels are translated into either method calls to the SUT (or adapter) that implement the call/return pair, or expected events. For call/return pairs, the generated test code will call the implementation (or adapter) method (call action step). The test code then will note the response with the actual out and result values given by the SUT (return action step). For events coming from the SUT (or adapter), all parameters will be considered as outputs. The actual values found at run time (for out parameters, results and event parameters) will be compared to the expected values from the model ("the oracle"). Only if these values meet all corresponding conditions will the test case succeed.

Like all behavioral modeling, Spec Explorer is ultimately interested in what can actually be seen in terms of inputs and outputs to the System Under Test (SUT), i.e. the actions. Everything else in Spec Explorer exists just to determine the legal sequence of steps (behavior) that a compliant SUT will be expected to follow in a test case. Even Spec Explorer's advanced notion of "state" is used only at modeling (exploration) time by a rule (see below) to determine if a particular step label would be permitted at that point in the sequence, but state does not partake in the actual test execution. Only step labels interpreted as invocations to the SUT (or adapter) and events are relevant to testing, as just described above.

Rules

Rules determine what steps can be produced leading from the current state in the model program. All rules are tried out by exploration from each state.

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

Since rules exist to specify what steps the model program allows from a given state, the true 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 quite possible for a single rule to yield multiple instances of step labels for a given state. Of course 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, but each step label will have a different combination of parameter values.

When a rule method is explored in order 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 (as discussed below). A step label that cannot be produced by a rule due to violating a constraint in a Condition class method (e.g., 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:

  1. The name of the action invocation annotating a rule does not need to match the name of the rule method. It must however match the name of an action declaration in the Cord config that the model program is constructed from (e.g. "construct model from MyConfig").

  2. Remember that action invocation arguments must always match in position and type compatibility with the corresponding action declaration signature in Cord.

  3. 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 what it wants when the action invocation parameter has that value without having to explicitly test for it.

  4. 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). Note that the apparent return value of a C# rule method simply maps to the "result" output parameter.

  5. All parameters of a rule method must appear in the action invocation annotating it. If one or more of the rule parameters do not appear in the corresponding action invocation, a validation error will result. This includes the special parameters "this" (for instance-based rules) and "result" (for non-void rules). For Example,

    In Cord:

    action abstract Sum(int x);

     

    In Model Program:

    static int stateTotal;

             [Rule(Action = "this.Sum(op) / result")]

       int AddtoTotal(int op) {

       return stateTotal += op;}

  6. If the Action keyword is not specified in the rule annotation (e.g. "[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".

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 position.

An Example

  Action Declaration in Cord:

action abstract static bool Login(string user,int securityLevel);  

Rules in the Model Program

  1. The rule for a power user at security level 1 to login successfully (if unknown user, the rule itself fails, i.e. the action label will not be produced).
  2. The rule for a power user at security level 1 to login unsuccessfully (if unknown user, the rule fails).
  3. The rule for a normal user at any other security level allows login only if the user is already known and legal security levels also must be a positive integer value.

public static class MyModel

{

    static bool loggedIn; // State variable for Login status

  static string userName; // current user id with prefix

  static int securityRing; // current security level

  static Set<string> PowerUsers; // Level 1 people (initialized elsewhere)

  static Set<string> NormalUsers;// Normal users (initialized elsewhere)

 

// Rule for successful login at security level 1

[Rule(Action="Login(userId, 1) / true")]    

static void LoginLevel1Worked(string userId)

{

  Condition.IsTrue(PowerUsers.Contains(userId)); //Unknown-step fails

  userName="P."+userId; // Step possible; add Power User Prefix

  securityRing=1; // Assumed due to Action label

  loggedIn=true; // Already know this login is good

                        // result==true assumed due to Action label

}

 

// Rule for failed login at security Level 1

[Rule(Action="Login(string userId, 1)/ false")]

static void LoginLevel2Failed(string userId)

{

  Condition.IsFalse(PowerUsers.Contains(userId)); //Unknown-step fails

  loggedIn=false; // Still in rule; so assumed due to Action label

  securityRing=0; // Logged out default state values

  userName="";

                 // result==false assumed due to Action label

}

 

// Rule for login attempt at any level except security level 1

[Rule(Action="Login(userId, securityCode) / result")]

static bool LoginNotLevel1(string userId, int securityCode)

{

  Condition.IsTrue(securityCode > 1); // Rule only for legal non-level 1

  if (NormalUsers.Contains(userId)) // Step OK; check if user known

  {

  userName="U."+userId; // User known, so login succeeds

  securityRing=securityCode;

  loggedIn=true;

  }

  else // User unknown, so login fails

{    

  loggedIn=false;

  securityRing=0;

  userName="";

  }

  return loggedIn; // result == returned value

}

}

 

Rob DuWors