diff --git a/Example01_SimpleMessageFlow_EventCoordination.mp b/Example01_SimpleMessageFlow_EventCoordination.mp index 61cfaf9869eedebd3ec599ff96232e617ee6e1b8..9b604dda1cc74f22d4dd49e386405b745399a643 100644 --- a/Example01_SimpleMessageFlow_EventCoordination.mp +++ b/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 *); diff --git a/Example01a_UnreliableMessageFlow_VirtualEvents.mp b/Example01a_UnreliableMessageFlow_VirtualEvents.mp index 31bd783ef15a5fab3552e50b078bae15c28bdb05..207b96aadbf147c2a0633db89901d9fbd79704ba 100644 --- a/Example01a_UnreliableMessageFlow_VirtualEvents.mp +++ b/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) *); diff --git a/Example02_DataFlow_EventSharing.mp b/Example02_DataFlow_EventSharing.mp index 1015c8c24350af7db9534724f0c865a74739ad4c..47d18b6e276ae9354eba0feb9c5b97b8f0a43b6b 100644 --- a/Example02_DataFlow_EventSharing.mp +++ b/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 ) *); diff --git a/Example03_ATMWithdrawal_BehaviorOfEnvironment.mp b/Example03_ATMWithdrawal_BehaviorOfEnvironment.mp index 69f18a3cda77892f8eec74b806dbfc62f204c3f6..245fcaeb0080d63c5164d87b504529c49e103c32 100644 --- a/Example03_ATMWithdrawal_BehaviorOfEnvironment.mp +++ b/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 diff --git a/Example04_StackBehavior_EnsureCondition.mp b/Example04_StackBehavior_EnsureCondition.mp new file mode 100644 index 0000000000000000000000000000000000000000..1ddf8bc4ea0e8a63783298761fbe318918476557 --- /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 diff --git a/Example04a_Queue_behavior.mp b/Example04a_StackBehavior_UserDefinedRelations.mp similarity index 98% rename from Example04a_Queue_behavior.mp rename to Example04a_StackBehavior_UserDefinedRelations.mp index 3aed579e46c93823948700930d49e3ef8b7bcbcf..196b5878e4b4ec1319cf760d6fa392fb31523255 100644 --- a/Example04a_Queue_behavior.mp +++ b/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 { diff --git a/Example04b_QueueBehavior_UserDefinedRelations.mp b/Example04b_QueueBehavior_UserDefinedRelations.mp index bc6a37d22214e57189dac1901786bc1b0c2f1ca9..b22b82ef05b93e533f7b6b526f88439a54d1109c 100644 --- a/Example04b_QueueBehavior_UserDefinedRelations.mp +++ b/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 { diff --git a/Example05_CarRace_NestedComposition.mp b/Example05_CarRace_NestedComposition.mp index 0a5d65f5666214223c6a800cee25d1acfa1eea50..766eda91bccf7545f6c952f49c9f090d06a8c77f 100644 --- a/Example05_CarRace_NestedComposition.mp +++ b/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 *) diff --git a/Example06_UnreliableChannel_AssertionChecking.mp b/Example06_UnreliableChannel_AssertionChecking.mp index 22437cefb4814977fcf524dee2cffe33de86b122..5a021feabe7963a6faaa1897361f5592fca79683 100644 --- a/Example06_UnreliableChannel_AssertionChecking.mp +++ b/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 | diff --git a/Example11_RingTopology_UserDefinedRelations.mp b/Example11_RingTopology_UserDefinedRelations.mp index 44e84786c4bb1e03722e479a2ea5dea1c01e0ae2..0ce90612f833c3039cc743b5f0e4c66231867026 100644 --- a/Example11_RingTopology_UserDefinedRelations.mp +++ 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. */ diff --git a/Example12_CardiacArrestWorkflow_VirtualEvents.mp b/Example12_CardiacArrestWorkflow_VirtualEvents.mp index 76c9b85632f4be2b58f1e745dd8155b43b5254f8..a29f138af7ff5fd806accba8353b1d0440554ff3 100644 --- a/Example12_CardiacArrestWorkflow_VirtualEvents.mp +++ b/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] } diff --git a/Example13_ConsumersSuppliers_DependencyTracking.mp b/Example13_ConsumersSuppliers_DependencyTracking.mp index 1ee9d9ac3480bd6b9c7e0af376c389f89cc266d8..f1a8117f95741353bd72032f34dd60de899fa8af 100644 --- a/Example13_ConsumersSuppliers_DependencyTracking.mp +++ b/Example13_ConsumersSuppliers_DependencyTracking.mp @@ -11,7 +11,7 @@ on Gryphon: ==========================================================*/ -SCHEMA Suppliers +SCHEMA Consumers_Suppliers /*=========================================*/ ROOT Consumers: {+ Consumer +}; diff --git a/Example14_ShoppingSpree_NumberAttributes.mp b/Example14_ShoppingSpree_NumberAttributes.mp index 3a0bb725727da958f7ef954af23000612cedc2a9..f6ce753b261f4f6aba37bc7a5472588e7e2f30d4 100644 --- a/Example14_ShoppingSpree_NumberAttributes.mp +++ b/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 */ diff --git a/Example15_BackpackWeight_IntervalAttributes.mp b/Example15_BackpackWeight_IntervalAttributes.mp index 643b66bd5e480827cf9f301c8286313fa04bced2..c596c95d38f88791bc64043fb189109a77ffba32 100644 --- a/Example15_BackpackWeight_IntervalAttributes.mp +++ b/Example15_BackpackWeight_IntervalAttributes.mp @@ -9,8 +9,7 @@ run for scopes 1 and up ==========================================================*/ - -SCHEMA backpack +SCHEMA Backpack_Weight ATTRIBUTES{ interval weight; }; 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 diff --git a/Example17_SharedEvents_ProbabilityCalculationsType1.mp b/Example17_SharedEvents_ProbabilityCalculationsType1.mp new file mode 100644 index 0000000000000000000000000000000000000000..c08f59d00876241b87d0f5dc6b4bc2a2c9af8d67 --- /dev/null +++ b/Example17_SharedEvents_ProbabilityCalculationsType1.mp @@ -0,0 +1,13 @@ +/* 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 diff --git a/Example18_RedGreen_BayesianProbabilityCalculationsType2.mp b/Example18_RedGreen_BayesianProbabilityCalculationsType2.mp index 043925922c2ba5c5cf0e2d3ca9e62f3d1aae0d02..a7c160f6d67faf5f5ddeda736f347b8ec4484064 100644 --- a/Example18_RedGreen_BayesianProbabilityCalculationsType2.mp +++ b/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; }; diff --git a/Example19_StackBehavior_BayesianProbabilityCalculationsType2.mp b/Example19_StackBehavior_BayesianProbabilityCalculationsType2.mp index f46cc9d12d596098438db42c843e1d2e774d1678..d8c8db1ea87b6a41c24c9abae5f2a899c691eda5 100644 --- a/Example19_StackBehavior_BayesianProbabilityCalculationsType2.mp +++ b/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 diff --git a/Example20_Activity_Diagram.mp b/Example20_Activity_Diagram.mp new file mode 100644 index 0000000000000000000000000000000000000000..8091ca50cdb23a2aa3f98290e2e6b0de6c3d80f8 --- /dev/null +++ b/Example20_Activity_Diagram.mp @@ -0,0 +1,18 @@ +/* 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 diff --git a/Example21_DataFlow_LocalReport.mp b/Example21_DataFlow_LocalReport.mp index a8fa082d5ff625372e5cba5e89c54130dbb16b91..01c847f708b3f6494ce9f097d4a21cf5660a9812 100644 --- a/Example21_DataFlow_LocalReport.mp +++ b/Example21_DataFlow_LocalReport.mp @@ -1,12 +1,8 @@ -/* 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 ) *); diff --git a/Example22_SimpleMessageFlow_GlobalReport.mp b/Example22_SimpleMessageFlow_GlobalReport.mp index b8bb2adad55b0bd197c2ef73bb7b917837217eee..6bbc765738776eb451122404312d1c65c05d8bae 100644 --- a/Example22_SimpleMessageFlow_GlobalReport.mp +++ b/Example22_SimpleMessageFlow_GlobalReport.mp @@ -4,7 +4,7 @@ ==========================================================*/ -SCHEMA simple_message_flow +SCHEMA Simple_Message_Flow ROOT Sender: (* send *); diff --git a/Example24_Compiler_ComponentDiagram.mp b/Example24_Compiler_ComponentDiagram.mp index cc761dd52c6bcabcdfd0eda13e64de63ae01ecb8..f8c232283d3d675238c3b3b939f18ce3441d18d0 100644 --- a/Example24_Compiler_ComponentDiagram.mp +++ b/Example24_Compiler_ComponentDiagram.mp @@ -11,9 +11,8 @@ run for scope 1, 20 traces, approx. 5 sec. -==========================================================*/ - -SCHEMA compiler_example +====================================================*/ +SCHEMA Compiler ROOT Source_code: (+<1.. $$scope + 1> get_characters diff --git a/Example25_Graph_as_Data_Structure.mp b/Example25_Graph_as_Data_Structure.mp index bd472e8ee470ad08859bb61ac817fb10c9510856..019fea311476321a730ac20a02352c45297f578b 100644 --- a/Example25_Graph_as_Data_Structure.mp +++ b/Example25_Graph_as_Data_Structure.mp @@ -2,10 +2,8 @@ Accumulating and rendering statistics from event traces. Graphs as container data structures - -==========================================================*/ - -SCHEMA Statistics +============================================================*/ +SCHEMA Graph_as_Data_Structure ROOT A: (* ( a | b) *); ROOT B: (+ c +); diff --git a/Example26_UnreliableMessageFlow_GlobalQuery.mp b/Example26_UnreliableMessageFlow_GlobalQuery.mp index e7c1cdb446b3b345c9662653b030ac02c8895016..84f651dd637e0fb0dc82cc707571c95018d0b8f1 100644 --- a/Example26_UnreliableMessageFlow_GlobalQuery.mp +++ b/Example26_UnreliableMessageFlow_GlobalQuery.mp @@ -17,10 +17,8 @@ ROOT Sender: (+<1..7> send +); ROOT Receiver: (+<1..7> (receive |<<0.2>> does_not_receive) +); Run for scopes 1 and up. - -==========================================================*/ - -SCHEMA unreliable_message_flow +*/ +SCHEMA Unreliable_Message_Flow ROOT Sender: (+ send +); ROOT Receiver: (+ (receive |<<0.2>> does_not_receive) +); diff --git a/Example27_AssemblingStatistics_Table_and_Bar_Chart.mp b/Example27_AssemblingStatistics_Table_and_Bar_Chart.mp index 2909722664c0909563b0c0895d57ff43c41a9ccf..c3f18e079016599ab10ee3487f24de4f78260941 100644 --- a/Example27_AssemblingStatistics_Table_and_Bar_Chart.mp +++ b/Example27_AssemblingStatistics_Table_and_Bar_Chart.mp @@ -5,7 +5,7 @@ ==========================================================*/ -SCHEMA Example +SCHEMA Table_and_Bar_Chart ROOT A: a b c a; TABLE trace_stats { diff --git a/Example28_AssemblingStatistics_Histogram.mp b/Example28_AssemblingStatistics_Histogram.mp index 1a316cb419c450cfe81688858c33cdd6f80a8f5b..908ca95543fca3c0e5e8472edfb4e475a7712866 100644 --- a/Example28_AssemblingStatistics_Histogram.mp +++ b/Example28_AssemblingStatistics_Histogram.mp @@ -1,10 +1,8 @@ /* Example 28. Model of [Histogram] Histogram example, run for scopes 1, 2, 3, and up - -==========================================================*/ - -SCHEMA Example +*/ +SCHEMA Histogram ROOT A: (<<0.2>> a1 | <<0.3>> a2 | (* a3 *)); ATTRIBUTES { number count; }; diff --git a/Example29_AssemblingStatistics_Gantt_Chart.mp b/Example29_AssemblingStatistics_Gantt_Chart.mp index b68924593b8da4f4e0994461f4cd69493e0e83e3..dc1ad1b86d876f8023b3c341305cce0d8ca4e28d 100644 --- a/Example29_AssemblingStatistics_Gantt_Chart.mp +++ b/Example29_AssemblingStatistics_Gantt_Chart.mp @@ -1,10 +1,8 @@ /* Example 29. Model of [Gantt_Chart] Gantt chart example - -==========================================================*/ - -SCHEMA S +*/ +SCHEMA Gantt_Chart ROOT A: a1 a2; ROOT B: b1 a2 b2; diff --git a/Example30_MicrowaveOven_ModelingModelChecking.mp b/Example30_MicrowaveOven_ModelingModelChecking.mp index a45440df87091e46135372a773c578cd6feb6e31..a8c23e4deb2326556bd577ccca330268f8baa7fd 100644 --- a/Example30_MicrowaveOven_ModelingModelChecking.mp +++ b/Example30_MicrowaveOven_ModelingModelChecking.mp @@ -32,7 +32,7 @@ ==========================================================*/ -SCHEMA oven +SCHEMA Microwave_Oven ROOT Microwave: S1 (* R7 S1 *); diff --git a/Example31_Aspect_Oriented_Paradigm.mp b/Example31_Aspect_Oriented_Paradigm.mp new file mode 100644 index 0000000000000000000000000000000000000000..63efa4a0c0359b3661ef555f971e604f71d8548e --- /dev/null +++ b/Example31_Aspect_Oriented_Paradigm.mp @@ -0,0 +1,32 @@ +/* Example31_Aspect_Oriented_Paradigm.mp + + The COORDINATE operation supports a “cause-effect†refinement for +the behavior of two components and it bears a certain similarity +to Aspect-Oriented Programming (AOP) paradigm [Kiczales et al. 1997] +(or read https://en.wikipedia.org/wiki/Aspect-oriented_programming). +For example, the following AOP pattern could be modeled by MP schema +where event coordination implements AOP join point and advice +coordination. + + Suppose that the main stream of execution contains calls to +methods M1 and M2 as join points, and the aspect behavior requires +a call to Prolog before, and to Epilog after each method call as an +advice. The corresponding MP model may look like the following. + +*/ + +SCHEMA Aspect_Oriented_Paradigm + +ROOT Main: (* ( M1 | M2 | do_something_else ) *); +ROOT PreAdvice: (* Prolog *); +ROOT PostAdvice: (* Epilog *); + +COORDINATE + $jp: ( M1 | M2 ) FROM Main, + $a1: Prolog FROM PreAdvice, + $a2: Epilog FROM PostAdvice + +DO ADD + $a1 PRECEDES $jp, + $jp PRECEDES $a2; +OD; \ No newline at end of file diff --git a/Example32_Petri_Net.mp b/Example32_Petri_Net.mp index a350b9f4b32d4f93defdfe5fe93b205335c8f700..01ef7c726ba4fb6df7a2a67911faa645ad85cde5 100644 --- a/Example32_Petri_Net.mp +++ b/Example32_Petri_Net.mp @@ -10,7 +10,7 @@ ==========================================================*/ -SCHEMA petri_net +SCHEMA Petri_Net /* behavior of each place and transition is modeled by a separate root event */ diff --git a/Example33_ATMWithdrawal_StatechartView.mp b/Example33_ATMWithdrawal_StatechartView.mp index d679b4d0e17baf137d3e9e520e4a8024a23f7f1d..79a83402139cc4e988b74875c8f39d28be3c3536 100644 --- a/Example33_ATMWithdrawal_StatechartView.mp +++ b/Example33_ATMWithdrawal_StatechartView.mp @@ -5,8 +5,7 @@ run for scope 1 and up ==========================================================*/ - -SCHEMA ATM_withdrawal_with_Statechart_view +SCHEMA ATM_Withdrawal ROOT Customer: (* insert_card ( identification_succeeds diff --git a/Example34_FiniteStateDiagram_PathAnnotation.mp b/Example34_FiniteStateDiagram_PathAnnotation.mp index e20c8477120e999691419756330a221c6f58e49e..6946cd08910773cff2568782cece1a573bb64735 100644 --- a/Example34_FiniteStateDiagram_PathAnnotation.mp +++ b/Example34_FiniteStateDiagram_PathAnnotation.mp @@ -36,7 +36,7 @@ ==========================================================*/ -SCHEMA FiniteStateDiagram +SCHEMA Finite_State_Diagram_with _Path_Annotation S1_to_S3: a; S1_to_S4: (a | b); diff --git a/Example35_FiniteStateDiagram_PathDiagram.mp b/Example35_FiniteStateDiagram_PathDiagram.mp index be477cbc91b941002c3468551f81bc4b3c13fa56..7b6af2b8227a651b3a9c6c1025ba5f4dfedfae63 100644 --- a/Example35_FiniteStateDiagram_PathDiagram.mp +++ b/Example35_FiniteStateDiagram_PathDiagram.mp @@ -6,8 +6,7 @@ run for scope 2 ==========================================================*/ - -SCHEMA Finite_State_Diagram_with_path +SCHEMA Finite_State_Diagram_with_Path_Diagram ROOT S1_behavior: Start Start_to_S1 S1 diff --git a/Example37_Compiler1_ComponentReuse.mp b/Example37_Compiler1_ComponentReuse.mp index 87ba688b653986efc082ad94078331607021e273..1b90df9d7c29ab0a5212e8166e92aba64e202706 100644 --- a/Example37_Compiler1_ComponentReuse.mp +++ b/Example37_Compiler1_ComponentReuse.mp @@ -11,7 +11,7 @@ scope 3, 11988 traces, approx. time 148 sec. ==========================================================*/ -SCHEMA compiler1 +SCHEMA Compiler1 ROOT Source_code: (* get_characters unget_some_characters *) diff --git a/Example38_Compiler2_ComponentReuse.mp b/Example38_Compiler2_ComponentReuse.mp index 81a64a0294f4ea4ef9a98a120c5803659fbc70c2..1c2fc025b06598e6ade7be5bdf3c19978a7c888a 100644 --- a/Example38_Compiler2_ComponentReuse.mp +++ b/Example38_Compiler2_ComponentReuse.mp @@ -11,7 +11,7 @@ scope 3, 4860 traces, approx. time 55 sec. ==========================================================*/ -SCHEMA compiler2 +SCHEMA Compiler2 ROOT Source_code: (* get_characters unget_some_characters *) diff --git a/Example39_Merging_Root_Events_to_Reduce_Run_Time.mp b/Example39_Merging_Root_Events_to_Reduce_Run_Time.mp new file mode 100644 index 0000000000000000000000000000000000000000..28cf824720516f298f5c3ae63df45fec9da66c2c --- /dev/null +++ b/Example39_Merging_Root_Events_to_Reduce_Run_Time.mp @@ -0,0 +1,46 @@ +/* Example39_Merging_Root_Events_to_Reduce_Run_Time.mp + + Complex MP models may have large number of root events with several +coordination operations performed on clusters of roots. This may be +system’s architecture model with a large number of actors (components) +and interactions (connectors) between them. Usually coordination operations +will be placed in schema’s body following the corresponding root event +descriptions and performed during the derivation as described in Section +3. Derivation for such “heavy†MP models in Firebird may take too much +time even for scope 1. Fortunately, the “layered derivation†strategy +implemented in MP may help to speed up the trace derivation, and in +many cases makes it possible to work with a pretty large and complex +MP models. The idea is simple – organize the derivation as a hierarchy +of smaller derivations. + + Here is an example of how to benefit from the “layered derivationâ€. +Schema S1 has several interacting root events, where roots B and C have +several coordination operations between them. These coordination operations +will be performed repeatedly each time when derivation process backtracks +and performs new top-down pass through schema’s code for the next trace +derivation. + + B and C have two coordination operations between them: COORDINATE +and SHARE ALL. To delegate this “heavy†coordination to a separate +derivation task we introduce a separate root event B_and_C to +encapsulate the trace segment derivation (including the coordination) +for B and C. + +*/ +SCHEMA Merging_Root_Events_to_Reduce_Run_Time +ROOT A: (* ( work | send_to_B) *); +ROOT B: (*<1.. $$scope + 1> +( work | receive_from_A | send_to_C ) *); +COORDINATE $a: send_to_B, +$b: receive_from_A +DO ADD $a PRECEDES $b; OD; +ROOT C: (*<1.. $$scope + 1> +( work | receive_from_B | send_to_D ) *); +COORDINATE $a: send_to_C, +$b: receive_from_B +DO ADD $a PRECEDES $b; OD; +B, C SHARE ALL work; +ROOT D: (* (work | receive_from_C ) *); +COORDINATE $a: send_to_D, +$b: receive_from_C +DO ADD $a PRECEDES $b; OD; diff --git a/Example40_ApplicationProcess_partitioningLargeSchemaIntoSeparateSchemas.mp b/Example40_ApplicationProcess_partitioningLargeSchemaIntoSeparateSchemas.mp new file mode 100644 index 0000000000000000000000000000000000000000..38c2edccb15bd8554720fe9a5729e511818ba4db --- /dev/null +++ b/Example40_ApplicationProcess_partitioningLargeSchemaIntoSeparateSchemas.mp @@ -0,0 +1,57 @@ +/* Example40_ApplicationProcess_partitioningLargeSchemaIntoSeparateSchemas.mp + + An applicant submits application and needs to get it approved by +the bureaucratic chain of two officials. If the first official approves, +he forwards the application to the second official. Application is +approved only after it receives both approvals. Each official can +approve/reject the application or request it reworked and resubmitted. +Rework and resubmit events may be repeated several times. Each rejection +is final and cannot be followed by rework and resubmit events. + +*/ +SCHEMA Application_approval_process + +ROOT Applicant: + prepare_application + submit_application + (* rework + submit_application *) + ( application_is_approved | + application_is_rejected ); + +ROOT Official_1: + (+ receives_application_from_Applicant + (approves_and_forwards_to_Official_2 | + request_rework | + reject ) +) +BUILD{ ENSURE #reject <= 1; + +ENSURE FOREACH $r: reject #$$EVENT AFTER $r == 0; }; +COORDINATE $s: submit_application FROM Applicant, +$r: receives_application_from_Applicant FROM Official_1 +DO ADD $s PRECEDES $r; OD; + +ROOT Official_2: + (* receives_application_from_Official_1 + (approves_and_forwards_to_Applicant | + request_rework | reject ) *) +BUILD{ ENSURE #reject <= 1; +ENSURE FOREACH $r: reject #$$EVENT AFTER $r == 0; }; + +COORDINATE $s: approves_and_forwards_to_Official_2 FROM Official_1, +$r: receives_application_from_Official_1 FROM +Official_2 +DO ADD $s PRECEDES $r; OD; + +/*--- interactions with Applicant ---------*/ +COORDINATE $r: reject, /* this may come from several actors */ +$rr: application_is_rejected FROM Applicant +DO ADD $r PRECEDES $rr; OD; + +COORDINATE $r: request_rework, /* this may come from several actors */ +$rr: rework FROM Applicant +DO ADD $r PRECEDES $rr; OD; + +COORDINATE $a: approves_and_forwards_to_Applicant FROM Official_2, +$aa: application_is_approved FROM Applicant +DO ADD $a PRECEDES $aa; OD; \ No newline at end of file