Loop (Combined Fragment)   A loop interaction operator (signified by the value of loop) defines a combined fragment where the messages contained in the fragment are repeated a number of times. The guard contains a lower bound defining the minimum number of times the operand must loop, an upper bound defining the maximum number of times the operand will be executed and a boolean expression (evaluated after the operand has looped the minimum number of times) which if false will terminate the loop.

Explanation

The loop operator is a way of expressing that a set of traces can occur a number of times. There can only be one operand when a loop is used and all the traces contained in the operand will be repeated a number of times. The guard condition has a number of parts: it must have a lower bound (minint) which defines the minimum number of times the loop must be performed. It can also contain an upper bound (maxint) defining the maximum number of times the loop must be executed. It can also contain a boolean (two outcomes) expression, which is only evaluated after the loop has been performed the minint number of times and every turn of the loop after that. If the boolean expression evaluates to FALSE the loop is terminated, regardless of the value of the upper bound (maxint).