LetBehavior
This construct introduces a set of local variables with an optional associated constraint. The scope of the declared variables is the given behavior. Variables in behaviors are declarative and not imperative, that is, constraints can be expressed over them, but they cannot be updated (assignment is not allowed).
Syntax Definition
LetBehavior ::= let LocalVarList [ where ConstraintList ] in Behavior .
LocalVarList ::= VarDeclaration { , VarDeclaration } .
ConstraintList ::= ( Ident in Domain { , Ident in Domain } ) | EmbeddedCode .
Remarks
The offered signature of the declaration behavior is that of its enclosed behavior.
Spec Explorer performs parameter expansion as part of model exploration. However, Spec Explorer can expand parameters for a behavior only when the behavior is composed with a model program defined in Cord. For more information on parameter expansion, see Parameter Generation.
The following example shows a declaration.
using Microsoft.Test;
config AxBx
{
action abstract static void MyAbstractActions.A(int x);
action abstract static void MyAbstractActions.B(int x);
}
machine M1() : AxBx { let int x in A(x); B(x) }
machine M2() : AxBx { let int x in (A(x); B(x)) }
machine M3() : AxBx { let int x, int y where (. x > y .) in A(x); B(y) }
machine M4() : AxBx { let int x in A(x)* }
machine M5() : AxBx { (let int x where (. x > 0 .) in A(x))* }
Machine M1 produces the set of traces consisting of A(x) followed by B(x), where x is arbitrary but unique in each trace.
Machine M1 and M2 are semantically the same.
Machine M3 produces the set of traces consisting of A(x) followed by B(y) where x is always greater than y.
Machine M4 produces the set of traces with consecutive A(x), where x represents a single value in each trace.
Machine M5 produces the set of traces with A(x1),A(x2),A(x3), . . . with each xi greater than zero.