Merge branch 'Keane_Branch' into 'master'

Keane branch

See merge request !6

Example01_SimpleMessageFlow_EventCoordination.mp

@@ -13,7 +13,7 @@ the most appropriate for browsing traces here.
 
 ==========================================================*/
 
-SCHEMA simple_message_flow
+SCHEMA Simple_Message_Flow
 
 ROOT Sender:   (* send *);
 ROOT Receiver: (* receive *);

Example01a_UnreliableMessageFlow_VirtualEvents.mp

@@ -7,7 +7,7 @@ run for scopes 1 and up.
 
 ==========================================================*/
 
-SCHEMA unreliable_message_flow
+SCHEMA Unreliable_Message_Flow
 ROOT 	Sender: 	(* send *);
 ROOT 	Receiver: 	(* (receive | does_not_receive) *);
 

Example02_DataFlow_EventSharing.mp

@@ -25,7 +25,7 @@ the most appropriate for browsing traces here.
 
 ==========================================================*/
 
-SCHEMA Data_flow
+SCHEMA Data_Flow
 
 ROOT Writer: (* ( working | writing ) *);
 

Example03_ATMWithdrawal_BehaviorOfEnvironment.mp

@@ -28,7 +28,7 @@ to view a traditional "box-and-arrow" architecture diagram, i.e. to visualize an
 
 ==========================================================*/
 
-SCHEMA ATM_withdrawal
+SCHEMA ATM_Withdrawal
 
 ROOT Customer: 	(*  insert_card  
 		    		( identification_succeeds 

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

Example04a_Queue_behavior.mp → Example04a_StackBehavior_UserDefinedRelations.mp

@@ -20,7 +20,7 @@ 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 Queue_behavior
+SCHEMA Queue_Behavior
 
 ROOT Queue: (* ( enqueue | dequeue ) *)
 	BUILD { 

Example04b_QueueBehavior_UserDefinedRelations.mp

@@ -29,7 +29,7 @@ example of combining imperative (event grammar) and declarative
 
 ==========================================================*/
 
-SCHEMA Stack_behavior
+SCHEMA Stack_Behavior
 
 ROOT Stack: (* ( push | pop ) *)
 		BUILD { 

Example05_CarRace_NestedComposition.mp

@@ -11,7 +11,7 @@ layouts are the most appropriate for browsing traces here.
 
 ==========================================================*/
 
-SCHEMA Example5_Car_Race
+SCHEMA Car_Race
 
 Car:    Start 
         (* drive_lap *) 

Example06_UnreliableChannel_AssertionChecking.mp

@@ -22,7 +22,7 @@
 
 ==========================================================*/
 
-SCHEMA AtoB
+SCHEMA Unreliable_Channel
 
 ROOT TaskA: (* 	A_sends_request_to_B
 		    	( 	A_receives_data_from_B   	|  

Example11_RingTopology_UserDefinedRelations.mp

@@ -8,7 +8,7 @@
     
 ==========================================================*/
 
-SCHEMA ring
+SCHEMA Ring_Topology
 /* model of networking ring, where each node sends/receives
 to/from its left and right neighbor.
 */

Example12_CardiacArrestWorkflow_VirtualEvents.mp

@@ -16,7 +16,7 @@ run for scope 1
 
 ==========================================================*/
 
-SCHEMA Cardiac_Arrest
+SCHEMA Cardiac_Arrest_Workflow
 
 ROOT Phase1: {  check_breathing [finish_first], 
                 check_pulse 	[finish_first]   }

Example13_ConsumersSuppliers_DependencyTracking.mp

@@ -11,7 +11,7 @@ on Gryphon:
 
 ==========================================================*/
 
-SCHEMA Suppliers
+SCHEMA Consumers_Suppliers 
 
 /*=========================================*/
 ROOT Consumers: {+ Consumer +};

Example14_ShoppingSpree_NumberAttributes.mp

@@ -2,7 +2,7 @@
 
 ==========================================================*/
 
-SCHEMA Shopping_spree
+SCHEMA Shopping_Spree
 
 ROOT Buyer: (*<0.. 2 * $$scope>  Buy *);
 /* Increase the iteration to ensure enough Buy events to coordinate with both Shops */

Example15_BackpackWeight_IntervalAttributes.mp

@@ -9,8 +9,7 @@
     run for scopes 1 and up
 
 ==========================================================*/
-
-SCHEMA backpack
+SCHEMA Backpack_Weight
 
 ATTRIBUTES{ interval weight; };
 

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

Example17_SharedEvents_ProbabilityCalculationsType1.mp

+/* Example17_SharedEvents_ProbabilityCalculationsType1.mp
+
+	A simple example of shared events. If one root has a, the other root
+also has a. If neither root has a, then root 1 must have b, and root 2
+must have c. Additionally, probabilities show how "SHARE ALL" increases
+the chances of the shared event.
+
+*/
+SCHEMA Shared_Events
+
+ROOT R1: (<<0.6>> a | b);
+ROOT R2: (<<0.8>> a | c);
+R1, R2 SHARE ALL a;
\ No newline at end of file

Example18_RedGreen_BayesianProbabilityCalculationsType2.mp

@@ -14,10 +14,8 @@
     constant for the whole derivation process.
 
     run for scope 1
-
-==========================================================*/
-
-SCHEMA RedGreen
+*/
+SCHEMA Red_Green
 
 ATTRIBUTES{ number selection_probability; };
 

Example19_StackBehavior_BayesianProbabilityCalculationsType2.mp

@@ -26,7 +26,7 @@
 
 ==========================================================*/
 
-SCHEMA stack1
+SCHEMA Stack_Behavior
 
 ROOT Stack: (* ( <<0.75>> push | <<0.25>> pop ) *)
 		/* probabilities for alternatives are here to enable also 

Example20_Activity_Diagram.mp

+/* Example20_Activity_Diagram.mp
+
+	This model demonstrates how to use "SHOW ACTIVITY DIAGRAM" to
+display the possible traces in flowchart form. Root A has 4 different
+possible traces at scope 1, and the flowchart displays those possiblities.
+
+*/
+
+SCHEMA Activity_Diagram
+
+ROOT A:
+	a1
+	[a2]
+	{ a3, a4, a5 }
+	a6
+	( a7 | a8 );
+
+SHOW ACTIVITY DIAGRAM A;
\ No newline at end of file

Example21_DataFlow_LocalReport.mp

-/* Example 21. Model of [Data_Flow]
 
-Local Report within a trace.
-	
-run for scope 1 and up.
-
-==========================================================*/
-
-SCHEMA Data_flow
+/* Example 30. Local Report within a trace.
+	run for scope 1 and up.
+*/
+SCHEMA Data_Flow
 
 ROOT Writer: (* ( working | writing ) *);