diff --git a/Application_examples/Authentication.mp b/Application_examples/Authentication.mp
index c9b6910a2f419ed793249dc98cedc1ad1e6efb93..3456b61b70a204e4b5acf2218faa0db7c9792d15 100644
--- a/Application_examples/Authentication.mp
+++ b/Application_examples/Authentication.mp
@@ -1,4 +1,4 @@
-/*******************************************************************************
+/* Model of [Authentication]
A Model for Simple Authentication
@@ -9,7 +9,7 @@ constraints.
modified by K.Giammarco on 08/07/2017 for capitalization of state events
modified by K.Giammarco on 08/07/2017 for ENSURE constraints
-********************************************************************************/
+==========================================================*/
SCHEMA Authentication
@@ -53,4 +53,4 @@ ENSURE #CREDS_INVALID <= 3;
ENSURE #Deny_access >= 3 <-> #Lock_account == 1;
-ENSURE #Grant_access >= 1 -> #Lock_account == 0;
\ No newline at end of file
+ENSURE #Grant_access >= 1 -> #Lock_account == 0;
diff --git a/Application_examples/Autonomous_Car.mp b/Application_examples/Autonomous_Car.mp
index 7d88365fed2f335c382f1060ca51badd16f2cbce..4fa4d845a7773d9856f1c9059084720ccc379aec 100644
--- a/Application_examples/Autonomous_Car.mp
+++ b/Application_examples/Autonomous_Car.mp
@@ -1,7 +1,10 @@
-/* A model of an autonomous car that was used to support a failure mode
+/* Model of [Autonomous_Car]
+
+A model of an autonomous car that was used to support a failure mode
analysis of autonomous automobile technology (student project).
Created by G. Kaminski, November 2015
-*/
+
+==========================================================*/
SCHEMA Autonomous_Car
@@ -55,4 +58,4 @@ COORDINATE $a: Confirm_Destination_Found FROM Car,
COORDINATE $a: ( Enter_New_Destination |
Confirm_Destination ) FROM User,
$b: Begin_Trip FROM Car
- DO ADD $a PRECEDES $b; OD;
\ No newline at end of file
+ DO ADD $a PRECEDES $b; OD;
diff --git a/Application_examples/Beginner_Use_of_MP.mp b/Application_examples/Beginner_Use_of_MP.mp
index 3f610381547febae925d6287c78eef0813bd955e..360182fd828b7f9b4cccf5cd57af2380de5bd55a 100644
--- a/Application_examples/Beginner_Use_of_MP.mp
+++ b/Application_examples/Beginner_Use_of_MP.mp
@@ -1,4 +1,6 @@
-/* A Simple Model of Beginner MP-Firebird Use
+/* Model of [Beginner_Use_of_MP]
+
+A Simple Model of Beginner MP-Firebird Use
created by K.Giammarco 2021-02-08
This model provides an orientation for those just getting started using
@@ -19,8 +21,9 @@ You may also make changes to this model and run it with your changes.
Save your model using the EXPORT button ("Code" exports a .mp text file
of the contents of the text editor, and "Code and Event Trace" exports
the contents of the text editor plus the graphs and any changes you made
-to the graph element positions. */
+to the graph element positions.
+==========================================================*/
SCHEMA Beginner_Use_of_MP
@@ -86,4 +89,4 @@ IF #Find_issue >1 THEN
ELSE IF #Find_issue ==1 THEN
SAY( #Find_issue " issue was discovered");
FI;
-FI;
\ No newline at end of file
+FI;
diff --git a/Application_examples/CargoScreening.mp b/Application_examples/CargoScreening.mp
index 13fe2283d993b66b14f1d52881729320e9936a03..ccb6969ef2ba590b1f20e730407d4f393fb13af4 100644
--- a/Application_examples/CargoScreening.mp
+++ b/Application_examples/CargoScreening.mp
@@ -1,4 +1,6 @@
-/* Cargo Screening process model
+/* Model of [CargoScreening]
+
+Cargo Screening process model
May 6, 2011, draft written by Mikhail Auguston, NPS, Monterey, CA
source:
Department of Homeland Security
@@ -18,7 +20,7 @@ MP-Firebird may be used at least for the following:
was it always preceded by ThreatIsNotFound or No_high_risk_cargo_selected events?"
- typical query may be: "show all scenarios when Loading event does not happen"
-*/
+==========================================================*/
SCHEMA CargoScreening
diff --git a/Application_examples/Commercial_Flight b/Application_examples/Commercial_Flight
index ff64ab55e84b04e1869deb021d9870a80a1a5b60..e5af78cf62d665685e6560a8e236fb9002f663dc 100644
--- a/Application_examples/Commercial_Flight
+++ b/Application_examples/Commercial_Flight
@@ -1,11 +1,13 @@
-/* Model of a commercial flight, November 27, 2013
+/* Model of [Commercial_Flight]
+
+Model of a commercial flight, November 27, 2013
This model demonstrates the interlacing of root events as Phases
and as Actors. The commented out code at the bottom represents
a simulation of COORDINATE statements with SHARE ALL statements before
COORDINATE statements were implemented in the early MP tools.
-*/
+==========================================================*/
/*-----------------------------------------------------
Phases
diff --git a/Application_examples/Cycle_Pattern.mp b/Application_examples/Cycle_Pattern.mp
index 8d75d0f4292bc25b24a8237c9ab0f2a8f9832482..fa7a43db1dd447ec434a82c99c1838bb810cc89d 100644
--- a/Application_examples/Cycle_Pattern.mp
+++ b/Application_examples/Cycle_Pattern.mp
@@ -1,4 +1,5 @@
-/***************************************
+/* Model of [Cycle_Pattern]
+
Cycle_ISP Model for Systems Journal Article
Available at https://www.mdpi.com/2079-8954/6/2/18
created 2018-03-10 by K.Giammarco
@@ -18,7 +19,7 @@ the different possible patterns for Cycle.
Running at scope 1 will generate zero traces because
of the ENSURE constraint on line 29.
-****************************************/
+==========================================================*/
SCHEMA Cycle_ISP_v2
diff --git a/Application_examples/Dining_Philosophers.mp b/Application_examples/Dining_Philosophers.mp
index 6a2330a892b959217997c816aae07682034f5340..c97601ca71082ed411f277c1ef5b587977411057 100644
--- a/Application_examples/Dining_Philosophers.mp
+++ b/Application_examples/Dining_Philosophers.mp
@@ -1,4 +1,6 @@
-/* Example 17, Dining_Philosophers.mp
+/* Model of [Dining_Philosophers]
+
+Example 17, Dining_Philosophers.mp
Five silent philosophers sit at a table around a bowl of spaghetti.
A fork is placed between each pair of adjacent philosophers.
It was originally formulated in 1965 by Edsger Dijkstra.
@@ -30,7 +32,8 @@ scope 3 yields 6 traces in approx. 0.05 sec.
scope 4 yields 14 traces in approx. 0.44 sec.
scope 5 yields 30 traces in approx. 1.6 sec.
-============================================================================*/
+==========================================================*/
+
SCHEMA Dining_Philosophers
ROOT Philosophers: {+<$$scope> Philosopher +};
diff --git a/Application_examples/Elevator.mp b/Application_examples/Elevator.mp
index 48189b3b39099220fadc227d6a12035c8bf38aab..dfc63a626c1ce6e0b35eae3c7b821fad8cefc974 100644
--- a/Application_examples/Elevator.mp
+++ b/Application_examples/Elevator.mp
@@ -1,4 +1,6 @@
-/*Elevator Model
+/* Model of [Elevator]
+
+Elevator Model
K.Giammarco circa 2011
@@ -13,7 +15,7 @@ in the case of this model,
( Elevator_works_fine Get_Off |
Emergency_Situation Call_for_help )
-*/
+==========================================================*/
SCHEMA ELEVATOR
@@ -40,4 +42,4 @@ COORDINATE $a: Call_for_help FROM Passenger,
Passenger, Elevator SHARE ALL Available, Non_Available;
Passenger, Maintenance_Personnel SHARE ALL Emergency_Situation, Elevator_works_fine;
-
\ No newline at end of file
+
diff --git a/Application_examples/FindAdvisor.mp b/Application_examples/FindAdvisor.mp
index dfd51aee5a9d74b131abb4ef77bc1ca188c6ea98..9a164f225b98b27cad70611de90f45e7e3c0db9d 100644
--- a/Application_examples/FindAdvisor.mp
+++ b/Application_examples/FindAdvisor.mp
@@ -1,5 +1,7 @@
-/* example63_Find_Advisor.mp
- modeling human interactions
+/* Model of [FindAdvisor]
+
+example63_Find_Advisor.mp
+modeling human interactions
Human interaction and organizational processes can be modeled as well as technological
system and subsystem interactions.
@@ -18,8 +20,7 @@ produce more scenarios).
The "Sequence" or "Swim Lanes" layouts are the most appropriate for browsing traces here.
The "Sequence" mode yields views very similar to the UML or SysML Sequence Diagrams.
-*/
-
+==========================================================*/
/*—————————————————————————————
Actors
@@ -62,4 +63,4 @@ COORDINATE $a: Recommend_another_approach FROM Advisor,
$b: Find_another_approach FROM Student
DO ADD $a PRECEDES $b; OD;
-Student, Advisor SHARE ALL Discuss_research_interests;
\ No newline at end of file
+Student, Advisor SHARE ALL Discuss_research_interests;
diff --git a/Application_examples/First_Responder.mp b/Application_examples/First_Responder.mp
index 0f25d9d0a75cfc706c9c575a6a9fe8cdb0277c7a..5259d4a9d6e49d865c102e855c12224f993417cf 100644
--- a/Application_examples/First_Responder.mp
+++ b/Application_examples/First_Responder.mp
@@ -1,4 +1,6 @@
-/* A first responder scenario involving the administation of a rescue
+/* Model of [First_Responder]
+
+A first responder scenario involving the administation of a rescue
medication (Narcan) to an overdose victim by a First Responder or a
Bystander.
@@ -9,7 +11,7 @@ scenarios emerged that was previously not considered. Trace 6 and others
show a double administration of Narcan by both the bystander and the first
responder.
-*/
+==========================================================*/
SCHEMA Narcan_Administration
diff --git a/Application_examples/Knapsack_Weight_Limit.mp b/Application_examples/Knapsack_Weight_Limit.mp
index ebe7c4de00ebb093a0cf5f545cb2b2153068062b..3301053af6edef66bf7738fd6164b3f98318609f 100644
--- a/Application_examples/Knapsack_Weight_Limit.mp
+++ b/Application_examples/Knapsack_Weight_Limit.mp
@@ -1,4 +1,6 @@
-/* Example 38 Knapsack
+/* Model of [Knapsack_Weight_Limit]
+
+Example 38 Knapsack
This is a case of well-known Knapsack Dynamic Programming Problem.
In general it is NP-hard and NP-complete
@@ -12,7 +14,9 @@
small N,in particular, it stabilizes at scope 4).
Run for scope 1 and up to 5
-*/
+
+==========================================================*/
+
SCHEMA Knapsack
ATTRIBUTES { number limit, accumulated_total, current_max,
diff --git a/Application_examples/MP_Architecture_Specification.mp b/Application_examples/MP_Architecture_Specification.mp
index 36264184995df0d7cc631065432f261384f703c3..2903eeb7441a984368f6910b3ebe28122c70a644 100644
--- a/Application_examples/MP_Architecture_Specification.mp
+++ b/Application_examples/MP_Architecture_Specification.mp
@@ -1,9 +1,12 @@
-/* Example 28
+/* Model of [MP_Architecture_Specification]
+
+Example 28
MP compiler/trace generator architecture model
run for scope 1 or more
-===================================================*/
+==========================================================*/
+
SCHEMA MP_architecture
ROOT User:
diff --git a/Application_examples/Manufacturing_Process.mp b/Application_examples/Manufacturing_Process.mp
index 6eeb2831553b74ab0df671fb8de519ca3cf5d1f0..bbb615f055363687ecb5b5cc54572460c7e964ed 100644
--- a/Application_examples/Manufacturing_Process.mp
+++ b/Application_examples/Manufacturing_Process.mp
@@ -1,4 +1,4 @@
-/*
+/* Model of [Manufacturing_Process]
Application of Monterey Phoenix Modeling to Manufacturing Product Systems
An example pre-dating MP-Firebird application that was used to generate scenarios
@@ -7,7 +7,7 @@ MP version 4 may be used to conduct such analysis with its native capabilities.
Created by: John Palmer
August 2014
-*/
+==========================================================*/
SCHEMA Manufacturing_System
diff --git a/Application_examples/Martian_Lander.mp b/Application_examples/Martian_Lander.mp
index 10b3b3a4fc8ad6e14215d21f31e284fd1b61b052..2880cb041dd583594f863ed7b3d0081f262797d8 100644
--- a/Application_examples/Martian_Lander.mp
+++ b/Application_examples/Martian_Lander.mp
@@ -1,4 +1,6 @@
-/* Example 45. Real time system behavior modeling.
+/* Model of [Martian_Lander]
+
+Example 45. Real time system behavior modeling.
Landing system for Martian Lander.
MP model written by M.Auguston following example 1 and Appendix B from
@@ -52,7 +54,9 @@ CKDT 10
RRM 10
run for scope 1 and up.
-*/
+
+==========================================================*/
+
SCHEMA Martian_Lander
ROOT Measure_and_display:
diff --git a/Application_examples/Prisoners_Dilemma.mp b/Application_examples/Prisoners_Dilemma.mp
index c9e7f0a5a7954584c82e333cf091311aed42827d..850e37a785634e745e7c866f523646bed122365a 100644
--- a/Application_examples/Prisoners_Dilemma.mp
+++ b/Application_examples/Prisoners_Dilemma.mp
@@ -1,4 +1,6 @@
-/* The Prisoner's Dilemma
+/* Model of [Prisoners_Dilemma]
+
+The Prisoner's Dilemma
Michael Collins
August 10, 2020.
https://en.wikipedia.org/wiki/Prisoner%27s_dilemma
@@ -54,8 +56,7 @@ in all other circumstances the payoff for Bob = 0.
To map it to classic values to show negative payoffs -- that is a sort of normalizing.
The total payoff is computed from the assignments above and then subtracting 2.
-*/
-
+==========================================================*/
/*—————————————————————————————
Actors
@@ -83,4 +84,4 @@ payout_bob := SUM{ $act:( do_not_confess_alice | confess_alice | do_not_confess
Interactions
———————————————————————————————*/
SAY( "Payout Alice = " payout_alice);
-SAY( "Payout Bob = " payout_bob );
\ No newline at end of file
+SAY( "Payout Bob = " payout_bob );
diff --git a/Application_examples/Railroad_Crossing_Safety.mp b/Application_examples/Railroad_Crossing_Safety.mp
index c6c9332e8e18764433ef3a5a683e02a1988d8e57..912828a507c815c41dfb4926fdab742f26ccc27b 100644
--- a/Application_examples/Railroad_Crossing_Safety.mp
+++ b/Application_examples/Railroad_Crossing_Safety.mp
@@ -1,4 +1,5 @@
-/*
+/* Model of [Railroad_Crossing_Safety]
+
Example 27. Timing attribute use.
Railroad crossing example from [Formal Methods for Real-Time Computing, 1996].
@@ -8,7 +9,7 @@ each train enters and exits the crossing’s region.
The main safety requirement is: if a train is in the crossing region,
then gate must be down.
-*/
+==========================================================*/
SCHEMA Railroad_Crossing
diff --git a/Application_examples/Replay_Attack.mp b/Application_examples/Replay_Attack.mp
index 5749bbec43b43fc58ccc58c29120d8ca58160316..29ddd31385218a984dcbfd60e64053b26bd5dc27 100644
--- a/Application_examples/Replay_Attack.mp
+++ b/Application_examples/Replay_Attack.mp
@@ -1,9 +1,12 @@
-/* Example 41. The description of Replay Attack
+/* Model of [Replay_Attack]
+
+Example 41. The description of Replay Attack
is available at
https://en.wikipedia.org/wiki/Replay_attack
run scope up to 5
-======================================*/
+
+==========================================================*/
SCHEMA Replay_Attack
diff --git a/Application_examples/Small_Package_Delivery.mp b/Application_examples/Small_Package_Delivery.mp
index 578f4d30360565601b1893a84ebe5cca0ab0114d..e98252e5e91349fd9ab17dd71bf40f788efde8f8 100644
--- a/Application_examples/Small_Package_Delivery.mp
+++ b/Application_examples/Small_Package_Delivery.mp
@@ -1,4 +1,4 @@
-/* Small Package Delivery
+/* Model of [Small_Package_Delivery]
Taken from use case description in the Skyzer IM20 Mission Model
(Non-Combatant Operations Scenario):
@@ -33,7 +33,7 @@ root (line 36 and lines 114-128) and running that model subset, one can
see 6 event traces, one of which is unexpected: the Air_Vehicle drops
the payload with no vessel in sight (trace 6).
-*/
+==========================================================*/
SCHEMA Small_Package_Delivery
diff --git a/Application_examples/Spent_Fuel_Cooling_and_Cleanup.mp b/Application_examples/Spent_Fuel_Cooling_and_Cleanup.mp
index de834307bf8ff094a53a2febec99c72c546df38c..d3879a0f071d0b2b1d01e26bfb986ca7c58da75f 100644
--- a/Application_examples/Spent_Fuel_Cooling_and_Cleanup.mp
+++ b/Application_examples/Spent_Fuel_Cooling_and_Cleanup.mp
@@ -1,4 +1,6 @@
-/* Cooling Pool
+/* Model of [Spent_Fuel_Cooling_and_Cleanup]
+
+Cooling Pool
created by K.Giammarco 5/4/2020
modified by K.Giammarco 5/8/2020 with D.VanBossuyt
@@ -7,8 +9,7 @@ modified by K.Giammarco 5/13/2020 with D.VanBossuyt
The purpose of this model is to identify the components of and
interactions among a spent nuclear fuel cooling pool and its environment.
-*/
-
+==========================================================*/
/*—————————————————————————————
Actors
diff --git a/Application_examples/Spiral_Software_Process b/Application_examples/Spiral_Software_Process
index f8d21425998fbfe8c472101decf9945a3ff8bc6d..c628ab408f08d99c69e78db15fb97b97f127c56a 100644
--- a/Application_examples/Spiral_Software_Process
+++ b/Application_examples/Spiral_Software_Process
@@ -1,4 +1,6 @@
-/* Example 16, model of the spiral software process
+/* Model of [Spiral_Software_Process]
+
+Example 16, model of the spiral software process
This example also illustrates how Melvin Conway's law
can be modeled in MP: "organizations which design systems ...
@@ -6,7 +8,8 @@
communication structures of these organizations."
run scope up to 5
-======================================*/
+
+==========================================================*/
SCHEMA spiral
diff --git a/Application_examples/Surgery.mp b/Application_examples/Surgery.mp
index 624cc75c1045624d994b5a39bee607b7274e9c43..94a753e2810b25a12c7f5c58d9027f35a2f11033 100644
--- a/Application_examples/Surgery.mp
+++ b/Application_examples/Surgery.mp
@@ -1,4 +1,6 @@
-/* Surgery example
+/* Model of [Surgery]
+
+Surgery example
This model shows an example of decisions made by a leader (Physician),
a subordinate(s) (Nurse(s)), and the Environment as applied in a surgery
setting.
@@ -8,7 +10,8 @@ Available at https://ieeexplore.ieee.org/abstract/document/7994952
Created by: J. Quartuccio (2017)
Naval Postgraduate School
-*/
+
+==========================================================*/
/*Actors*/
SCHEMA Surgery
@@ -83,4 +86,4 @@ ENSURE (#Correct_decision FROM Physician == 1 ->
#Successful_outcome FROM Environment
==1);
ENSURE (#Incorrect_decision FROM Physician == 1 ->
-#Failed_outcome FROM Environment ==1);
\ No newline at end of file
+#Failed_outcome FROM Environment ==1);
diff --git a/Application_examples/Swarm_Search_and_Track.mp b/Application_examples/Swarm_Search_and_Track.mp
index 5677443d7c03c84ca544bc2728b6dcc34e16f02a..1359a151646b929f0e8d4afa1d88a6eaae11f98d 100644
--- a/Application_examples/Swarm_Search_and_Track.mp
+++ b/Application_examples/Swarm_Search_and_Track.mp
@@ -1,4 +1,5 @@
-/*
+/* Model of [Swarm_Search_and_Track]
+
Michael Revill
22 February 2016
Incorporating Failure Modes and Failsafe Behaviors
@@ -14,7 +15,7 @@ Verb-oriented events in title case are states
This model demonstrates the found unexpected behavior for
object discovery after bingo fuel (trace 6)
-*/
+==========================================================*/
SCHEMA Swarm_Search_and_Track
diff --git a/Application_examples/Swarm_UAV.mp b/Application_examples/Swarm_UAV.mp
index b7dcb004945e04a0aa77340182afb1f01afd7c6c..a686609bc017c9971dad1c1b2190e723f13abbbd 100644
--- a/Application_examples/Swarm_UAV.mp
+++ b/Application_examples/Swarm_UAV.mp
@@ -1,4 +1,5 @@
-/*
+/* Model of [Swarm_UAV]
+
Kristin Giammarco and Mikhail Auguston
MP Model based on "Swarm CONOPs" Draft 11 February 2015
11 February 2015 - Initial Model Started by KGiammarco
@@ -9,7 +10,8 @@
This model demonstrates how to get several instances of the same actor (UAV)
coordinated with external events (run for scopes 2 and 3 to see 2 and 3 UAVs,
respectively).
-*/
+
+==========================================================*/
SCHEMA Swarm_UAV
diff --git a/Application_examples/Turtles_in_the_Desert.mp b/Application_examples/Turtles_in_the_Desert.mp
index bedbdb0b29519d639f1fa1bff8dfaf9a88d42b88..4ee3aa0468892faab08885cc3b10a1512b5c3e8b 100644
--- a/Application_examples/Turtles_in_the_Desert.mp
+++ b/Application_examples/Turtles_in_the_Desert.mp
@@ -1,4 +1,6 @@
-/* Example39 turtles.mp
+/* Model of [Turtles_in_the_Desert]
+
+Example39 turtles.mp
Demonstration of the benefits for complete
example set generation in MP.
@@ -24,7 +26,8 @@ Don't try to construct a non-Euclidean geometry to
There are 13 possible scenarios, and none when all three
are telling the truth.
- ==================================*/
+==========================================================*/
+
SCHEMA Turtles
neighbors: { (nobody_before | one_before | two_before ),
diff --git a/Application_examples/UAV_Ingress.mp b/Application_examples/UAV_Ingress.mp
index 9d7d5db3f7ee6f3dc00e437f1069522c34450c49..7276c3ddcbe5d12aaa4820302b830d18f909df19 100644
--- a/Application_examples/UAV_Ingress.mp
+++ b/Application_examples/UAV_Ingress.mp
@@ -1,4 +1,4 @@
-/*******************************************************************
+/* Model of [UAV_Ingress]
UAV HADR Mission
@@ -11,8 +11,7 @@ is acceptable but the operator aborts the ingress (trace 2).
created by A. Constable May 2017
-********************************************************************/
-
+==========================================================*/
SCHEMA UAV_Ingress
diff --git a/Application_examples/UAV_OnStation.mp b/Application_examples/UAV_OnStation.mp
index b0a4843a6de5b0aa90def20feb3aee5dea139043..a793dca50c7b94af3cb141fc87c17caec469d977 100644
--- a/Application_examples/UAV_OnStation.mp
+++ b/Application_examples/UAV_OnStation.mp
@@ -1,4 +1,4 @@
-/*********************************************************************************************
+/* Model of [UAV_OnStation]
A Model for an Unmanned Aerial Vehicle in the OnStation Phase of an ISR Mission
@@ -14,8 +14,7 @@ Paper available at https://ieeexplore.ieee.org/abstract/document/7994950
modified by K.Giammarco on 02-05-2017 to add normal events back to failure mode scenarios
and added annotations
-*********************************************************************************************/
-
+==========================================================*/
SCHEMA UAV_OnStation
diff --git a/Application_examples/Unmanned_Spacecraft_Comms.mp b/Application_examples/Unmanned_Spacecraft_Comms.mp
index 710b2de7af357fa04c29451b6c228a478470eb5e..2b1f670714afae6869f308076fd92c592649e1bd 100644
--- a/Application_examples/Unmanned_Spacecraft_Comms.mp
+++ b/Application_examples/Unmanned_Spacecraft_Comms.mp
@@ -1,4 +1,6 @@
-/* Heartbeat.mp
+/* Model of [Unmanned_Spacecraft_Comms]
+
+Heartbeat.mp
October 4, 2015
Created by: C. Nelson
@@ -9,7 +11,7 @@ the ISS.
Run for scope 1 and up.
-*/
+==========================================================*/
/*—————————————————————————————
Actors
diff --git a/Application_examples/Web_Browser_Formal_Security.mp b/Application_examples/Web_Browser_Formal_Security.mp
index 5c6181c2b66620c1dbe23fbebf301592c0f564b2..86f8c3eb4c34d4af44bb6fb758a721f4c5b38db6 100644
--- a/Application_examples/Web_Browser_Formal_Security.mp
+++ b/Application_examples/Web_Browser_Formal_Security.mp
@@ -1,4 +1,6 @@
-/* Example 40. MP Web browsers formal security model.
+/* Model of [Web_Browser_Formal_Security]
+
+Example 40. MP Web browsers formal security model.
based on the papers by:
@@ -36,7 +38,8 @@ in order to model the vulnerabilities explained in the papers above.
how MP can check whether Client's web query may
be indirectly affected by Bad Server's Redirect intervention.
-==============================================================================*/
+==========================================================*/
+
SCHEMA Web_browser
/* Response may embed some Request events,
diff --git a/Application_examples/Wide_Range_Search_for_Wreckage_and_Survivors b/Application_examples/Wide_Range_Search_for_Wreckage_and_Survivors
index e930176a2b7dbc5bc020ee3929f3a03147a92e4b..6f9e9046b46ea2fe21a169900154d56ff34c9f77 100644
--- a/Application_examples/Wide_Range_Search_for_Wreckage_and_Survivors
+++ b/Application_examples/Wide_Range_Search_for_Wreckage_and_Survivors
@@ -1,4 +1,6 @@
-/* Example8_OperationalProcess.mp
+/* Model of [Wide_Range_Search_for_Wreckage_and_Survivors]
+
+Example8_OperationalProcess.mp
modeling operational processes
Operational processes can be modeled to provide a common baseline against which
@@ -24,8 +26,7 @@ added to this model yet.
The "Sequence" or "Swim Lanes" layouts are the most appropriate for browsing traces here.
The "Sequence" mode yields views very similar to the UML or SysML Sequence Diagrams.
-*/
-
+==========================================================*/
/* Actors */
diff --git a/Application_examples/Work_Productivity.mp b/Application_examples/Work_Productivity.mp
index 65df381f75de10949a8bd56f80d22c734145cab4..8927bcd989a91c0456ecb5b8ce46ba73aa9564e6 100644
--- a/Application_examples/Work_Productivity.mp
+++ b/Application_examples/Work_Productivity.mp
@@ -1,11 +1,15 @@
-/* Example 26, timing attribute use
+/* Model of [Work_Productivity]
+
+Example 26, timing attribute use
also demonstrates how to print all
events present in the trace
with timing attributes
run for scopes 1 and up
-*/
+
+==========================================================*/
+
SCHEMA Delays
Work:
diff --git a/Example01_SimpleMessageFlow_EventCoordination.mp b/Example01_SimpleMessageFlow_EventCoordination.mp
index 9b8074122d9da9b77c551f2603b5690b06d448db..9b604dda1cc74f22d4dd49e386405b745399a643 100644
--- a/Example01_SimpleMessageFlow_EventCoordination.mp
+++ b/Example01_SimpleMessageFlow_EventCoordination.mp
@@ -1,5 +1,4 @@
-/*
-Example1_simple_message_flow.mp
+/* Example 01. Model of [Simple_Message_Flow]
Event grammar rules for each root define derivations for event traces,
in this case a simple sequence of zero or more events for each root.
@@ -12,7 +11,7 @@ The coordination operation behaves as a "cross-cutting" derivation rule.
Run for scopes 1 and up. The "Sequence" or "Swim Lanes" layouts are
the most appropriate for browsing traces here.
-*/
+==========================================================*/
SCHEMA Simple_Message_Flow
diff --git a/Example01a_UnreliableMessageFlow_VirtualEvents.mp b/Example01a_UnreliableMessageFlow_VirtualEvents.mp
index 7368c227075d4df94748fea64e3a2d76b7718bb7..31bd783ef15a5fab3552e50b078bae15c28bdb05 100644
--- a/Example01a_UnreliableMessageFlow_VirtualEvents.mp
+++ b/Example01a_UnreliableMessageFlow_VirtualEvents.mp
@@ -1,13 +1,13 @@
-/* Example 1a
-Unreliable message flow.
+/* Example 01a. Model of [Unreliable_Message_Flow]
We may want to specify behaviors when some messages get lost in the transition.
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 83b39076e55401b0a1c247faa57f8201015787cf..47d18b6e276ae9354eba0feb9c5b97b8f0a43b6b 100644
--- a/Example02_DataFlow_EventSharing.mp
+++ b/Example02_DataFlow_EventSharing.mp
@@ -1,5 +1,6 @@
-/* Example2_DataAsEvents.mp
- data items as behaviors
+/* Example 02. Model of [Data_Flow]
+
+data items as behaviors
MP employs the Abstract Data Type (ADT) principle introduced by
Barbara Liskov to represent data items as operations
@@ -22,7 +23,7 @@ This is a toy example of System_of_Systems emerging behavior modeling.
Run for scopes 1 and up. The "Sequence" or "Swim Lanes" layouts are
the most appropriate for browsing traces here.
-*/
+==========================================================*/
SCHEMA Data_Flow
diff --git a/Example03_ATMWithdrawal_BehaviorOfEnvironment.mp b/Example03_ATMWithdrawal_BehaviorOfEnvironment.mp
index 36b871f75beed38661d3740577aeb32392e98846..245fcaeb0080d63c5164d87b504529c49e103c32 100644
--- a/Example03_ATMWithdrawal_BehaviorOfEnvironment.mp
+++ b/Example03_ATMWithdrawal_BehaviorOfEnvironment.mp
@@ -1,5 +1,6 @@
-/* Example3_ATM_withdrawal.mp
- Integrated system and environment behaviors
+/* Example 03. Model of [ATM_Withdrawal]
+
+Integrated system and environment behaviors
MP separates models of component behaviors and component interactions
to permit elaboration on behaviors of multiple interacting actors.
@@ -25,7 +26,7 @@ By selecting a representative enough trace (containing all events and interactio
like traces 2 or 3 for scope 1), and then collapsing root event, it becomes possible
to view a traditional "box-and-arrow" architecture diagram, i.e. to visualize an architecture view.
-*/
+==========================================================*/
SCHEMA ATM_Withdrawal
diff --git a/Example04b_QueueBehavior_UserDefinedRelations.mp b/Example04b_QueueBehavior_UserDefinedRelations.mp
index fd56e213b635630923105fa016a0285b2bee25be..b22b82ef05b93e533f7b6b526f88439a54d1109c 100644
--- a/Example04b_QueueBehavior_UserDefinedRelations.mp
+++ b/Example04b_QueueBehavior_UserDefinedRelations.mp
@@ -1,4 +1,4 @@
-/* Example4_Stack_behavior.mp
+/* Example 04b. Model of [Queue_Behavior]
The event trace is a set of events and the Boolean expression constructs in MP
can support the traditional first order predicate calculus notation.
@@ -8,9 +8,8 @@ grammar rules, composition operations, and some additional constraints –
ENSURE conditions.
run for scopes 1, 2, 3, and up.
-*/
-/* This rule specifies the behavior of a stack in terms of stack operations
+This rule specifies the behavior of a stack in terms of stack operations
push and pop. It is assumed that initially Stack is empty.
The BUILD block associated with a root or composite event
contains composition operations performed when event trace segment
@@ -27,7 +26,8 @@ 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
diff --git a/Example05_CarRace_NestedComposition.mp b/Example05_CarRace_NestedComposition.mp
index 92fdabd18593939a67fa5f461140bd1ec651588c..766eda91bccf7545f6c952f49c9f090d06a8c77f 100644
--- a/Example05_CarRace_NestedComposition.mp
+++ b/Example05_CarRace_NestedComposition.mp
@@ -1,14 +1,15 @@
-/* Example5_CarRace.mp
+/* Example 05. Model of [Car_Race]
- more coordination patterns:
- - ordering of selected events in concurrent threads
- can be modeled by coordinating them with event sequence;
-
- - one-many coordination.
+more coordination patterns:
+- ordering of selected events in concurrent threads
+ can be modeled by coordinating them with event sequence;
+
+- one-many coordination.
- Run for scopes 1 and up. The "Sequence" or "Swim Lanes"
- layouts are the most appropriate for browsing traces here.
-*/
+Run for scopes 1 and up. The "Sequence" or "Swim Lanes"
+layouts are the most appropriate for browsing traces here.
+
+==========================================================*/
SCHEMA Car_Race
diff --git a/Example06_UnreliableChannel_AssertionChecking.mp b/Example06_UnreliableChannel_AssertionChecking.mp
index 284fd6b869f0747a6c72d6335a36f35ad4b5a305..5a021feabe7963a6faaa1897361f5592fca79683 100644
--- a/Example06_UnreliableChannel_AssertionChecking.mp
+++ b/Example06_UnreliableChannel_AssertionChecking.mp
@@ -1,4 +1,6 @@
-/* Example6 Assertion checking, Communicating via unreliable channel.
+/* Example 06. Model of [Unreliable_Channel]
+
+ 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
@@ -17,7 +19,8 @@
This can significantly speed up the testing process. Of course,
if the property should always hold, it makes sense to convert it
into the ENSURE condition.
-*/
+
+==========================================================*/
SCHEMA Unreliable_Channel
diff --git a/Example07_UnconstrainedStack_TraceAnnotation.mp b/Example07_UnconstrainedStack_TraceAnnotation.mp
index 001d79310f8eec89ec6603416837a36f54a3355a..258745355c1180ebf82c62ba6a303e33f77c266d 100644
--- a/Example07_UnconstrainedStack_TraceAnnotation.mp
+++ b/Example07_UnconstrainedStack_TraceAnnotation.mp
@@ -1,4 +1,6 @@
-/* Example7 Trace annotation techniques
+/* Example 07. Model of [Unconstrained_Stack]
+
+Trace annotation techniques
Assertion checking with the CHECK clause may be the simplest and most
common tool for finding counterexamples of traces, which violate some
@@ -14,7 +16,8 @@ unwanted behaviors. The MP code illustrates how to pinpoint events that
might violate certain property, and how to annotate these particular
events in the trace with additional messages. Programmers will recognize
the use of debugging print statements for traditional program testing/debugging.
-*/
+
+==========================================================*/
SCHEMA Unconstrained_Stack
ROOT Stack: (* ( push | pop [ bang ]) *)
diff --git a/Example08_EmployeeEmployer_CoordinationAcrossHierarchyLevels.mp b/Example08_EmployeeEmployer_CoordinationAcrossHierarchyLevels.mp
index b4423996067a0807558a1252a928e9d1aae4e2d7..92d6736d9baeebdeac72b31e0cf12d0b08da2064 100644
--- a/Example08_EmployeeEmployer_CoordinationAcrossHierarchyLevels.mp
+++ b/Example08_EmployeeEmployer_CoordinationAcrossHierarchyLevels.mp
@@ -1,4 +1,4 @@
-/* Example9_Employee_Employer.mp
+/* Example 08. Model of [Employee_Employer]
The web site http://www.infoq.com/articles/bpelbpm
“Why BPEL is not the holy grail for BPM “
@@ -23,7 +23,8 @@ parallel workflow [in BPEL] that is equivalent to this one ..."
Run for scope 1. The "Sequence" or "Swim Lanes"
layouts are the most appropriate for browsing traces here.
Some box reshuffling may be needed to improve the trace layout.
-*/
+
+==========================================================*/
SCHEMA Employee_Employer
diff --git a/Example09_PipeFilter_TraceAnnotationQueries.mp b/Example09_PipeFilter_TraceAnnotationQueries.mp
index 93047b9df548d758f7f4bee59fc0227b5825f474..2a59ae8a69a96e3cce51f8dba94c3ee3de626623 100644
--- a/Example09_PipeFilter_TraceAnnotationQueries.mp
+++ b/Example09_PipeFilter_TraceAnnotationQueries.mp
@@ -1,4 +1,5 @@
-/* Example10_Pipe_Filter.mp
+/* Example 09. Model of [Pipe_Filter]
+
pipe/filter architecture model with 2 filters
assumptions:
@@ -6,7 +7,8 @@
2) after a message has been sent, it cannot be send repeatedly,
3) received message can stay in the Filter for while,
before being sent (if at all).
-*/
+
+==========================================================*/
SCHEMA Pipe_Filter
diff --git a/Example10_PublishSubscribe_EventReshuffling.mp b/Example10_PublishSubscribe_EventReshuffling.mp
index b885a2ed08874cd27fd08df23391baf5caf8dbfd..45a0b63acc70847e5fe23d5ba129785674c29b53 100644
--- a/Example10_PublishSubscribe_EventReshuffling.mp
+++ b/Example10_PublishSubscribe_EventReshuffling.mp
@@ -1,4 +1,4 @@
-/* Example 11 Publish/Subscribe architecture model.
+/* Example 10. Model of [Publish_Subscribe]
Publisher sends a notification to all active Subscribers
when new information is available.
@@ -6,7 +6,8 @@
scope 1, 1 trace in less than 1 sec.
scope 2, 51 traces in less than 1 sec.
scope 3 3813 traces in approx. 5 min.
-*/
+
+==========================================================*/
SCHEMA Publish_Subscribe
diff --git a/Example11_RingTopology_UserDefinedRelations.mp b/Example11_RingTopology_UserDefinedRelations.mp
index 6c8cf8a7fefbe63c63cb22c6998a400a7e11b12d..0ce90612f833c3039cc743b5f0e4c66231867026 100644
--- a/Example11_RingTopology_UserDefinedRelations.mp
+++ b/Example11_RingTopology_UserDefinedRelations.mp
@@ -1,10 +1,12 @@
-/* ring.mp
+/* Example 11. Model of [Ring_Topology]
+
ring topology
an example of user-defined relation use
The following is a model of network ring,
- where each node interacts with its left and right neighbors only.
-------------------------------------------*/
+ where each node interacts with its left and right neighbors only.
+
+==========================================================*/
SCHEMA Ring_Topology
/* model of networking ring, where each node sends/receives
diff --git a/Example12_CardiacArrestWorkflow_VirtualEvents.mp b/Example12_CardiacArrestWorkflow_VirtualEvents.mp
index 9984e7c127e2c8110e98162acf91558497193155..a29f138af7ff5fd806accba8353b1d0440554ff3 100644
--- a/Example12_CardiacArrestWorkflow_VirtualEvents.mp
+++ b/Example12_CardiacArrestWorkflow_VirtualEvents.mp
@@ -1,4 +1,4 @@
-/* Example18 Workflow pattern
+/* Example 12. Model of [Cardiac_Arrest_Workflow]
the web site
http://workflowpatterns.com/patterns/control/index.php
@@ -13,7 +13,8 @@ is commenced. Completion of the other task is ignored and does not result
in a second instance of the triage task.
run for scope 1
-*/
+
+==========================================================*/
SCHEMA Cardiac_Arrest_Workflow
diff --git a/Example13_ConsumersSuppliers_DependencyTracking.mp b/Example13_ConsumersSuppliers_DependencyTracking.mp
index 7367cdf21b3b724666bd44fd262e65fd5aa23e92..f1a8117f95741353bd72032f34dd60de899fa8af 100644
--- a/Example13_ConsumersSuppliers_DependencyTracking.mp
+++ b/Example13_ConsumersSuppliers_DependencyTracking.mp
@@ -1,4 +1,4 @@
-/* Example 19, Consumers/Suppliers
+/* Example 13. Model of [Consumers_Suppliers]
Asynchronous coordination and dependency definition example.
@@ -8,7 +8,8 @@ single Request_delivery -> Consume chain
on Gryphon:
scope 1, 2 traces, in less than 1 sec.
scope 2, 670 traces, approx. time 2.5 min.
-*/
+
+==========================================================*/
SCHEMA Consumers_Suppliers
diff --git a/Example14_ShoppingSpree_NumberAttributes.mp b/Example14_ShoppingSpree_NumberAttributes.mp
index 22df21c42bb7ac8e85a4ad737af4ea161d0e7d96..f6ce753b261f4f6aba37bc7a5472588e7e2f30d4 100644
--- a/Example14_ShoppingSpree_NumberAttributes.mp
+++ b/Example14_ShoppingSpree_NumberAttributes.mp
@@ -1,4 +1,6 @@
-/* Example23.mp number attribute test */
+/* Example 14. Model of [Shopping_Spree]
+
+==========================================================*/
SCHEMA Shopping_Spree
diff --git a/Example15_BackpackWeight_IntervalAttributes.mp b/Example15_BackpackWeight_IntervalAttributes.mp
index 28132298a57b89e5b99f3844f2e428d76f028277..c596c95d38f88791bc64043fb189109a77ffba32 100644
--- a/Example15_BackpackWeight_IntervalAttributes.mp
+++ b/Example15_BackpackWeight_IntervalAttributes.mp
@@ -1,9 +1,13 @@
-/* Example 25, Use of interval attributes.
+/* Example 15. Model of [Backpack_Weight]
+
+ Use of interval attributes.
+
The task is to load a backpack with items not exceeding
the total weight of 30 units.
There may be several instances of the same item.
run for scopes 1 and up
+
==========================================================*/
SCHEMA Backpack_Weight
diff --git a/Example18_RedGreen_BayesianProbabilityCalculationsType2.mp b/Example18_RedGreen_BayesianProbabilityCalculationsType2.mp
index ec66135921246f9ba5909506747dc2596f7cf48c..a7c160f6d67faf5f5ddeda736f347b8ec4484064 100644
--- a/Example18_RedGreen_BayesianProbabilityCalculationsType2.mp
+++ b/Example18_RedGreen_BayesianProbabilityCalculationsType2.mp
@@ -1,4 +1,6 @@
-/* Example24.mp Bayesian attribute example
+/* Example 18. Model of [Red_Green]
+
+ Bayesian attribute example
Suppose there are 3 red and 2 green balls in a box.
We pick at random three balls, one at a time.
diff --git a/Example19_StackBehavior_BayesianProbabilityCalculationsType2.mp b/Example19_StackBehavior_BayesianProbabilityCalculationsType2.mp
index 1905ece887376ccb36b2b3435f46a63abfe0de29..d8c8db1ea87b6a41c24c9abae5f2a899c691eda5 100644
--- a/Example19_StackBehavior_BayesianProbabilityCalculationsType2.mp
+++ b/Example19_StackBehavior_BayesianProbabilityCalculationsType2.mp
@@ -1,4 +1,4 @@
-/* Example 29
+/* Example 19. Model of [Stack_Behavior]
An example of Bayesian probability calculation.
@@ -23,7 +23,8 @@
ROOT Stack: (*<0..M> ( <<0.75>> push | <<0.25>> pop ) *)
this will require to update the first step in p2 assignment (line 57)
it will become p2 := 1/(M + 1);
-==================================================================*/
+
+==========================================================*/
SCHEMA Stack_Behavior
diff --git a/Example23_CarRace_LocalGraph.mp b/Example23_CarRace_LocalGraph.mp
index 625c9e85a465c6f0d4788fc17751d37aa2da2ccb..6ec84f2b0b5367ffe012f020364c61b994233202 100644
--- a/Example23_CarRace_LocalGraph.mp
+++ b/Example23_CarRace_LocalGraph.mp
@@ -1,6 +1,10 @@
-/* Example 32. Local graph within the event trace.
+/* Example 23. Model of [Car_Race]
+
+ Local graph within the event trace.
run for scope 1 and up
-------------------------------------------------*/
+
+==========================================================*/
+
SCHEMA Car_Race
Car: Start
diff --git a/Example24_Compiler_ComponentDiagram.mp b/Example24_Compiler_ComponentDiagram.mp
index 56eab22a3789249300211bf5a0cf86b555a07b27..f8c232283d3d675238c3b3b939f18ce3441d18d0 100644
--- a/Example24_Compiler_ComponentDiagram.mp
+++ b/Example24_Compiler_ComponentDiagram.mp
@@ -1,4 +1,5 @@
-/* Example 33
+/* Example 24. Model of [Compiler]
+
Compiler front end, bottom-up parser
Lexer and parser in interactive mode.
diff --git a/Example25_Graph_as_Data_Structure.mp b/Example25_Graph_as_Data_Structure.mp
index 77297eed44b18d88a865d6cf2676f116098088d7..019fea311476321a730ac20a02352c45297f578b 100644
--- a/Example25_Graph_as_Data_Structure.mp
+++ b/Example25_Graph_as_Data_Structure.mp
@@ -1,5 +1,6 @@
-/* Example 34.
- Accumulating and rendering statistics from event traces.
+/* Example 25. Model of [Graph_as_Data_Structure]
+
+ Accumulating and rendering statistics from event traces.
Graphs as container data structures
============================================================*/
SCHEMA Graph_as_Data_Structure
diff --git a/Example26_UnreliableMessageFlow_GlobalQuery.mp b/Example26_UnreliableMessageFlow_GlobalQuery.mp
index 86aa2df919a4936063f3ef6b721e44c695123998..84f651dd637e0fb0dc82cc707571c95018d0b8f1 100644
--- a/Example26_UnreliableMessageFlow_GlobalQuery.mp
+++ b/Example26_UnreliableMessageFlow_GlobalQuery.mp
@@ -1,4 +1,6 @@
-/* Example 37 GLOBAL query
+/* Example 26. Model of [Unreliable_Message_Flow]
+
+GLOBAL query
Unreliable message flow.
Assuming that probability for a message to get lost is 0.2,
diff --git a/Example27_AssemblingStatistics_Table_and_Bar_Chart.mp b/Example27_AssemblingStatistics_Table_and_Bar_Chart.mp
index 35172a1e6d489705c97818136eca06bf86cd415e..c3f18e079016599ab10ee3487f24de4f78260941 100644
--- a/Example27_AssemblingStatistics_Table_and_Bar_Chart.mp
+++ b/Example27_AssemblingStatistics_Table_and_Bar_Chart.mp
@@ -1,8 +1,9 @@
-/*
- Example42
+/* Example 27. Model of [Table_and_Bar_Chart]
+
Assembling statistics about a current trace in a TABLE and rendering it.
Table and bar chart example, run for scope 1
-*/
+
+==========================================================*/
SCHEMA Table_and_Bar_Chart
ROOT A: a b c a;
diff --git a/Example28_AssemblingStatistics_Histogram.mp b/Example28_AssemblingStatistics_Histogram.mp
index 18f2402eb5bec97e607644cb78965c70e9324925..908ca95543fca3c0e5e8472edfb4e475a7712866 100644
--- a/Example28_AssemblingStatistics_Histogram.mp
+++ b/Example28_AssemblingStatistics_Histogram.mp
@@ -1,4 +1,5 @@
-/* Example 43
+/* Example 28. Model of [Histogram]
+
Histogram example, run for scopes 1, 2, 3, and up
*/
SCHEMA Histogram
diff --git a/Example29_AssemblingStatistics_Gantt_Chart.mp b/Example29_AssemblingStatistics_Gantt_Chart.mp
index 1463d3c7da2f92a9482c295c83a73e8babd40bd8..dc1ad1b86d876f8023b3c341305cce0d8ca4e28d 100644
--- a/Example29_AssemblingStatistics_Gantt_Chart.mp
+++ b/Example29_AssemblingStatistics_Gantt_Chart.mp
@@ -1,4 +1,5 @@
-/* Example44
+/* Example 29. Model of [Gantt_Chart]
+
Gantt chart example
*/
SCHEMA Gantt_Chart
diff --git a/Example30_MicrowaveOven_ModelingModelChecking.mp b/Example30_MicrowaveOven_ModelingModelChecking.mp
index 416ef7c0587bcf7c691f18ab46e33c9243dd3315..a8c23e4deb2326556bd577ccca330268f8baa7fd 100644
--- a/Example30_MicrowaveOven_ModelingModelChecking.mp
+++ b/Example30_MicrowaveOven_ModelingModelChecking.mp
@@ -1,4 +1,4 @@
-/* Example14, microwave_oven.mp
+/* Example 30. Model of [Microwave_Oven]
example of finite state diagram behavior model,
CTL formula representation in MP, and model checking for a small scope.
@@ -29,7 +29,8 @@
run for:
scope 1 (28 traces, 2 counterexamples, 1.75 sec.)
-*/
+
+==========================================================*/
SCHEMA Microwave_Oven
diff --git a/Example32_Petri_Net.mp b/Example32_Petri_Net.mp
index 6a6546444fc2c2050a6c603c856fca1b14c765eb..01ef7c726ba4fb6df7a2a67911faa645ad85cde5 100644
--- a/Example32_Petri_Net.mp
+++ b/Example32_Petri_Net.mp
@@ -1,4 +1,5 @@
-/* Example15_Petri_net.mp
+/* Example 32. Model of [Petri_Net]
+
modeling Petri net behavior
see the Petri net diagram in Sec. 2.16.2 in the MP v.4 Language Manual
scope 1 (2 traces, 0.02 sec.)
@@ -6,7 +7,8 @@
to obtain in the Global view Petri net diagram
extracted from the event traces, run scope 2
-=======================================================*/
+
+==========================================================*/
SCHEMA Petri_Net
/* behavior of each place and transition
diff --git a/Example33_ATMWithdrawal_StatechartView.mp b/Example33_ATMWithdrawal_StatechartView.mp
index 871883ba606b7ccbe52cbd547ef9b14074a8c961..79a83402139cc4e988b74875c8f39d28be3c3536 100644
--- a/Example33_ATMWithdrawal_StatechartView.mp
+++ b/Example33_ATMWithdrawal_StatechartView.mp
@@ -1,8 +1,9 @@
-/* Example 36.
+/* Example 33. Model of [ATM_Withdrawal]
Extracting Statechart view from MP model.
run for scope 1 and up
+
==========================================================*/
SCHEMA ATM_Withdrawal
diff --git a/Example34_FiniteStateDiagram_PathAnnotation.mp b/Example34_FiniteStateDiagram_PathAnnotation.mp
index fd488cb97d8d34e17b872dcfebe51af6a816d49b..6946cd08910773cff2568782cece1a573bb64735 100644
--- a/Example34_FiniteStateDiagram_PathAnnotation.mp
+++ b/Example34_FiniteStateDiagram_PathAnnotation.mp
@@ -1,4 +1,4 @@
-/* Example13_FiniteStateDiagram.mp
+/* Example 34. Model of [Finite_State_Diagram_with_Path_Annotation]
example of finite state diagram behavior model,
contains non-deterministic transitions (from S1 with symbol a),
@@ -33,7 +33,8 @@
scope 1 (4 traces),
scope 2 (30 traces),
scope 3 (258 traces)
-*/
+
+==========================================================*/
SCHEMA Finite_State_Diagram_with _Path_Annotation
diff --git a/Example35_FiniteStateDiagram_PathDiagram.mp b/Example35_FiniteStateDiagram_PathDiagram.mp
index b642abb13f7456344b67b2780bd13457cf51dfb2..7b6af2b8227a651b3a9c6c1025ba5f4dfedfae63 100644
--- a/Example35_FiniteStateDiagram_PathDiagram.mp
+++ b/Example35_FiniteStateDiagram_PathDiagram.mp
@@ -1,9 +1,10 @@
-/* Example 35.
+/* Example 35. Model of [Finite_State_Diagram_with_Path_Diagram]
Adding path and state transition diagrams to
the Finite Automaton behavior model.
run for scope 2
+
==========================================================*/
SCHEMA Finite_State_Diagram_with_Path_Diagram
diff --git a/Example36_Authentication_SystemReuse.mp b/Example36_Authentication_SystemReuse.mp
index 56a1c43bddc0206ae6b19f1b9dc4e727503cf4e8..993b889edf3882feae7e47550271038f8e39fc61 100644
--- a/Example36_Authentication_SystemReuse.mp
+++ b/Example36_Authentication_SystemReuse.mp
@@ -1,6 +1,5 @@
-SCHEMA Authentication_System
-
-/* Example 20.
+/* Example 36. Model of [Authentication_System]
+
Authentication system's behavior for reuse with MAP operation.
run for scope 3 or more to see attempts_exhausted event
@@ -8,6 +7,9 @@ SCHEMA Authentication_System
since the User will copy all Requestor's behavior
============== reused MP code starts here ==================*/
+
+SCHEMA Reuse_of_a_system
+
ROOT Data_Base: (* check_ID *);
ROOT Authentication_Service:
diff --git a/Example37_Compiler1_ComponentReuse.mp b/Example37_Compiler1_ComponentReuse.mp
index b691978ea61874f72a347a40a978711d5e6c1e7f..1b90df9d7c29ab0a5212e8166e92aba64e202706 100644
--- a/Example37_Compiler1_ComponentReuse.mp
+++ b/Example37_Compiler1_ComponentReuse.mp
@@ -1,5 +1,6 @@
-/* Example 21
- Compiler front end,
+/* Example 37. Model of [Compiler1]
+
+ Compiler front end,
bottom-up parser
Lexer and parser in batch mode
@@ -7,7 +8,8 @@ run for
scope 1, 2 traces, less than 1 sec.
scope 2, 147 traces, approx. time 0.87 sec.
scope 3, 11988 traces, approx. time 148 sec.
-====================================================*/
+
+==========================================================*/
SCHEMA Compiler1
diff --git a/Example38_Compiler2_ComponentReuse.mp b/Example38_Compiler2_ComponentReuse.mp
index 3874d70063e5a162dbf0f77a20f4bf0bd0262f43..1c2fc025b06598e6ade7be5bdf3c19978a7c888a 100644
--- a/Example38_Compiler2_ComponentReuse.mp
+++ b/Example38_Compiler2_ComponentReuse.mp
@@ -1,5 +1,6 @@
-/* Example 22
- Compiler front end,
+/* Example 38. Model of [Compiler2]
+
+ Compiler front end,
bottom-up parser
Lexer and parser in interaction mode
@@ -7,7 +8,8 @@ run for
scope 1, 2 traces, less than 1 sec.
scope 2, 111 traces, approx. time 0.65 sec.
scope 3, 4860 traces, approx. time 55 sec.
-====================================================*/
+
+==========================================================*/
SCHEMA Compiler2