Share via


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

Concepts

Cord Syntax Definition

Other Resources

Cord Scripting Language