The NModel Library
provides attributes and data types for writing
The library is most thoroughly documented in the online help that is included when you
To access the online help: Start Menu -> All programs -> NModel -> NModel documentation
The library is also documented in this
(45-page PDF document).
Model programs must use the library data types for collections and objects, not the usual C# and .NET data types.
Some of the attributes in the library are:
- [Action], a method which is an action (state transition) of a model program.
- [AcceptingStateCondition], a Boolean method, property, or field that is true in all
accepting states where runs of a model program are allowed to stop.
- [Domain("name")], applied to an action parameter, where
name identifies the set of values to be assigned to that parameter during
exploration of a model program. Used to finitize exploration.
- [StateFilter], a Boolean method, property, or field which must be true in all states that are included in the
finite state machine generated by exploration of a model program. Used to finitize exploration.
- [StateInvariant], a Boolean method, property, or field that must be true in every state. Failure of the state invariant in any state indicates a modeling error.
- [Feature], a class which is a feature, a collection of related state variables and actions that can optionally be included in a model program.
- [Requirement("text")], applied to any attributable element, can document the relation between a model program and a natural language document. A tool can monitor requirements coverage, or print the text when a
test fails or an invariant is violated.
Some of these attributes can take additional arguments not shown here, consult the documentation. The documentation describes more attributes as well.
Some of the data types in the library are:
- CompoundValue, a value type similar to a C#
struct, but may also implement tree structures. Base type for the following collection types.
- Set, an unordered collection of distinct values.
- Map, a finite mapping of keys to values.
- Sequence, an ordered collection of (possibly repeating) values.
- Bag, an unordered collection of possibly repeating values, also called a
- ValueArray, an immutable type that provides structural equality for arrays.
- LabeledInstance, base class for types with instance fields as state variables.
Collections in model programs must belong to the library collection types
etc., not the usual .NET collection types such as
The library collection types all behave as value types
. They use structural equality
and they are
, so you must code s = s.Add(x)
, not just
For object-oriented modeling, where instance fields are used as state variables, classes in model programs must be derived from the library class type
, not just