Microsoft.Modeling Namespace
The Microsoft.Modeling namespace contains classes that are used to develop Spec Explorer models.
There are three major categories of types in this namespace.
The attribute classes, which declare rule methods, accepting state conditions, type bindings, and so on. Spec Explorer uses these attributes to find modeling elements. These include the RuleAttribute, AcceptingStateConditionAttribute, and TypeBindingAttribute attributes.
The value types defined by Spec Explorer, which include collections and compound values. These value types support various modeling features in Spec Explorer, such as state identification and parameter expansion. To benefit from these features, use the Spec Explorer defined collections instead of standard .Net Framework collections, both for action parameters and for state variables. These include the CompoundValue, Map, and MapContainer classes.
Classes that contain helper methods to control various aspects of model behavior, such as parameter expansion, condition checking, requirement capture, and so on. These include the Combination, Condition, and Requirement classes.
Classes
| Class | Description |
|---|---|
| AcceptingModeAttribute | Defines a set of mode tags that identifies an accepting mode set of the model program. |
| AcceptingStateConditionAttribute | Indicates that a parameter-free method or Boolean property is an accepting state condition. |
| AxiomaticMethodAttribute | This API supports the exploration infrastructure and is not intended to be used directly from your code. |
| Choice | Models non-determinism, and allows a rule to generate more than one step from a state. |
| Combination | Provides methods for controlling how Spec Explorer produces value or parameter combinations. |
| CompoundValue | Defines a value type that is suitable for use as an action parameter. |
| Condition | Provides conditions that can control the exploration of a rule, such as whether the rule is enabled and which parameter values can be generated for the rule. |
| DomainAttribute | Specifies a domain for a rule method parameter. |
| ErrorModeAttribute | Defines a set of mode tags that identifies an error mode set of the model program. |
| FeatureAttribute | Indicates that a class belongs to a named feature. |
| InitialModeAttribute | Defines a set of mode tags that is assigned to the initial state of the model program. |
| LogicalOperations | Provides methods that perform common logic operations and that have a control flow that does not depend on the operators. These methods do not create a branch in the execution flow and are suitable for building up constraints in enabling conditions and in parameter constraints. |
| Map | Contains a map, which is an unordered collection mapping keys to elements. Map values are immutable. See MapContainer for a mutable version of Map. |
| MapContainer | Contains a map. A MapContainer wraps a map value, to provide a mutable version of Map. The Map type itself is immutable. See Map for more details on the Map type. |
| ModelingAssemblyAttribute | Indicates that an assembly contains modeling constructs and should be scanned for them. By default, only the main project assembly is scanned for modeling constructs. Apply this attribute to modeling assemblies that are intended to be referenced. |
| Probability | Indicates that Spec Explorer should make a stochastic choice during model exploration. |
| ProbeAttribute | Marks the target method or property as a state probe. State probes provide state information that can be accessed when examining exploration results for the model. |
| Requirement | Allows a requirement to be marked as captured at a point in a model program. |
| RuleAttribute | Indicates that a method, constructor, or property is a rule for a model program and associates the rule with an action invocation. |
| Sequence | Specifies a Sequence, an ordered collection of elements similar to a list but immutable. See SequenceContainer for a mutable version of sequences. |
| SequenceContainer | Contains a Sequence. A SequenceContainer wraps a Sequence, providing a mutable version of Sequence. |
| SequenceGroup | A Sequence Group for given key. |
| Set | Contains a set, an unordered collection of elements without repetitions. Set values are immutable. See SetContainer for a mutable version of sets. |
| SetContainer | Contains a Set. A SetContainer wraps a set value, to provide a mutable version of Set. See Set for more details on the Set type. |
| SetGroup | A Set Group of Key K. |
| StateFilterAttribute | Indicates that parameterless method or property is a state filter. |
| StateInvariantAttribute | Indicates that a Boolean property, field, or parameter-free method is a state invariant. |
| TypeBindingAttribute | Binds a model type to a target type. Target types are those used in an implementation or adapter. |
| Untracked | Attribute indicates the value stored in this field should be excluded from model state. Value in an untracked field is stored in a global place so retrieving the field value from different states will result in same value, and altering field value will reflect to all states. Untracked fields won't affect state identification. Obsolete. |
Enumerations
| Enumeration | Description |
|---|---|
| CombinationStrategy | Specifies a strategy for generating parameter combinations. |
| ParameterExpansionPoint | Indicates when during exploration Spec Explorer performs parameter expansion for a rule. |