Returning Values From External Functions

As already frequently used in the examples in this document, the construct is used to specify the return value of a monitored external function. In terms of ASMs, ``'' is realized as follows: In each asm B that is used as monitored function, a 0-ary dynamic function B_result is declared and initialized with no_result, a specific element of the superuniverse. Let R be the rule of B as defined by the user, then the internally used rule representing the body of B is given by the following conditional:

In other words, updating B_result with value different from the special no_result element directly forces the asm to terminate. The notation ``t'' in an asm B is then simply an abbreviation for the update ``B_result := t''.