diff --git a/Example01_SimpleMessageFlow_EventCoordination.mp b/Example01_SimpleMessageFlow_EventCoordination.mp
index 0ea964f0c5e1a5d3a3606c2f1e02bec47ca3fad6..9b8074122d9da9b77c551f2603b5690b06d448db 100644
--- a/Example01_SimpleMessageFlow_EventCoordination.mp
+++ b/Example01_SimpleMessageFlow_EventCoordination.mp
@@ -1,4 +1,4 @@
-/*
+/*
Example1_simple_message_flow.mp
Event grammar rules for each root define derivations for event traces,
@@ -14,7 +14,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 d714bd0c5ba15a37e7cebecd62e4b7ba4df54d5a..7368c227075d4df94748fea64e3a2d76b7718bb7 100644
--- a/Example01a_UnreliableMessageFlow_VirtualEvents.mp
+++ b/Example01a_UnreliableMessageFlow_VirtualEvents.mp
@@ -1,4 +1,4 @@
-/* Example 1a
+/* Example 1a
Unreliable message flow.
We may want to specify behaviors when some messages get lost in the transition.
@@ -7,7 +7,7 @@ It can be done using ‘virtual’ events.
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 811e1de5c05900631a534383e10924fd91038d20..83b39076e55401b0a1c247faa57f8201015787cf 100644
--- a/Example02_DataFlow_EventSharing.mp
+++ b/Example02_DataFlow_EventSharing.mp
@@ -1,4 +1,4 @@
-/* Example2_DataAsEvents.mp
+/* Example2_DataAsEvents.mp
data items as behaviors
MP employs the Abstract Data Type (ADT) principle introduced by
@@ -24,7 +24,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 0c33381eeedc80f433f26581a87f283271eb48f1..36b871f75beed38661d3740577aeb32392e98846 100644
--- a/Example03_ATMWithdrawal_BehaviorOfEnvironment.mp
+++ b/Example03_ATMWithdrawal_BehaviorOfEnvironment.mp
@@ -1,4 +1,4 @@
-/* Example3_ATM_withdrawal.mp
+/* Example3_ATM_withdrawal.mp
Integrated system and environment behaviors
MP separates models of component behaviors and component interactions
@@ -27,7 +27,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
@@ -80,4 +80,4 @@ COORDINATE $x: identification_fails FROM Customer,
$y: id_failed FROM ATM_system
DO ADD $y PRECEDES $x; OD;
-
\ No newline at end of file
+
diff --git a/Example04a_Queue_behavior.mp b/Example04a_Queue_behavior.mp
index 3aed579e46c93823948700930d49e3ef8b7bcbcf..196b5878e4b4ec1319cf760d6fa392fb31523255 100644
--- a/Example04a_Queue_behavior.mp
+++ b/Example04a_Queue_behavior.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 0c660075f65c5c6248d423abf77219494b29c336..fd56e213b635630923105fa016a0285b2bee25be 100644
--- a/Example04b_QueueBehavior_UserDefinedRelations.mp
+++ b/Example04b_QueueBehavior_UserDefinedRelations.mp
@@ -29,7 +29,7 @@ example of combining imperative (event grammar) and declarative
(Boolean expressions) constructs for behavior specification.
*/
-SCHEMA Stack_behavior
+SCHEMA Stack_Behavior
ROOT Stack: (* ( push | pop ) *)
BUILD {
diff --git a/Example05_CarRace_NestedComposition.mp b/Example05_CarRace_NestedComposition.mp
index 4f6a8fd1696640cb494f27500d720ebb288be6c6..92fdabd18593939a67fa5f461140bd1ec651588c 100644
--- a/Example05_CarRace_NestedComposition.mp
+++ b/Example05_CarRace_NestedComposition.mp
@@ -10,7 +10,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 61d2cdd5ddbcfc7abbdceb49229fa295b8a4fb03..284fd6b869f0747a6c72d6335a36f35ad4b5a305 100644
--- a/Example06_UnreliableChannel_AssertionChecking.mp
+++ b/Example06_UnreliableChannel_AssertionChecking.mp
@@ -1,4 +1,4 @@
-/* Example6 Assertion checking, Communicating via unreliable channel.
+/* Example6 Assertion checking, Communicating via unreliable channel.
MP models need to be tested and debugged like any other
programming artifacts. Trace generation for a given scope
@@ -19,7 +19,7 @@
into the ENSURE condition.
*/
-SCHEMA AtoB
+SCHEMA Unreliable_Channel
ROOT TaskA: (* A_sends_request_to_B
( A_receives_data_from_B |
diff --git a/Example07_UnconstrainedStack_TraceAnnotation.mp b/Example07_UnconstrainedStack_TraceAnnotation.mp
index 817cee81c00edf2727d9cdd9a669b80d280eb5bb..001d79310f8eec89ec6603416837a36f54a3355a 100644
--- a/Example07_UnconstrainedStack_TraceAnnotation.mp
+++ b/Example07_UnconstrainedStack_TraceAnnotation.mp
@@ -47,4 +47,4 @@ ROOT Stack: (* ( push | pop [ bang ]) *)
/* Now traces where Stack behavior is incorrect will be MARKed and
corresponding pop events will be pointed to by PRECEDES arrow leading
from the message box associated with this event.
-*/
\ No newline at end of file
+*/
diff --git a/Example09_PipeFilter_TraceAnnotationQueries.mp b/Example09_PipeFilter_TraceAnnotationQueries.mp
index 63896c93432204eb441999ce30cdc279d45a82f6..93047b9df548d758f7f4bee59fc0227b5825f474 100644
--- a/Example09_PipeFilter_TraceAnnotationQueries.mp
+++ b/Example09_PipeFilter_TraceAnnotationQueries.mp
@@ -1,4 +1,4 @@
-/* Example10_Pipe_Filter.mp
+/* Example10_Pipe_Filter.mp
pipe/filter architecture model with 2 filters
assumptions:
@@ -52,4 +52,4 @@ IF #receive FROM Consumer != #send FROM Producer THEN
SAY( #send FROM Producer - #receive FROM Consumer
" messages did not reach Consumer");
MARK;
-FI;
\ No newline at end of file
+FI;
diff --git a/Example11_RingTopology_UserDefinedRelations.mp b/Example11_RingTopology_UserDefinedRelations.mp
index d3dcba336d47cf365b1ea1017c60c6ae41bf21c8..6c8cf8a7fefbe63c63cb22c6998a400a7e11b12d 100644
--- a/Example11_RingTopology_UserDefinedRelations.mp
+++ b/Example11_RingTopology_UserDefinedRelations.mp
@@ -6,7 +6,7 @@
where each node interacts with its left and right neighbors only.
------------------------------------------*/
-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 6c3b9601b4316f26231d0145cbcb7db6601c78e7..9984e7c127e2c8110e98162acf91558497193155 100644
--- a/Example12_CardiacArrestWorkflow_VirtualEvents.mp
+++ b/Example12_CardiacArrestWorkflow_VirtualEvents.mp
@@ -1,4 +1,4 @@
-/* Example18 Workflow pattern
+/* Example18 Workflow pattern
the web site
http://workflowpatterns.com/patterns/control/index.php
@@ -15,7 +15,7 @@ in a second instance of the triage task.
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 cb771e90ffca161946487229e76e2359ff87cc8a..7367cdf21b3b724666bd44fd262e65fd5aa23e92 100644
--- a/Example13_ConsumersSuppliers_DependencyTracking.mp
+++ b/Example13_ConsumersSuppliers_DependencyTracking.mp
@@ -10,7 +10,7 @@ on Gryphon:
scope 2, 670 traces, approx. time 2.5 min.
*/
-SCHEMA Suppliers
+SCHEMA Consumers_Suppliers
/*=========================================*/
ROOT Consumers: {+ Consumer +};
diff --git a/Example14_ShoppingSpree_NumberAttributes.mp b/Example14_ShoppingSpree_NumberAttributes.mp
index a0405536bb737d65c41b996e273fcf80c12c5037..22df21c42bb7ac8e85a4ad737af4ea161d0e7d96 100644
--- a/Example14_ShoppingSpree_NumberAttributes.mp
+++ b/Example14_ShoppingSpree_NumberAttributes.mp
@@ -1,6 +1,6 @@
/* Example23.mp number attribute test */
-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 cfef3eb3d82e9c64579cae0d7288b7571e4e0aa5..28132298a57b89e5b99f3844f2e428d76f028277 100644
--- a/Example15_BackpackWeight_IntervalAttributes.mp
+++ b/Example15_BackpackWeight_IntervalAttributes.mp
@@ -5,7 +5,7 @@
run for scopes 1 and up
==========================================================*/
-SCHEMA backpack
+SCHEMA Backpack_Weight
ATTRIBUTES{ interval weight; };
diff --git a/Example18_RedGreen_BayesianProbabilityCalculationsType2.mp b/Example18_RedGreen_BayesianProbabilityCalculationsType2.mp
index 5022d189337f73d5b9c6343a766ba09eeb0aeeab..ec66135921246f9ba5909506747dc2596f7cf48c 100644
--- a/Example18_RedGreen_BayesianProbabilityCalculationsType2.mp
+++ b/Example18_RedGreen_BayesianProbabilityCalculationsType2.mp
@@ -13,7 +13,7 @@
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 b0fc26dbd9263b07ec7b73467da1566e9f259b92..1905ece887376ccb36b2b3435f46a63abfe0de29 100644
--- a/Example19_StackBehavior_BayesianProbabilityCalculationsType2.mp
+++ b/Example19_StackBehavior_BayesianProbabilityCalculationsType2.mp
@@ -25,7 +25,7 @@
it will become p2 := 1/(M + 1);
==================================================================*/
-SCHEMA stack1
+SCHEMA Stack_Behavior
ROOT Stack: (* ( <<0.75>> push | <<0.25>> pop ) *)
/* probabilities for alternatives are here to enable also
diff --git a/Example21_DataFlow_LocalReport.mp b/Example21_DataFlow_LocalReport.mp
index 0271dd2c88233d5fb169237fedbaa2204edc6ee4..01c847f708b3f6494ce9f097d4a21cf5660a9812 100644
--- a/Example21_DataFlow_LocalReport.mp
+++ b/Example21_DataFlow_LocalReport.mp
@@ -1,8 +1,8 @@
-
+
/* Example 30. Local Report within a trace.
run for scope 1 and up.
*/
-SCHEMA Data_flow
+SCHEMA Data_Flow
ROOT Writer: (* ( working | writing ) *);
diff --git a/Example22_SimpleMessageFlow_GlobalReport.mp b/Example22_SimpleMessageFlow_GlobalReport.mp
index ad102ee91a6a0220854021bff9da9e385119ee92..0a6f1bb703172ed0117a1c6d380ba1a100f2da73 100644
--- a/Example22_SimpleMessageFlow_GlobalReport.mp
+++ b/Example22_SimpleMessageFlow_GlobalReport.mp
@@ -1,7 +1,7 @@
-/* Example 31. Global report.
+/* Example 31. Global report.
run for scope 1 and up
-----------------------------*/
-SCHEMA simple_message_flow
+SCHEMA Simple_Message_Flow
ROOT Sender: (* send *);
diff --git a/Example24_Compiler_ComponentDiagram.mp b/Example24_Compiler_ComponentDiagram.mp
index 5c1236ec9fc52bff59c61e00fa75594f76fedc25..56eab22a3789249300211bf5a0cf86b555a07b27 100644
--- a/Example24_Compiler_ComponentDiagram.mp
+++ b/Example24_Compiler_ComponentDiagram.mp
@@ -11,7 +11,7 @@
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 873759c781757149f84a0b2642b20dc4adcd44b8..77297eed44b18d88a865d6cf2676f116098088d7 100644
--- a/Example25_Graph_as_Data_Structure.mp
+++ b/Example25_Graph_as_Data_Structure.mp
@@ -2,7 +2,7 @@
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 d6f37e17a2f685fa129f560b3cae2711caae5099..86aa2df919a4936063f3ef6b721e44c695123998 100644
--- a/Example26_UnreliableMessageFlow_GlobalQuery.mp
+++ b/Example26_UnreliableMessageFlow_GlobalQuery.mp
@@ -16,7 +16,7 @@ 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 dade7edfb50152ab420057c88fe4d2ebbb1150ae..35172a1e6d489705c97818136eca06bf86cd415e 100644
--- a/Example27_AssemblingStatistics_Table_and_Bar_Chart.mp
+++ b/Example27_AssemblingStatistics_Table_and_Bar_Chart.mp
@@ -4,7 +4,7 @@
Table and bar chart example, run for scope 1
*/
-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 c40bdfa07024449cf9eaed6019578d65aafe051f..18f2402eb5bec97e607644cb78965c70e9324925 100644
--- a/Example28_AssemblingStatistics_Histogram.mp
+++ b/Example28_AssemblingStatistics_Histogram.mp
@@ -1,7 +1,7 @@
/* Example 43
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 fe4483df5b9e157783ebab43411f026c402a9199..1463d3c7da2f92a9482c295c83a73e8babd40bd8 100644
--- a/Example29_AssemblingStatistics_Gantt_Chart.mp
+++ b/Example29_AssemblingStatistics_Gantt_Chart.mp
@@ -1,7 +1,7 @@
/* Example44
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 fa6ad1cab52efde09ccde8b0361c9edc2bd051fc..416ef7c0587bcf7c691f18ab46e33c9243dd3315 100644
--- a/Example30_MicrowaveOven_ModelingModelChecking.mp
+++ b/Example30_MicrowaveOven_ModelingModelChecking.mp
@@ -1,4 +1,4 @@
-/* Example14, microwave_oven.mp
+/* Example14, microwave_oven.mp
example of finite state diagram behavior model,
CTL formula representation in MP, and model checking for a small scope.
@@ -31,7 +31,7 @@
scope 1 (28 traces, 2 counterexamples, 1.75 sec.)
*/
-SCHEMA oven
+SCHEMA Microwave_Oven
ROOT Microwave: S1 (* R7 S1 *);
diff --git a/Example32_Petri_Net.mp b/Example32_Petri_Net.mp
index b0ecf3becf6a41206e611e1fb1438a76fad6f5f5..6a6546444fc2c2050a6c603c856fca1b14c765eb 100644
--- a/Example32_Petri_Net.mp
+++ b/Example32_Petri_Net.mp
@@ -8,7 +8,7 @@
extracted from the event traces, run scope 2
=======================================================*/
-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 f41f30f641c63d9521dfe27e34c1781395d4d882..871883ba606b7ccbe52cbd547ef9b14074a8c961 100644
--- a/Example33_ATMWithdrawal_StatechartView.mp
+++ b/Example33_ATMWithdrawal_StatechartView.mp
@@ -4,7 +4,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 90b775634588e05da0c86ff492d65dc9b3949e01..fd488cb97d8d34e17b872dcfebe51af6a816d49b 100644
--- a/Example34_FiniteStateDiagram_PathAnnotation.mp
+++ b/Example34_FiniteStateDiagram_PathAnnotation.mp
@@ -35,7 +35,7 @@
scope 3 (258 traces)
*/
-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 ff0ca8160c4696f5154ba4491eac0ad2b88b95d3..b642abb13f7456344b67b2780bd13457cf51dfb2 100644
--- a/Example35_FiniteStateDiagram_PathDiagram.mp
+++ b/Example35_FiniteStateDiagram_PathDiagram.mp
@@ -5,7 +5,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/Example36_Authentication_SystemReuse.mp b/Example36_Authentication_SystemReuse.mp
index c09d654b8a85e7deac2951b79e8f5049c06ed9b2..56a1c43bddc0206ae6b19f1b9dc4e727503cf4e8 100644
--- a/Example36_Authentication_SystemReuse.mp
+++ b/Example36_Authentication_SystemReuse.mp
@@ -1,4 +1,4 @@
-SCHEMA Reuse_of_a_system
+SCHEMA Authentication_System
/* Example 20.
Authentication system's behavior for reuse with MAP operation.
diff --git a/Example37_Compiler1_ComponentReuse.mp b/Example37_Compiler1_ComponentReuse.mp
index 371f385233024744bdf39fae36ce112121a6f447..b691978ea61874f72a347a40a978711d5e6c1e7f 100644
--- a/Example37_Compiler1_ComponentReuse.mp
+++ b/Example37_Compiler1_ComponentReuse.mp
@@ -9,7 +9,7 @@ scope 2, 147 traces, approx. time 0.87 sec.
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 b18d9af47f41bf5a8b60a61f6f7e72744f52c7c3..3874d70063e5a162dbf0f77a20f4bf0bd0262f43 100644
--- a/Example38_Compiler2_ComponentReuse.mp
+++ b/Example38_Compiler2_ComponentReuse.mp
@@ -9,7 +9,7 @@ scope 2, 111 traces, approx. time 0.65 sec.
scope 3, 4860 traces, approx. time 55 sec.
====================================================*/
-SCHEMA compiler2
+SCHEMA Compiler2
ROOT Source_code: (* get_characters
unget_some_characters *)