Uploaded Example 4 from the manual

Example04_StackBehavior_EnsureCondition.mp

+/* Example04_StackBehavior_EnsureCondition.mp
+
+	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.
+
+*/
+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 );
+};
\ No newline at end of file