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.

ClassDescription
AcceptingModeAttributeDefines a set of mode tags that identifies an accepting mode set of the model program.
AcceptingStateConditionAttributeIndicates that a parameter-free method or Boolean property is an accepting state condition.
AxiomaticMethodAttributeThis API supports the exploration infrastructure and is not intended to be used directly from your code.
ChoiceModels non-determinism, and allows a rule to generate more than one step from a state.
CombinationProvides methods for controlling how Spec Explorer produces value or parameter combinations.
CompoundValueDefines a value type that is suitable for use as an action parameter.
ConditionProvides 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.
DomainAttributeSpecifies a domain for a rule method parameter.
ErrorModeAttributeDefines a set of mode tags that identifies an error mode set of the model program.
FeatureAttributeIndicates that a class belongs to a named feature.
InitialModeAttributeDefines a set of mode tags that is assigned to the initial state of the model program.
LogicalOperationsProvides 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.
MapContains a map, which is an unordered collection mapping keys to elements. Map values are immutable. See MapContainer for a mutable version of Map.
MapContainerContains 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.
ModelingAssemblyAttributeIndicates 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.
ProbabilityIndicates that Spec Explorer should make a stochastic choice during model exploration.
ProbeAttributeMarks 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.
RequirementAllows a requirement to be marked as captured at a point in a model program.
RuleAttributeIndicates that a method, constructor, or property is a rule for a model program and associates the rule with an action invocation.
SequenceSpecifies a Sequence, an ordered collection of elements similar to a list but immutable. See SequenceContainer for a mutable version of sequences.
SequenceContainerContains a Sequence. A SequenceContainer wraps a Sequence, providing a mutable version of Sequence.
SequenceGroupA Sequence Group for given key.
SetContains a set, an unordered collection of elements without repetitions. Set values are immutable. See SetContainer for a mutable version of sets.
SetContainerContains a Set. A SetContainer wraps a set value, to provide a mutable version of Set. See Set for more details on the Set type.
SetGroupA Set Group of Key K.
StateFilterAttributeIndicates that parameterless method or property is a state filter.
StateInvariantAttributeIndicates that a Boolean property, field, or parameter-free method is a state invariant.
TypeBindingAttributeBinds a model type to a target type. Target types are those used in an implementation or adapter.
UntrackedAttribute 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.

EnumerationDescription
CombinationStrategySpecifies a strategy for generating parameter combinations.
ParameterExpansionPointIndicates when during exploration Spec Explorer performs parameter expansion for a rule.



Community Additions

ADD
Show: