State Attributes
The state space of a model program is composed of all memory reachable from the annotated rule methods, either directly or indirectly by calling other methods. The state space may contain objects that are dynamically created during rule execution or passed in as parameters to rules. For more information, see Rule Attribute.
Note that action-related constraints should never be used in methods marked with a state attribute. Use of action-related constraints in such methods will cause the method to abort without returning a value.
Accepting State Conditions
States can be characterized as accepting states if they represent legal termination points of the runs of the modeled system. An accepting state is a state where a test can successfully end, leaving the system in a stable state. The predicates that determine whether a state is an accepting state are annotated with the AcceptingStateCondition attribute. The target of this attribute can be a method without parameters, or a property that returns a Boolean.
If the target of an AcceptingStateCondition attribute is a method, it can be static or instance-based. In the latter case, the state is accepting if the condition holds for all reachable instances of the class.
If no accepting state condition is specified, every state is considered accepting.
Example
namespace Microsoft.MyModel
{
class Client
{
Sequence<object> mailbox;
[AcceptingStateCondition]
static bool AllMailDelivered()
{
return mailbox.Count == 0;
}
}
}
States of this model program are accepting only if the mailboxes of all clients that have ever been created are empty.
State Invariants
It is possible to define Boolean conditions called state invariants that must hold in every state. The failure of any state invariant indicates a modeling error.
The target of this attribute can be a method without parameters, a property, or a field that returns a Boolean. The StateInvariant attribute indicates that the annotated method, property, or field must hold in every state.
If the target of a StateInvariant attribute is a method, it can be static or instance-based. In the latter case, the state invariant is said to hold if the return value is true for all reachable instances of the type. The return type must be System.Boolean.
State Filters
A state filter is a Boolean condition causing states to be excluded from exploration. The StateFilter attribute indicates that its target method, property, or field is a state filter. The target of this attribute can be a method without parameters, a property, or a field that returns a Boolean. A value of TRUE indicates that the state is included; FALSE indicates exclusion from exploration.
If the target of a StateFilter attribute is a method, it can be static or instance-based. In the latter case, the state invariant is said to hold if the return value is true for all reachable instances of the type. The return type must be System.Boolean.
See Also
Reference
AcceptingStateConditionAttribute
StateInvariantAttribute
StateFilterAttribute