diff --git a/models/Application_examples/Prisoners_Dilemma.mp b/models/Application_examples/Prisoners_Dilemma.mp index 55d1eb4d7c1e5aa3a298b28ed6beca0766bf6888..92fc5b2aee5bc7210c961b599f998096388e20bc 100644 --- a/models/Application_examples/Prisoners_Dilemma.mp +++ b/models/Application_examples/Prisoners_Dilemma.mp @@ -75,15 +75,6 @@ Kuhn, Steven. "Prisoner’s Dilemma." The Stanford https://plato.stanford.edu/archives/win2019/entries/prisoner-dilemma/ -**** Remove this part **** -"Game Theory and Strategy" by Philip D. Straffin -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 diff --git a/models/Application_examples/Railroad_Crossing_Safety.mp b/models/Application_examples/Railroad_Crossing_Safety.mp index 17091b4ed4891cc6459df20e93792ce5d7b161f2..764bd18f69b116d0c7f62700824a4282f1e267ae 100644 --- a/models/Application_examples/Railroad_Crossing_Safety.mp +++ b/models/Application_examples/Railroad_Crossing_Safety.mp @@ -1,6 +1,6 @@ /* Model of Railroad Crossing Safety -Created by Mikhail Auguston. +Created by Mikhail Auguston in 2018. Edited by Keane Reynolds in July, 2021. Edited by Pamela Dyer in July and August, 2021. @@ -16,11 +16,11 @@ 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, +The original railroad crossing example was provided +by 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: diff --git a/models/Application_examples/Replay_Attack.mp b/models/Application_examples/Replay_Attack.mp index 4e2cedd70a269574ce18915c87368567c5bb81dc..2e07444f75d6f21277ba5f5f5a5cd39df28e60a8 100644 --- a/models/Application_examples/Replay_Attack.mp +++ b/models/Application_examples/Replay_Attack.mp @@ -1,17 +1,16 @@ /* Model of Replay Attack -Created by Mikhail Auguston. +Created by Mikhail Auguston in 2019. Edited by Keane Reynolds in July, 2021. 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 -as an example of possible 3rd parties in other systems, -and using COORDINATE statements to form relationships. +Description: This model demonstrates a well known +attack strategy on a communication system. Users may +use this model as an example way to model possible 3rd +parties listening in other systems. References: "Replay attack." Wikipedia. Wikimedia Foundation, @@ -19,14 +18,8 @@ July 1, 2021. https://en.wikipedia.org/wiki/Replay_attack -**** Remove this part **** -The description of Replay Attack -is available at -https://en.wikipedia.org/wiki/Replay_attack -******** - Search terms: behavior, replay attack; -message eavesdropping; coordination, event +behavior, 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 587c138bebfc04de00ef7047c68fcc2de25f1528..1edd08821d217a1b5afbe3d5a716b182e715e1c2 100644 --- a/models/Application_examples/Small_Package_Delivery.mp +++ b/models/Application_examples/Small_Package_Delivery.mp @@ -1,23 +1,22 @@ /* 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). +Created by David Shifflett and Kristin Giammarco based on + a non-combatant scenario authored by Nataki Roberts. 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. +Purpose: To demonstrate unexpected emergent behavior in a +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 -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. +emergency situation that has been overconstrained. Building +a complex scenario without frequently running the model can +make finding parts of the model overloaded with constraints +difficult. During debugging, an unexpected emergent behavior +was found in which payload was dropped without a vessel in +sight. Taken from use case description in the Skyzer IM20 Mission Model (Non-Combatant Operations Scenario): @@ -53,22 +52,22 @@ USA, 2018. Available online: https://apps.dtic.mil/sti/citations/AD1063328 -Search terms: small package delivery; autonomous; -ENSURE condition; probability, Type 1 +Search terms: behavior, small package delivery; autonomous; +ENSURE condition 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 +This model shows fewer scenarios than intended by the +authors due to overloading constraints (constraints that +suppress entire branches of execution that a user intended +to permit). After an initial run and inspection, comment 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. +Air_Vehicle root, run at Scope 1, and inspect the six +resulting event traces. 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 48a592cab20c4d25842902e7d6145d4815e69680..e47e77791c9d9f78df09a991686cc4ffd26d42f0 100644 --- a/models/Application_examples/Spent_Fuel_Cooling_and_Cleanup.mp +++ b/models/Application_examples/Spent_Fuel_Cooling_and_Cleanup.mp @@ -10,19 +10,18 @@ Edited by Pamela Dyer in July and August, 2021. Purpose: To illustrate the modeling of a complex cooling and purification system, specifically a spent nuclear fuel -cooling pool in this particular case. +cooling pool. 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. +to learn about interactions in a nuclear cooling system and +user-defined relationships. References: Search terms: behavior, nuclear fuel cooling; -coordination, event; heat exchanger; -purification subsystem +user-defined relations 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 9b4ee1af43f7ce238137a021011bc44751e6c371..642776a8543bc16940921ccb1a663493764f1084 100644 --- a/models/Application_examples/Spiral_Software_Process +++ b/models/Application_examples/Spiral_Software_Process @@ -1,11 +1,11 @@ /* Model of Spiral Software Process -Created by Mikhail Auguston. +Created by Mikhail Auguston 2018. Edited by Keane Reynolds in July, 2021. 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. +Purpose: 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 @@ -14,13 +14,13 @@ 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." +copies of the communication structures of these +organizations." References: Search terms: behavior, spiral software process; -communication; architecture; event sharing +event sharing Instructions: Run for Scopes 1 and up. Scope 1: 3 traces in less than 1 sec. @@ -31,7 +31,7 @@ Instructions: Run for Scopes 1 and up. ==========================================================*/ -SCHEMA spiral +SCHEMA Spiral_Software_Development_Process ROOT Stakeholders: Initial_communication_with_stakeholders 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 812d0997772b51086332041af99e8a8603ddf269..82403108c554d4801ce36e8d250967d289ab5b4f 100644 --- a/models/Application_examples/Supply_Chain_with_Two_Cyber_Threats.mp +++ b/models/Application_examples/Supply_Chain_with_Two_Cyber_Threats.mp @@ -237,4 +237,4 @@ SAY("Average Risk: " GLOBAL.sum_risk_score/#$$TRACE) SAY("Sort by Marked to view traces with above average risk >=9.") => Global_Risk; -SHOW Global_Risk; \ No newline at end of file +SHOW Global_Risk; diff --git a/models/Application_examples/Surgery.mp b/models/Application_examples/Surgery.mp index ac486f820bea69f316d6b607cd182f91a3e8590b..e6e2f7d630a34772586ee250ac607a0ddf3774ef 100644 --- a/models/Application_examples/Surgery.mp +++ b/models/Application_examples/Surgery.mp @@ -1,6 +1,6 @@ /* Model of Surgery -Created by John Quartuccio circa 2017 (NPS). +Created by John Quartuccio in 2017. Edited by Keane Reynolds in July, 2021. Edited by Pamela Dyer in July and August, 2021.