BindBehavior
This behavior enables attaching constraints to parameters of actions occurring in its scope. The invocation list provides action patterns that are matched against each action produced by the behavior.
Syntax Definition
BindBehavior ::= bind InvocationList in Behavior .
InvocationList ::= Invocation { , Invocation } .
Invocation ::= [ AtomicQualifier ] Target [ ( ArgList ) ] [ / Expression ] .
AtomicQualifier ::= call | return | event .
Target := new [ Expression . ] Type | Expression . Ident | QualIdent .
ArgList ::= [ out | ref ] Expression { , [ out | ref ] Expression } .
Remarks
The offered signature of the binding behavior is that of its enclosed behavior.
Spec Explorer performs parameter expansion as part of model exploration. However, Spec Explorer can only expand parameters for a behavior when the behavior is composed with a model program defined in Cord. For more information on parameter expansion, see Parameter Generation.
Example
using Microsoft.Test;
config AxB
{
action abstract static void MyAbstractActions.A(int x);
action abstract static void MyAbstractActions.B();
}
machine M1() : AxB { B(); A(_)*; B() }
machine M2() : AxB { bind A({1..3}) in M1 }
machine M3() : AxB { let int x where x in {1..3} in bind A(x) in M1 }
Machine M1 produces the set of traces consisting of B followed by an arbitrary number of As with an arbitrary parameter, followed by another B.
Machine M2 constrains the parameter for each occurrence of A to be between 1 and 3.
Machine M3 is semantically identical to machine M2.
See Also
Reference
Machine
Invocation
ParallelBehavior
CordScript