From ff0a1672471cbafb08c93c085de04d85bd4a1ba2 Mon Sep 17 00:00:00 2001
From: Keane Reynolds <keane.reynolds@gmail.com>
Date: Mon, 19 Jul 2021 21:05:33 +0000
Subject: [PATCH] Added several model purposes
---
Application_examples/Authentication.mp | 11 +++++--
Application_examples/Autonomous_Car.mp | 10 +++++-
Application_examples/Beginner_Use_of_MP.mp | 33 ++++++++++++-------
Application_examples/CargoScreening.mp | 6 ++++
Application_examples/Commercial_Flight | 6 ++++
Application_examples/Cycle_Pattern.mp | 9 +++--
Application_examples/First_Responder.mp | 2 +-
Application_examples/Prisoners_Dilemma.mp | 2 +-
.../Railroad_Crossing_Safety.mp | 2 +-
Application_examples/Replay_Attack.mp | 10 +++---
Application_examples/UAV_OnStation.mp | 2 +-
Application_examples/Work_Productivity.mp | 12 +++----
12 files changed, 70 insertions(+), 35 deletions(-)
diff --git a/Application_examples/Authentication.mp b/Application_examples/Authentication.mp
index 275b59a..b34f8d8 100644
--- a/Application_examples/Authentication.mp
+++ b/Application_examples/Authentication.mp
@@ -2,9 +2,16 @@
Purpose:
-Description:
+This model demonstrates how to correctly model a 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), demostrating how users can remove unwanted traces in their
+models using ENSURE.
-A Model for Simple Authentication
+Description:
A demonstration that shows how to reject unwanted behaviors with ENSURE
constraints.
diff --git a/Application_examples/Autonomous_Car.mp b/Application_examples/Autonomous_Car.mp
index 05984df..ec15902 100644
--- a/Application_examples/Autonomous_Car.mp
+++ b/Application_examples/Autonomous_Car.mp
@@ -2,6 +2,13 @@
Purpose:
+This model 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.
+
Description:
A model of an autonomous car that was used to support a failure mode
@@ -12,7 +19,8 @@ References:
Search terms:
-Instructions:
+Instructions: Try running with the COORDINATE statements commented out or removed.
+Watch the differences in the traces. (Note: scope does not change this model)
==========================================================*/
diff --git a/Application_examples/Beginner_Use_of_MP.mp b/Application_examples/Beginner_Use_of_MP.mp
index 6cd3631..ae55d38 100644
--- a/Application_examples/Beginner_Use_of_MP.mp
+++ b/Application_examples/Beginner_Use_of_MP.mp
@@ -2,6 +2,13 @@
Purpose:
+This model uses its traces to provide an example of how to use MP as a
+beginner. See the intructions section for detailed advice. This model
+incorporates COORDINATE, ENSURE, and IF-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.
+
Description:
A Simple Model of Beginner MP-Firebird Use
@@ -9,10 +16,9 @@ created by K.Giammarco 2021-02-08
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 navigae the resulting traces. Use the scope slider
-bar next to the Run button to control the number of loop iterations.
+in the high-level MP language.
+
+References:
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
@@ -20,6 +26,15 @@ ROOT A: B C; A is a root event that includes events B followed by C
(* B *) iterate B zero or more times
{ B , C } B and C are unordered
+Search terms:
+
+Instructions:
+
+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 navigae the
+resulting traces. Use the scope slider bar next to the Run button to
+control the number of loop iterations.
+
Experiment with this model by running it at scopes 1, 2, 3, 4 and 5.
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
@@ -27,12 +42,6 @@ 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.
-References:
-
-Search terms:
-
-Instructions:
-
==========================================================*/
SCHEMA Beginner_Use_of_MP
@@ -88,7 +97,7 @@ COORDINATE $a: Display_scenarios,
/*Additional Constraints */
/*Assumption that existing model has no verification issues. */
-ENSURE #Import_existing_model >=1 -> #Find_issue == 0;
+ENSURE #Import_existing_model >= 1 -> #Find_issue == 0;
/* Trace annotations */
@@ -96,7 +105,7 @@ ENSURE #Import_existing_model >=1 -> #Find_issue == 0;
IF #Find_issue >1 THEN
SAY( #Find_issue " issues were discovered");
- ELSE IF #Find_issue ==1 THEN
+ ELSE IF #Find_issue == 1 THEN
SAY( #Find_issue " issue was discovered");
FI;
FI;
diff --git a/Application_examples/CargoScreening.mp b/Application_examples/CargoScreening.mp
index 5d18b3a..961c41b 100644
--- a/Application_examples/CargoScreening.mp
+++ b/Application_examples/CargoScreening.mp
@@ -2,6 +2,12 @@
Purpose:
+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 actions leads to
+several more.
+
Description:
Cargo Screening process model
diff --git a/Application_examples/Commercial_Flight b/Application_examples/Commercial_Flight
index b609d0d..2087a0e 100644
--- a/Application_examples/Commercial_Flight
+++ b/Application_examples/Commercial_Flight
@@ -2,6 +2,12 @@
Purpose:
+This example shows a system with many roots performing multiple actions,
+and links these actions together using COORDINATE and SHARE ALL statements
+to make a complex web of linked actions. 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.
+
Description:
Model of a commercial flight, November 27, 2013
diff --git a/Application_examples/Cycle_Pattern.mp b/Application_examples/Cycle_Pattern.mp
index aaa8d59..c2f79ec 100644
--- a/Application_examples/Cycle_Pattern.mp
+++ b/Application_examples/Cycle_Pattern.mp
@@ -2,11 +2,11 @@
Purpose:
+This model uses say statements to add commentary to the traces
+
Description:
-Cycle_ISP Model for Systems Journal Article
- Available at https://www.mdpi.com/2079-8954/6/2/18
- created 2018-03-10 by K.Giammarco
+created 2018-03-10 by K.Giammarco
The model below describes a cycle in terms of a
series of one or more steps, each step either
@@ -25,6 +25,9 @@ of the ENSURE constraint on line 29.
References:
+Cycle_ISP Model for Systems Journal Article
+Available at https://www.mdpi.com/2079-8954/6/2/18
+
Search terms:
Instructions:
diff --git a/Application_examples/First_Responder.mp b/Application_examples/First_Responder.mp
index 53a2fbb..6ad4883 100644
--- a/Application_examples/First_Responder.mp
+++ b/Application_examples/First_Responder.mp
@@ -1,4 +1,4 @@
-/* Model of First Responder
+/* Model of Narcan Administration
Purpose:
diff --git a/Application_examples/Prisoners_Dilemma.mp b/Application_examples/Prisoners_Dilemma.mp
index ee66e9f..ea484af 100644
--- a/Application_examples/Prisoners_Dilemma.mp
+++ b/Application_examples/Prisoners_Dilemma.mp
@@ -1,4 +1,4 @@
-/* Model of Prisoners Dilemma
+/* Model of Prisoner's Dilemma
Purpose:
diff --git a/Application_examples/Railroad_Crossing_Safety.mp b/Application_examples/Railroad_Crossing_Safety.mp
index 0433f8a..aa148fa 100644
--- a/Application_examples/Railroad_Crossing_Safety.mp
+++ b/Application_examples/Railroad_Crossing_Safety.mp
@@ -1,4 +1,4 @@
-/* Model of Railroad Crossing Safety
+/* Model of Railroad Crossing
Purpose:
diff --git a/Application_examples/Replay_Attack.mp b/Application_examples/Replay_Attack.mp
index 35f1450..44ffaa9 100644
--- a/Application_examples/Replay_Attack.mp
+++ b/Application_examples/Replay_Attack.mp
@@ -4,17 +4,17 @@ Purpose:
Description:
+
+
+References:
+
Example 41. The description of Replay Attack
is available at
https://en.wikipedia.org/wiki/Replay_attack
- run scope up to 5
-
-References:
-
Search terms:
-Instructions:
+Instructions: run scope up to 5
==========================================================*/
diff --git a/Application_examples/UAV_OnStation.mp b/Application_examples/UAV_OnStation.mp
index 94555c4..449c961 100644
--- a/Application_examples/UAV_OnStation.mp
+++ b/Application_examples/UAV_OnStation.mp
@@ -1,4 +1,4 @@
-/* Model of UAV On Station
+/* Model of UAV on Station
Purpose:
diff --git a/Application_examples/Work_Productivity.mp b/Application_examples/Work_Productivity.mp
index c7db03e..351be81 100644
--- a/Application_examples/Work_Productivity.mp
+++ b/Application_examples/Work_Productivity.mp
@@ -4,19 +4,15 @@ Purpose:
Description:
-Example 26, timing attribute use
-
- also demonstrates how to print all
- events present in the trace
- with timing attributes
-
- run for scopes 1 and up
+demonstrates how to print all
+events present in the trace
+with timing attributes
References:
Search terms:
-Instructions:
+Instructions: run for scopes 1 and up
==========================================================*/
--
GitLab