Actions

In general, an action describes an interaction with the system under test (SUT) as seen from the test system's perspective. Spec Explorer recognizes three kinds of atomic actions that are discrete and indivisible: call actions, return actions, and events. 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. Events represent autonomous messages coming from the SUT.

Action Declarations

All actions used in a machine must be declared in a Cord configuration or configurations upon which the machine is based. Such declarations assume that the target SUT assemblies, or the assemblies of adapters that wrap access to the SUT, provide the .NET code that corresponds to each action. Once declared, actions can then be used in various ways as part of a model. There are two kinds of action declarations:

1. A call-return action declaration introduces a pair of atomic actions: a call and a return. They represent synchronous blocking operations on the system being modeled. In practice this means that the system will perform the operation before returning control to the caller. It can also mean that once the caller invokes the action, it will not perform other operations or expect any response until the operation is completed. Spec Explorer ensures that after an atomic call action, only matching atomic return actions are enabled. The target of a call-return pair is implemented by a single method in the SUT or adapter. Tests generated from Spec Explorer models invoke each method and block while waiting for the matching return. This kind of action declaration is the default.

2. An event action declaration introduces a single atomic action that represents a response coming from the system being modeled. The response can be autonomous, or correspond to a previously received request. Events are used when the system can issue asynchronous responses; that is, the system can send messages to the environment that are not immediate responses to a received stimulus. Based on the .NET event facility, tests generated from Spec Explorer models subscribe to these events and add them to the event queue as they arrive. Events from this queue are consumed when the test reaches a point where one or more events are expected.

These two declaration types are distinguished by using the event keyword to declare an event action.

// Cord code
config AConfig
{
    // The following is a call-return action declaration:
    action int Implementation.AnAction(string a);

    // The following is an event action declaration:
    action event void Implementation.AnEventAction(string a);
}

All action declarations require a declaring type. The declaring type is the type name appearing before the action name in the declarations shown in the preceding code example, separated by a dot. The declaring type is used to resolve the action name to an actual member of the declaring type in the system implementation or test adapter. Therefore, the declaring type of an action is never a type in the model, but rather a type in the system being tested.

If the declaration introduces a call-return action, it must match a method in the declaring type. If it introduces an event action, it must match an event variable in the declaring type. If the action is declared to be static, the corresponding member (method or event variable) must be static as well. Conversely, nonstatic actions must correspond to instance (nonstatic) members. The declaring type must reside in an assembly referenced by the project containing the Cord script with the configuration. However, if the model is being authored without an implementation of the system being available, actions are marked abstract (for example, action abstract); this means that the declaring type or the specific member does not necessarily exist.

The Cord modeling language supports a short way to declare as actions many members of an existing type (class, struct, or interface), which is done with the action all clause. If no modifier is specified (just a type name), actions are declared for all methods and events in the type. If a modifier is specified (for example, action all public), actions are declared only for the members with the corresponding access.

Using Actions

Actions appear in Spec Explorer in many contexts:

