Skip to content
Snippets Groups Projects
Commit ff0a1672 authored by Keane Reynolds's avatar Keane Reynolds
Browse files

Added several model purposes

parent 6ebab462
No related branches found
No related tags found
No related merge requests found
...@@ -2,9 +2,16 @@ ...@@ -2,9 +2,16 @@
Purpose: 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 A demonstration that shows how to reject unwanted behaviors with ENSURE
constraints. constraints.
......
...@@ -2,6 +2,13 @@ ...@@ -2,6 +2,13 @@
Purpose: 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: Description:
A model of an autonomous car that was used to support a failure mode A model of an autonomous car that was used to support a failure mode
...@@ -12,7 +19,8 @@ References: ...@@ -12,7 +19,8 @@ References:
Search terms: 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)
==========================================================*/ ==========================================================*/
......
...@@ -2,6 +2,13 @@ ...@@ -2,6 +2,13 @@
Purpose: 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: Description:
A Simple Model of Beginner MP-Firebird Use A Simple Model of Beginner MP-Firebird Use
...@@ -9,10 +16,9 @@ created by K.Giammarco 2021-02-08 ...@@ -9,10 +16,9 @@ created by K.Giammarco 2021-02-08
This model provides an orientation for those just getting started using This model provides an orientation for those just getting started using
MP-Firebird. This text editor pane allows you to compose and edit code 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 in the high-level MP language.
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 References:
bar next to the Run button to control the number of loop iterations.
ROOT A: B C; A is a root event that includes events B followed by C 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 ( 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 ...@@ -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 *) iterate B zero or more times
{ B , C } B and C are unordered { 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. 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. 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 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 ...@@ -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 the contents of the text editor plus the graphs and any changes you made
to the graph element positions. to the graph element positions.
References:
Search terms:
Instructions:
==========================================================*/ ==========================================================*/
SCHEMA Beginner_Use_of_MP SCHEMA Beginner_Use_of_MP
...@@ -88,7 +97,7 @@ COORDINATE $a: Display_scenarios, ...@@ -88,7 +97,7 @@ COORDINATE $a: Display_scenarios,
/*Additional Constraints */ /*Additional Constraints */
/*Assumption that existing model has no verification issues. */ /*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 */ /* Trace annotations */
...@@ -96,7 +105,7 @@ ENSURE #Import_existing_model >=1 -> #Find_issue == 0; ...@@ -96,7 +105,7 @@ ENSURE #Import_existing_model >=1 -> #Find_issue == 0;
IF #Find_issue >1 THEN IF #Find_issue >1 THEN
SAY( #Find_issue " issues were discovered"); SAY( #Find_issue " issues were discovered");
ELSE IF #Find_issue ==1 THEN ELSE IF #Find_issue == 1 THEN
SAY( #Find_issue " issue was discovered"); SAY( #Find_issue " issue was discovered");
FI; FI;
FI; FI;
...@@ -2,6 +2,12 @@ ...@@ -2,6 +2,12 @@
Purpose: 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: Description:
Cargo Screening process model Cargo Screening process model
......
...@@ -2,6 +2,12 @@ ...@@ -2,6 +2,12 @@
Purpose: 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: Description:
Model of a commercial flight, November 27, 2013 Model of a commercial flight, November 27, 2013
......
...@@ -2,11 +2,11 @@ ...@@ -2,11 +2,11 @@
Purpose: Purpose:
This model uses say statements to add commentary to the traces
Description: Description:
Cycle_ISP Model for Systems Journal Article created 2018-03-10 by K.Giammarco
Available at https://www.mdpi.com/2079-8954/6/2/18
created 2018-03-10 by K.Giammarco
The model below describes a cycle in terms of a The model below describes a cycle in terms of a
series of one or more steps, each step either series of one or more steps, each step either
...@@ -25,6 +25,9 @@ of the ENSURE constraint on line 29. ...@@ -25,6 +25,9 @@ of the ENSURE constraint on line 29.
References: References:
Cycle_ISP Model for Systems Journal Article
Available at https://www.mdpi.com/2079-8954/6/2/18
Search terms: Search terms:
Instructions: Instructions:
......
/* Model of First Responder /* Model of Narcan Administration
Purpose: Purpose:
......
/* Model of Prisoners Dilemma /* Model of Prisoner's Dilemma
Purpose: Purpose:
......
/* Model of Railroad Crossing Safety /* Model of Railroad Crossing
Purpose: Purpose:
......
...@@ -4,17 +4,17 @@ Purpose: ...@@ -4,17 +4,17 @@ Purpose:
Description: Description:
References:
Example 41. The description of Replay Attack Example 41. The description of Replay Attack
is available at is available at
https://en.wikipedia.org/wiki/Replay_attack https://en.wikipedia.org/wiki/Replay_attack
run scope up to 5
References:
Search terms: Search terms:
Instructions: Instructions: run scope up to 5
==========================================================*/ ==========================================================*/
......
/* Model of UAV On Station /* Model of UAV on Station
Purpose: Purpose:
......
...@@ -4,19 +4,15 @@ Purpose: ...@@ -4,19 +4,15 @@ Purpose:
Description: Description:
Example 26, timing attribute use demonstrates how to print all
events present in the trace
also demonstrates how to print all with timing attributes
events present in the trace
with timing attributes
run for scopes 1 and up
References: References:
Search terms: Search terms:
Instructions: Instructions: run for scopes 1 and up
==========================================================*/ ==========================================================*/
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment