From 23cf12565ad53797b82bb5f048f78bcf34eefe37 Mon Sep 17 00:00:00 2001
From: Keane Reynolds <keane.reynolds@gmail.com>
Date: Fri, 18 Jun 2021 14:22:14 +0000
Subject: [PATCH] Uploaded Example 4 from the manual

---
 Example04_StackBehavior_EnsureCondition.mp | 38 ++++++++++++++++++++++
 1 file changed, 38 insertions(+)
 create mode 100644 Example04_StackBehavior_EnsureCondition.mp

diff --git a/Example04_StackBehavior_EnsureCondition.mp b/Example04_StackBehavior_EnsureCondition.mp
new file mode 100644
index 0000000..1ddf8bc
--- /dev/null
+++ b/Example04_StackBehavior_EnsureCondition.mp
@@ -0,0 +1,38 @@
+/* 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
-- 
GitLab