1. In Cord the use of an action in a behavioral expression is called an action invocation (for example, 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 configuration. Cord allows for polymorphic overloading of action declarations; Spec Explorer will choose the correct action declaration accordingly. Actions are used to validate action invocations appearing explicitly in Cord behaviors. If an action invocation occurs in the behavior (body) or a machine, Spec Explorer will validate that the action with the correct parameter types is declared in the configuration or configurations on which the machine is based. If it is not declared, a validation error will result. Here is a code example showing action invocations.

   // Cord code
   
   machine AMachine() : AConfig, AnotherConfig
   {
     // The following action invocations must match an action declaration in AConfig or AnotherConfig.
     // The first two can be either call-return or event actions.
     // The third one must be a call-return (only the call is being invoked).
     AnAction("hello"); AnEventAction("goodbye"); call AnAction("hello");
   }
   

   Note

   Because action invocations belong solely to the model, they do not directly call the SUT implementation. The implementation becomes available only at test execution time. By that time the model is no longer involved; it was used beforehand to generate the tests. It is important to keep in mind that the model is different from the implementation.

2. Action invocations are also used to annotate rules, which are the other major part of modeling. The ModelProgramConstruct is used in Cord behaviors to obtain a model program from .NET rule method declarations. Rule methods are identified (within the optional namespace or class provided to the construct) because they are annotated with the Rule attribute in a model program. The optional argument to the Rule attribute is an action invocation. That argument must match an action declaration in the mandatory configuration provided as part of the construct. If the argument to the Rule attribute is omitted, Spec Explorer will infer that the invocation is exactly the same as the method header (same name and parameter list) and still validated against action declarations in the configuration. If the configuration used to construct the model program does not contain an action declaration matching the invocation (this may be caused by the lack of a declaration, or an explicit exclusion of the declaration), a validation error will result.

   // C# code
   namespace Model
   {
     // Since the action is not static, a type binding must be established
     // between the model type and a type in the implementation.
     [TypeBinding("ImplementationNamespace.ImplementationClass")]
     public class RuleContainer
     {
       [Rule(Action = "this.AnAction(s)/r)")]
       public void ARule(string s, int r)
       {
         Condition.IsTrue(r == s.Length);
       }
     }
   }
   
   // Cord code
   machine AMachine() : Aconfig
   {
     // Configuration AnotherConfig must have a declaration for action int AnAction(string).
     // The declaring type of the action must be ImplementationNamespace.ImplementationClass   
     // (according to the type binding).
     Construct model program from AnotherConfig
       where scope = "Model.RuleContainer"
   }
   

3. Actions are used to expand universal behaviors. There are two kinds of universal behaviors that can be used in the body of a machine in Cord: any single step, and any sequence of steps. The notations for the universal behaviors are an underscore (_) and an ellipsis (…), respectively (see UniversalBehavior). Universal behaviors are expanded to all (atomic) actions declared in the configuration (or configurations) upon which the machine where they appear is based. Negated invocations are prefixed with an exclamation mark (!). They are expanded to all (atomic) actions in the corresponding configuration, except the action being negated, which must also be declared in the configuration to avoid a validation error. The following code example shows actions expanding universal behaviors.

   // Cord Code
   config AConfig
   {
     action int Implementation.AnAction(string a);
     action event void Implementation.AnEventAction(string a);
   }
   
   machine AMachine() : AConfig
   {
     // The following behavior is equivalent to: 
     // call AnAction | return AnAction | AnEventAction
     _
   }
   
   machine AnotherMachine() : AConfig
   {
     // The following behavior is equivalent to: 
     //  (call AnAction | return AnAction | AnEventAction)*
     ... 
   }
   
   machine YetAnotherMachine() : AConfig
   {
     // The following behavior is equivalent to:
     // call AnAction | AnEventAction
     !return AnAction
   }
   

Non-Determinism

Non-determinism occurs when the system under test (SUT) may have more than one legitimate response. The model can predict all acceptable responses but cannot predict which response will be observed at a particular time. In Spec Explorer this means that either more than one event can happen, or more than one atomic return action may follow an atomic call action.

A nonatomic action always implicitly consists of a call action and companion return action. If the model allows multiple returns from the same call action, then the model is non-deterministic. In Spec Explorer, instances of actions are steps that appear as transition labels in the exploration graph. Thus, when the call step has the possibility of one of several return steps, the exploration result is also non-deterministic. Spec Explorer offers the choice to slice away non-determinism in test cases, but it is an additional strength of Spec Explorer to directly support non-deterministic test cases. A single Rule can be used to model non-deterministic steps by using the Choice class. Here is a model program illustrating this use.

public enum Platform
{
    Windows7,
    WindowsVista,
    WindowsXP
}
/// <summary>
/// An example model program.
/// </summary>
public static class MyModelProgram
{
    static Platform currentPlatform;
    [Rule(Action = "GetPlatform(out platform)")]
    public static void GetPlatformRule(out Platform platform)
    {
        platform = Choice.Some<Platform>();
        currentPlatform = platform;
    }
}

This rule will create the following behavior (expressed in Cord).

call GetPlatform(out_); ( return GetPlatform(out Windows7) 
    | return GetPlatform(out WindowsVista)
    | return GetPlatform(out WindowsXP) )

The following model program illustrates the longer, traditional way of doing this in Spec Explorer.

public enum Platform
{
    Windows7,
    WindowsVista,
    WindowsXP
}
/// <summary>
/// An example model program.
/// </summary>
public static class MyModelProgram
{
    static Platform currentPlatform;
 
    [Rule(Action = "call GetPlatform(out _)")]
    public static void GetPlatformCall()
    {
    }

    [Rule(Action = "return GetPlatform(out platform)")]
    public static void GetPlatformReturn(Platform platform)
    {
        currentPlatform = platform;
    }
}

See Also

Reference

DeclaredAction
Invocation
UniversalBehavior
ModelProgramConstruct
SwitchClause

Concepts

Spec Explorer Concepts
Behavior Signatures
Rule Attribute