diff --git a/Example16_StackBehavior_ProbabilityCalculationsType1.mp b/Example16_StackBehavior_ProbabilityCalculationsType1.mp new file mode 100644 index 0000000000000000000000000000000000000000..f35fec747f74f1fa279d92bf3a5f9802ca0fde99 --- /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