From bd04fc77220c849e0ccaab44492f8c48c623276d Mon Sep 17 00:00:00 2001
From: Pamela Dyer <pamela.dyer@uconn.edu>
Date: Sun, 26 Dec 2021 20:07:46 -0800
Subject: [PATCH] Pamela 3 into Pamela 4
---
...roduction_Platform_Customer_Interactions.mp | 2 +-
...uction_Platform_Supply_Chain_Interaction.mp | 2 +-
.../Application_Process.mp | 2 +-
.../Aspect_Oriented_Paradigm.mp | 2 +-
models/Application_examples/Authentication.mp | 2 +-
models/Application_examples/Autonomous_Car.mp | 2 +-
.../Application_examples/Beginner_Use_of_MP.mp | 8 ++++----
models/Application_examples/CargoScreening.mp | 2 +-
.../Application_examples/Commercial_Flight.mp | 2 +-
...orrelation_and_Fusion_Process_Ungoverned.mp | 2 +-
..._and_Fusion_Process_with_Data_Governance.mp | 2 +-
models/Application_examples/Cycle_Pattern.mp | 4 ++--
.../Dining_Philosophers.mp | 2 +-
models/Application_examples/Elevator.mp | 6 +++---
.../Falcon_9_Launch_with_Gantt.mp | 2 +-
models/Application_examples/FindAdvisor.mp | 2 +-
models/Application_examples/First_Responder.mp | 2 +-
.../Knapsack_Weight_Limit.mp | 2 +-
.../MP_Architecture_Specification.mp | 2 +-
.../Manufacturing_Process.mp | 2 +-
models/Application_examples/Martian_Lander.mp | 18 +++++++++---------
.../Application_examples/Prisoners_Dilemma.mp | 2 +-
.../Railroad_Crossing_Safety.mp | 2 +-
models/Application_examples/Replay_Attack.mp | 2 +-
.../Small_Package_Delivery.mp | 2 +-
.../Spent_Fuel_Cooling_and_Cleanup.mp | 2 +-
.../Spiral_Software_Process.mp | 2 +-
.../Supply_Chain_with_Two_Cyber_Threats.mp | 2 +-
models/Application_examples/Surgery.mp | 2 +-
.../Swarm_Search_and_Track.mp | 2 +-
models/Application_examples/Swarm_UAV.mp | 2 +-
.../Turtles_in_the_Desert.mp | 2 +-
models/Application_examples/UAV_Ingress.mp | 4 ++--
models/Application_examples/UAV_OnStation.mp | 2 +-
.../Unmanned_Spacecraft_Comms.mp | 2 +-
.../Web_Browser_Formal_Security.mp | 2 +-
..._Range_Search_for_Wreckage_and_Survivors.mp | 2 +-
.../Application_examples/Work_Productivity.mp | 2 +-
...le01_SimpleMessageFlow_EventCoordination.mp | 6 +++---
...e01a_UnreliableMessageFlow_VirtualEvents.mp | 2 +-
models/Example02_DataFlow_EventSharing.mp | 2 +-
...le03_ATMWithdrawal_BehaviorOfEnvironment.mp | 2 +-
.../Example04_StackBehavior_EnsureCondition.mp | 2 +-
...le04a_StackBehavior_UserDefinedRelations.mp | 2 +-
...le04b_QueueBehavior_UserDefinedRelations.mp | 2 +-
models/Example05_CarRace_NestedComposition.mp | 2 +-
...le06_UnreliableChannel_AssertionChecking.mp | 2 +-
...ple07_UnconstrainedStack_TraceAnnotation.mp | 2 +-
...ployer_CoordinationAcrossHierarchyLevels.mp | 2 +-
...le09_CardiacArrestWorkflow_VirtualEvents.mp | 2 +-
...mple10_PipeFilter_TraceAnnotationQueries.mp | 2 +-
...ublishSubscribe_AsynchronousCoordination.mp | 2 +-
...mple12_RingTopology_UserDefinedRelations.mp | 2 +-
...13_ConsumersSuppliers_DependencyTracking.mp | 2 +-
...Example14_ShoppingSpree_NumberAttributes.mp | 2 +-
...mple15_BackpackWeight_IntervalAttributes.mp | 2 +-
...ackBehavior_ProbabilityCalculationsType1.mp | 2 +-
...haredEvents_ProbabilityCalculationsType1.mp | 2 +-
...een_BayesianProbabilityCalculationsType2.mp | 2 +-
...ior_BayesianProbabilityCalculationsType2.mp | 2 +-
models/Example20_Activity_Diagram.mp | 2 +-
models/Example21_DataFlow_LocalReport.mp | 2 +-
...ple22_UnreliableMessageFlow_GlobalReport.mp | 2 +-
models/Example23_CarRace_LocalGraph.mp | 2 +-
...Example24_ATMWithdrawal_ComponentDiagram.mp | 2 +-
models/Example24a_Compiler_ComponentDiagram.mp | 2 +-
models/Example25_Graph_as_Data_Structure.mp | 2 +-
...mple26_UnreliableMessageFlow_GlobalQuery.mp | 8 ++++----
models/Example27_Table_and_Bar_Chart.mp | 2 +-
models/Example28_Histogram.mp | 2 +-
models/Example29_Gantt_Chart.mp | 2 +-
...le30_MicrowaveOven_ModelingModelChecking.mp | 2 +-
models/Example31_Petri_Net.mp | 2 +-
.../Example32_ATMWithdrawal_StatechartView.mp | 2 +-
...mple33_FiniteStateDiagram_PathAnnotation.mp | 2 +-
...Example34_FiniteStateDiagram_PathDiagram.mp | 2 +-
models/Example35_Authentication_SystemReuse.mp | 2 +-
models/Example36_Compiler1_ComponentReuse.mp | 2 +-
models/Example37_Compiler2_ComponentReuse.mp | 2 +-
...8_Merging_Root_Events_to_Reduce_Run_Time.mp | 2 +-
...vent_Sharing_Using_COORDINATE_with_SHARE.mp | 12 ++++++------
.../Event_Sharing_in_Composite_Events.mp | 18 +++++++++---------
82 files changed, 115 insertions(+), 115 deletions(-)
diff --git a/models/Application_examples/Agile_Production_Platform_Customer_Interactions.mp b/models/Application_examples/Agile_Production_Platform_Customer_Interactions.mp
index 6a5b45e..fd755a1 100644
--- a/models/Application_examples/Agile_Production_Platform_Customer_Interactions.mp
+++ b/models/Application_examples/Agile_Production_Platform_Customer_Interactions.mp
@@ -18,7 +18,7 @@
│*│ │ Platform" (APP). Here the order is for face │ │
│*│ │ shields in response to the COVID-19 pandemic. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model demonstrates using MP to find both │ │
│*│ │ desired and undesired scenarios of Personal │ │
diff --git a/models/Application_examples/Agile_Production_Platform_Supply_Chain_Interaction.mp b/models/Application_examples/Agile_Production_Platform_Supply_Chain_Interaction.mp
index 216843c..89526e2 100644
--- a/models/Application_examples/Agile_Production_Platform_Supply_Chain_Interaction.mp
+++ b/models/Application_examples/Agile_Production_Platform_Supply_Chain_Interaction.mp
@@ -15,7 +15,7 @@
│*│ │ material on-hand to produce the component │ │
│*│ │ correctly. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model demonstrates using MP to find both │ │
│*│ │ desired and undesired scenarios resulting from │ │
diff --git a/models/Application_examples/Application_Process.mp b/models/Application_examples/Application_Process.mp
index c430342..45c7741 100644
--- a/models/Application_examples/Application_Process.mp
+++ b/models/Application_examples/Application_Process.mp
@@ -9,7 +9,7 @@
│*│ │ To provide a template for an application approval │ │
│*│ │ process involving multiple levels of approval. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ An applicant submits application and needs to get │ │
│*│ │ it approved by the bureaucratic chain of two │ │
diff --git a/models/Application_examples/Aspect_Oriented_Paradigm.mp b/models/Application_examples/Aspect_Oriented_Paradigm.mp
index 787510e..192a503 100644
--- a/models/Application_examples/Aspect_Oriented_Paradigm.mp
+++ b/models/Application_examples/Aspect_Oriented_Paradigm.mp
@@ -9,7 +9,7 @@
│*│ │ To demonstrate the Aspect-Oriented Programming │ │
│*│ │ paradigm in MP. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ Aspect-Oriented Programming (AOP) [Kiczales et al. │ │
│*│ │ 1997] is a programming approach that separates the │ │
diff --git a/models/Application_examples/Authentication.mp b/models/Application_examples/Authentication.mp
index ebead15..1dd8c28 100644
--- a/models/Application_examples/Authentication.mp
+++ b/models/Application_examples/Authentication.mp
@@ -14,7 +14,7 @@
│*│ │ To demonstrate how to reject unwanted behaviors │ │
│*│ │ with ENSURE constraints. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model demonstrates how to correctly model a │ │
│*│ │ simple user authentication system with ENSURE │ │
diff --git a/models/Application_examples/Autonomous_Car.mp b/models/Application_examples/Autonomous_Car.mp
index eb7aa5b..744b001 100644
--- a/models/Application_examples/Autonomous_Car.mp
+++ b/models/Application_examples/Autonomous_Car.mp
@@ -11,7 +11,7 @@
│*│ │ To illustrate the use of COORDINATE statements to │ │
│*│ │ improve the quality of trace analysis. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This is a model of an autonomous car that was │ │
│*│ │ developed as part of a student project to support │ │
diff --git a/models/Application_examples/Beginner_Use_of_MP.mp b/models/Application_examples/Beginner_Use_of_MP.mp
index 71fd182..2d9302a 100644
--- a/models/Application_examples/Beginner_Use_of_MP.mp
+++ b/models/Application_examples/Beginner_Use_of_MP.mp
@@ -15,7 +15,7 @@
│*│ │ 2) the modeling process of formalizing a previously│ │
│*│ │ unstated assumption. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model provides an orientation for those just │ │
│*│ │ getting started using MP-Firebird. The text editor │ │
@@ -27,12 +27,12 @@
│*│ │ scope slider bar next to the Run button to control │ │
│*│ │ the number of loop iterations. │ │
│*│ │ │ │
-│*│ │ ROOT A: B C; A is a root event that includes │ │
+│*│ │ ROOT A: B C; A is a root event that includes │ │
│*│ │ events B followed by C │ │
│*│ │ ( B | C ) Alternative events B or C (but not │ │
│*│ │ both together in the same trace) │ │
-│*│ │ (* B *) iterate B zero or more times │ │
-│*│ │ { B , C } B and C are unordered │ │
+│*│ │ (* B *) iterate B zero or more times │ │
+│*│ │ { B , C } B and C are unordered │ │
│*│ └────────────────────────────────────────────────────┘ │
│*│ │
│*│ ┌─[ References ]─────────────────────────────────────┠│
diff --git a/models/Application_examples/CargoScreening.mp b/models/Application_examples/CargoScreening.mp
index c1c2633..8bec9d3 100644
--- a/models/Application_examples/CargoScreening.mp
+++ b/models/Application_examples/CargoScreening.mp
@@ -12,7 +12,7 @@
│*│ │ logic, in this case outlining a cargo screening │ │
│*│ │ process. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model demonstrates using composite statements │ │
│*│ │ under roots to make a long chain of logic. This │ │
diff --git a/models/Application_examples/Commercial_Flight.mp b/models/Application_examples/Commercial_Flight.mp
index a1a5dc5..5da79d3 100644
--- a/models/Application_examples/Commercial_Flight.mp
+++ b/models/Application_examples/Commercial_Flight.mp
@@ -13,7 +13,7 @@
│*│ │ statements to make a web of actions linked │ │
│*│ │ together through phases. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model demonstrates the interlacing of root │ │
│*│ │ events as Phases and as Actors, in order to model │ │
diff --git a/models/Application_examples/Correlation_and_Fusion_Process_Ungoverned.mp b/models/Application_examples/Correlation_and_Fusion_Process_Ungoverned.mp
index 6f5065f..edc3f6d 100644
--- a/models/Application_examples/Correlation_and_Fusion_Process_Ungoverned.mp
+++ b/models/Application_examples/Correlation_and_Fusion_Process_Ungoverned.mp
@@ -11,7 +11,7 @@
│*│ │ reporting data flows showing existing data path │ │
│*│ │ behaviors. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ Models the data flow from sensors all the way to │ │
│*│ │ the human analyst at a tactical location. The │ │
diff --git a/models/Application_examples/Correlation_and_Fusion_Process_with_Data_Governance.mp b/models/Application_examples/Correlation_and_Fusion_Process_with_Data_Governance.mp
index 76d2d94..1e1d516 100644
--- a/models/Application_examples/Correlation_and_Fusion_Process_with_Data_Governance.mp
+++ b/models/Application_examples/Correlation_and_Fusion_Process_with_Data_Governance.mp
@@ -12,7 +12,7 @@
│*│ │ data path behaviors with the application of a data │ │
│*│ │ governance framework. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ Models the data flow from sensors all the way to │ │
│*│ │ the human analyst at a tactical location │ │
diff --git a/models/Application_examples/Cycle_Pattern.mp b/models/Application_examples/Cycle_Pattern.mp
index 2c4c4b3..08b2877 100644
--- a/models/Application_examples/Cycle_Pattern.mp
+++ b/models/Application_examples/Cycle_Pattern.mp
@@ -12,9 +12,9 @@
│*│ │ can be modeled in MP, and to show how rule-based │ │
│*│ │ comments can be added to the traces. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
-│*│ │ The model below describes a cyclein terms of a │ │
+│*│ │ The model below describes a cycle in terms of a │ │
│*│ │ series of one or more steps, each step either │ │
│*│ │ moving the system "forward" or "backward" as the │ │
│*│ │ process unfolds. "Forward" and "backward" are │ │
diff --git a/models/Application_examples/Dining_Philosophers.mp b/models/Application_examples/Dining_Philosophers.mp
index a00b032..efa7e50 100644
--- a/models/Application_examples/Dining_Philosophers.mp
+++ b/models/Application_examples/Dining_Philosophers.mp
@@ -11,7 +11,7 @@
│*│ │ solving capabilities of MP, using the dining │ │
│*│ │ philosophers problem as the topic. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model demonstrates using COORDINATE, ENSURE, │ │
│*│ │ and IF statements to come up with an answer to a │ │
diff --git a/models/Application_examples/Elevator.mp b/models/Application_examples/Elevator.mp
index 244dc8e..62ca21c 100644
--- a/models/Application_examples/Elevator.mp
+++ b/models/Application_examples/Elevator.mp
@@ -11,17 +11,17 @@
│*│ │ be beneficial, because it can lead to emergent │ │
│*│ │ behavior showing up in the traces. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This demonstrates the modeling of situations and │ │
│*│ │ consequential events in MP. The pattern is: │ │
│*│ │ │ │
-│*│ │ ( SituationA do_one_thing | │ │
+│*│ │ ( SituationA do_one_thing | │ │
│*│ │ SituationB do_another_thing ) │ │
│*│ │ │ │
│*│ │ in the case of this model, │ │
│*│ │ │ │
-│*│ │ ( Elevator_works_fine Get_Off | │ │
+│*│ │ ( Elevator_works_fine Get_Off | │ │
│*│ │ Emergency_Situation Call_for_help ) │ │
│*│ │ │ │
│*│ │ Ultimately, this is a simple model of an emergency │ │
diff --git a/models/Application_examples/Falcon_9_Launch_with_Gantt.mp b/models/Application_examples/Falcon_9_Launch_with_Gantt.mp
index 2f768c1..abd4adb 100644
--- a/models/Application_examples/Falcon_9_Launch_with_Gantt.mp
+++ b/models/Application_examples/Falcon_9_Launch_with_Gantt.mp
@@ -13,7 +13,7 @@
│*│ │ and first stage booster recover through system │ │
│*│ │ behavior modeling. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ A Falcon 9 Rocket is a two booster stage rocket │ │
│*│ │ that is designed to carry payloads into space │ │
diff --git a/models/Application_examples/FindAdvisor.mp b/models/Application_examples/FindAdvisor.mp
index 630b8cd..1607147 100644
--- a/models/Application_examples/FindAdvisor.mp
+++ b/models/Application_examples/FindAdvisor.mp
@@ -10,7 +10,7 @@
│*│ │ To show that human interaction and organizational │ │
│*│ │ processes can be modeled using MP. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ Alternate behaviors for humans are described in │ │
│*│ │ terms of possible decisions they could make. This │ │
diff --git a/models/Application_examples/First_Responder.mp b/models/Application_examples/First_Responder.mp
index 8a15136..1593181 100644
--- a/models/Application_examples/First_Responder.mp
+++ b/models/Application_examples/First_Responder.mp
@@ -12,7 +12,7 @@
│*│ │ administation of a rescue medication (Narcan) to │ │
│*│ │ an overdose victim. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model demonstrates the administration of │ │
│*│ │ Narcan by bystanders in order to determine the │ │
diff --git a/models/Application_examples/Knapsack_Weight_Limit.mp b/models/Application_examples/Knapsack_Weight_Limit.mp
index 2404923..45d1426 100644
--- a/models/Application_examples/Knapsack_Weight_Limit.mp
+++ b/models/Application_examples/Knapsack_Weight_Limit.mp
@@ -11,7 +11,7 @@
│*│ │ optimal solutions in a certain scope, with a limit │ │
│*│ │ set for the weight of the knapsack. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This is a case of well-known Knapsack Dynamic │ │
│*│ │ Programming Problem. In general it is NP-hard and │ │
diff --git a/models/Application_examples/MP_Architecture_Specification.mp b/models/Application_examples/MP_Architecture_Specification.mp
index 861af21..7b8edc7 100644
--- a/models/Application_examples/MP_Architecture_Specification.mp
+++ b/models/Application_examples/MP_Architecture_Specification.mp
@@ -11,7 +11,7 @@
│*│ │ MP compiler/trace generator components built from │ │
│*│ │ the component behaviors. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model demonstrates how a user might use an MP │ │
│*│ │ IDE to extract a component diagram from an MP │ │
diff --git a/models/Application_examples/Manufacturing_Process.mp b/models/Application_examples/Manufacturing_Process.mp
index 2ece47e..c8ffe97 100644
--- a/models/Application_examples/Manufacturing_Process.mp
+++ b/models/Application_examples/Manufacturing_Process.mp
@@ -10,7 +10,7 @@
│*│ │ To demonstrate a model of a system manufacturing │ │
│*│ │ process. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model demonstrates application of Monterey │ │
│*│ │ Phoenix Modeling to Manufacturing Product Systems. │ │
diff --git a/models/Application_examples/Martian_Lander.mp b/models/Application_examples/Martian_Lander.mp
index 3699a65..8c6fc31 100644
--- a/models/Application_examples/Martian_Lander.mp
+++ b/models/Application_examples/Martian_Lander.mp
@@ -13,7 +13,7 @@
│*│ │ Lander, which is an example of real-time system │ │
│*│ │ behavior modeling. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ The landing system operates in one of two modes: │ │
│*│ │ normal or emergency. When the system is turned on │ │
@@ -59,14 +59,14 @@
│*│ │ Action Time in ms │ │
│*│ │ RACC 10 │ │
│*│ │ STMR 10 │ │
-│*│ │ ADJM 20 │ │
-│*│ │ TDP 10 │ │
-│*│ │ IEM 10 │ │
-│*│ │ ETC 10 │ │
-│*│ │ IVEL 20 │ │
-│*│ │ IALT 20 │ │
-│*│ │ CKDT 10 │ │
-│*│ │ RRM 10 │ │
+│*│ │ ADJM 20 │ │
+│*│ │ TDP 10 │ │
+│*│ │ IEM 10 │ │
+│*│ │ ETC 10 │ │
+│*│ │ IVEL 20 │ │
+│*│ │ IALT 20 │ │
+│*│ │ CKDT 10 │ │
+│*│ │ RRM 10 │ │
│*│ │ │ │
│*│ │ In summary, this model demonstrates the use of │ │
│*│ │ COORDINATE statements to model the relationships │ │
diff --git a/models/Application_examples/Prisoners_Dilemma.mp b/models/Application_examples/Prisoners_Dilemma.mp
index ad08453..437225b 100644
--- a/models/Application_examples/Prisoners_Dilemma.mp
+++ b/models/Application_examples/Prisoners_Dilemma.mp
@@ -11,7 +11,7 @@
│*│ │ To demonstrate using MP to model the logic of a │ │
│*│ │ game scenario. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ Users looking to model exhaustive logical game │ │
│*│ │ scenarios may want to use this model as an │ │
diff --git a/models/Application_examples/Railroad_Crossing_Safety.mp b/models/Application_examples/Railroad_Crossing_Safety.mp
index ab65284..af64619 100644
--- a/models/Application_examples/Railroad_Crossing_Safety.mp
+++ b/models/Application_examples/Railroad_Crossing_Safety.mp
@@ -10,7 +10,7 @@
│*│ │ To illustrate timing attribute use in MP, here for │ │
│*│ │ displaying a railroad crossing scenario. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model demonstrates using BUILD statements to │ │
│*│ │ add time to a model of car and train interactions │ │
diff --git a/models/Application_examples/Replay_Attack.mp b/models/Application_examples/Replay_Attack.mp
index 83a4913..73c0671 100644
--- a/models/Application_examples/Replay_Attack.mp
+++ b/models/Application_examples/Replay_Attack.mp
@@ -10,7 +10,7 @@
│*│ │ To illustrate MP modeling of a replay attack │ │
│*│ │ involving data transmission. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model demonstrates a well known attack │ │
│*│ │ strategy on a communication system. Users may use │ │
diff --git a/models/Application_examples/Small_Package_Delivery.mp b/models/Application_examples/Small_Package_Delivery.mp
index e79412b..c44a016 100644
--- a/models/Application_examples/Small_Package_Delivery.mp
+++ b/models/Application_examples/Small_Package_Delivery.mp
@@ -13,7 +13,7 @@
│*│ │ search and rescue scenario and to illustrate the │ │
│*│ │ impacts of overloading constraints in an MP model. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model demonstrates overusing COORDINATE and │ │
│*│ │ ENSURE statements to create a model of a complex │ │
diff --git a/models/Application_examples/Spent_Fuel_Cooling_and_Cleanup.mp b/models/Application_examples/Spent_Fuel_Cooling_and_Cleanup.mp
index b5721b9..26b1511 100644
--- a/models/Application_examples/Spent_Fuel_Cooling_and_Cleanup.mp
+++ b/models/Application_examples/Spent_Fuel_Cooling_and_Cleanup.mp
@@ -16,7 +16,7 @@
│*│ │ and purification system, specifically a spent │ │
│*│ │ nuclear fuel cooling pool. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model demonstrates identifying the components │ │
│*│ │ of and interactions among a spent nuclear fuel │ │
diff --git a/models/Application_examples/Spiral_Software_Process.mp b/models/Application_examples/Spiral_Software_Process.mp
index 4b7b291..3ceb14a 100644
--- a/models/Application_examples/Spiral_Software_Process.mp
+++ b/models/Application_examples/Spiral_Software_Process.mp
@@ -10,7 +10,7 @@
│*│ │ To illustrate event sharing in order to model the │ │
│*│ │ spiral software development process. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model demonstrates the usage of shared events │ │
│*│ │ to model the spiral software process to develop a │ │
diff --git a/models/Application_examples/Supply_Chain_with_Two_Cyber_Threats.mp b/models/Application_examples/Supply_Chain_with_Two_Cyber_Threats.mp
index 4fa7d12..ba68f3a 100644
--- a/models/Application_examples/Supply_Chain_with_Two_Cyber_Threats.mp
+++ b/models/Application_examples/Supply_Chain_with_Two_Cyber_Threats.mp
@@ -37,7 +37,7 @@
│*│ │ to demonstrate calculating individual and total │ │
│*│ │ risk scores. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model demonstrates performing detailed risk │ │
│*│ │ analysis on a supply chain potentially affected by │ │
diff --git a/models/Application_examples/Surgery.mp b/models/Application_examples/Surgery.mp
index c742ff8..0259f15 100644
--- a/models/Application_examples/Surgery.mp
+++ b/models/Application_examples/Surgery.mp
@@ -11,7 +11,7 @@
│*│ │ involving several actors, including the │ │
│*│ │ environment. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model shows an example of decisions made by a │ │
│*│ │ leader (Physician), a subordinate(s) (Nurse(s)), │ │
diff --git a/models/Application_examples/Swarm_Search_and_Track.mp b/models/Application_examples/Swarm_Search_and_Track.mp
index 516a447..eb1df3e 100644
--- a/models/Application_examples/Swarm_Search_and_Track.mp
+++ b/models/Application_examples/Swarm_Search_and_Track.mp
@@ -14,7 +14,7 @@
│*│ │ unmanned aerial vehicle scenario involving a │ │
│*│ │ low fuel condition. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model was developed by an NPS student with │ │
│*│ │ UAV operation experience with the intent to │ │
diff --git a/models/Application_examples/Swarm_UAV.mp b/models/Application_examples/Swarm_UAV.mp
index 7354dd9..30cb3d4 100644
--- a/models/Application_examples/Swarm_UAV.mp
+++ b/models/Application_examples/Swarm_UAV.mp
@@ -22,7 +22,7 @@
│*│ │ are possible to appear within event traces, taking │ │
│*│ │ effect when the scope is increased. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model demonstrates using iteration to model │ │
│*│ │ multiple unmanned aerial vehicles (UAVs) with │ │
diff --git a/models/Application_examples/Turtles_in_the_Desert.mp b/models/Application_examples/Turtles_in_the_Desert.mp
index d45d70d..72d1c6e 100644
--- a/models/Application_examples/Turtles_in_the_Desert.mp
+++ b/models/Application_examples/Turtles_in_the_Desert.mp
@@ -12,7 +12,7 @@
│*│ │ highlighting the benefits of complete example set │ │
│*│ │ generation in MP. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ Three turtles are moving on a desert plain, all in │ │
│*│ │ the same direction. The first has been asked: │ │
diff --git a/models/Application_examples/UAV_Ingress.mp b/models/Application_examples/UAV_Ingress.mp
index f135743..fbe3883 100644
--- a/models/Application_examples/UAV_Ingress.mp
+++ b/models/Application_examples/UAV_Ingress.mp
@@ -11,7 +11,7 @@
│*│ │ unmanned aerial vehicle (UAV) launch and ingress │ │
│*│ │ scenario. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model was developed by an NPS student to │ │
│*│ │ specify the ingress phase of a UAV on a │ │
@@ -51,7 +51,7 @@
│*│ ┌─[ Instructions ]───────────────────────────────────┠│
│*│ │ Run for Scope 1. This model contains an unexpected │ │
│*│ │ behavior in which the UAV status is acceptable but │ │
-│*│ │ the operator aborts the ingress (trace 2). │ │
+│*│ │ the operator aborts the ingress (trace 2). │ │
│*│ ├─[ Run Statistics ]─────────────────────────────────┤ │
│*│ │ Scope 1: 2 traces in less than 1 sec. │ │
│*│ └────────────────────────────────────────────────────┘ │
diff --git a/models/Application_examples/UAV_OnStation.mp b/models/Application_examples/UAV_OnStation.mp
index f871719..d19581b 100644
--- a/models/Application_examples/UAV_OnStation.mp
+++ b/models/Application_examples/UAV_OnStation.mp
@@ -17,7 +17,7 @@
│*│ │ To illustrate the modeling for system of systems │ │
│*│ │ behaviors that include failure mode scenarios. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This is a model for an Unmanned Aerial Vehicle in │ │
│*│ │ the OnStation Phase of an ISR mission. It │ │
diff --git a/models/Application_examples/Unmanned_Spacecraft_Comms.mp b/models/Application_examples/Unmanned_Spacecraft_Comms.mp
index 41bca24..4f02f0b 100644
--- a/models/Application_examples/Unmanned_Spacecraft_Comms.mp
+++ b/models/Application_examples/Unmanned_Spacecraft_Comms.mp
@@ -13,7 +13,7 @@
│*│ │ spacecraft docking with the International Space │ │
│*│ │ Station (ISS). │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model describes a spacecraft communication │ │
│*│ │ system that works with the International Space │ │
diff --git a/models/Application_examples/Web_Browser_Formal_Security.mp b/models/Application_examples/Web_Browser_Formal_Security.mp
index 66db696..66d9d57 100644
--- a/models/Application_examples/Web_Browser_Formal_Security.mp
+++ b/models/Application_examples/Web_Browser_Formal_Security.mp
@@ -11,7 +11,7 @@
│*│ │ communication involving a bad server and a good │ │
│*│ │ server. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This example borrowed from (Jackson 2019) │ │
│*│ │ demonstrates how MP can check whether Client's web │ │
diff --git a/models/Application_examples/Wide_Range_Search_for_Wreckage_and_Survivors.mp b/models/Application_examples/Wide_Range_Search_for_Wreckage_and_Survivors.mp
index 487622a..ab7a81a 100644
--- a/models/Application_examples/Wide_Range_Search_for_Wreckage_and_Survivors.mp
+++ b/models/Application_examples/Wide_Range_Search_for_Wreckage_and_Survivors.mp
@@ -12,7 +12,7 @@
│*│ │ rescue operation with several environmental and │ │
│*│ │ coordination concerns to address. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model represents an operational process for │ │
│*│ │ use as a common baseline against which alternative │ │
diff --git a/models/Application_examples/Work_Productivity.mp b/models/Application_examples/Work_Productivity.mp
index 63dad67..dfdf5df 100644
--- a/models/Application_examples/Work_Productivity.mp
+++ b/models/Application_examples/Work_Productivity.mp
@@ -10,7 +10,7 @@
│*│ │ To demonstrate how to print all events present in │ │
│*│ │ the trace with timing attributes. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model demonstrates using MP to show how │ │
│*│ │ visitors can distract workers with stacked time │ │
diff --git a/models/Example01_SimpleMessageFlow_EventCoordination.mp b/models/Example01_SimpleMessageFlow_EventCoordination.mp
index 765f2eb..11533a0 100644
--- a/models/Example01_SimpleMessageFlow_EventCoordination.mp
+++ b/models/Example01_SimpleMessageFlow_EventCoordination.mp
@@ -9,7 +9,7 @@
│*│ │ rules and how to coordinate events from each of │ │
│*│ │ those rules. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ Event grammar rules for each root define the │ │
│*│ │ derivations for event traces. In this case, we │ │
@@ -44,8 +44,8 @@
│*│ │ to view the trace in an activity diagram format. │ │
│*│ ├─[ Run Statistics ]─────────────────────────────────┤ │
│*│ │ Scope 1: 2 traces in less than 1 sec. │ │
-│*│ │ Scope 2: 3 traces in less than 1 sec. │ │
-│*│ │ Scope 3: 4 traces in less than 1 sec. │ │
+│*│ │ Scope 2: 3 traces in less than 1 sec. │ │
+│*│ │ Scope 3: 4 traces in less than 1 sec. │ │
│*│ └────────────────────────────────────────────────────┘ │
└*┴───────────────────────────────────────────────────────*/
diff --git a/models/Example01a_UnreliableMessageFlow_VirtualEvents.mp b/models/Example01a_UnreliableMessageFlow_VirtualEvents.mp
index 0705f59..25b7db8 100644
--- a/models/Example01a_UnreliableMessageFlow_VirtualEvents.mp
+++ b/models/Example01a_UnreliableMessageFlow_VirtualEvents.mp
@@ -9,7 +9,7 @@
│*│ │ representing the absence or lack of activity, in │ │
│*│ │ this case, the event "does_not_receive." │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model of sending and receiving events │ │
│*│ │ incorporates a possibility that some messages get │ │
diff --git a/models/Example02_DataFlow_EventSharing.mp b/models/Example02_DataFlow_EventSharing.mp
index 56e7f7d..55a0efb 100644
--- a/models/Example02_DataFlow_EventSharing.mp
+++ b/models/Example02_DataFlow_EventSharing.mp
@@ -8,7 +8,7 @@
│*│ │ To illustrate the representation of data items as │ │
│*│ │ behaviors. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ MP employs the Abstract Data Type (ADT) principle │ │
│*│ │ introduced by Barbara Liskov to represent data │ │
diff --git a/models/Example03_ATMWithdrawal_BehaviorOfEnvironment.mp b/models/Example03_ATMWithdrawal_BehaviorOfEnvironment.mp
index 8fe96b8..9423a08 100644
--- a/models/Example03_ATMWithdrawal_BehaviorOfEnvironment.mp
+++ b/models/Example03_ATMWithdrawal_BehaviorOfEnvironment.mp
@@ -8,7 +8,7 @@
│*│ │ To illustrate integrated system and environment │ │
│*│ │ behaviors. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ MP separates models of component behaviors and │ │
│*│ │ component interactions to permit elaboration on │ │
diff --git a/models/Example04_StackBehavior_EnsureCondition.mp b/models/Example04_StackBehavior_EnsureCondition.mp
index dc50faf..d2fb349 100644
--- a/models/Example04_StackBehavior_EnsureCondition.mp
+++ b/models/Example04_StackBehavior_EnsureCondition.mp
@@ -8,7 +8,7 @@
│*│ │ To demonstrate the use of the ENSURE condition │ │
│*│ │ containing an example Boolean expression. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ The event trace is a set of events and the Boolean │ │
│*│ │ expressions in MP can embrace the traditional │ │
diff --git a/models/Example04a_StackBehavior_UserDefinedRelations.mp b/models/Example04a_StackBehavior_UserDefinedRelations.mp
index 8a5240d..b128cab 100644
--- a/models/Example04a_StackBehavior_UserDefinedRelations.mp
+++ b/models/Example04a_StackBehavior_UserDefinedRelations.mp
@@ -16,7 +16,7 @@
│*│ │ "Paired_with" to show which "push" events are │ │
│*│ │ paired with which "pop" events. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model is an expansion on Example 04. Model of │ │
│*│ │ Stack Behavior. │ │
diff --git a/models/Example04b_QueueBehavior_UserDefinedRelations.mp b/models/Example04b_QueueBehavior_UserDefinedRelations.mp
index 2987fe6..34b7392 100644
--- a/models/Example04b_QueueBehavior_UserDefinedRelations.mp
+++ b/models/Example04b_QueueBehavior_UserDefinedRelations.mp
@@ -18,7 +18,7 @@
│*│ │ 4) present the concept of isomorphism with respect │ │
│*│ │ to models in MP. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model is isomorphic to Example 04a. Model of │ │
│*│ │ Stack Behavior. │ │
diff --git a/models/Example05_CarRace_NestedComposition.mp b/models/Example05_CarRace_NestedComposition.mp
index 819854c..1e36711 100644
--- a/models/Example05_CarRace_NestedComposition.mp
+++ b/models/Example05_CarRace_NestedComposition.mp
@@ -9,7 +9,7 @@
│*│ │ 1) one-to-many event coordination and │ │
│*│ │ 2) trace annotation. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model of a car race ties the number of Cars │ │
│*│ │ in the race to the scope (running at scope 1 will │ │
diff --git a/models/Example06_UnreliableChannel_AssertionChecking.mp b/models/Example06_UnreliableChannel_AssertionChecking.mp
index b35da18..a9777b7 100644
--- a/models/Example06_UnreliableChannel_AssertionChecking.mp
+++ b/models/Example06_UnreliableChannel_AssertionChecking.mp
@@ -7,7 +7,7 @@
│*│ ┌─[ Purpose ]────────────────────────────────────────┠│
│*│ │ To demonstrate assertion checking with MP. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This is a behavior model of communicating via an │ │
│*│ │ unreliable channel. It is considered isomorphic │ │
diff --git a/models/Example07_UnconstrainedStack_TraceAnnotation.mp b/models/Example07_UnconstrainedStack_TraceAnnotation.mp
index a1d787c..de0137c 100644
--- a/models/Example07_UnconstrainedStack_TraceAnnotation.mp
+++ b/models/Example07_UnconstrainedStack_TraceAnnotation.mp
@@ -8,7 +8,7 @@
│*│ │ To demonstrate a technique for debugging using │ │
│*│ │ trace annotation. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ Assertion checking with the CHECK clause may be │ │
│*│ │ the simplest and most common tool for finding │ │
diff --git a/models/Example08_EmployeeEmployer_CoordinationAcrossHierarchyLevels.mp b/models/Example08_EmployeeEmployer_CoordinationAcrossHierarchyLevels.mp
index 600d1c6..090f4aa 100644
--- a/models/Example08_EmployeeEmployer_CoordinationAcrossHierarchyLevels.mp
+++ b/models/Example08_EmployeeEmployer_CoordinationAcrossHierarchyLevels.mp
@@ -8,7 +8,7 @@
│*│ │ To demonstrate the modeling of a business process │ │
│*│ │ in MP. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ The site http://www.infoq.com/articles/bpelbpm │ │
│*│ │ "Why BPEL is not the holy grail for BPM" provides │ │
diff --git a/models/Example09_CardiacArrestWorkflow_VirtualEvents.mp b/models/Example09_CardiacArrestWorkflow_VirtualEvents.mp
index 72df180..1bfbdb3 100644
--- a/models/Example09_CardiacArrestWorkflow_VirtualEvents.mp
+++ b/models/Example09_CardiacArrestWorkflow_VirtualEvents.mp
@@ -7,7 +7,7 @@
│*│ ┌─[ Purpose ]────────────────────────────────────────┠│
│*│ │ To demonstrate the modeling of a workflow in MP. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ When handling a cardiac arrest, the │ │
│*│ │ check_breathing and check_pulse tasks run in │ │
diff --git a/models/Example10_PipeFilter_TraceAnnotationQueries.mp b/models/Example10_PipeFilter_TraceAnnotationQueries.mp
index d58b8c8..ab5c1fa 100644
--- a/models/Example10_PipeFilter_TraceAnnotationQueries.mp
+++ b/models/Example10_PipeFilter_TraceAnnotationQueries.mp
@@ -8,7 +8,7 @@
│*│ │ To demonstrate how to conduct a queries for model │ │
│*│ │ properties using automatic trace annotation. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This is a behavior model of a pipe/filter │ │
│*│ │ architecture with two filters. The assumptions are │ │
diff --git a/models/Example11_PublishSubscribe_AsynchronousCoordination.mp b/models/Example11_PublishSubscribe_AsynchronousCoordination.mp
index 641ed05..28ed4be 100644
--- a/models/Example11_PublishSubscribe_AsynchronousCoordination.mp
+++ b/models/Example11_PublishSubscribe_AsynchronousCoordination.mp
@@ -9,7 +9,7 @@
│*│ │ coordination to get all valid permutations of │ │
│*│ │ coordinated events. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This is a model of a Publish-Subscribe │ │
│*│ │ architecture. A Publisher sends a notification to │ │
diff --git a/models/Example12_RingTopology_UserDefinedRelations.mp b/models/Example12_RingTopology_UserDefinedRelations.mp
index 2e2a8e2..0010eb5 100644
--- a/models/Example12_RingTopology_UserDefinedRelations.mp
+++ b/models/Example12_RingTopology_UserDefinedRelations.mp
@@ -7,7 +7,7 @@
│*│ ┌─[ Purpose ]────────────────────────────────────────┠│
│*│ │ To demonstrate the use of user-defined relations. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ The following is a model of network ring, where │ │
│*│ │ each node interacts with its left and right │ │
diff --git a/models/Example13_ConsumersSuppliers_DependencyTracking.mp b/models/Example13_ConsumersSuppliers_DependencyTracking.mp
index d8b118f..3d9f19e 100644
--- a/models/Example13_ConsumersSuppliers_DependencyTracking.mp
+++ b/models/Example13_ConsumersSuppliers_DependencyTracking.mp
@@ -9,7 +9,7 @@
│*│ │ and event dependency tracking for chains of │ │
│*│ │ related events. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This is a model of consumers and suppliers │ │
│*│ │ interacting in a general supply chain. A │ │
diff --git a/models/Example14_ShoppingSpree_NumberAttributes.mp b/models/Example14_ShoppingSpree_NumberAttributes.mp
index 1ffdcb4..63eea97 100644
--- a/models/Example14_ShoppingSpree_NumberAttributes.mp
+++ b/models/Example14_ShoppingSpree_NumberAttributes.mp
@@ -10,7 +10,7 @@
│*│ │ and an average cost of items across all events in │ │
│*│ │ a trace. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ In this model, a Buyer goes to two different shops │ │
│*│ │ that are selling items. Each item has a price. The │ │
diff --git a/models/Example15_BackpackWeight_IntervalAttributes.mp b/models/Example15_BackpackWeight_IntervalAttributes.mp
index fd9edde..60f9395 100644
--- a/models/Example15_BackpackWeight_IntervalAttributes.mp
+++ b/models/Example15_BackpackWeight_IntervalAttributes.mp
@@ -11,7 +11,7 @@
│*│ │ individual items in each trace, and to ensure a │ │
│*│ │ total weight limit is not exceeded by any trace. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ The task is to load a backpack with items not │ │
│*│ │ exceeding a total weight of 30 units. There may be │ │
diff --git a/models/Example16_StackBehavior_ProbabilityCalculationsType1.mp b/models/Example16_StackBehavior_ProbabilityCalculationsType1.mp
index d054f85..a589824 100644
--- a/models/Example16_StackBehavior_ProbabilityCalculationsType1.mp
+++ b/models/Example16_StackBehavior_ProbabilityCalculationsType1.mp
@@ -7,7 +7,7 @@
│*│ ┌─[ Purpose ]────────────────────────────────────────┠│
│*│ │ To obtain the probability of each valid trace. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This is a behavior model of simple stack behavior. │ │
│*│ │ Valid behaviors don’t permit a scenario when the │ │
diff --git a/models/Example17_SharedEvents_ProbabilityCalculationsType1.mp b/models/Example17_SharedEvents_ProbabilityCalculationsType1.mp
index 37503da..3cfb81d 100644
--- a/models/Example17_SharedEvents_ProbabilityCalculationsType1.mp
+++ b/models/Example17_SharedEvents_ProbabilityCalculationsType1.mp
@@ -7,7 +7,7 @@
│*│ ┌─[ Purpose ]────────────────────────────────────────┠│
│*│ │ To obtain the probability of each valid trace. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This is a behavior model of two friends out to │ │
│*│ │ lunch. Menu options include a large salad, a half │ │
diff --git a/models/Example18_RedGreen_BayesianProbabilityCalculationsType2.mp b/models/Example18_RedGreen_BayesianProbabilityCalculationsType2.mp
index f80fa92..15b8d29 100644
--- a/models/Example18_RedGreen_BayesianProbabilityCalculationsType2.mp
+++ b/models/Example18_RedGreen_BayesianProbabilityCalculationsType2.mp
@@ -10,7 +10,7 @@
│*│ │ probability of an event appearing within a given │ │
│*│ │ trace. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This behavior model demonstrates how to compute │ │
│*│ │ probabilities for events that depend on other │ │
diff --git a/models/Example19_StackBehavior_BayesianProbabilityCalculationsType2.mp b/models/Example19_StackBehavior_BayesianProbabilityCalculationsType2.mp
index af078a9..c8c4f91 100644
--- a/models/Example19_StackBehavior_BayesianProbabilityCalculationsType2.mp
+++ b/models/Example19_StackBehavior_BayesianProbabilityCalculationsType2.mp
@@ -11,7 +11,7 @@
│*│ │ how to make the probability of an event dependent │ │
│*│ │ on events happening before it. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model uses the stack behavior model to │ │
│*│ │ illustrate the main parts in probabilistic MP │ │
diff --git a/models/Example20_Activity_Diagram.mp b/models/Example20_Activity_Diagram.mp
index d7602e7..86de9ff 100644
--- a/models/Example20_Activity_Diagram.mp
+++ b/models/Example20_Activity_Diagram.mp
@@ -8,7 +8,7 @@
│*│ │ To show how to extract Activity Diagrams of root │ │
│*│ │ events in a schema. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model demonstrates how to use "SHOW ACTIVITY │ │
│*│ │ DIAGRAM" to display events as a flowcharts similar │ │
diff --git a/models/Example21_DataFlow_LocalReport.mp b/models/Example21_DataFlow_LocalReport.mp
index 9caea1a..c1d40c4 100644
--- a/models/Example21_DataFlow_LocalReport.mp
+++ b/models/Example21_DataFlow_LocalReport.mp
@@ -8,7 +8,7 @@
│*│ │ To show how to produce a local report within a │ │
│*│ │ trace. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ A report is a sequence of related SAY clauses │ │
│*│ │ assembled together to make it easier to read and │ │
diff --git a/models/Example22_UnreliableMessageFlow_GlobalReport.mp b/models/Example22_UnreliableMessageFlow_GlobalReport.mp
index e6a08ae..59b17df 100644
--- a/models/Example22_UnreliableMessageFlow_GlobalReport.mp
+++ b/models/Example22_UnreliableMessageFlow_GlobalReport.mp
@@ -9,7 +9,7 @@
│*│ │ To show how to produce a global report across all │ │
│*│ │ traces. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ A global report may be used to assemble │ │
│*│ │ information about all traces, e.g., total number │ │
diff --git a/models/Example23_CarRace_LocalGraph.mp b/models/Example23_CarRace_LocalGraph.mp
index 1df7825..f38b4a8 100644
--- a/models/Example23_CarRace_LocalGraph.mp
+++ b/models/Example23_CarRace_LocalGraph.mp
@@ -8,7 +8,7 @@
│*│ │ To demonstrate the construction of a local graph │ │
│*│ │ on a trace. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ Graphs are "entity-relation" models extracted from │ │
│*│ │ event traces in order to visualize certain │ │
diff --git a/models/Example24_ATMWithdrawal_ComponentDiagram.mp b/models/Example24_ATMWithdrawal_ComponentDiagram.mp
index 580ad09..150a5c8 100644
--- a/models/Example24_ATMWithdrawal_ComponentDiagram.mp
+++ b/models/Example24_ATMWithdrawal_ComponentDiagram.mp
@@ -8,7 +8,7 @@
│*│ │ To demonstrate the construction of a global graph │ │
│*│ │ from all traces in the schema. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model builds upon the ATM Withdrawal behavior │ │
│*│ │ from Example 4 in the MP manual. It shows how to │ │
diff --git a/models/Example24a_Compiler_ComponentDiagram.mp b/models/Example24a_Compiler_ComponentDiagram.mp
index 034db4f..9b7c679 100644
--- a/models/Example24a_Compiler_ComponentDiagram.mp
+++ b/models/Example24a_Compiler_ComponentDiagram.mp
@@ -8,7 +8,7 @@
│*│ │ To demonstrate the construction of a global graph │ │
│*│ │ from all traces in the schema. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model builds upon the Compiler behavior from │ │
│*│ │ Example 42 in the MP manual. It shows how to │ │
diff --git a/models/Example25_Graph_as_Data_Structure.mp b/models/Example25_Graph_as_Data_Structure.mp
index 764dc19..3aac428 100644
--- a/models/Example25_Graph_as_Data_Structure.mp
+++ b/models/Example25_Graph_as_Data_Structure.mp
@@ -9,7 +9,7 @@
│*│ │ structure for accumulating and rendering │ │
│*│ │ statistics from event traces. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ Graphs can be used as container data structures │ │
│*│ │ (associative arrays) to store and retrieve data │ │
diff --git a/models/Example26_UnreliableMessageFlow_GlobalQuery.mp b/models/Example26_UnreliableMessageFlow_GlobalQuery.mp
index df1be32..49ed81a 100644
--- a/models/Example26_UnreliableMessageFlow_GlobalQuery.mp
+++ b/models/Example26_UnreliableMessageFlow_GlobalQuery.mp
@@ -8,7 +8,7 @@
│*│ ┌─[ Purpose ]────────────────────────────────────────┠│
│*│ │ To demonstrate the use of GLOBAL attributes. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This example uses the Unreliable Message Flow from │ │
│*│ │ Example 8 in the MP manual to show how to │ │
@@ -29,9 +29,9 @@
│*│ │ than 5. That can be done using explicit iteration │ │
│*│ │ limit (running for instance, for scope 1), like: │ │
│*│ │ │ │
-│*│ │ ROOT Sender: (+<1..7> send +); │ │
-│*│ │ ROOT Receiver: (+<1..7> (receive |<<0.2>> │ │
-│*│ │ does_not_receive) +); │ │
+│*│ │ ROOT Sender: (+<1..7> send +); │ │
+│*│ │ ROOT Receiver: (+<1..7> (receive |<<0.2>> │ │
+│*│ │ does_not_receive) +); │ │
│*│ └────────────────────────────────────────────────────┘ │
│*│ │
│*│ ┌─[ References ]─────────────────────────────────────┠│
diff --git a/models/Example27_Table_and_Bar_Chart.mp b/models/Example27_Table_and_Bar_Chart.mp
index 87f4d1a..922b7e3 100644
--- a/models/Example27_Table_and_Bar_Chart.mp
+++ b/models/Example27_Table_and_Bar_Chart.mp
@@ -9,7 +9,7 @@
│*│ │ current trace in a table and then render the table │ │
│*│ │ as a bar chart. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This example model shows how to create and │ │
│*│ │ populate a table with data collected from a graph │ │
diff --git a/models/Example28_Histogram.mp b/models/Example28_Histogram.mp
index 878d4ca..aa966ac 100644
--- a/models/Example28_Histogram.mp
+++ b/models/Example28_Histogram.mp
@@ -9,7 +9,7 @@
│*│ │ histogram from Type 1 probabilities of traces in │ │
│*│ │ an MP model. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ A histogram represents the distribution of │ │
│*│ │ numerical data into "bins" or "buckets." The first │ │
diff --git a/models/Example29_Gantt_Chart.mp b/models/Example29_Gantt_Chart.mp
index ba31d39..e0caca6 100644
--- a/models/Example29_Gantt_Chart.mp
+++ b/models/Example29_Gantt_Chart.mp
@@ -8,7 +8,7 @@
│*│ │ To demonstrate how to construct a Gantt Chart │ │
│*│ │ using event timing attributes. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model shows how to assign non-zero timing │ │
│*│ │ attributes to events and visualize the whole-trace │ │
diff --git a/models/Example30_MicrowaveOven_ModelingModelChecking.mp b/models/Example30_MicrowaveOven_ModelingModelChecking.mp
index 59e5dd5..138220f 100644
--- a/models/Example30_MicrowaveOven_ModelingModelChecking.mp
+++ b/models/Example30_MicrowaveOven_ModelingModelChecking.mp
@@ -7,7 +7,7 @@
│*│ ┌─[ Purpose ]────────────────────────────────────────┠│
│*│ │ To demonstrate model checking for a small scope. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This is a behavior model of a microwave oven built │ │
│*│ │ from states and transitions [Clarke et al. 1999, │ │
diff --git a/models/Example31_Petri_Net.mp b/models/Example31_Petri_Net.mp
index 8a15fe4..18dc70c 100644
--- a/models/Example31_Petri_Net.mp
+++ b/models/Example31_Petri_Net.mp
@@ -7,7 +7,7 @@
│*│ ┌─[ Purpose ]────────────────────────────────────────┠│
│*│ │ To demonstrate the modeling of a Petri net in MP. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This is a behavior model of the Petri net diagram │ │
│*│ │ above Example 28 in the MP v.4 Language Manual. │ │
diff --git a/models/Example32_ATMWithdrawal_StatechartView.mp b/models/Example32_ATMWithdrawal_StatechartView.mp
index 5e140ac..e25ba1f 100644
--- a/models/Example32_ATMWithdrawal_StatechartView.mp
+++ b/models/Example32_ATMWithdrawal_StatechartView.mp
@@ -9,7 +9,7 @@
│*│ │ To demonstrate how to extract a Statechart view │ │
│*│ │ from an MP model. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ A statechart model is a diagram where states │ │
│*│ │ represent states of the system and transitions │ │
diff --git a/models/Example33_FiniteStateDiagram_PathAnnotation.mp b/models/Example33_FiniteStateDiagram_PathAnnotation.mp
index 73b639f..ad6037b 100644
--- a/models/Example33_FiniteStateDiagram_PathAnnotation.mp
+++ b/models/Example33_FiniteStateDiagram_PathAnnotation.mp
@@ -12,7 +12,7 @@
│*│ │ 2) generate event traces as annotated paths │ │
│*│ │ through the diagram. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ The following MP schema models the behavior of a │ │
│*│ │ finite state diagram with a single state loop │ │
diff --git a/models/Example34_FiniteStateDiagram_PathDiagram.mp b/models/Example34_FiniteStateDiagram_PathDiagram.mp
index 25cb804..e7c81b3 100644
--- a/models/Example34_FiniteStateDiagram_PathDiagram.mp
+++ b/models/Example34_FiniteStateDiagram_PathDiagram.mp
@@ -12,7 +12,7 @@
│*│ │ 2) the state transition diagram in the global │ │
│*│ │ view. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ The following MP code modifies the code in Example │ │
│*│ │ 26 from the MP Language Manual to add a path graph │ │
diff --git a/models/Example35_Authentication_SystemReuse.mp b/models/Example35_Authentication_SystemReuse.mp
index 021423d..116566b 100644
--- a/models/Example35_Authentication_SystemReuse.mp
+++ b/models/Example35_Authentication_SystemReuse.mp
@@ -9,7 +9,7 @@
│*│ │ composition operation. Authentication system's │ │
│*│ │ behavior for reuse with MAP operation. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model of an authentication subsystem maps │ │
│*│ │ reusable behaviors of a generic Requester onto │ │
diff --git a/models/Example36_Compiler1_ComponentReuse.mp b/models/Example36_Compiler1_ComponentReuse.mp
index 1e4c9c6..1297eb7 100644
--- a/models/Example36_Compiler1_ComponentReuse.mp
+++ b/models/Example36_Compiler1_ComponentReuse.mp
@@ -11,7 +11,7 @@
│*│ │ the specification of component behavior and the │ │
│*│ │ specification of interactions between components. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ Examples 36 and 37 are models of a bottom-up │ │
│*│ │ parser with lexical analyzer based on regular │ │
diff --git a/models/Example37_Compiler2_ComponentReuse.mp b/models/Example37_Compiler2_ComponentReuse.mp
index 7a2827c..f8c98e4 100644
--- a/models/Example37_Compiler2_ComponentReuse.mp
+++ b/models/Example37_Compiler2_ComponentReuse.mp
@@ -10,7 +10,7 @@
│*│ │ the specification of component behavior and the │ │
│*│ │ specification of interactions between components. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ Examples 36 and 37 are models of a bottom-up │ │
│*│ │ parser with lexical analyzer based on regular │ │
diff --git a/models/Example38_Merging_Root_Events_to_Reduce_Run_Time.mp b/models/Example38_Merging_Root_Events_to_Reduce_Run_Time.mp
index 86f4296..fdfc824 100644
--- a/models/Example38_Merging_Root_Events_to_Reduce_Run_Time.mp
+++ b/models/Example38_Merging_Root_Events_to_Reduce_Run_Time.mp
@@ -10,7 +10,7 @@
│*│ │ derivations in order to reduce run time for larger │ │
│*│ │ models. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model has several interacting root events, │ │
│*│ │ where roots B and C have several coordination │ │
diff --git a/models/Language_concepts/Event_Sharing_Using_COORDINATE_with_SHARE.mp b/models/Language_concepts/Event_Sharing_Using_COORDINATE_with_SHARE.mp
index f54c410..5518b1b 100644
--- a/models/Language_concepts/Event_Sharing_Using_COORDINATE_with_SHARE.mp
+++ b/models/Language_concepts/Event_Sharing_Using_COORDINATE_with_SHARE.mp
@@ -1,15 +1,15 @@
/*┬────────────────────────────────────────────────────────â”
│*│ ┌─[ Title and Authors ]──────────────────────────────┠│
-│*│ │ Event Sharing Using COORDINATE with SHARE │ │
+│*│ │ Event Sharing Using COORDINATE with SHARE │ │
│*│ │ Created by Kristin Giammarco and Mike Collins │ │
-│*│ │ 2021-11-11 │ │
+│*│ │ 2021-11-11 │ │
│*│ └────────────────────────────────────────────────────┘ │
│*│ │
│*│ ┌─[ Purpose ]────────────────────────────────────────┠│
│*│ │ To illustrate how SHARE ALL is a shortcut for a │ │
│*│ │ COORDINATE statement with SHARE. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model shows the use of COORDINATE statements │ │
│*│ │ in lieu of SHARE ALL statements, illustrating how │ │
@@ -22,7 +22,7 @@
│*│ │ Understanding how SHARE and SHARE ALL work is │ │
│*│ │ helpful when there is a need to compose more │ │
│*│ │ complex sharing operations, such as sharing among │ │
-│*│ │ composite events. │ │
+│*│ │ composite events. │ │
│*│ └────────────────────────────────────────────────────┘ │
│*│ │
│*│ ┌─[ References ]─────────────────────────────────────┠│
@@ -31,9 +31,9 @@
│*│ │ Workflow Modeling Language Manual" (Version 4). │ │
│*│ │ 2020. Available online: │ │
│*│ │ https://wiki.nps.edu/display/MP/Documentation │ │
-│*│ │ │ │
+│*│ │ │ │
│*│ │ Example02_DataFlow_EventSharing. Available online:│ │
-│*│ │ https://nps.edu/mp/models > Language_concepts │ │
+│*│ │ https://nps.edu/mp/models > Language_concepts │ │
│*│ └────────────────────────────────────────────────────┘ │
│*│ │
│*│ ┌─[ Search Terms ]───────────────────────────────────┠│
diff --git a/models/Language_concepts/Event_Sharing_in_Composite_Events.mp b/models/Language_concepts/Event_Sharing_in_Composite_Events.mp
index c8ba31c..3d6408f 100644
--- a/models/Language_concepts/Event_Sharing_in_Composite_Events.mp
+++ b/models/Language_concepts/Event_Sharing_in_Composite_Events.mp
@@ -1,20 +1,20 @@
/*┬────────────────────────────────────────────────────────â”
│*│ ┌─[ Title and Authors ]──────────────────────────────┠│
-│*│ │ Event Sharing in Composite Events │ │
+│*│ │ Event Sharing in Composite Events │ │
│*│ │ Created by Kristin Giammarco and Mike Collins │ │
-│*│ │ 2021-11-11 │ │
+│*│ │ 2021-11-11 │ │
│*│ └────────────────────────────────────────────────────┘ │
│*│ │
│*│ ┌─[ Purpose ]────────────────────────────────────────┠│
│*│ │ To illustrate how to share events within composite │ │
-│*│ │ events. │ │
+│*│ │ events. │ │
│*│ └────────────────────────────────────────────────────┘ │
-│*│ │
+│*│ │
│*│ ┌─[ Description ]────────────────────────────────────┠│
│*│ │ This model shows the use of COORDINATE statements │ │
-│*│ │ to perform event sharing inside of composite │ │
-│*│ │ events. This operation uses nested COORDINATE │ │
-│*│ │ statements to navigate the event hierarchy. │ │
+│*│ │ to perform event sharing inside of composite │ │
+│*│ │ events. This operation uses nested COORDINATE │ │
+│*│ │ statements to navigate the event hierarchy. │ │
│*│ └────────────────────────────────────────────────────┘ │
│*│ │
│*│ ┌─[ References ]─────────────────────────────────────┠│
@@ -23,9 +23,9 @@
│*│ │ Workflow Modeling Language Manual" (Version 4). │ │
│*│ │ 2020. Available online: │ │
│*│ │ https://wiki.nps.edu/display/MP/Documentation │ │
-│*│ │ │ │
+│*│ │ │ │
│*│ │ Example02_DataFlow_EventSharing. Available online:│ │
-│*│ │ https://nps.edu/mp/models > Language_concepts │ │
+│*│ │ https://nps.edu/mp/models > Language_concepts │ │
│*│ └────────────────────────────────────────────────────┘ │
│*│ │
│*│ ┌─[ Search Terms ]───────────────────────────────────┠│
--
GitLab