/* Example 04. Model of Stack Behavior

	The event trace is a set of events and the Boolean expressions
in MP can embrace the traditional predicate calculus notation. A set
of behaviors (event traces) may be defined by the event grammar rules,
composition operations, and some additional constraints – ENSURE
conditions.

	Stack implements the “last in, first out” behavior for
storing/retrieving elements. It is assumed that initially Stack
is empty.

	This rule specifies the behavior of a stack in terms of stack
operations push and pop. The BUILD block associated with a root or
composite event contains composition operations performed when event
trace segment representing the behavior of that root or composite is
generated. The ENSURE Boolean expression provides a condition that
each valid trace should satisfy. The domain of the universal quantifier
is the set of all pop events inside Stack. The FROM Stack part is
optional, by default it is assumed to be FROM THIS.

The function #pop BEFORE $x yields the number of pop events preceding
$x. The set of valid event traces specified by this schema contains
only traces that satisfy the constraint. This example presents a
filtering operation as yet another kind of behavior composition,
and demonstrates an example of combining imperative (event grammar)
and declarative (Boolean expressions) constructs for behavior
specification.

Instructions: Run for Scopes 1 and up. Viewing of traces also 
includes a "Swim Lanes" option.

==========================================================*/

SCHEMA Stack_Behavior

ROOT Stack: (* ( push | pop ) *)
BUILD {
/* If an element is retrieved, it should have been stored before */
ENSURE FOREACH $x: pop FROM Stack
( #pop BEFORE $x < #push BEFORE $x );
};