diff --git a/models/Application_examples/Aspect_Oriented_Paradigm.mp b/models/Application_examples/Aspect_Oriented_Paradigm.mp
index 54172f8dc69351922d4ddc14be04776bfe026d27..63c36459f1aa6072b21365baf8ad894483280cb0 100644
--- a/models/Application_examples/Aspect_Oriented_Paradigm.mp
+++ b/models/Application_examples/Aspect_Oriented_Paradigm.mp
@@ -27,16 +27,17 @@ after each method call as an advice. The corresponding
MP model may look like the following.
References:
-"Example 2: Modeling Aspect-Oriented Paradigm" from Auguston,
- M. "Monterey Phoenix System and Software Architecture and
- Workflow Modeling Language Manual" (Version 4). 2020.
- Available online:
+"Example 2: Modeling Aspect-Oriented Paradigm" from
+ Auguston, M. "Monterey Phoenix System and Software
+ Architecture and Workflow Modeling Language Manual"
+ (Version 4). 2020. Available online:
https://wiki.nps.edu/display/MP/Documentation
-Kiczales, G., J. Lamping, A. Mehdbekar, C. Maeda, C.V. Lopes,
- J. Loingtier, J. Irwin. "Aspect-Oriented Programming",
- Proceedings of the European Conference on Object-Oriented
- Programming (ECOOP), Springer-Verlag LNCS 1241. June 1997.
+Kiczales, G., J. Lamping, A. Mehdbekar, C. Maeda,
+ C.V. Lopes, J. Loingtier, J. Irwin. "Aspect-Oriented
+ Programming", Proceedings of the European Conference
+ on Object-Oriented Programming (ECOOP), Springer-Verlag
+ LNCS 1241. June 1997.
Search terms: behavior, aspect-oriented paradigm;
coordination, event
diff --git a/models/Application_examples/Authentication.mp b/models/Application_examples/Authentication.mp
index 80249ef1c8792da8ba1c9a74f79d90966206612f..8f24f86ea673bcd29fd62191d7991902ff99445e 100644
--- a/models/Application_examples/Authentication.mp
+++ b/models/Application_examples/Authentication.mp
@@ -1,26 +1,30 @@
/* Model of Authentication
Created by Kristin Giammarco on the 16th of May, 2017.
-Modified by Kristin Giammarco on the 7th of August, 2017 to add capitalization to state events.
-Modified by Kristin Giammarco on the 7th of August, 2017 to add ENSURE constraints.
+Modified by Kristin Giammarco on the 7th of August, 2017
+ to add capitalization to state events.
+Modified by Kristin Giammarco on the 7th of August, 2017
+ to add ENSURE constraints.
Edited by Keane Reynolds in July, 2021.
Edited by Pamela Dyer in July and August, 2021.
-Purpose: To demonstrate how to reject unwanted behaviors with ENSURE
-constraints.
+Purpose: 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 statements. ENSURE statements in this model are
-used to lock the account if 3 or more incorrect passwords are input,
-and guarantee that the account will not be locked if a correct password
-is input within the maximum number of attempts. This provides a maximum
-and prevents unwanted traces (ex. correct password leading to lock
-account), demonstrating how users can remove unwanted traces in their
-models using ENSURE.
+Description: This model demonstrates how to correctly model
+a simple user authentication system with ENSURE statements.
+ENSURE statements in this model are used to lock the account
+if 3 or more incorrect passwords are input, and guarantee
+that the account will not be locked if a correct password is
+input within the maximum number of attempts. This provides a
+maximum and prevents unwanted traces (ex. correct password
+leading to lock account), demonstrating how users can remove
+unwanted traces in their models using ENSURE.
References:
-Search terms: behavior, authentication system; coordination, event; ENSURE condition; event sharing
+Search terms: behavior, authentication system;
+coordination, event; ENSURE condition; event sharing
Instructions: Run for Scopes 1, 2, and 3.
Scope 1: 2 traces in less than 1 sec.
diff --git a/models/Application_examples/Autonomous_Car.mp b/models/Application_examples/Autonomous_Car.mp
index c8d0d80f623ef240501b8e32604e8ee6dbf23c86..1d6b92e6383752c2db8b070fab2de0361d0c7008 100644
--- a/models/Application_examples/Autonomous_Car.mp
+++ b/models/Application_examples/Autonomous_Car.mp
@@ -4,19 +4,23 @@ Created by Gregory Kaminski in November, 2015.
Edited by Keane Reynolds in July, 2021.
Edited by Pamela Dyer in July and August, 2021.
-Purpose: 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 used to support a failure mode
-analysis of autonomous automobile technology (student project). It applies COORDINATE statements to link the content under the
-roots "Car" and "User" together. This is important as, without the
-COORDINATE statements, the events under each root are random and
-confusing, making understanding the traces much more difficult.
-Users should keep this in mind and use COORDINATE statements in their
-models to improve clarity.
+Purpose: 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 used to support a failure mode analysis of autonomous
+automobile technology (student project). It applies
+COORDINATE statements to link the content under the roots
+"Car" and "User" together. This is important as, without
+the COORDINATE statements, the events under each root are
+random and confusing, making understanding the traces much
+more difficult. Users should keep this in mind and use
+COORDINATE statements in their models to improve clarity.
References:
-Search terms: behavior, autonomous car; autonomous; failure mode analysis; coordination, event
+Search terms: behavior, autonomous car; autonomous;
+failure mode analysis; coordination, event
Instructions: Run for Scope 1.
Scope 1: 8 traces in less than 1 sec.
diff --git a/models/Application_examples/Beginner_Use_of_MP.mp b/models/Application_examples/Beginner_Use_of_MP.mp
index 61aef3d7c14d4704996f104cc7df6b22debf7cf2..1b52f889bb638eb1d715ecb714ddb735094eb7d8 100644
--- a/models/Application_examples/Beginner_Use_of_MP.mp
+++ b/models/Application_examples/Beginner_Use_of_MP.mp
@@ -4,35 +4,43 @@ Created by Kristin Giammarco on the 8th of February, 2021.
Edited by Keane Reynolds in July, 2021.
Edited by Pamela Dyer in July and August, 2021.
-Purpose: To use traces to provide a simple example of how to use MP-Firebird as a
-beginner.
-
-Description: This model provides an orientation for those just getting started using
-MP-Firebird. This text editor pane allows you to compose and edit code
-in the high-level MP language. Press the Run button to generate event
-traces from the code, then inspect the results in the center pane. Use
-the far right pane to navigate the resulting traces. Use the scope slider
-bar next to the Run button to control the number of loop iterations.
-This model incorporates COORDINATE, ENSURE, and IF-THEN-ELSE statements, so beginner
-users will want to look at the whole model to learn about all of these
-statements, while more experienced users can skip to the parts that are
-more relevant to their specific goals. See the instructions section for additional advice.
-
-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)
+Purpose: To use traces to provide a simple example of
+how to use MP-Firebird as a beginner.
+
+Description: This model provides an orientation for those
+just getting started using MP-Firebird. This text editor
+pane allows you to compose and edit code in the high-level
+MP language. Press the Run button to generate event traces
+from the code, then inspect the results in the center pane.
+Use the far right pane to navigate the resulting traces.
+Use the scope slider bar next to the Run button to control
+the number of loop iterations. This model incorporates
+COORDINATE, ENSURE, and IF-THEN-ELSE statements, so
+beginner users will want to look at the whole model to
+learn about all of these statements, while more
+experienced users can skip to the parts that are more
+relevant to their specific goals. See the instructions
+section for additional advice.
+
+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
References:
-Search terms: beginner use of MP; use of MP-Firebird; trace annotation; SAY statement
+Search terms: beginner use of MP; use of MP-Firebird;
+trace annotation; SAY statement
-Instructions: Run for Scopes 1 and up. 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).
+Instructions: Run for Scopes 1 and up. 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).
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.
diff --git a/models/Application_examples/CargoScreening.mp b/models/Application_examples/CargoScreening.mp
index 23c256c8763675c8017c59e626d853c5d5122714..e4daf917c72488f6b89baf0019f342c31c054b97 100644
--- a/models/Application_examples/CargoScreening.mp
+++ b/models/Application_examples/CargoScreening.mp
@@ -1,33 +1,42 @@
/* Model of Cargo Screening
-Draft written by Mikhail Auguston on the 6th of May, 2011 (NPS, Monterey, CA).
+Draft written by Mikhail Auguston on the 6th of May, 2011
+ (NPS, Monterey, CA).
Edited by Keane Reynolds in July, 2021.
Edited by Pamela Dyer in July and August, 2021.
-Purpose: To illustrate a model using a single long chain of logic,
-in this case outlining a cargo screening process.
+Purpose: To illustrate a model using a single long chain of
+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 makes sense for models where 1 individual or machine is doing many tasks.
-Users should remember that multiple roots should be used if multiple people or objects
-are performing these actions, but use composite statements when one action leads to
-several more.
+Description: This model demonstrates using composite
+statements under roots to make a long chain of logic. This
+makes sense for models where 1 individual or machine is
+doing many tasks. Users should remember that multiple roots
+should be used if multiple people or objects are performing
+these actions, but use composite statements when one action
+leads to several more.
-An error that was found was that the original flowchart does not specify what happens if
-selection_has_not_been_accepted, I've added PhysicalExamination
-and AnomalyResolution as a follow-up, but this scenario should be approved by the customer.
+An error that was found was that the original flowchart does
+not specify what happens if selection_has_not_been_accepted,
+I've added PhysicalExamination and AnomalyResolution as a
+follow-up, but this scenario should be approved by
+the customer.
MP-Firebird may be used at least for the following:
- generate all possible scenarios and inspect them manually,
- this way it becomes possible to find out the deficiency pointed out above
-- typical assertion that may be verified: "if the cargo has been loaded,
- 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"
+ this way it becomes possible to find out the deficiency
+ pointed out above
+- typical assertion that may be verified: "if the cargo has
+ been loaded, 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"
References:
Skinner, Richard. "CBP's Container Security Initiative Has
-Proactive Management and Oversight but Future Direction Is Uncertain (OIG-10-52)."
-Office of Inspector General, Department of Homeland Security. February 3, 2010.
+Proactive Management and Oversight but Future Direction Is
+Uncertain (OIG-10-52)." Office of Inspector General,
+Department of Homeland Security. February 3, 2010.
https://www.oig.dhs.gov/assets/Mgmt/OIG_10-52_Feb10.pdf
@@ -35,10 +44,12 @@ https://www.oig.dhs.gov/assets/Mgmt/OIG_10-52_Feb10.pdf
Department of Homeland Security
Ofï¬ce of Inspector General
CBP's Container Security Initiative Has
-Proactive Management and Oversight but Future Direction Is Uncertain
-OIG-10-52 February 2010
+Proactive Management and Oversight but Future Direction
+Is Uncertain OIG-10-52 February 2010
+********
-Search terms: behavior, cargo screening process; graph, flowchart
+Search terms: behavior, cargo screening process;
+graph, flowchart
Instructions: Run for Scope 1.
Scope 1: 6 traces in less than 1 sec.
diff --git a/models/Application_examples/Commercial_Flight b/models/Application_examples/Commercial_Flight
index 59e816829a6ad9e94b4592c8764f409d07d88a8a..87cd3951b834f20e3b6b57ef64ff64135a2a186f 100644
--- a/models/Application_examples/Commercial_Flight
+++ b/models/Application_examples/Commercial_Flight
@@ -4,19 +4,24 @@ Created by Mikhail Auguston on the 27th of November, 2013.
Edited by Keane Reynolds in July, 2021.
Edited by Pamela Dyer in July and August, 2021.
-Purpose: To show a system with many roots performing multiple actions, using COORDINATE and SHARE ALL statements
+Purpose: To show a system with many roots performing
+multiple actions, using COORDINATE and SHARE ALL statements
to make a complex web of actions linked together.
-Description: This model demonstrates the interlacing of root events as Phases
-and as Actors, in order to model a commercial flight. While complicated, users who take
-the time to understand this model can learn about how to use SHARE ALL to
-improve their models, and when to use COORDINATE instead. In addition, 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.
+Description: This model demonstrates the interlacing of
+root events as Phases and as Actors, in order to model a
+commercial flight. While complicated, users who take the
+time to understand this model can learn about how to use
+SHARE ALL to improve their models, and when to use
+COORDINATE instead. In addition, 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.
References:
-Search terms: behavior, commercial flight; event sharing; coordination, event
+Search terms: behavior, commercial flight; event sharing;
+coordination, event
Instructions: Run for Scope 1.
Scope 1: 2 traces in less than 1 sec.
diff --git a/models/Application_examples/Cycle_Pattern.mp b/models/Application_examples/Cycle_Pattern.mp
index 600d7f75f4d84db10fd5b03b7406bc1628db6b2a..40af3e137a3280989595a1028ac0edfa75da80aa 100644
--- a/models/Application_examples/Cycle_Pattern.mp
+++ b/models/Application_examples/Cycle_Pattern.mp
@@ -4,14 +4,14 @@ Created by Kristin Giammarco on the 10th of March, 2018.
Edited by Keane Reynolds in July, 2021.
Edited by Pamela Dyer in July and August, 2021.
-Purpose: To illustrate a cycle as a form of pattern that
-can be modeled in MP, and to show how commentary can be
-added to the traces.
-
-Description: 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
+Purpose: To illustrate a cycle as a form of pattern
+that can be modeled in MP, and to show how commentary
+can be added to the traces.
+
+Description: 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
generic terms that may be substituted with synonyms
such as "up" and "down," "in" and "out", "over"
and "under", "increase" and "decrease", etc., or
@@ -29,8 +29,9 @@ model when looking to use SAY or IF statements to
add the story to their traces.
References:
-Giammarco, Kristin, and Len Troncale. "Modeling Isomorphic Systems Processes Using
-Monterey Phoenix." Systems 6, no. 2 (2018): 18.
+Giammarco, Kristin, and Len Troncale. "Modeling
+Isomorphic Systems Processes Using Monterey Phoenix."
+Systems 6, no. 2 (2018): 18.
https://doi.org/10.3390/systems6020018
https://www.mdpi.com/2079-8954/6/2/18
@@ -38,11 +39,13 @@ https://www.mdpi.com/2079-8954/6/2/18
**** Remove this part ****
Cycle_ISP Model for Systems Journal Article
Available at https://www.mdpi.com/2079-8954/6/2/18
+********
-Search terms: behavior, cycle pattern; ENSURE condition; IF statement; SAY statement; isomorphism
+Search terms: behavior, cycle pattern; ENSURE condition;
+IF statement; SAY statement; isomorphism
-Instructions: Run for Scopes 2 and 3. (Scope 1 generates zero traces because
-of the ENSURE constraint.)
+Instructions: Run for Scopes 2 and 3. (Scope 1 generates
+zero traces because of the ENSURE constraint.)
Scope 1: 0 traces in less than 1 sec.
Scope 2: 40 traces in less than 1 sec.
Scope 3: 2952 traces in approx. 2.9 sec.
diff --git a/models/Application_examples/Dining_Philosophers.mp b/models/Application_examples/Dining_Philosophers.mp
index 7cd8dd42257cffdf3ae4e15a30806748765e95d2..5aec54755810e585e1920658ee10542b03667700 100644
--- a/models/Application_examples/Dining_Philosophers.mp
+++ b/models/Application_examples/Dining_Philosophers.mp
@@ -8,48 +8,58 @@ Purpose: To illustrate the extensive logic and problem
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 sort of riddle. The logic and problem
-solving potential of Monterey Phoenix is showcased through its ability
-to come up with exhaustive solutions to multiple variations of a complex
+Description: This model demonstrates using COORDINATE, ENSURE,
+and IF statements to come up with an answer to a sort of
+riddle. The logic and problem solving potential of Monterey
+Phoenix is showcased through its ability to come up with
+exhaustive solutions to multiple variations of a complex
puzzle with some code and constraints.
-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.
-
-Each philosopher must alternately think and eat. However, a philosopher
-can only eat spaghetti when he has both left and right forks.
-Each fork can be held by one philosopher only and so a philosopher can use
-the fork only if it's not being used by another philosopher.
-After he finishes eating, he needs to put down both forks so they become
-available to others. A philosopher can grab the fork on his right or
-the one on his left as they become available, but can't start eating
-before getting both of them.
-
-Eating is not limited by the amount of spaghetti left: assume an infinite
-supply. The problem is how to design a discipline of behavior (a concurrent
-algorithm) such that each philosopher won't starve; i.e., can forever
-continue to alternate between eating and thinking assuming that any
+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.
+
+Each philosopher must alternately think and eat. However, a
+philosopher can only eat spaghetti when he has both left and
+right forks. Each fork can be held by one philosopher only
+and so a philosopher can use the fork only if it's not being
+used by another philosopher. After he finishes eating, he
+needs to put down both forks so they become available to
+others. A philosopher can grab the fork on his right or the
+one on his left as they become available, but can't start
+eating before getting both of them.
+
+Eating is not limited by the amount of spaghetti left: assume
+an infinite supply. The problem is how to design a discipline
+of behavior (a concurrent algorithm) such that each
+philosopher won't starve; i.e., can forever continue to
+alternate between eating and thinking assuming that any
philosopher cannot know when others may want to eat or think.
This MP model provides abstract specification of correct
behaviors, but does not provide implementation details.
-Since MP supports automated use case extraction, this model may be used
-as a source of test cases for testing the implementation.
+Since MP supports automated use case extraction, this model
+may be used as a source of test cases for testing
+the implementation.
References:
-"Dining philosophers problem." Wikipedia. Wikimedia Foundation, August 6, 2021.
+"Dining philosophers problem." Wikipedia. Wikimedia
+Foundation, August 6, 2021.
https://en.wikipedia.org/wiki/Dining_philosophers_problem
**** Remove this part ****
Explanation of the problem from Wikipedia: http://en.wikipedia.org/wiki/Dining_philosophers_problem
+********
-Search terms: behavior, dining philosophers; riddles; behavior, ring topology; event reshuffling; BUILD block; isomorphism
+Search terms: behavior, dining philosophers; riddles;
+behavior, ring topology; event reshuffling; BUILD block;
+isomorphism
-Instructions: Run for Scope 1. This will generate zero traces because
-a philosopher cannot eat with a single fork. Then run for Scopes 2 and up.
+Instructions: Run for Scope 1. This will generate zero
+traces because a philosopher cannot eat with a single fork.
+Then run for Scopes 2 and up.
Scope 1: 0 traces in less than 1 sec.
Scope 2: 2 traces in less than 1 sec.
Scope 3: 6 traces in less than 1 sec.
diff --git a/models/Application_examples/Elevator.mp b/models/Application_examples/Elevator.mp
index 104617bca352e252d281dacdcb418466be478d54..7721515c5581e7dfc36fe29b26d1d5926d925d69 100644
--- a/models/Application_examples/Elevator.mp
+++ b/models/Application_examples/Elevator.mp
@@ -4,11 +4,12 @@ Created by Kristin Giammarco circa 2011.
Edited by Keane Reynolds in July, 2021.
Edited by Pamela Dyer in July and August, 2021.
-Purpose: To demonstrate how under-constraining a model can be beneficial,
-because it can lead to emergent behavior showing up in the traces.
+Purpose: To demonstrate how under-constraining a model
+can 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:
+Description: This demonstrates the modeling of situations
+and consequential events in MP. The pattern is:
( SituationA do_one_thing |
SituationB do_another_thing )
@@ -18,17 +19,19 @@ in the case of this model,
( Elevator_works_fine Get_Off |
Emergency_Situation Call_for_help )
-Ultimately, this is a simple model of an emergency scenario involving an
-elevator with very few constraints. This allows
-for more variance, which leads to emergent behavior. Users should use
-this as an example of how under-constraining your model can be beneficial.
-Constraints should only be limited to necessity, or to remove traces that
-no longer need to be considered. When in doubt, add a constraint, and then
-comment it out. Bring it back later if needed.
+Ultimately, this is a simple model of an emergency scenario
+involving an elevator with very few constraints. This
+allows for more variance, which leads to emergent behavior.
+Users should use this as an example of how under-constraining
+your model can be beneficial. Constraints should only be
+limited to necessity, or to remove traces that no longer
+need to be considered. When in doubt, add a constraint, and
+then comment it out. Bring it back later if needed.
References:
-Search terms: behavior, elevator; event sharing; coordination, event; behavior, emergent
+Search terms: behavior, elevator; event sharing;
+coordination, event; behavior, emergent
Instructions: Run for Scope 1.
Scope 1: 3 traces in less than 1 sec.
diff --git a/models/Application_examples/FindAdvisor.mp b/models/Application_examples/FindAdvisor.mp
index 7c494ff7c5547444c4dff3359541b26b9967f145..de0fa912b07b2027f562604678f31b1da8f3863e 100644
--- a/models/Application_examples/FindAdvisor.mp
+++ b/models/Application_examples/FindAdvisor.mp
@@ -4,25 +4,32 @@ Created by Kristin Giammarco.
Edited by Keane Reynolds in July, 2021.
Edited by Pamela Dyer in July and August, 2021.
-Purpose: To show that human interaction and organizational processes can be modeled as well as technological
-system and subsystem interactions.
-
-Description: Alternate behaviors for humans are described in
-terms of possible decisions they could make. In this example, the process of a student finding an advisor for a potentially
-MP-related research topic is modeled. To do so, it only uses
-roots, composites, "or" blocks, and COORDINATE statements. Users should inspect this
-model when considering the process of finding a mentor, or looking to learn how to
-use COORDINATE statements to make a model. Because the same modeling approach can be used for human systems and technological systems,
-it becomes possible to have integrated behavior models containing both humans and
+Purpose: To show that human interaction and organizational
+processes can be modeled as well as technological system
+and subsystem interactions.
+
+Description: Alternate behaviors for humans are described
+in terms of possible decisions they could make. In this
+example, the process of a student finding an advisor for a
+potentially MP-related research topic is modeled. To do so,
+it only uses roots, composites, "or" blocks, and COORDINATE
+statements. Users should inspect this model when considering
+the process of finding a mentor, or looking to learn how to
+use COORDINATE statements to make a model. Because the same
+modeling approach can be used for human systems and
+technological systems, it becomes possible to have
+integrated behavior models containing both humans and
technology to study the possible interactions among them.
References:
-Search terms: behavior, finding advisor; human interactions modeling; behavior, human systems
+Search terms: behavior, finding advisor;
+human interactions modeling; behavior, human systems
-Instructions: Run for Scope 1 (there is no iteration in this example, so increasing the scope will not
-produce more scenarios). "Sequence" mode yields views very similar to the UML or SysML
-Sequence Diagrams.
+Instructions: Run for Scope 1 (there is no iteration in
+this example, so increasing the scope will not produce more
+scenarios). "Sequence" mode yields views very similar to
+the UML or SysML Sequence Diagrams.
Scope 1: 3 traces in less than 1 sec.
==========================================================*/
diff --git a/models/Application_examples/First_Responder.mp b/models/Application_examples/First_Responder.mp
index 9dd808ddab8250b3216e394dd4943784c33cbc15..0586f2d6dfc76153951ad488b6cdd847c774cf81 100644
--- a/models/Application_examples/First_Responder.mp
+++ b/models/Application_examples/First_Responder.mp
@@ -4,26 +4,31 @@ Created by Jordan Bryant in May, 2016.
Edited by Keane Reynolds in July, 2021.
Edited by Pamela Dyer in July and August, 2021.
-Purpose: To demonstrate a first responder scenario involving the administation of a rescue
-medication (Narcan) to an overdose victim by a First Responder or a
-Bystander.
-
-Description: This model demonstrates the administration of Narcan by bystanders
-in order to determine the possible consequences of allowing or even
-encouraging bystanders to administer medication in an overdose scenario.
-The model accomplishes this using "or" blocks and COORDINATE statements.
-Users may find this model useful when looking into COORDINATE statements,
-or scenarios with bystanders who could possibly become involved in whatever
-process is being modeled.
+Purpose: To demonstrate a first responder scenario
+involving the administation of a rescue medication (Narcan)
+to an overdose victim by a First Responder or a Bystander.
+
+Description: This model demonstrates the administration of
+Narcan by bystanders in order to determine the possible
+consequences of allowing or even encouraging bystanders to
+administer medication in an overdose scenario. The model
+accomplishes this using "or" blocks and COORDINATE
+statements. Users may find this model useful when looking
+into COORDINATE statements, or scenarios with bystanders
+who could possibly become involved in whatever process
+is being modeled.
References:
-Search terms: behavior, first responder; behavior, bystander; behavior, unexpected; behavior, emergent
+Search terms: behavior, first responder;
+behavior, bystander; behavior, unexpected;
+behavior, emergent
-Instructions: Run for Scope 1. The model was developed to compare response times, but unexpected
-scenarios emerged that were previously not considered. Trace 6 and others
-show a double administration of Narcan by both the bystander and the first
-responder.
+Instructions: Run for Scope 1. The model was developed to
+compare response times, but unexpected scenarios emerged
+that were previously not considered. Trace 6 and others
+show a double administration of Narcan by both the
+bystander and the first responder.
Scope 1: 8 traces in less than 1 sec.
==========================================================*/
diff --git a/models/Application_examples/Knapsack_Weight_Limit.mp b/models/Application_examples/Knapsack_Weight_Limit.mp
index faec4d2625dbdb1800e618bd8a654cc384f76b16..6a77a33182ee89c2e0caa26a00947c3ae12ef6f3 100644
--- a/models/Application_examples/Knapsack_Weight_Limit.mp
+++ b/models/Application_examples/Knapsack_Weight_Limit.mp
@@ -8,30 +8,36 @@ Purpose: To illustrate the process of searching for all
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 NP-complete
-with respect to the number N of items and to the weight limit W.
-It has been proven that the computational complexity is O(N * W)
-
-This example demonstrates MP template for performing "brute force" search
-for all optimal solutions within the given scope
-(certainly not the optimal performance, but is acceptable for relatively
-small N,in particular, it stabilizes at scope 4).
-
-Ultimately, this model demonstrates using GLOBAL limits to exhaustively calculate all
-the combinations of items that can be put into a bag to not exceed the weight
-limit. Users can reference this model to learn about solving logic problems
-with MP constraints.
+Description: This is a case of well-known Knapsack Dynamic
+Programming Problem. In general it is NP-hard and
+NP-complete with respect to the number N of items and to
+the weight limit W. It has been proven that the
+computational complexity is O(N * W)
+
+This example demonstrates MP template for performing
+"brute force" search for all optimal solutions within the
+given scope (certainly not the optimal performance, but is
+acceptable for relatively small N, in particular, it
+stabilizes at scope 4).
+
+Ultimately, this model demonstrates using GLOBAL limits to
+exhaustively calculate all the combinations of items that
+can be put into a bag to not exceed the weight limit.
+Users can reference this model to learn about solving
+logic problems with MP constraints.
References:
-"Knapsack problem." Wikipedia. Wikimedia Foundation, August 26, 2021.
+"Knapsack problem." Wikipedia. Wikimedia Foundation,
+August 26, 2021.
https://en.wikipedia.org/wiki/Knapsack_problem
**** Remove this part ****
Information on computational complexity from Wikipedia at https://en.wikipedia.org/wiki/Knapsack_problem
+********
-Search terms: event attribute, number; optimization, weight; BUILD block; WITHIN command; report, global
+Search terms: event attribute, number; optimization, weight;
+BUILD block; WITHIN command; report, global
Instructions: Run for Scopes 1 and up.
Scope 1: 4 traces in less than 1 sec.
diff --git a/models/Application_examples/MP_Architecture_Specification.mp b/models/Application_examples/MP_Architecture_Specification.mp
index a142008d1c593ee19a435cd3a809d1cf69607f7b..33c156569bddee4783e81ae597d9bdcef4349838 100644
--- a/models/Application_examples/MP_Architecture_Specification.mp
+++ b/models/Application_examples/MP_Architecture_Specification.mp
@@ -7,8 +7,8 @@ Edited by Pamela Dyer in July and August, 2021.
Purpose: To illustrate an architecture model surrounding
the MP compiler/trace generator process.
-Description: This model demonstrates how a user might use an MP
-IDE to develop an MP model. This model contains many
+Description: This model demonstrates how a user might use
+an MP IDE to develop an MP model. This model contains many
types of interactions and goes through the process of
making a model, so beginner and intermediate users may
find this model helpful for learning about the modeling
@@ -17,7 +17,9 @@ SHARE ALL, SAY, GRAPH, etc.) can create relationships.
References:
-Search terms: architecture; trace annotation; behavior, compiler; behavior, parser; graph, component diagram; report, global; isomorphism
+Search terms: architecture; trace annotation;
+behavior, compiler; behavior, parser;
+graph, component diagram; report, global; isomorphism
Instructions: Run for Scopes 1 and 2.
Scope 1: 16 traces in less than 1 sec.
diff --git a/models/Application_examples/Manufacturing_Process.mp b/models/Application_examples/Manufacturing_Process.mp
index 3396de1db6fda191fd0cde4c8a57526875446b88..68380d0c5abf0ed827eebfe5dcc2d7adbf621d84 100644
--- a/models/Application_examples/Manufacturing_Process.mp
+++ b/models/Application_examples/Manufacturing_Process.mp
@@ -4,22 +4,30 @@ Created by John Palmer in August, 2014.
Edited by Keane Reynolds in July, 2021.
Edited by Pamela Dyer in July and August, 2021.
-Purpose: To demonstrate a model of a system manufacturing process,
-while taking advantage of being able to use local scopes.
-
-Description: This model demonstrates application of Monterey Phoenix Modeling to Manufacturing Product Systems.
-This is an example pre-dating MP-Firebird application that was used to generate scenarios
-for separately estimating probability, time, and cost of each of these scenarios.
-MP version 4 may be used to conduct such analysis with its native capabilities.
-
-Ultimately, this model demonstrates a manufacturing system made from only standard ROOT
-statements, "or" blocks, SHARE ALL statements, iteration, and scope limits.
-This manufacturing system has several actors simultaniously performing jobs,
-so users may look to this model for a simple way of designing a system.
+Purpose: To demonstrate a model of a system manufacturing
+process, while taking advantage of being able to use
+local scopes.
+
+Description: This model demonstrates application of Monterey
+Phoenix Modeling to Manufacturing Product Systems. This is
+an example pre-dating MP-Firebird application that was used
+to generate scenarios for separately estimating probability,
+time, and cost of each of these scenarios. MP version 4
+may be used to conduct such analysis with its
+native capabilities.
+
+Ultimately, this model demonstrates a manufacturing system
+made from only standard ROOT statements, "or" blocks,
+SHARE ALL statements, iteration, and scope limits. This
+manufacturing system has several actors simultaniously
+performing jobs, so users may look to this model for
+a simple way of designing a system.
References:
-Search terms: behavior, manufacturing process; manufacturing system; event sharing; probability analysis; nested iteration
+Search terms: behavior, manufacturing process;
+manufacturing system; event sharing; probability analysis;
+nested iteration
Instructions: Run for Scope 1.
Scope 1: 8 traces in approx. 1.4 min.
diff --git a/models/Application_examples/Martian_Lander.mp b/models/Application_examples/Martian_Lander.mp
index b3b6746f38aa964eefbbaf95048979acf057ce92..afdd53ca9873c53fc73828e8d1f10a383f3a7921 100644
--- a/models/Application_examples/Martian_Lander.mp
+++ b/models/Application_examples/Martian_Lander.mp
@@ -1,33 +1,37 @@
/* Model of Martian Lander
MP model written by Mikhail Auguston following example 1
-and Appendix B from (Jahanian and Mok 1986).
+ and Appendix B from (Jahanian and Mok 1986).
Edited by Keane Reynolds in July, 2021.
Edited by Pamela Dyer in July and August, 2021.
Purpose: To illustrate a landing system for a Martian 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 (an external event), it operates in the
-normal mode. While in the normal landing mode, the pilot can control
-acceleration, velocity, and position by adjusting the downward thrust
-generated by the rocket motor, thus bringing the space vehicle to a
-safe landing. This task is continually performed in two phases.
-
-In phase 1, an I/O device is started to read the acceleration set
-by the pilot, and a hardware timer is started which generates a timer
-interrupt (i.e., external event TMRINT) after 100 ms. In phase 2,
-when the I/O operation is completed (i.e., external event IOINT),
-the motor thrust is adjusted appropriately. However, if for some
-reason the I/O operation is not done within 100 ms, the timer interrupt
-initiates the emergency landing mode. While in the emergency mode,
-the altitude and velocity is periodically sampled and a retro-rocket
-is automatically fired to bring the vehicle to a safe landing.
+Description: The landing system operates in one of two modes:
+normal or emergency. When the system is turned on (an external
+event), it operates in the normal mode. While in the normal
+landing mode, the pilot can control acceleration, velocity,
+and position by adjusting the downward thrust generated by
+the rocket motor, thus bringing the space vehicle to a safe
+landing. This task is continually performed in two phases.
+
+In phase 1, an I/O device is started to read the acceleration
+set by the pilot, and a hardware timer is started which
+generates a timer interrupt (i.e., external event TMRINT)
+after 100 ms. In phase 2, when the I/O operation is completed
+(i.e., external event IOINT), the motor thrust is adjusted
+appropriately. However, if for some reason the I/O operation
+is not done within 100 ms, the timer interrupt initiates the
+emergency landing mode. While in the emergency mode, the
+altitude and velocity is periodically sampled and a
+retro-rocket is automatically fired to bring the vehicle
+to a safe landing.
Events and actions:
RACC Starts IO device to read acceleration
-STMR Start hardware watchdog timer, this model has two timers
+STMR Start hardware watchdog timer, this model has
+ two timers
ADJM Adjust motor thrust
TDP Transmit info to display panel
IEM Initiate emergency mode
@@ -38,7 +42,8 @@ CKDT Check input data for consistency
RRM Retro-rocket module
START Systems start up,
IOINT I/O device signals completion
-TMRINT Timer Interrupt, occurs at least 100 ms after start of STMR
+TMRINT Timer Interrupt, occurs at least 100 ms after
+ start of STMR
Action Time in ms
RACC 10
@@ -52,12 +57,13 @@ IALT 20
CKDT 10
RRM 10
-In summary, this model demonstrates the use of COORDINATE statements to model
-the relationships of an unlikely and unfamiliar situation, and then
-make the situation easier to understand using charts and "comments"
-from SAY statements. Users can reference this model for advice on
-COORDINATE statements and using MP to add graphs and commentary to
-traces automatically.
+In summary, this model demonstrates the use of COORDINATE
+statements to model the relationships of an unlikely and
+unfamiliar situation, and then make the situation easier
+to understand using charts and "comments" from
+SAY statements. Users can reference this model for advice
+on COORDINATE statements and using MP to add graphs and
+commentary to traces automatically.
References:
Jahanian, Farnam, and Aloysius Ka-Lau Mok. "Safety Analysis
@@ -73,8 +79,12 @@ Farnam Jahanian, Aloysius Ka-Lau Mok
"Safety analysis of timing properties in real-time systems",
IEEE Transactions on Software Engineering
Year: 1986, Volume SE-12, Issue 9, pp.890-904
+********
-Search terms: Martian Lander system; behavior, landing system; event attribute, timing; trace annotation; table; graph, Gantt chart; graph, bar chart
+Search terms: Martian Lander system;
+behavior, landing system; event attribute, timing;
+trace annotation; table; graph, Gantt chart;
+graph, bar chart
Instructions: Run for Scopes 1 and up.
Scope 1: 3 traces in less than 1 sec.
diff --git a/models/Application_examples/Prisoners_Dilemma.mp b/models/Application_examples/Prisoners_Dilemma.mp
index a9ff341917c8dc507a6841896bc3b6c254a5caaf..55d1eb4d7c1e5aa3a298b28ed6beca0766bf6888 100644
--- a/models/Application_examples/Prisoners_Dilemma.mp
+++ b/models/Application_examples/Prisoners_Dilemma.mp
@@ -10,36 +10,39 @@ game scenario.
Description: Users looking to model exhaustive logical
game scenarios may want to use this model as an example.
-In this case, the classic model is the output in the traces
+In this case, the classic model is the output in the traces
of the model with the payouts as documented in (Straffin 1993).
-Different in this MP model is how the payouts
-are computed. Most models just assume the final
-amount of payouts for the matrix game.
+Different in this MP model is how the payouts
+are computed. Most models just assume the final
+amount of payouts for the matrix game.
-Here the payout for Alice, and Bob respectively,
+Here the payout for Alice, and Bob respectively,
is computed from
-"Alice's view of the payoff for each possible event independently of Bob's view"
+"Alice's view of the payoff for each possible event
+independently of Bob's view"
This is represented by the columns in the tables below.
-A simple arithmetic derivation from those columns is computed to have the
-trace generation output each matrix element of the game as
-a separate trace in the MP output.
+A simple arithmetic derivation from those columns is
+computed to have the trace generation output each matrix
+element of the game as a separate trace in the MP output.
-Future work is to include other obvious matrices readily constructed
-from this to be generated as part of the trace generation.
+Future work is to include other obvious matrices readily
+constructed from this to be generated as part of the
+trace generation.
This would represent something like a class of matrix games
to be constructed by the schema, one of which would be
the classic two person prisoners dilemma.
-Notice that this code is almost exactly like
-MP native Example 23 -- number attributes.
-That example is about a buyer purchasing different products
+Notice that this code is almost exactly like
+MP native Example 23 -- number attributes.
+That example is about a buyer purchasing different products
from different stores.
-A related version of the prisoners dilemma to shopping is
-documented at the Wikipedia article cited below. "The donation game."
+A related version of the prisoners dilemma to shopping is
+documented at the Wikipedia article cited below.
+"The donation game."
This model is only meant to be run at Scope 1.
@@ -53,8 +56,9 @@ the payoff for Bob when he confesses = 1.
the payoff for Bob when Alice does not confess = 2.
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.
+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.
References:
Straffin, Philip D. "12. The Prisoner's Dilemma." in Game
@@ -76,12 +80,13 @@ Kuhn, Steven. "Prisoner’s Dilemma." The Stanford
Mathematical Association of America 1993
isbn: 0-88385-637-9
Chapter 12, page 73.
-
https://en.wikipedia.org/wiki/Prisoner%27s_dilemma
-
https://plato.stanford.edu/entries/prisoner-dilemma/#Symm2t2PDOrdiPayo
+********
-Search terms: behavior, prisoners dilemma; behavior, matrix game; event attribute, number; BUILD block; SAY statement; isomorphism
+Search terms: behavior, prisoners dilemma;
+behavior, matrix game; event attribute, number;
+BUILD block; SAY statement; isomorphism
Instructions: Run for Scope 1.
Scope 1: 4 traces in less than 1 sec.
diff --git a/models/Application_examples/Railroad_Crossing_Safety.mp b/models/Application_examples/Railroad_Crossing_Safety.mp
index 704e95b0cc367e5ebca9a6db5f7b4562e1a1755f..17091b4ed4891cc6459df20e93792ce5d7b161f2 100644
--- a/models/Application_examples/Railroad_Crossing_Safety.mp
+++ b/models/Application_examples/Railroad_Crossing_Safety.mp
@@ -7,16 +7,20 @@ Edited by Pamela Dyer in July and August, 2021.
Purpose: 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 at a railroad crossing, in which time is a defining
-factor of many events. Users should look to this model when in need of an
-example of using BUILD statements to add time, COORDINATE constraint usage,
-CHECK statements used to catch unwanted behavior, and SAY statement comments to
-improve a model's clarity.
-
-The original railroad crossing example was from (Heitmeyer and Mandrioli 1996).
-The system operates a gate at a railroad crossing. A sensor determines when
-each train enters and exits the crossing’s region. The main safety requirement is: if a train is in the crossing region,
+Description: This model demonstrates using BUILD statements
+to add time to a model of car and train interactions at a
+railroad crossing, in which time is a defining factor of
+many events. Users should look to this model when in need
+of an example of using BUILD statements to add time,
+COORDINATE constraint usage, CHECK statements used to catch
+unwanted behavior, and SAY statement comments to improve
+a model's clarity.
+
+The original railroad crossing example was from (Heitmeyer
+and Mandrioli 1996). The system operates a gate at a
+railroad crossing. A sensor determines when 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.
References:
@@ -24,7 +28,8 @@ Heitmeyer, Constance, and Dino Mandrioli. Formal Methods
for Real-Time Computing. New York, NY: John Wiley & Sons,
Inc., 1996.
-Search terms: behavior, railroad crossing; safety requirement; failure mode; event attribute, timing
+Search terms: behavior, railroad crossing;
+safety requirement; failure mode; event attribute, timing
Instructions: Run for Scopes 1 and up.
Scope 1: 1 trace in less than 1 sec.
diff --git a/models/Application_examples/Replay_Attack.mp b/models/Application_examples/Replay_Attack.mp
index 34b1e65d9298bac1e829bd948697078d142d6a34..4e2cedd70a269574ce18915c87368567c5bb81dc 100644
--- a/models/Application_examples/Replay_Attack.mp
+++ b/models/Application_examples/Replay_Attack.mp
@@ -7,14 +7,15 @@ Edited by Pamela Dyer in July and August, 2021.
Purpose: To illustrate MP modeling of a replay attack
involving data transmission.
-Description: This model demonstrates using COORDINATE statements
-to form relationships in a communication system with
-a 3rd party listening in. Users should use this model
+Description: This model demonstrates using COORDINATE
+statements to form relationships in a communication system
+with a 3rd party listening in. Users should use this model
as an example of possible 3rd parties in other systems,
and using COORDINATE statements to form relationships.
References:
-"Replay attack." Wikipedia. Wikimedia Foundation, July 1, 2021.
+"Replay attack." Wikipedia. Wikimedia Foundation,
+July 1, 2021.
https://en.wikipedia.org/wiki/Replay_attack
@@ -22,8 +23,10 @@ https://en.wikipedia.org/wiki/Replay_attack
The description of Replay Attack
is available at
https://en.wikipedia.org/wiki/Replay_attack
+********
-Search terms: behavior, replay attack; message eavesdropping; coordination, event
+Search terms: behavior, replay attack;
+message eavesdropping; coordination, event
Instructions: Run for Scopes 1 and up.
Scope 1: 2 traces in less than 1 sec.
diff --git a/models/Application_examples/Small_Package_Delivery.mp b/models/Application_examples/Small_Package_Delivery.mp
index 7007e3810ca00a063e45810b220178d135f0d029..89de12c04ae27f3eedf4fd9f7302c11dd1d9553a 100644
--- a/models/Application_examples/Small_Package_Delivery.mp
+++ b/models/Application_examples/Small_Package_Delivery.mp
@@ -1,41 +1,47 @@
/* Model of Small Package Delivery
Non-combatant Scenario 1 authored by Nataki Roberts (Engility).
-MP model authored by Kristin Giammarco (NPS) and David Shifflett (NPS).
+MP model authored by Kristin Giammarco (NPS) and
+ David Shifflett (NPS).
Edited by Keane Reynolds in July, 2021.
Edited by Pamela Dyer in July and August, 2021.
-Purpose: To illustrate the impacts of overloading constraints
-in a model in MP, by means of a complex emergency situation
-out at sea.
-
-Description: This model demonstrates overusing COORDINATE and ENSURE statements to
-create a model of a complex emergency situation that has been
-overconstrained to the point that intended behavior has also been
-constrained out. Users should consider this model a demonstration of how
-building a complex scenario without frequently running the model can
-make finding parts of the model overloaded with constraints difficult.
-
-Taken from use case description in the Skyzer IM20 Mission Model
-(Non-Combatant Operations Scenario):
-
-"Family traveling from PR to Florida in a 1984 Catalina 36 have an
-emergency out on sea. A 40 year old father is diabetic and has ran [sic]
-out of insulin and because he is the main sail operator, the family is
-suck [sic] at sea until medical attention can arrived [sic]. The major
-problem is that the USCG Cutter is four hours out on another mission, from
-the last known location point of the sailboat last communication
-beacon. But the there is a Navy ship in closer proximity with UAV
-capabilities. The USS Fitzgerald is 75 nm from that last know location
-point and has the needed medical supplies. USS Fitzgerald also has
-UAV capabilities to transport the supplies in the required time line.
-This Navy capability can provide the needed supplies within the
-required time line without risk of placing the patient at risk of a
-diabetic coma. The Navy’s UAV can fly out to the sailboat and drop
-off the medical supplies until the USCG can arrived to transport
+Purpose: To illustrate the impacts of overloading
+constraints in a model in MP, by means of a complex
+emergency situation out at sea.
+
+Description: This model demonstrates overusing COORDINATE
+and ENSURE statements to create a model of a complex
+emergency situation that has been overconstrained to the
+point that intended behavior has also been constrained
+out. Users should consider this model a demonstration of
+how building a complex scenario without frequently
+running the model can make finding parts of the model
+overloaded with constraints difficult.
+
+Taken from use case description in the Skyzer IM20 Mission
+Model (Non-Combatant Operations Scenario):
+
+"Family traveling from PR to Florida in a 1984 Catalina 36
+have an emergency out on sea. A 40 year old father is
+diabetic and has ran [sic] out of insulin and because he
+is the main sail operator, the family is suck [sic] at sea
+until medical attention can arrived [sic]. The major
+problem is that the USCG Cutter is four hours out on
+another mission, from the last known location point of the
+sailboat last communication beacon. But the there is a
+Navy ship in closer proximity with UAV capabilities. The
+USS Fitzgerald is 75 nm from that last know location point
+and has the needed medical supplies. USS Fitzgerald also
+has UAV capabilities to transport the supplies in the
+required time line. This Navy capability can provide the
+needed supplies within the required time line without risk
+of placing the patient at risk of a diabetic coma. The
+Navy’s UAV can fly out to the sailboat and drop off the
+medical supplies until the USCG can arrived to transport
the family to safety.
-Depends on: range, sea states, weather, visibility, day, Night. Is it
-raining? Hailing?"
+Depends on: range, sea states, weather, visibility, day,
+Night. Is it raining? Hailing?"
References:
"Skyzer IM20 Mission Model (Non-Combatant Operations
@@ -45,17 +51,22 @@ Specifications." Final Technical Report SERC-2018-TR-116;
Systems Engineering Research Center: Hoboken, NJ,
USA, 2018.
-Search terms: small package delivery; autonomous; ENSURE condition; probability, Type 1
+Search terms: small package delivery; autonomous;
+ENSURE condition; probability, Type 1
Instructions: Run for Scope 1.
Scope 1: 2 traces in less than 1 sec.
-This model shows only two scenarios due to overloading constraints
-(constraints that suppress entire branches of execution that a user
-intended to permit). Commenting everything out except the SCHEMA definition and the Air_Vehicle
-root, and running that model subset at Scope 1, there are 6 event traces that can be seen.
-Two of these are unexpected. In Trace 5, there is no vessel in sight but the Air_Vehicle still
-drops the payload and the payload is on target. In Trace 6, there is no vessel in sight but
-the Air_Vehicle still drops the payload and the payload misses the target.
+This model shows only two scenarios due to overloading
+constraints (constraints that suppress entire branches of
+execution that a user intended to permit). Commenting
+everything out except the SCHEMA definition and the
+Air_Vehicle root, and running that model subset at Scope 1,
+there are 6 event traces that can be seen. Two of these are
+unexpected. In Trace 5, there is no vessel in sight but the
+Air_Vehicle still drops the payload and the payload is on
+target. In Trace 6, there is no vessel in sight but the
+Air_Vehicle still drops the payload and the payload misses
+the target.
==========================================================*/
diff --git a/models/Application_examples/Spent_Fuel_Cooling_and_Cleanup.mp b/models/Application_examples/Spent_Fuel_Cooling_and_Cleanup.mp
index 0d474421e541744fc3cbbf749f659cd169517ade..48a592cab20c4d25842902e7d6145d4815e69680 100644
--- a/models/Application_examples/Spent_Fuel_Cooling_and_Cleanup.mp
+++ b/models/Application_examples/Spent_Fuel_Cooling_and_Cleanup.mp
@@ -1,8 +1,10 @@
/* Model of Spent Fuel Cooling and Cleanup
Created by Kristin Giammarco on the 4th of May, 2020.
-Modified by Kristin Giammarco with Douglas VanBossuyt on the 8th of May, 2020.
-Modified by Kristin Giammarco with Douglas VanBossuyt on the 13th of May, 2020.
+Modified by Kristin Giammarco with Douglas VanBossuyt
+ on the 8th of May, 2020.
+Modified by Kristin Giammarco with Douglas VanBossuyt
+ on the 13th of May, 2020.
Edited by Keane Reynolds in July, 2021.
Edited by Pamela Dyer in July and August, 2021.
@@ -10,15 +12,17 @@ Purpose: To illustrate the modeling of a complex cooling
and purification system, specifically a spent nuclear fuel
cooling pool in this particular case.
-Description: This model demonstrates identifying the components of
-and interactions among a spent nuclear fuel cooling
-pool and its environment. Users may use this model to
-learn about interactions in a system and using COORDINATE
-statements to make comments on relationships.
+Description: This model demonstrates identifying the
+components of and interactions among a spent nuclear fuel
+cooling pool and its environment. Users may use this model
+to learn about interactions in a system and using
+COORDINATE statements to make comments on relationships.
References:
-Search terms: behavior, nuclear fuel cooling; coordination, event; heat exchanger; purification subsystem
+Search terms: behavior, nuclear fuel cooling;
+coordination, event; heat exchanger;
+purification subsystem
Instructions: Run for Scope 1.
Scope 1: 6 traces in approx. 1.4 sec.
diff --git a/models/Application_examples/Spiral_Software_Process b/models/Application_examples/Spiral_Software_Process
index 44d9540675191ea0a4c8caa8178f448ad285a6c1..9b4ee1af43f7ce238137a021011bc44751e6c371 100644
--- a/models/Application_examples/Spiral_Software_Process
+++ b/models/Application_examples/Spiral_Software_Process
@@ -7,17 +7,20 @@ Edited by Pamela Dyer in July and August, 2021.
Purpose: To illustrate significant usage of event sharing
in order to model the spiral software process.
-Description: This model demonstrates the usage of shared events to model the
-spiral software process to develop a prototype and release a product.
-Users may use this model to learn about SHARE ALL usage to make
-connections between roots. This example also illustrates how Melvin Conway's law
-can be modeled in MP: "organizations which design systems ...
-are constrained to produce designs which are copies of the
-communication structures of these organizations."
+Description: This model demonstrates the usage of shared
+events to model the spiral software process to develop a
+prototype and release a product. Users may use this model
+to learn about SHARE ALL usage to make connections between
+roots. This example also illustrates how Melvin Conway's
+law can be modeled in MP: "organizations which design
+systems ... are constrained to produce designs which are
+copies of the communication structures of
+these organizations."
References:
-Search terms: behavior, spiral software process; communication; architecture; event sharing
+Search terms: behavior, spiral software process;
+communication; architecture; event sharing
Instructions: Run for Scopes 1 and up.
Scope 1: 3 traces in less than 1 sec.
diff --git a/models/Application_examples/Surgery.mp b/models/Application_examples/Surgery.mp
index 40175548c991309bffca87736b26c0e323a1c53a..ac486f820bea69f316d6b607cd182f91a3e8590b 100644
--- a/models/Application_examples/Surgery.mp
+++ b/models/Application_examples/Surgery.mp
@@ -7,12 +7,14 @@ Edited by Pamela Dyer in July and August, 2021.
Purpose: To illustrate the modeling of a decision pattern
involving several actors, including the environment.
-Description: 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. In general, it demonstrates decisionmaking in a system with several actors
-capable of making choices that could affect the situation. Users may
-reference this model to learn about using ENSURE and COORDINATE statements
-to constrain a model and how to make a decision structure.
+Description: 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. In general,
+it demonstrates decisionmaking in a system with several
+actors capable of making choices that could affect the
+situation. Users may reference this model to learn about
+using ENSURE and COORDINATE statements to constrain a model
+and how to make a decision structure.
References:
Quartuccio, John, Kristin Giammarco, and Mikhail Auguston.
@@ -27,8 +29,10 @@ https://ieeexplore.ieee.org/document/7994952
"Identifying decision patterns using Monterey Phoenix" by Quartuccio, John,
Kristin Giammarco, and Mikhail Auguston.
Available at https://ieeexplore.ieee.org/abstract/document/7994952
+********
-Search terms: surgery process; behavior, environment; decision pattern; failure mode
+Search terms: surgery process; behavior, environment;
+decision pattern; failure mode
Instructions: Run for Scope 1.
Scope 1: 12 traces in less than 1 sec.
diff --git a/models/Application_examples/Swarm_Search_and_Track.mp b/models/Application_examples/Swarm_Search_and_Track.mp
index 51f9cacbad0099e4ec00864b98143ed65a3413f2..f74ab27792abe39e43c7d2b8006601785039810b 100644
--- a/models/Application_examples/Swarm_Search_and_Track.mp
+++ b/models/Application_examples/Swarm_Search_and_Track.mp
@@ -8,11 +8,11 @@ Edited by Pamela Dyer in July and August, 2021.
Purpose: To illustrate the incorporations of both
failure modes and failsafe behaviors into MP models.
-Description: This model demonstrates using a decision structure to
-model a UAV drone's target acquisition. Users may
-reference this model to learn about COORDINATE statements
-and or blocks when automatically generating traces with
-connections between roots.
+Description: This model demonstrates using a decision
+structure to model a UAV drone's target acquisition.
+Users may reference this model to learn about COORDINATE
+statements and "or" blocks when automatically generating
+traces with connections between roots.
Established naming convention:
Noun-oriented events are actors (root events)
@@ -24,7 +24,9 @@ This MP model "Swarm_Search_and_Track.mp" incorporates
Failure Modes and Failsafe Behaviors by elaborating on
the "Perform_Mission" event in the MP model "Swarm_UAV.mp".
-Search terms: behavior, swarm; search and track; autonomous; behavior, environment; failure mode; behavior, failsafe; behavior, unexpected; behavior, emergent
+Search terms: behavior, swarm; search and track; autonomous;
+behavior, environment; failure mode; behavior, failsafe;
+behavior, unexpected; behavior, emergent
Instructions: Run for Scope 1.
This model demonstrates the found unexpected behavior for
diff --git a/models/Application_examples/Swarm_UAV.mp b/models/Application_examples/Swarm_UAV.mp
index 8e7af8cd2a64ea8384d1fc224a75977036a9f3d1..f6987bfad89bdf410efdec2b564e935b48f6b54c 100644
--- a/models/Application_examples/Swarm_UAV.mp
+++ b/models/Application_examples/Swarm_UAV.mp
@@ -1,29 +1,35 @@
/* Model of Swarm UAV
Kristin Giammarco and Mikhail Auguston.
-MP Model based on "Swarm CONOPs" Draft on the 11th of February, 2015.
-Initial Model Started by Kristin Giammarco on the 11th of February, 2015.
-Mikhail Auguston merged several COORDINATE, SHARE ALL to speed up
-trace generation on the 25th of May, 2015.
-A few more coordinate statements were added to capture dependencies on the 22nd of July, 2015.
+MP Model based on "Swarm CONOPs" Draft on the 11th of
+ February, 2015.
+Initial Model Started by Kristin Giammarco on the 11th of
+ February, 2015.
+Mikhail Auguston merged several COORDINATE, SHARE ALL to
+ speed up trace generation on the 25th of May, 2015.
+A few more coordinate statements were added to capture
+ dependencies on the 22nd of July, 2015.
Edited by Keane Reynolds in July, 2021.
Edited by Pamela Dyer in July and August, 2021.
Purpose: To demonstrate the process of using iteration
within a root, taking effect when the scope is increased.
-Description: This model demonstrates using iteration to model multiple drones with similar
-duties. Users may reference this model as an example of using iteration to make
-multiple "roots" and connecting them with COORDINATE statements.
+Description: This model demonstrates using iteration to
+model multiple drones with similar duties. Users may
+reference this model as an example of using iteration to
+make multiple "roots" and connecting them with
+COORDINATE statements.
References:
-Search terms: behavior, swarm; autonomous; dependency tracking; coordination, nested composition
+Search terms: behavior, swarm; autonomous;
+dependency tracking; coordination, nested composition
Instructions: Run for Scopes 1, 2, and 3.
-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).
+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).
Scope 1: 1 trace in less than 1 sec.
Scope 2: 3 traces in approx. 2.2 sec.
Scope 3: 6 traces in approx. 21 sec.
diff --git a/models/Application_examples/Turtles_in_the_Desert.mp b/models/Application_examples/Turtles_in_the_Desert.mp
index 37f0a2a776f5762ac981826e514cb081ba156681..f00bdbfea95e9df22a0f656f6d35838ac209049c 100644
--- a/models/Application_examples/Turtles_in_the_Desert.mp
+++ b/models/Application_examples/Turtles_in_the_Desert.mp
@@ -4,27 +4,40 @@ Created by Mikhail Auguston.
Edited by Keane Reynolds in July, 2021.
Edited by Pamela Dyer in July and August, 2021.
-Purpose: To demonstrate using MP to solve a logic puzzle with exhaustive trace
-generation, thereby 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: "What do you see?" It answered: "I see nobody before me and two turtles behind." The second turtle has been asked the same question: "What do you see?" and answered "I see one turtle before me and one behind." When the third turtle is asked the same question, it answers: "I see one turtle before me and one behind." How could that be?
+Purpose: To demonstrate using MP to solve a logic puzzle
+with exhaustive trace generation, thereby 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: "What
+do you see?" It answered: "I see nobody before me and two
+turtles behind." The second turtle has been asked the same
+question: "What do you see?" and answered "I see one turtle
+before me and one behind." When the third turtle is asked
+the same question, it answers: "I see one turtle before me
+and one behind." How could that be?
Don't try to construct a non-Euclidean geometry to
-accommodate the possible turtle configuration. A person with common sense
-after a short moment of time will say: "The third is lying!" The
-reaction will be: "Ahh, yes! But wait, maybe the first is lying, or the second,
+accommodate the possible turtle configuration. A person
+with common sense after a short moment of time will say:
+"The third is lying!" The reaction will be: "Ahh, yes! But
+wait, maybe the first is lying, or the second,
or all three of them. It becomes too complicated...."
-Now it is time to use MP to obtain all possible scenarios for that story.
+Now it is time to use MP to obtain all possible scenarios
+for that story.
-Users may use this model as an example of using IF, ENSURE, and
-BUILD statements to constrain models as logical problem solving tools.
+Users may use this model as an example of using IF, ENSURE,
+and BUILD statements to constrain models as logical problem
+solving tools.
References:
-Search terms: riddles; ENSURE condition; BUILD block; SAY statement; MARK command; predicate logic
+Search terms: riddles; ENSURE condition; BUILD block;
+SAY statement; MARK command; predicate logic
-Instructions: Run for Scope 1. There are 13 possible scenarios, and none when all three are telling the truth.
+Instructions: Run for Scope 1. There are 13 possible
+scenarios, and none when all three are telling the truth.
Scope 1: 13 traces in less than 1 sec.
==========================================================*/
diff --git a/models/Application_examples/UAV_Ingress.mp b/models/Application_examples/UAV_Ingress.mp
index 8dbf3aa4d72482943987d6230bce85e24f19ece2..b6250d535016d3c1f2f8a440ebe0c51ad8535aa2 100644
--- a/models/Application_examples/UAV_Ingress.mp
+++ b/models/Application_examples/UAV_Ingress.mp
@@ -4,21 +4,25 @@ Created by Anthony Constable in May, 2017.
Edited by Keane Reynolds in July, 2021.
Edited by Pamela Dyer in July and August, 2021.
-Purpose: To demonstrate a coordinated UAV flight scenario with
-multiple teams involved in making the launch and flight happen.
+Purpose: To demonstrate a coordinated UAV flight scenario
+with multiple teams involved in making the launch and
+flight happen.
-Description: This model specifies the ingress phase of the UAS HADR
-reference mission. The ingress phase is preceded by the preflight
-phase, and followed by the on-station phase. Users may use this model to learn about forming relationships
-between roots using COORDINATE statements.
+Description: This model specifies the ingress phase of the
+UAS HADR reference mission. The ingress phase is preceded
+by the preflight phase, and followed by the on-station
+phase. Users may use this model to learn about forming
+relationships between roots using COORDINATE statements.
References:
-Search terms: behavior, UAV ingress; autonomous; behavior, unexpected; behavior, emergent
+Search terms: behavior, UAV ingress; autonomous;
+behavior, unexpected; behavior, emergent
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).
+This model contains an unexpected behavior in which the
+UAV status is acceptable but the operator aborts
+the ingress (trace 2).
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 6fd0b5aa9452ec6fbc8f2d3be90049b013f730e8..f40c2e7698ffbfb6f5e4e7de44a7acba0d25c715 100644
--- a/models/Application_examples/UAV_OnStation.mp
+++ b/models/Application_examples/UAV_OnStation.mp
@@ -1,20 +1,24 @@
/* Model of UAV On Station
Created by Kristin Giammarco on the 3rd of February, 2017.
-Modified by Kristin Giammarco on the 4th of February, 2017 to remove normal events from failure mode scenarios.
-Modified by Kristin Giammarco on the 5th of February, 2017 to add normal events back to failure mode scenarios
-and added annotations.
+Modified by Kristin Giammarco on the 4th of February, 2017
+ to remove normal events from failure mode scenarios.
+Modified by Kristin Giammarco on the 5th of February, 2017
+ to add normal events back to failure mode scenarios and
+ added annotations.
Edited by Keane Reynolds in July, 2021.
Edited by Pamela Dyer in July and August, 2021.
Purpose: 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 demonstrates the use of concurrent events within a root (system of systems) and annotations
-with SAY and MARK in order to improve the clarity of the model. Users may use this
-model as an example of COORDINATE, IF, and MARK statement usage in order to generate
-"stories" for traces automatically.
+Description: This is a model for an Unmanned Aerial Vehicle
+in the OnStation Phase of an ISR Mission. It demonstrates
+the use of concurrent events within a root (system of
+systems) and annotations with SAY and MARK in order to
+improve the clarity of the model. Users may use this model
+as an example of COORDINATE, IF, and MARK statement usage
+in order to generate "stories" for traces automatically.
References:
Giammarco, Kristin, Kathleen Giles, and Clifford A. Whitcomb.
@@ -29,8 +33,12 @@ https://ieeexplore.ieee.org/document/7994950
"Comprehensive use case scenario generation: An approach for modeling system
of systems behaviors" by Kristin Giammarco, Kathleen Giles, and Clifford A. Whitcomb
Paper available at https://ieeexplore.ieee.org/abstract/document/7994950
+********
-Search terms: behavior, UAV OnStation; autonomous; behavior, system of systems; behavior, environment; SAY statement; MARK command; failure mode; behavior, failsafe
+Search terms: behavior, UAV OnStation; autonomous;
+behavior, system of systems; behavior, environment;
+SAY statement; MARK command; failure mode;
+behavior, failsafe
Instructions: Run for Scopes 1 and 2.
Scope 1: 16 traces in less than 1 sec.
diff --git a/models/Application_examples/Unmanned_Spacecraft_Comms.mp b/models/Application_examples/Unmanned_Spacecraft_Comms.mp
index 11bc3fe53ec15e1eebe7ebf5929740dc23f886ae..d08c0e9b78ebab0d115952c8c67e32c4c0f1205d 100644
--- a/models/Application_examples/Unmanned_Spacecraft_Comms.mp
+++ b/models/Application_examples/Unmanned_Spacecraft_Comms.mp
@@ -4,19 +4,21 @@ Created by Cassie Nelson on the 4th of October, 2015.
Edited by Keane Reynolds in July, 2021.
Edited by Pamela Dyer in July and August, 2021.
-Purpose: To demonstrate using MP to model communications between a
-spacecraft and a station.
+Purpose: To demonstrate using MP to model communications
+between a spacecraft and a station.
-Description: The communication link between a spacecraft and the ISS is monitored
-through a frame counter called the "Heartbeat". This model represents
-the behavior of the Heartbeat while a Spacecraft is approaching
-the ISS. Users may reference this model as an example
-of using COORDINATE and SHARE ALL statements to mark relationships
-between roots.
+Description: The communication link between a spacecraft
+and the ISS is monitored through a frame counter called
+the "Heartbeat". This model represents the behavior of
+the Heartbeat while a Spacecraft is approaching the ISS.
+Users may reference this model as an example of using
+COORDINATE and SHARE ALL statements to mark
+relationships between roots.
References:
-Search terms: unmanned spacecraft; Heartbeat; communication; autonomous
+Search terms: unmanned spacecraft; Heartbeat;
+communication; autonomous
Instructions: Run for Scopes 1, 2, 3, and 4.
Scope 1: 4 traces in less than 1 sec.
diff --git a/models/Application_examples/Web_Browser_Formal_Security.mp b/models/Application_examples/Web_Browser_Formal_Security.mp
index 336acc2322625e8510c4235f2c26c4634df6a8f4..69dc959171ad8a2779d7b3c9312c040f09192537 100644
--- a/models/Application_examples/Web_Browser_Formal_Security.mp
+++ b/models/Application_examples/Web_Browser_Formal_Security.mp
@@ -4,31 +4,32 @@ Created by Mikhail Auguston.
Edited by Keane Reynolds in July, 2021.
Edited by Pamela Dyer in July and August, 2021.
-Purpose: To demonstrate using MP to model server-client communication
-involving a bad server and a good server.
+Purpose: To demonstrate using MP to model server-client
+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 query may be indirectly affected by Bad Server's
-Redirect intervention. This has motivated to design the MP behavior model of
-the web activities in order to model the vulnerabilities explained in the
-papers below.
+Description: This example borrowed from (Jackson 2019)
+demonstrates how MP can check whether Client's web query
+may be indirectly affected by Bad Server's Redirect
+intervention. This has motivated to design the MP behavior
+model of the web activities in order to model the
+vulnerabilities explained in the papers below.
-In particular, we've found very inspiring the sentences from
-(Akhawe et al. 2010):
+In particular, we've found very inspiring the sentences
+from (Akhawe et al. 2010):
-"We believe that examining the set of possible events
-accurately captures the way that web security mechanisms
+"We believe that examining the set of possible events
+accurately captures the way that web security mechanisms
are designed" (page 292)
and
-"The browser, server, and network behavior
+"The browser, server, and network behavior
form the “backbone†of the model" (page 292).
-Users may reference this model
-for learning about using BUILD, ENSURE, COORDINATE, and scope limitations
-in order to add clarity to traces that would be difficult to understand
-otherwise, and cut out unwanted traces.
+Users may reference this model for learning about using
+BUILD, ENSURE, COORDINATE, and scope limitations in order
+to add clarity to traces that would be difficult to
+understand otherwise, and cut out unwanted traces.
References:
Jackson, Daniel. "Alloy: A Language and Tool for Exploring
@@ -49,20 +50,25 @@ Akhawe, Devdatta, Adam Barth, Peifung E. Lam, John Mitchell,
Daniel Jackson
Alloy: A Language and Tool for Exploring Software Designs
Communications of the ACM, September 2019, Vol. 62 No. 9, Pages 66-76
-
-and
-
+and
Akhawe, D., Barth, A., Lam, P.E., Mitchell, J. and Song, D.
Towards a formal foundation of Web security.
In Proceedings of the 23rd IEEE Computer Security Foundations Symp.
Edinburgh, 2010, 290–304.
+********
-Search terms: web browser formal security; behavior, browser; behavior, server; BUILD block; coordination, one-to-many; coordination, nested composition
+Search terms: web browser formal security;
+behavior, browser; behavior, server; BUILD block;
+coordination, one-to-many;
+coordination, nested composition
Instructions: Run for Scopes 1, 2, and 3.
- Scope 1: 3 traces (no counterexamples for Property1) in less than 1 sec.
- Scope 2: 7 traces (including 1 counterexample for Property1) in less than 1 sec.
- Scope 3: 52 traces (including 16 counterexamples for Property1) in approx. 20 sec.
+ Scope 1: 3 traces (no counterexamples for Property1)
+ in less than 1 sec.
+ Scope 2: 7 traces (including 1 counterexample for
+ Property1) in less than 1 sec.
+ Scope 3: 52 traces (including 16 counterexamples for
+ Property1) in approx. 20 sec.
==========================================================*/
diff --git a/models/Application_examples/Wide_Range_Search_for_Wreckage_and_Survivors b/models/Application_examples/Wide_Range_Search_for_Wreckage_and_Survivors
index 49bb8fe54c14a77326f3269169f0d3e7f7921c1a..e9b504fe35073ca8ea8bc26d69aaca61b8e9e5d9 100644
--- a/models/Application_examples/Wide_Range_Search_for_Wreckage_and_Survivors
+++ b/models/Application_examples/Wide_Range_Search_for_Wreckage_and_Survivors
@@ -4,34 +4,46 @@ Created by Spencer Hunt.
Edited by Keane Reynolds in July, 2021.
Edited by Pamela Dyer in July and August, 2021.
-Purpose: To demonstrate using MP to model a search and rescue operation with
-several environmental and coordination concerns to address.
-
-Description: Users may reference this model when learning about
-using COORDINATE statements to create complex diagrams through traces. Operational processes can be modeled to provide a common baseline against which
+Purpose: To demonstrate using MP to model a search and
+rescue operation with several environmental and
+coordination concerns to address.
+
+Description: Users may reference this model when learning
+about using COORDINATE statements to create complex
+diagrams through traces. Operational processes can be
+modeled to provide a common baseline against which
alternative proposed solutions may be assessed.
-In this example, humans are conducting a wide area search in roles of Command and Control
-(C2), On Scene Commander (OSC), Person in Distress (PID), and Search And Rescue Assets
-(SAR Assets) apart from the OSC.
-An actor called Physical Environment represents behaviors in the natural environment.
+In this example, humans are conducting a wide area search
+in roles of Command and Control (C2), On Scene Commander
+(OSC), Person in Distress (PID), and Search And Rescue
+Assets (SAR Assets) apart from the OSC.
+An actor called Physical Environment represents behaviors
+in the natural environment.
-Actors may be partitioned and scoped according to the focus of the analysis. The analysis
-prompting this model calls for an analysis of alternatives for the On Scene Commander role
-(e.g., manned helicopter, cutter, unmanned aerial/surface/underwater vehicles).
+Actors may be partitioned and scoped according to the
+focus of the analysis. The analysis prompting this model
+calls for an analysis of alternatives for the On Scene
+Commander role (e.g., manned helicopter, cutter, unmanned
+aerial/surface/underwater vehicles).
-A System of Systems (SoS) analysis might expand the "SAR Asset" actor into distinct SAR assets
-participating in or potentially participating in the scenario to study emergent behaviors of
-those interacting systems in a SoS construct.
+A System of Systems (SoS) analysis might expand the "SAR
+Asset" actor into distinct SAR assets participating in or
+potentially participating in the scenario to study emergent
+behaviors of those interacting systems in a SoS construct.
References:
-Search terms: behavior, operational process; wide range search; behavior, environment; behavior, system of systems; behavior, emergent
+Search terms: behavior, operational process;
+wide range search; behavior, environment;
+behavior, system of systems; behavior, emergent
-Instructions: Run for Scope 1 (there is no iteration in this example, so increasing the scope will not
-produce more scenarios). Only one scenario is produced because no decision points have been
-added to this model yet. "Sequence" mode yields views very similar to the UML or SysML
-Sequence Diagrams.
+Instructions: Run for Scope 1 (there is no iteration in
+this example, so increasing the scope will not produce
+more scenarios). Only one scenario is produced because
+no decision points have been added to this model yet.
+"Sequence" mode yields views very similar to the UML or
+SysML Sequence Diagrams.
Scope 1: 1 trace in less than 1 sec.
==========================================================*/
diff --git a/models/Application_examples/Work_Productivity.mp b/models/Application_examples/Work_Productivity.mp
index 34365819834adf2d89418fed5d9760c2b22c6fad..3f8516f98dd8cc924072b918926cbdc5db455c76 100644
--- a/models/Application_examples/Work_Productivity.mp
+++ b/models/Application_examples/Work_Productivity.mp
@@ -4,17 +4,20 @@ Created by Mikhail Auguston.
Edited by Keane Reynolds in July, 2021.
Edited by Pamela Dyer in July and August, 2021.
-Purpose: To demonstrate how to print all events present in the trace with timing attributes.
+Purpose: 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 usage. Users may reference
-this model when learning about BUILD, COORDINATE, and SAY
-statements in order to constrain models and comment on models
-directly in the traces.
+Description: This model demonstrates using MP to show how
+visitors can distract workers with stacked time usage.
+Users may reference this model when learning about BUILD,
+COORDINATE, and SAY statements in order to constrain
+models and comment on models directly in the traces.
References:
-Search terms: behavior, work productivity; behavior, distraction; event attribute, timing; event attribute, interval; BUILD block
+Search terms: behavior, work productivity;
+behavior, distraction; event attribute, timing;
+event attribute, interval; BUILD block
Instructions: Run for Scopes 1 and up.
Scope 1: 2 traces in less than 1 sec.
diff --git a/models/Example08_EmployeeEmployer_CoordinationAcrossHierarchyLevels.mp b/models/Example08_EmployeeEmployer_CoordinationAcrossHierarchyLevels.mp
index 2b8e37234610861b30ef8debcc1dd4227a7b6030..b34260209d392522ab685d58f1095bc9faaf488b 100644
--- a/models/Example08_EmployeeEmployer_CoordinationAcrossHierarchyLevels.mp
+++ b/models/Example08_EmployeeEmployer_CoordinationAcrossHierarchyLevels.mp
@@ -31,9 +31,16 @@ References:
Available online:
https://wiki.nps.edu/display/MP/Documentation
+Vigneras, Pierre. "Why BPEL is not the holy grail for BPM."
+ InfoQ. October 21, 2008.
+ https://www.infoq.com/articles/bpelbpm/
+
+
+**** Remove this part ****
"Why BPEL is not the holy grail for BPM"
Available online:
http://www.infoq.com/articles/bpelbpm
+********
Search terms: behavior, business process;
coordination, across hierarchy levels
diff --git a/models/Example09_CardiacArrestWorkflow_VirtualEvents.mp b/models/Example09_CardiacArrestWorkflow_VirtualEvents.mp
index e02f776808ab5c12d3a7c3f9f9aad8d6f539c4f4..18677b07e2eaab8fc3a31ff19d811e32ffb127a5 100644
--- a/models/Example09_CardiacArrestWorkflow_VirtualEvents.mp
+++ b/models/Example09_CardiacArrestWorkflow_VirtualEvents.mp
@@ -15,12 +15,20 @@ References:
Manual" (Version 4). 2020. Available online:
https://wiki.nps.edu/display/MP/Documentation
+"Control-Flow Patterns." Workflow Patterns, 2011.
+ http://workflowpatterns.com/patterns/control/index.php
+
+"Pattern 9 (Structured Discriminator)." Workflow Patterns, 2011.
+ http://workflowpatterns.com/patterns/control/advanced_branching/wcp9.php
+
+
+**** Remove this part ****
http://workflowpatterns.com/patterns/control/index.php
contains a collection of workflow patterns
specified with Petri nets.
-
Pattern 9 (Structured Discriminator)
http://workflowpatterns.com/patterns/control/advanced_branching/wcp9.php
+********
Search terms: behavior, triage; behavior, workflow