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.