Machine
Named in honor of the concept of abstract state machine, the machine element in a Cord script expresses the behavior of the modeled system in various ways. Machines are defined in Cord scripts to assign a name to a behavior or set of behaviors. They are also the unit of exploration. Each machine is based on one or more configurations.
The machine can be referenced from other behaviors, which amounts to expanding its body in the reference context after parameter substitution. The notation for machines distinguishes a list of parameter declarations between parentheses from a result declaration, although technically no difference is made between inputs and outputs; all are equally substituted.
Allowable machine parameter types are the same as those for action parameters. Essentially, all value types and certain reference types may be used. See DeclaredAction for more details on valid types.
There is no way to pass parameters from the UI to a machine. Thus if a top-level explored machine has parameters, they will be kept symbolic.
No cyclic references between machines are allowed, or in other words, a system of machines cannot be recursive.
Every machine must be based on one or more configurations. Configurations provide the signature, or set of actions, that determine how machine behavior is interpreted. Moreover, all other aspects of the machine configuration are used when the machine is selected in an exploration project.
Syntax Definition
Machine ::= machine Ident ( [ ParameterList ] ) [/ VarDeclaration /*Ret Val Declaration*/ ] : ConfigList
[ where Switch {, Switch } ] { Behavior } .
ParameterList ::= [ out | ref ] VarDeclaration { , [out | ref ] VarDeclaration } .
VarDeclaration ::= Type Ident .
ConfigList ::= ConfigId { , ConfigId } . // List of ancestor configurations
ConfigId ::= Ident .
Switch ::= Ident = ( Literal | Ident | none ) .
Elements
- Ident
Machine name
- ParameterList
Optional parameter list.
- / VarDeclaration
Optional return value.
- ConfigList
List of configuration names.
- Behavior
Behavior expression for the machine.
Remarks
Behavior expressions constitute the way machines are defined. They offer many mechanisms for model construction, transformation, and composition. Behaviors obey a set of typing rules as follows:
Every Cord behavior has an offered signature and a context signature.
The offered signature for a behavior is the set of actions derived from the behavior expression.
The context signature of a behavior is the context signature of the machine in which the behavior is declared.
The context signature of a machine is the union of the configuration signatures for the configurations on which the machine is based.
A configuration signature is the set of actions declared within a configuration.
The principal typing rule is that the offered signature must be a sub-signature of the context one, where signature inclusion is based on action-set inclusion.
Behaviors are introduced from lower binding priorities to higher ones; that is, a behavior mentioned in a later subsection binds its operands more strongly than one in an earlier subsection. Binary operators, if not stated otherwise, are left-associative.
Example 1
The following code example defines a machine that is a scenario for slicing.
/// Defines a scenario for slicing.
/// When explored on its own, this machine
/// leaves all its parameters unexpanded.
machine DoubleAddScenario() : Main where ForExploration = true
{
//Omitting the parenthesis for an action invocation
//is equivalent to setting all its parameters to _ (unknown).
(Add(_); Add; ReadAndReset)*
}
Example 2
The following code example shows the use of machine parameters. The code is based on the static model, generated by the Spec Explorer Model Wizard.
machine DoubleAddScenario(int x) : Main where ForExploration = true
{
(Add(x); Add; ReadAndReset)*
}
machine SlicedAccumulatorModelProgram() : Main where ForExploration = true
{
DoubleAddScenario(1) | DoubleAddScenario(2) || AccumulatorModelProgram
}
In This Section
This section of the documentation describes all Cord behavior elements of machine definitions.
See Also
Reference
Concepts
Cord Syntax Definition
Slicing with Scenarios
Symbolic Exploration