The ``Once''-Rule

Next: Grammar Definitions in XASM Up: Non-Standard Language Constructs of Previous: Regular Expressions

The ``Once''-Rule

A common situation occurring in ASM formalizations is that certain rules should fire only once during the run of an ASM. Normally, one has to introduce extra functions in order to ensure this behavior. XASM introduces a ``once'' rule for these situations:

$\begin{asmbox} \IFONCE R_1 \ELSE R_2 \ENDIF \end{asmbox}$

which is - in terms of ASMs - equivalent to the conditional rule

$\begin{asmbox} \IF once(n) \THEN R_1 once(n) := false \ELSE R_2 \ENDIF \end{asmbox}$

where n is a unique number representing the n'th occurrence of a ``once''-rule in the ASM, and once is a one-ary dynamic relation initialized with for all these numbers n. The notation ``once R'' is an abbreviation for

$\begin{asmbox} \IFONCE R \ELSE \SKIP \ENDIF \end{asmbox}$

Philipp Kutter 2002-03-18