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 0ea964f0c5e1a5d3a3606c2f1e02bec47ca3fad6..61cfaf9869eedebd3ec599ff96232e617ee6e1b8 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 d714bd0c5ba15a37e7cebecd62e4b7ba4df54d5a..31bd783ef15a5fab3552e50b078bae15c28bdb05 100644
--- a/Example01a_UnreliableMessageFlow_VirtualEvents.mp
+++ b/Example01a_UnreliableMessageFlow_VirtualEvents.mp
@@ -1,12 +1,12 @@
-/* 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
ROOT Sender: (* send *);
ROOT Receiver: (* (receive | does_not_receive) *);
diff --git a/Example02_DataFlow_EventSharing.mp b/Example02_DataFlow_EventSharing.mp
index 811e1de5c05900631a534383e10924fd91038d20..1015c8c24350af7db9534724f0c865a74739ad4c 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 0c33381eeedc80f433f26581a87f283271eb48f1..69f18a3cda77892f8eec74b806dbfc62f204c3f6 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
@@ -80,4 +81,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/Example04b_QueueBehavior_UserDefinedRelations.mp b/Example04b_QueueBehavior_UserDefinedRelations.mp
index 0c660075f65c5c6248d423abf77219494b29c336..bc6a37d22214e57189dac1901786bc1b0c2f1ca9 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 4f6a8fd1696640cb494f27500d720ebb288be6c6..0a5d65f5666214223c6a800cee25d1acfa1eea50 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 Example5_Car_Race
diff --git a/Example06_UnreliableChannel_AssertionChecking.mp b/Example06_UnreliableChannel_AssertionChecking.mp
index 61d2cdd5ddbcfc7abbdceb49229fa295b8a4fb03..22437cefb4814977fcf524dee2cffe33de86b122 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 AtoB
diff --git a/Example07_UnconstrainedStack_TraceAnnotation.mp b/Example07_UnconstrainedStack_TraceAnnotation.mp
index 817cee81c00edf2727d9cdd9a669b80d280eb5bb..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 ]) *)
@@ -47,4 +50,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/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 63896c93432204eb441999ce30cdc279d45a82f6..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
@@ -52,4 +54,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/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 d3dcba336d47cf365b1ea1017c60c6ae41bf21c8..44e84786c4bb1e03722e479a2ea5dea1c01e0ae2 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
/* model of networking ring, where each node sends/receives
diff --git a/Example12_CardiacArrestWorkflow_VirtualEvents.mp b/Example12_CardiacArrestWorkflow_VirtualEvents.mp
index 6c3b9601b4316f26231d0145cbcb7db6601c78e7..76c9b85632f4be2b58f1e745dd8155b43b5254f8 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
diff --git a/Example13_ConsumersSuppliers_DependencyTracking.mp b/Example13_ConsumersSuppliers_DependencyTracking.mp
index cb771e90ffca161946487229e76e2359ff87cc8a..1ee9d9ac3480bd6b9c7e0af376c389f89cc266d8 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 Suppliers
diff --git a/Example14_ShoppingSpree_NumberAttributes.mp b/Example14_ShoppingSpree_NumberAttributes.mp
index a0405536bb737d65c41b996e273fcf80c12c5037..3a0bb725727da958f7ef954af23000612cedc2a9 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 cfef3eb3d82e9c64579cae0d7288b7571e4e0aa5..643b66bd5e480827cf9f301c8286313fa04bced2 100644
--- a/Example15_BackpackWeight_IntervalAttributes.mp
+++ b/Example15_BackpackWeight_IntervalAttributes.mp
@@ -1,10 +1,15 @@
-/* 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
ATTRIBUTES{ interval weight; };
diff --git a/Example18_RedGreen_BayesianProbabilityCalculationsType2.mp b/Example18_RedGreen_BayesianProbabilityCalculationsType2.mp
index 5022d189337f73d5b9c6343a766ba09eeb0aeeab..043925922c2ba5c5cf0e2d3ca9e62f3d1aae0d02 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.
@@ -12,7 +14,9 @@
constant for the whole derivation process.
run for scope 1
-*/
+
+==========================================================*/
+
SCHEMA RedGreen
ATTRIBUTES{ number selection_probability; };
diff --git a/Example19_StackBehavior_BayesianProbabilityCalculationsType2.mp b/Example19_StackBehavior_BayesianProbabilityCalculationsType2.mp
index b0fc26dbd9263b07ec7b73467da1566e9f259b92..f46cc9d12d596098438db42c843e1d2e774d1678 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 stack1
diff --git a/Example21_DataFlow_LocalReport.mp b/Example21_DataFlow_LocalReport.mp
index 0271dd2c88233d5fb169237fedbaa2204edc6ee4..a8fa082d5ff625372e5cba5e89c54130dbb16b91 100644
--- a/Example21_DataFlow_LocalReport.mp
+++ b/Example21_DataFlow_LocalReport.mp
@@ -1,7 +1,11 @@
-
-/* Example 30. Local Report within a trace.
- run for scope 1 and up.
-*/
+/* Example 21. Model of [Data_Flow]
+
+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 ad102ee91a6a0220854021bff9da9e385119ee92..b8bb2adad55b0bd197c2ef73bb7b917837217eee 100644
--- a/Example22_SimpleMessageFlow_GlobalReport.mp
+++ b/Example22_SimpleMessageFlow_GlobalReport.mp
@@ -1,6 +1,9 @@
-/* Example 31. Global report.
+/* Example 22. Model of [Simple_Message_Flow]
+
run for scope 1 and up
------------------------------*/
+
+==========================================================*/
+
SCHEMA simple_message_flow
ROOT Sender: (* send *);
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 5c1236ec9fc52bff59c61e00fa75594f76fedc25..cc761dd52c6bcabcdfd0eda13e64de63ae01ecb8 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.
@@ -10,7 +11,8 @@
run for
scope 1, 20 traces, approx. 5 sec.
-====================================================*/
+==========================================================*/
+
SCHEMA compiler_example
ROOT Source_code: (+<1.. $$scope + 1>
diff --git a/Example25_Graph_as_Data_Structure.mp b/Example25_Graph_as_Data_Structure.mp
index 873759c781757149f84a0b2642b20dc4adcd44b8..bd472e8ee470ad08859bb61ac817fb10c9510856 100644
--- a/Example25_Graph_as_Data_Structure.mp
+++ b/Example25_Graph_as_Data_Structure.mp
@@ -1,7 +1,10 @@
-/* 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 Statistics
ROOT A: (* ( a | b) *);
ROOT B: (+ c +);
diff --git a/Example26_UnreliableMessageFlow_GlobalQuery.mp b/Example26_UnreliableMessageFlow_GlobalQuery.mp
index d6f37e17a2f685fa129f560b3cae2711caae5099..e7c1cdb446b3b345c9662653b030ac02c8895016 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,
@@ -15,7 +17,9 @@ 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
ROOT Sender: (+ send +);
diff --git a/Example27_AssemblingStatistics_Table_and_Bar_Chart.mp b/Example27_AssemblingStatistics_Table_and_Bar_Chart.mp
index dade7edfb50152ab420057c88fe4d2ebbb1150ae..2909722664c0909563b0c0895d57ff43c41a9ccf 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 Example
ROOT A: a b c a;
diff --git a/Example28_AssemblingStatistics_Histogram.mp b/Example28_AssemblingStatistics_Histogram.mp
index c40bdfa07024449cf9eaed6019578d65aafe051f..1a316cb419c450cfe81688858c33cdd6f80a8f5b 100644
--- a/Example28_AssemblingStatistics_Histogram.mp
+++ b/Example28_AssemblingStatistics_Histogram.mp
@@ -1,6 +1,9 @@
-/* Example 43
+/* Example 28. Model of [Histogram]
+
Histogram example, run for scopes 1, 2, 3, and up
-*/
+
+==========================================================*/
+
SCHEMA Example
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..b68924593b8da4f4e0994461f4cd69493e0e83e3 100644
--- a/Example29_AssemblingStatistics_Gantt_Chart.mp
+++ b/Example29_AssemblingStatistics_Gantt_Chart.mp
@@ -1,6 +1,9 @@
-/* Example44
+/* Example 29. Model of [Gantt_Chart]
+
Gantt chart example
-*/
+
+==========================================================*/
+
SCHEMA S
ROOT A: a1 a2;
diff --git a/Example30_MicrowaveOven_ModelingModelChecking.mp b/Example30_MicrowaveOven_ModelingModelChecking.mp
index fa6ad1cab52efde09ccde8b0361c9edc2bd051fc..a45440df87091e46135372a773c578cd6feb6e31 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 oven
diff --git a/Example32_Petri_Net.mp b/Example32_Petri_Net.mp
index b0ecf3becf6a41206e611e1fb1438a76fad6f5f5..a350b9f4b32d4f93defdfe5fe93b205335c8f700 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 f41f30f641c63d9521dfe27e34c1781395d4d882..d679b4d0e17baf137d3e9e520e4a8024a23f7f1d 100644
--- a/Example33_ATMWithdrawal_StatechartView.mp
+++ b/Example33_ATMWithdrawal_StatechartView.mp
@@ -1,9 +1,11 @@
-/* Example 36.
+/* Example 33. Model of [ATM_Withdrawal]
Extracting Statechart view from MP model.
run for scope 1 and up
+
==========================================================*/
+
SCHEMA ATM_withdrawal_with_Statechart_view
ROOT Customer: (* insert_card
diff --git a/Example34_FiniteStateDiagram_PathAnnotation.mp b/Example34_FiniteStateDiagram_PathAnnotation.mp
index 90b775634588e05da0c86ff492d65dc9b3949e01..e20c8477120e999691419756330a221c6f58e49e 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 FiniteStateDiagram
diff --git a/Example35_FiniteStateDiagram_PathDiagram.mp b/Example35_FiniteStateDiagram_PathDiagram.mp
index ff0ca8160c4696f5154ba4491eac0ad2b88b95d3..be477cbc91b941002c3468551f81bc4b3c13fa56 100644
--- a/Example35_FiniteStateDiagram_PathDiagram.mp
+++ b/Example35_FiniteStateDiagram_PathDiagram.mp
@@ -1,10 +1,12 @@
-/* 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
ROOT S1_behavior:
diff --git a/Example36_Authentication_SystemReuse.mp b/Example36_Authentication_SystemReuse.mp
index c09d654b8a85e7deac2951b79e8f5049c06ed9b2..993b889edf3882feae7e47550271038f8e39fc61 100644
--- a/Example36_Authentication_SystemReuse.mp
+++ b/Example36_Authentication_SystemReuse.mp
@@ -1,6 +1,5 @@
-SCHEMA Reuse_of_a_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 Reuse_of_a_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 371f385233024744bdf39fae36ce112121a6f447..87ba688b653986efc082ad94078331607021e273 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 b18d9af47f41bf5a8b60a61f6f7e72744f52c7c3..81a64a0294f4ea4ef9a98a120c5803659fbc70c2 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