Configurations
Configurations are used to control exploration and test generation. One of their purposes is to define the actions on which the model is based. This set of actions represents steps in a model trace or in the execution of an implementation. Actions are generally divided into controlled (stimuli) and observed (response), where responses are represented by events. Events are not used in the counter model generated from the template.
A configuration can also include a set of switches and parameters to control exploration and testing.
Action declarations use a notation similar to C#, prefixed with the keyword action:
config Main
{
action abstract static void Implementation.Add(int x);
action abstract static int Implementation.ReadAndReset();
}
Each declaration refers to a method or event in the implementation. However, do not confuse actions, which represent entities of the implementation, with methods in the model. Actions and rule methods can have the same short name, but they have different fully qualified names.
If an action is declared as abstract, it does not have to correspond to implementation methods or events. However, if a method or event with the same name and parameters exists in the implementation, it is used.
When validating a Cord script, Spec Explorer attempts to resolve action declarations to implementation methods or events, unless they are marked as abstract. Abstract actions do not need to correspond to implementation elements. However, methods or events with the same name need to exist in an implementation or adapter to run generated test cases.
To declare an event action, use the keyword event after the keyword action (or after the keyword abstract, if present), as shown in the following examples.
action event static void Implementation.Event1();
action abstract event static void Implementation.Event2();
Actions can be bulk imported from an implementation type with the following statement: action all ImplementationTypeName;. In this code, ImplementationTypename is not a keyword, but the name of a data type, whose methods and events are used as actions. This is particularly useful if an implementation is represented by an interface or adapter that contains exactly the set of actions relevant for testing.
Note
The static model template generated by the Spec Explorer Model Wizard does not contain events.