Export (0) Print
Expand All
This topic has not yet been rated - Rate this topic

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.

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 } .

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.

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.



Did you find this helpful?
(1500 characters remaining)
Thank you for your feedback
Show:
© 2014 Microsoft. All rights reserved.