Upload New File

Example16_StackBehavior_ProbabilityCalculationsType1.mp

+/* 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