Excluding Actions from a Configuration

Sometimes, a modeler may have constructed a full model of an implementation for testing, and then wishes to focus on specific rules in the exploration and not explore other rules. For example, an implementation of a bank account manager may have rules for generating a monthly statement and displaying all accounts for a given customer, but the modeler wishes to explore other aspects of the implementation.

Here is an example of a bank account management program that has 3 classes: authenticateCustomer, performTransaction, and displayAccount. The displayAccount class has three methods: listAccounts, displayCurrentBalance, and generateStatement.

A configuration that contains all rules in the implementation might look like:

config FullConfig
{
  action all authenticateCustomer;
  action all performTransaction;
  action all displayAccount;
}

The simplest way to exclude actions is to construct a scenario that does not include the undesired actions. This scenario can then be composed with a model program to exclude the corresponding rule methods, as follows:

machine displayCurrentBalanceOnly() : FullConfig
{
    (!call generateStatement || !call listAccounts)* || construct model program from FullConfig
}

Note

In the Spec Explorer static model template, each desired action is specifically declared in the Cord configuration file.

Excluding an action from a Cord configuration (for example, by using the action exclude keyword) does not result in excluding rules from model programs. Such an excluded action cannot be used in the action label of a rule (either explicitly in the Action parameter to the Rule attribute or implicitly by declaring a method with the same name as the action) in the associated model program. The Cord ModelProgramConstruct generates a validation error if the actions declared in the configuration do not include all actions used in Rule attributes in the model program. For more information about defining action labels, see Model Programs, Actions, Rules, and Rule Attribute.

The order of action declarations in a configuration does not matter. Explicitly excluding an action always takes precedence over declaring it in a configuration. Even if an action is declared explicitly--or implicitly using action all--an explicit action exclude declaration will keep the excluded action out of the configuration. This is the case regardless of the order of the declarations. For example, in the following Cord code, despite that an action all declaration occurs after an action exclude, the explicit exclude will take precedence and ReadAndReset() would be excluded from all actions.

config AConfiguration
{
    action exclude static int Implementation.ReadAndReset();
    action all Implementation;
}

See Also

Concepts

Configurations
Actions