From 48ff08f29ee6e37a18e81b96c90de7a9e53542e2 Mon Sep 17 00:00:00 2001
From: Keane Reynolds <keane.reynolds@gmail.com>
Date: Fri, 18 Jun 2021 14:22:37 +0000
Subject: [PATCH] Upload New File

---
 ...ckBehavior_ProbabilityCalculationsType1.mp | 22 +++++++++++++++++++
 1 file changed, 22 insertions(+)
 create mode 100644 Example16_StackBehavior_ProbabilityCalculationsType1.mp

diff --git a/Example16_StackBehavior_ProbabilityCalculationsType1.mp b/Example16_StackBehavior_ProbabilityCalculationsType1.mp
new file mode 100644
index 0000000..f35fec7
--- /dev/null
+++ b/Example16_StackBehavior_ProbabilityCalculationsType1.mp
@@ -0,0 +1,22 @@
+/* Example16_StackBehavior_ProbabilityCalculationsType1.mp
+
+	Here is a simple stack behavior model. Valid behaviors don’t permit
+a scenario when Pop operation is applied to the empty stack. For the
+example’s purpose we assume probability of Push is higher than
+probability of Pop. It is assumed also that probabilities to perform 0,
+1 or more iterations by the iterative event pattern (* … *) are equal.
+
+	Consider a test at scope 2. Because pop cannot occur before a push,
+the model rejects the scenarios where a single pop alone occurs, a pop
+occurs before a push, and 2 pops with no pushing. These would all be
+impossible in a real stack, so they are cut from the model.
+
+By removing some scenarios, the remaining probabilities change.
+
+*/
+SCHEMA Stack_Behavior
+
+ROOT Stack: (* (<<0.75>> Push | <<0.25>> 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