Naming Conventions

When you use the Model Wizard to create a new Spec Explorer solution, machines and files are created as an example of how your solution might look. They have generic names, such as ModelProgram, TestSuite, Config.cord, and TestSuite.cs. See Creating the Solution for more details on the Model Wizard.

When you create your own machines and files, give them descriptive names for each project.

Rule method names in a model program do not need to match the action name, although using the same names when there is a one-to-one correspondence is usually advised, as it leverages the default usage of the Rule attribute.

If an action label is provided as an argument to the Rule attribute, it must follow the syntax of action invocations. All rule method parameters must appear in the action label, including the reserved names this (for nonstatic methods) and result (for nonvoid methods). If this is not the case, a validation error will result.

See Also

Concepts

Using Spec Explorer
Rule Attribute
Creating the Solution