Selecting Single Elements from Sequences
Occasionally you may wish to use a particular element in a sequence or other collection as an action parameter. Since the only arguments allowed in action invocations are variables and constants, the following code sample shows how to select a particular element from a sequence variable for use in an action.
machine S() : Main
{
let
Sequence<RealType> objs,
RealType obj1,
RealType obj2
in
CreateObjs()/objs;
(. obj1 == objs[0] .) : UseElement(obj1);
(. obj2 == objs[1] .) : UseElement(obj2);
}
Several things to note here:
The C# expressions in the (. obj1 == objs[0] .) : UseElement(obj1); and (. obj2 == objs[1] .) : UseElement(obj2); Cord statements must evaluate to a Boolean value. The statements above are the equivalent of {. Condition.IsTrue(obj1 == objs[0]) .} and {. Condition.IsTrue(obj2 == objs[1]) .} .
{. C# statements .} blocks can perform assignment on state variables, but not on Cord names (such as those defined in let and bind statements) as Cord names are not state variables but Cord identifiers used in invocations. Cord names can, of course, be the target of constraints (e.g. the Condition type) including Cord statements using boolean C# expression notation.