From d79a26f58b21d04090cf47a12ab1280132c5fb11 Mon Sep 17 00:00:00 2001
From: Keane Reynolds <keane.reynolds@gmail.com>
Date: Thu, 17 Jun 2021 14:11:06 +0000
Subject: [PATCH] Updated Names for schemas 1-38, excluding the ones I haven't
made yet.
---
Example01_SimpleMessageFlow_EventCoordination.mp | 4 ++--
Example01a_UnreliableMessageFlow_VirtualEvents.mp | 4 ++--
Example02_DataFlow_EventSharing.mp | 4 ++--
Example03_ATMWithdrawal_BehaviorOfEnvironment.mp | 6 +++---
Example04a_Queue_behavior.mp | 2 +-
Example04b_QueueBehavior_UserDefinedRelations.mp | 2 +-
Example05_CarRace_NestedComposition.mp | 2 +-
Example06_UnreliableChannel_AssertionChecking.mp | 4 ++--
Example07_UnconstrainedStack_TraceAnnotation.mp | 2 +-
Example09_PipeFilter_TraceAnnotationQueries.mp | 4 ++--
Example11_RingTopology_UserDefinedRelations.mp | 2 +-
Example12_CardiacArrestWorkflow_VirtualEvents.mp | 4 ++--
Example13_ConsumersSuppliers_DependencyTracking.mp | 2 +-
Example14_ShoppingSpree_NumberAttributes.mp | 2 +-
Example15_BackpackWeight_IntervalAttributes.mp | 2 +-
Example18_RedGreen_BayesianProbabilityCalculationsType2.mp | 2 +-
...19_StackBehavior_BayesianProbabilityCalculationsType2.mp | 2 +-
Example21_DataFlow_LocalReport.mp | 4 ++--
Example22_SimpleMessageFlow_GlobalReport.mp | 4 ++--
Example24_Compiler_ComponentDiagram.mp | 2 +-
Example25_Graph_as_Data_Structure.mp | 2 +-
Example26_UnreliableMessageFlow_GlobalQuery.mp | 2 +-
Example27_AssemblingStatistics_Table_and_Bar_Chart.mp | 2 +-
Example28_AssemblingStatistics_Histogram.mp | 2 +-
Example29_AssemblingStatistics_Gantt_Chart.mp | 2 +-
Example30_MicrowaveOven_ModelingModelChecking.mp | 4 ++--
Example32_Petri_Net.mp | 2 +-
Example33_ATMWithdrawal_StatechartView.mp | 2 +-
Example34_FiniteStateDiagram_PathAnnotation.mp | 2 +-
Example35_FiniteStateDiagram_PathDiagram.mp | 2 +-
Example36_Authentication_SystemReuse.mp | 2 +-
Example37_Compiler1_ComponentReuse.mp | 2 +-
Example38_Compiler2_ComponentReuse.mp | 2 +-
33 files changed, 44 insertions(+), 44 deletions(-)
diff --git a/Example01_SimpleMessageFlow_EventCoordination.mp b/Example01_SimpleMessageFlow_EventCoordination.mp
index 0ea964f..9b80741 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 d714bd0..7368c22 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 811e1de..83b3907 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 0c33381..36b871f 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 3aed579..196b587 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 0c66007..fd56e21 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 4f6a8fd..92fdabd 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 61d2cdd..284fd6b 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 817cee8..001d793 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 63896c9..93047b9 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 d3dcba3..6c8cf8a 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 6c3b960..9984e7c 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 cb771e9..7367cdf 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 a040553..22df21c 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 cfef3eb..2813229 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 5022d18..ec66135 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 b0fc26d..1905ece 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 0271dd2..01c847f 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 ad102ee..0a6f1bb 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 5c1236e..56eab22 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 873759c..77297ee 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 d6f37e1..86aa2df 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 dade7ed..35172a1 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 c40bdfa..18f2402 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 fe4483d..1463d3c 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 fa6ad1c..416ef7c 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 b0ecf3b..6a65464 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 f41f30f..871883b 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 90b7756..fd488cb 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 ff0ca81..b642abb 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 c09d654..56a1c43 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 371f385..b691978 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 b18d9af..3874d70 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 *)
--
GitLab