diff --git a/Legacy_examples/.gitkeep b/Legacy_examples/.gitkeep
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/models/Legacy_examples/Example01_simple_message_flow.mp b/models/Legacy_examples/Example01_simple_message_flow.mp
new file mode 100644
index 0000000000000000000000000000000000000000..0ea964f0c5e1a5d3a3606c2f1e02bec47ca3fad6
--- /dev/null
+++ b/models/Legacy_examples/Example01_simple_message_flow.mp
@@ -0,0 +1,24 @@
+/*
+Example1_simple_message_flow.mp
+
+Event grammar rules for each root define derivations for event traces,
+in this case a simple sequence of zero or more events for each root.
+
+The COORDINATE composition takes two root traces and produces
+a modified event trace, merging behaviors of Sender and Receiver
+and adding the PRECEDES relation for the selected send/receive pairs.
+The coordination operation behaves as a "cross-cutting" derivation rule.
+
+Run for scopes 1 and up. The "Sequence" or "Swim Lanes" layouts are
+the most appropriate for browsing traces here.
+
+*/
+
+SCHEMA simple_message_flow
+
+ROOT Sender: (* send *);
+ROOT Receiver: (* receive *);
+
+COORDINATE $x: send FROM Sender,
+ $y: receive FROM Receiver
+ DO ADD $x PRECEDES $y; OD;
diff --git a/models/Legacy_examples/Example01a_unreliable_message_flow.mp b/models/Legacy_examples/Example01a_unreliable_message_flow.mp
new file mode 100644
index 0000000000000000000000000000000000000000..d714bd0c5ba15a37e7cebecd62e4b7ba4df54d5a
--- /dev/null
+++ b/models/Legacy_examples/Example01a_unreliable_message_flow.mp
@@ -0,0 +1,16 @@
+/* Example 1a
+Unreliable message flow.
+
+We may want to specify behaviors when some messages get lost in the transition.
+It can be done using ‘virtual’ events.
+
+run for scopes 1 and up.
+
+*/
+SCHEMA unreliable_message_flow
+ROOT Sender: (* send *);
+ROOT Receiver: (* (receive | does_not_receive) *);
+
+COORDINATE $x: send FROM Sender,
+ $y: (receive | does_not_receive) FROM Receiver
+ DO ADD $x PRECEDES $y; OD;
diff --git a/models/Legacy_examples/Example02_Data_flow.mp b/models/Legacy_examples/Example02_Data_flow.mp
new file mode 100644
index 0000000000000000000000000000000000000000..811e1de5c05900631a534383e10924fd91038d20
--- /dev/null
+++ b/models/Legacy_examples/Example02_Data_flow.mp
@@ -0,0 +1,39 @@
+/* Example2_DataAsEvents.mp
+ data items as behaviors
+
+MP employs the Abstract Data Type (ADT) principle introduced by
+Barbara Liskov to represent data items as operations
+being performed on those items.
+
+In this model all writing in the File should be accomplished before reading.
+File should not be empty. These constraints on behavior are
+captured by File root event grammar rule.
+
+On the other hand, Writer’s behavior allows scenarios that skip writing at all.
+Such behaviors are not compatible with File behavior patterns.
+
+The SHARE ALL composition ensures that the schema admits
+only event traces where corresponding event sharing is implemented.
+
+Event traces specified by the schema represent system’s emergent behavior,
+where behaviors of subsystems are influenced by the coordination.
+This is a toy example of System_of_Systems emerging behavior modeling.
+
+Run for scopes 1 and up. The "Sequence" or "Swim Lanes" layouts are
+the most appropriate for browsing traces here.
+
+*/
+
+SCHEMA Data_flow
+
+ROOT Writer: (* ( working | writing ) *);
+
+/* writing events should precede reading */
+ROOT File: (+ writing +) (* reading *);
+
+Writer, File SHARE ALL writing;
+
+
+ROOT Reader: (* ( reading | working ) *);
+
+Reader, File SHARE ALL reading;
diff --git a/models/Legacy_examples/Example03_ATM_withdrawal.mp b/models/Legacy_examples/Example03_ATM_withdrawal.mp
new file mode 100644
index 0000000000000000000000000000000000000000..0c33381eeedc80f433f26581a87f283271eb48f1
--- /dev/null
+++ b/models/Legacy_examples/Example03_ATM_withdrawal.mp
@@ -0,0 +1,83 @@
+/* Example3_ATM_withdrawal.mp
+ Integrated system and environment behaviors
+
+MP separates models of component behaviors and component interactions
+to permit elaboration on behaviors of multiple interacting actors.
+
+"Withdraw money from ATM" is a popular example in software architecture literature.
+This example demonstrates how behavior of both the system and its environment can be
+integrated into a single MP model.
+
+Separate behavior models account for alternative behaviors of not only the ATM System
+under design, but also those of external components Customer and Database.
+A separate specification of interactions captures the sharing and precedence dependencies
+among events in different components.
+
+The event traces produced from a model partitioned using this separation of concerns
+include all combinations of event selections allowed by the model.
+
+Run for scopes 1 and up.
+
+The "Sequence" or "Swim Lanes" layouts are the most appropriate for browsing traces here.
+The "Sequence" mode yields views very similar to the UML or SysML Sequence Diagrams.
+
+By selecting a representative enough trace (containing all events and interactions of interest,
+like traces 2 or 3 for scope 1), and then collapsing root event, it becomes possible
+to view a traditional "box-and-arrow" architecture diagram, i.e. to visualize an architecture view.
+
+*/
+
+SCHEMA ATM_withdrawal
+
+ROOT Customer: (* insert_card
+ ( identification_succeeds
+ request_withdrawal
+ (get_money | not_sufficient_funds) |
+
+ identification_fails )
+ *);
+
+ROOT ATM_system: (* read_card
+ validate_id
+ ( id_successful
+ check_balance
+ ( sufficient_balance
+ dispense_money |
+
+ unsufficient_balance ) |
+
+ id_failed )
+ *);
+
+/* behavior of the Data_Base follows interaction pattern with it in ATM_system,
+ this makes it easier to coordinate these behaviors with SHARE ALL */
+ROOT Data_Base: (* validate_id [ check_balance ] *);
+
+/* interactions */
+Data_Base, ATM_system SHARE ALL validate_id, check_balance;
+
+COORDINATE $x: insert_card FROM Customer,
+ $y: read_card FROM ATM_system
+ DO ADD $x PRECEDES $y; OD;
+
+COORDINATE $x: request_withdrawal FROM Customer,
+ $y: check_balance FROM ATM_system
+ DO ADD $x PRECEDES $y; OD;
+
+COORDINATE $x: identification_succeeds FROM Customer,
+ $y: id_successful FROM ATM_system
+ DO ADD $y PRECEDES $x; OD;
+
+COORDINATE $x: get_money FROM Customer,
+ $y: dispense_money FROM ATM_system
+ DO ADD $y PRECEDES $x; OD;
+
+COORDINATE $x: not_sufficient_funds FROM Customer,
+ $y: unsufficient_balance FROM ATM_system
+ DO ADD $y PRECEDES $x; OD;
+
+COORDINATE $x: identification_fails FROM Customer,
+ $y: id_failed FROM ATM_system
+ DO ADD $y PRECEDES $x; OD;
+
+
\ No newline at end of file
diff --git a/models/Legacy_examples/Example04_Stack_behavior.mp b/models/Legacy_examples/Example04_Stack_behavior.mp
new file mode 100644
index 0000000000000000000000000000000000000000..0c660075f65c5c6248d423abf77219494b29c336
--- /dev/null
+++ b/models/Legacy_examples/Example04_Stack_behavior.mp
@@ -0,0 +1,53 @@
+/* Example4_Stack_behavior.mp
+
+The event trace is a set of events and the Boolean expression constructs in MP
+can support the traditional first order predicate calculus notation.
+
+A set of behaviors (event traces) may be defined by the event
+grammar rules, composition operations, and some additional constraints –
+ENSURE conditions.
+
+run for scopes 1, 2, 3, and up.
+*/
+
+/* This rule specifies the behavior of a stack in terms of stack operations
+push and pop. It is assumed that initially Stack is empty.
+The BUILD block associated with a root or composite event
+contains composition operations performed when event trace segment
+representing the behavior of that root or composite is generated.
+
+The ENSURE Boolean expression provides a condition that each valid trace
+should satisfy. The domain of the universal quantifier is the set of all
+pop events inside Stack trace. The FROM Stack part is optional, by default it is
+assumed to be FROM THIS.
+
+The function #pop BEFORE $x yields the number of pop events preceding $x.
+The set of valid event traces specified by this schema contains only traces
+that satisfy the constraint. This example presents a filtering operation
+as yet another kind of behavior composition, and demonstrates an
+example of combining imperative (event grammar) and declarative
+(Boolean expressions) constructs for behavior specification.
+*/
+
+SCHEMA Stack_behavior
+
+ROOT Stack: (* ( push | pop ) *)
+ BUILD {
+ /* if an element is retrieved, it should have been stored before */
+ ENSURE FOREACH $x: pop FROM Stack
+ ( #pop BEFORE $x < #push BEFORE $x );
+
+ /* The following composition operation establishes push/pop pairs
+ in the Stack behavior. For each 'pop' the closest in time
+ preceding 'push' is selected, unless it has been already
+ consumed by another 'pop' */
+
+ COORDINATE $get: pop
+ DO COORDINATE <REVERSE> $put: push
+ SUCH THAT $put BEFORE $get
+ DO IF NOT ( EXISTS $g: pop $put Paired_with $g OR
+ EXISTS $p: push $p Paired_with $get )
+ THEN ADD $put Paired_with $get; FI;
+ OD;
+ OD;
+ };/* end BUILD for Stack */
diff --git a/models/Legacy_examples/Example04a_Queue_behavior.mp b/models/Legacy_examples/Example04a_Queue_behavior.mp
new file mode 100644
index 0000000000000000000000000000000000000000..3aed579e46c93823948700930d49e3ef8b7bcbcf
--- /dev/null
+++ b/models/Legacy_examples/Example04a_Queue_behavior.mp
@@ -0,0 +1,45 @@
+/* Example4a_Queue_behavior.mp
+
+run for scopes 1, 2, 3, and up.
+*/
+
+/* This rule specifies the behavior of a queue in terms of queue operations
+enqueue and dequeue. It is assumed that initially Queue is empty.
+The BUILD block associated with a root or composite event
+contains composition operations performed when event trace segment
+representing the behavior of that root or composite is generated.
+
+The ENSURE Boolean expression provides a condition that each valid trace
+should satisfy. The domain of the universal quantifier is the set of all
+dequeue events inside Queue trace.
+
+The function #dequeue BEFORE $x yields the number of dequeue events preceding $x.
+The set of valid event traces specified by this schema contains only traces
+that satisfy the constraint. This example presents a filtering operation
+as yet another kind of behavior composition, and demonstrates an
+example of combining imperative (event grammar) and declarative
+(Boolean expressions) constructs for behavior specification. */
+
+SCHEMA Queue_behavior
+
+ROOT Queue: (* ( enqueue | dequeue ) *)
+ BUILD {
+ /* if an element is retrieved, it should have been stored before,
+ this constraint is identical to Stack behavior constraint. */
+ ENSURE FOREACH $x: dequeue
+ ( #dequeue BEFORE $x < #enqueue BEFORE $x );
+
+ /* The following composition operation establishes enqueue/dequeue pairs
+ in the Queue behavior. For each 'dequeue' the earliest in time
+ preceding 'enqueue' is selected, unless it has been already
+ consumed by another 'dequeue' */
+
+ COORDINATE $get: dequeue
+ DO COORDINATE $put: enqueue
+ SUCH THAT $put BEFORE $get
+ DO IF NOT ( EXISTS $g: dequeue $put Paired_with $g OR
+ EXISTS $p: enqueue $p Paired_with $get )
+ THEN ADD $put Paired_with $get; FI;
+ OD;
+ OD;
+ };/* end BUILD for Queue */
diff --git a/models/Legacy_examples/Example05_Car_Race.mp b/models/Legacy_examples/Example05_Car_Race.mp
new file mode 100644
index 0000000000000000000000000000000000000000..4f6a8fd1696640cb494f27500d720ebb288be6c6
--- /dev/null
+++ b/models/Legacy_examples/Example05_Car_Race.mp
@@ -0,0 +1,64 @@
+/* Example5_CarRace.mp
+
+ more coordination patterns:
+ - ordering of selected events in concurrent threads
+ can be modeled by coordinating them with event sequence;
+
+ - one-many coordination.
+
+ Run for scopes 1 and up. The "Sequence" or "Swim Lanes"
+ layouts are the most appropriate for browsing traces here.
+*/
+
+SCHEMA Example5_Car_Race
+
+Car: Start
+ (* drive_lap *)
+ /* not necessary all cars will finish */
+ ( finish [ winner ] | break) ;
+
+ROOT Cars: {+ Car +}
+
+ BUILD{
+ /* everybody who finishes drives the same number of laps */
+ ENSURE FOREACH DISJ $c1: Car, $c2: Car
+ (#finish FROM $c1 == 1 AND #finish FROM $c2 == 1 ->
+ #drive_lap FROM $c1 == #drive_lap FROM $c2)
+
+ AND
+ /* if it breaks, then earlier */
+ (#finish FROM $c1 == 1 AND #break FROM $c2 == 1 ->
+ #drive_lap FROM $c1 >= #drive_lap FROM $c2);
+
+ /* there always will be at most one winner */
+ ENSURE #winner <= 1;
+
+ /* if at least one car finishes, there should be a winner */
+ ENSURE #finish > 0 -> #winner > 0;
+ };
+
+ROOT Judge: provide_start_signal
+ watch
+ (* finish *);
+
+/* one-many coordination can be done with nested COORDINATE */
+COORDINATE $a: provide_start_signal FROM Judge
+ DO COORDINATE $b: Start FROM Cars
+ DO ADD $a PRECEDES $b; OD;
+ OD;
+
+Cars, Judge SHARE ALL finish;
+
+/* now when the ordering of finish events is ensured
+ (because they are ordered in the Judge root traces),
+ we can state: the winner is the car which finishes first */
+COORDINATE $w: winner
+ DO ENSURE #finish BEFORE $w == 1; OD;
+
+/* this is an example of trace annotation with data
+ specific for the trace */
+
+IF #finish == #Car THEN SAY("All cars have finished");
+ELSE SAY( #finish " cars from " #Car
+ " have finished");
+FI;
diff --git a/models/Legacy_examples/Example06_Assertion_Checking.mp b/models/Legacy_examples/Example06_Assertion_Checking.mp
new file mode 100644
index 0000000000000000000000000000000000000000..61d2cdd5ddbcfc7abbdceb49229fa295b8a4fb03
--- /dev/null
+++ b/models/Legacy_examples/Example06_Assertion_Checking.mp
@@ -0,0 +1,57 @@
+/* Example6 Assertion checking, Communicating via unreliable channel.
+
+ MP models need to be tested and debugged like any other
+ programming artifacts. Trace generation for a given scope
+ yields exhaustive set of valid event traces.
+ Browsing these traces may result in finding examples of behavior
+ that are unwanted. Then we fix the issue in the MP code,
+ and run the trace generation again, until our expectations are
+ satisfied.
+
+ Browsing dozens or hundreds of event traces may be time
+ consuming and error prone. The CHECK construct makes it possible
+ to use automated trace monitoring. If the property
+ (Boolean expression in the CHECK) is not satisfied, the trace will
+ be marked and available for further inspection.
+
+ This can significantly speed up the testing process. Of course,
+ if the property should always hold, it makes sense to convert it
+ into the ENSURE condition.
+*/
+
+SCHEMA AtoB
+
+ROOT TaskA: (* A_sends_request_to_B
+ ( A_receives_data_from_B |
+ A_timeout_waiting_from_B )
+ *);
+
+ROOT Connector_A_to_B:
+ (* A_sends_request_to_B
+ ( B_receives_request_from_A
+ B_sends_data_to_A
+ ( A_receives_data_from_B |
+ A_timeout_waiting_from_B ) |
+
+ A_timeout_waiting_from_B )
+ *);
+/* A_timeout_waiting_from_B may happen because Connector_A_to_B
+ fails to pass a message from A to B, or from B to A */
+
+TaskA, Connector_A_to_B SHARE ALL A_sends_request_to_B,
+ A_timeout_waiting_from_B,
+ A_receives_data_from_B ;
+
+ROOT TaskB: (* B_receives_request_from_A
+ B_sends_data_to_A
+ *);
+
+TaskB, Connector_A_to_B SHARE ALL B_receives_request_from_A,
+ B_sends_data_to_A ;
+
+/* assertion checking will mark examples of traces where TaskA
+ does not receive the requested data and will attach a message
+ to the trace */
+CHECK #A_sends_request_to_B FROM TaskA ==
+ #A_receives_data_from_B FROM TaskA
+ ONFAIL SAY("loss of reception detected");
diff --git a/models/Legacy_examples/Example07_Unconstrained_Stack.mp b/models/Legacy_examples/Example07_Unconstrained_Stack.mp
new file mode 100644
index 0000000000000000000000000000000000000000..817cee81c00edf2727d9cdd9a669b80d280eb5bb
--- /dev/null
+++ b/models/Legacy_examples/Example07_Unconstrained_Stack.mp
@@ -0,0 +1,50 @@
+/* Example7 Trace annotation techniques
+
+Assertion checking with the CHECK clause may be the simplest and most
+common tool for finding counterexamples of traces, which violate some
+property. Traces violating the CHECK condition are marked, and the
+message provides some hint about the cause. The message is associated
+with the root, composite, or the whole schema, and further details may
+require browsing of the corresponding trace segment. The following example
+demonstrates how to make messages more specific and focused.
+
+Let’s consider again the Stack model, but this time without the ENSURE
+constraint on the Stack behavior. This Stack certainly will produce
+unwanted behaviors. The MP code illustrates how to pinpoint events that
+might violate certain property, and how to annotate these particular
+events in the trace with additional messages. Programmers will recognize
+the use of debugging print statements for traditional program testing/debugging.
+*/
+
+SCHEMA Unconstrained_Stack
+ROOT Stack: (* ( push | pop [ bang ]) *)
+ /* bang event represents the Stack underflow event */
+
+ BUILD {
+ /* By default the domain for event selection is FROM THIS.
+
+ The following ENSURE makes sure that each attempt to pop empty Stack
+ is followed by bang event */
+
+ ENSURE FOREACH $p: pop
+ /* pop associated with the bang event does not affect Stack contents,
+ hence only successful pop events do count */
+
+ (#pop BEFORE $p - #bang BEFORE $p) >= #push BEFORE $p
+ <-> #bang FOLLOWS $p == 1;
+
+ COORDINATE $b: bang
+
+ /* pick up pop event immediately preceding bang */
+ DO COORDINATE $x: pop SUCH THAT $x PRECEDES $b
+ DO ADD SAY("This event tries to pop empty Stack")
+ PRECEDES $x;
+ MARK;
+ OD;
+ OD;
+ };
+
+/* Now traces where Stack behavior is incorrect will be MARKed and
+ corresponding pop events will be pointed to by PRECEDES arrow leading
+ from the message box associated with this event.
+*/
\ No newline at end of file
diff --git a/models/Legacy_examples/Example08_Operational_Process.mp b/models/Legacy_examples/Example08_Operational_Process.mp
new file mode 100644
index 0000000000000000000000000000000000000000..e930176a2b7dbc5bc020ee3929f3a03147a92e4b
--- /dev/null
+++ b/models/Legacy_examples/Example08_Operational_Process.mp
@@ -0,0 +1,123 @@
+/* Example8_OperationalProcess.mp
+ modeling operational processes
+
+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.
+
+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.
+
+Run for scope 1 (there is no iteration in this example, so increaasing the scope will not
+produce more scenarios). Only one scenario is produced because no decision points have been
+added to this model yet.
+
+The "Sequence" or "Swim Lanes" layouts are the most appropriate for browsing traces here.
+The "Sequence" mode yields views very similar to the UML or SysML Sequence Diagrams.
+
+*/
+
+
+/* Actors */
+
+SCHEMA Wide_Range_Search_for_Wreckage_and_Survivors
+
+ROOT Command_and_Control: Receive_distress_signal
+ Pass_mission_information
+ Acknowledge_search_plan
+ Receive_relayed_survivor_location_and_situation;
+
+ROOT On_Scene_Commander: Receive_mission_information
+ Relay_mission_information
+ Attempt_contact_with_PID
+ Assess_environmental_conditions
+ Receive_environmental_conditions
+ Provide_search_plan
+ Communicate_search_plan_and_responsibilities
+ Scan_environment_for_signs_of_PID
+ Receive_updates_for_OSC
+ Receive_PID_location_and_situation
+ Relay_survivor_location_and_situation;
+
+ROOT PID: Send_distress_signal
+ Identify_self_as_PID
+ Present_for_rescue;
+
+ROOT Physical_Environment: Provide_environmental_conditions;
+
+ROOT SAR_Assets: Receive_relayed_mission_information
+ Confirm_search_plan_and_responsibilities
+ Scan_environment_for_signs_of_PID
+ Provide_updates_to_OSC
+ Spot_object_of_interest
+ Maneuver_to_rescue_PID
+ Notify_OSC_of_PID_location_and_situation;
+
+/* Interactions */
+
+COORDINATE $a: Send_distress_signal FROM PID,
+ $b: Receive_distress_signal FROM Command_and_Control
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Pass_mission_information FROM Command_and_Control,
+ $b: Receive_mission_information FROM On_Scene_Commander
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Relay_mission_information FROM On_Scene_Commander,
+ $b: Receive_relayed_mission_information FROM SAR_Assets
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Assess_environmental_conditions FROM On_Scene_Commander,
+ $b: Provide_environmental_conditions FROM Physical_Environment
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Provide_environmental_conditions FROM Physical_Environment,
+ $b: Receive_environmental_conditions FROM On_Scene_Commander
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Provide_search_plan FROM On_Scene_Commander,
+ $b: Acknowledge_search_plan FROM Command_and_Control
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Acknowledge_search_plan FROM Command_and_Control,
+ $b: Communicate_search_plan_and_responsibilities FROM On_Scene_Commander
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Communicate_search_plan_and_responsibilities FROM On_Scene_Commander,
+ $b: Confirm_search_plan_and_responsibilities FROM SAR_Assets
+ DO ADD $a PRECEDES $b; OD;
+
+On_Scene_Commander, SAR_Assets SHARE ALL Scan_environment_for_signs_of_PID;
+
+COORDINATE $a: Provide_updates_to_OSC FROM SAR_Assets,
+ $b: Receive_updates_for_OSC FROM On_Scene_Commander
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Spot_object_of_interest FROM SAR_Assets,
+ $b: Identify_self_as_PID FROM PID
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Identify_self_as_PID FROM PID,
+ $b: Maneuver_to_rescue_PID FROM SAR_Assets
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Maneuver_to_rescue_PID FROM SAR_Assets,
+ $b: Present_for_rescue FROM PID
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Notify_OSC_of_PID_location_and_situation FROM SAR_Assets,
+ $b: Receive_PID_location_and_situation FROM On_Scene_Commander
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Relay_survivor_location_and_situation FROM On_Scene_Commander,
+ $b: Receive_relayed_survivor_location_and_situation FROM Command_and_Control
+ DO ADD $a PRECEDES $b; OD;
diff --git a/models/Legacy_examples/Example09_Employee_Employer.mp b/models/Legacy_examples/Example09_Employee_Employer.mp
new file mode 100644
index 0000000000000000000000000000000000000000..b4423996067a0807558a1252a928e9d1aae4e2d7
--- /dev/null
+++ b/models/Legacy_examples/Example09_Employee_Employer.mp
@@ -0,0 +1,50 @@
+/* Example9_Employee_Employer.mp
+
+The web site http://www.infoq.com/articles/bpelbpm
+“Why BPEL is not the holy grail for BPM “
+provides an example of a process that can be described
+in BPMN but not in BPEL.
+It is claimed to be a challenge for process specification.
+
+Here is the description.
+“When a new employee arrives at a company, a workflow is instantiated.
+First a record needs to be created in the Human Resources database.
+Simultaneously, an office has to be provided.
+As soon as the Human Resources activity has been completed,
+the employee can undergo a medical check. During that time,
+a computer is provided. This is only possible when both an office
+has been set up and an account created in the information system
+from the human resource database. When both the computer and the
+medical check have been performed, the employee is ready to work.
+Of course, you may want to model this simple process differently,
+but the point here is that you cannot define a structured
+parallel workflow [in BPEL] that is equivalent to this one ..."
+
+ Run for scope 1. The "Sequence" or "Swim Lanes"
+ layouts are the most appropriate for browsing traces here.
+ Some box reshuffling may be needed to improve the trace layout.
+*/
+
+SCHEMA Employee_Employer
+
+ROOT Employee: SendArrivalDate
+ MedicalCheck
+ ReadyToWork;
+
+ROOT Employer: EmployeeArrival
+ /* these are concurrent threads */
+ { Fill_HR_DB MedicalCheck,
+ ProvideOffice ProvideComputer }
+ ReadyToWork;
+
+Employee, Employer SHARE ALL MedicalCheck, ReadyToWork;
+
+/* coordination of two events in different threads */
+COORDINATE $a: SendArrivalDate FROM Employee,
+ $b: EmployeeArrival FROM Employer
+ DO ADD $a PRECEDES $b; OD;
+
+/* coordination between two events deep inside the process */
+COORDINATE $a: Fill_HR_DB FROM Employer,
+ $b: ProvideComputer FROM Employer
+ DO ADD $a PRECEDES $b; OD;
diff --git a/models/Legacy_examples/Example10_Pipe_Filter.mp b/models/Legacy_examples/Example10_Pipe_Filter.mp
new file mode 100644
index 0000000000000000000000000000000000000000..63896c93432204eb441999ce30cdc279d45a82f6
--- /dev/null
+++ b/models/Legacy_examples/Example10_Pipe_Filter.mp
@@ -0,0 +1,55 @@
+/* Example10_Pipe_Filter.mp
+ pipe/filter architecture model with 2 filters
+
+ assumptions:
+ 1) not all items sent by Producer will be received by Consumer,
+ 2) after a message has been sent, it cannot be send repeatedly,
+ 3) received message can stay in the Filter for while,
+ before being sent (if at all).
+*/
+
+SCHEMA Pipe_Filter
+
+ROOT Producer: (* send *);
+
+ROOT Filter1: (* receive (* send *) *)
+/* Filter can send only after receive */
+ BUILD { /* can send only what has been received */
+ ENSURE FOREACH $s: send
+ (#receive BEFORE $s > #send BEFORE $s);
+
+ /* not everything received will be sent */
+ IF #send != #receive THEN
+ SAY("some messages have been lost in Filter1" ); FI;
+ };
+
+COORDINATE $s: send FROM Producer,
+ $r: receive FROM Filter1
+ DO ADD $s PRECEDES $r; OD;
+
+ROOT Filter2: (* receive (* send *) *)
+/* Filter can send only after receive */
+ BUILD { /* can send only what has been received */
+ ENSURE FOREACH $s: send
+ (#receive BEFORE $s > #send BEFORE $s);
+
+ /* not everything received will be sent */
+ IF #send != #receive THEN
+ SAY("some messages have been lost in Filter2" ); FI;
+ };
+
+COORDINATE $s: send FROM Filter1,
+ $r: receive FROM Filter2
+ DO ADD $s PRECEDES $r; OD;
+
+ROOT Consumer: (* receive *);
+
+COORDINATE $s: send FROM Filter2,
+ $r: receive FROM Consumer
+ DO ADD $s PRECEDES $r; OD;
+
+IF #receive FROM Consumer != #send FROM Producer THEN
+ SAY( #send FROM Producer - #receive FROM Consumer
+ " messages did not reach Consumer");
+ MARK;
+FI;
\ No newline at end of file
diff --git a/models/Legacy_examples/Example11_Publish_Subscribe.mp b/models/Legacy_examples/Example11_Publish_Subscribe.mp
new file mode 100644
index 0000000000000000000000000000000000000000..b885a2ed08874cd27fd08df23391baf5caf8dbfd
--- /dev/null
+++ b/models/Legacy_examples/Example11_Publish_Subscribe.mp
@@ -0,0 +1,89 @@
+/* Example 11 Publish/Subscribe architecture model.
+
+ Publisher sends a notification to all active Subscribers
+ when new information is available.
+
+ scope 1, 1 trace in less than 1 sec.
+ scope 2, 51 traces in less than 1 sec.
+ scope 3 3813 traces in approx. 5 min.
+*/
+
+SCHEMA Publish_Subscribe
+
+ROOT Publisher: Register
+ (+ <2 .. 3 + $$scope * 2> ( Register | Unsubscribe | Send ) +)
+/* Iteration_scope <2 .. 3 + $$scope * 2> is needed to provide enough events for
+ coordination, since each Client has Register/Unsubscribe event pair,
+ plus some Receive events */
+
+BUILD{
+ /* The Register and Unsubscribe events should be balanced */
+ ENSURE #Register == #Unsubscribe;
+
+ ENSURE FOREACH $u: Unsubscribe #Register BEFORE $u > #Unsubscribe BEFORE $u;
+
+ /* Publisher will Send only if there is at least one active Client.
+ This condition is specified with ENSURE. */
+
+ ENSURE FOREACH $s: Send #Register BEFORE $s > #Unsubscribe BEFORE $s;
+ };
+
+Client: Register (* Receive *) Unsubscribe;
+
+ROOT Subscribers: {+ Client +};
+
+/****** Coordination between Publisher and Subscribers ******/
+/* The ordering of composition operations is important, since Register and
+ Unsubscribe events are used to coordinate Send/Receive between
+ Publisher and Client.
+
+ First, we do SHARE ALL for Register events,
+ next will try all valid permutations of Register/Unsubscribe,
+ and then proceed with further coordination of Send/Receive,
+ using the shared Register and Unsubscribe events as pivots
+ to coordinate Send events for each Client */
+
+ /* Need to try all possible permutations of Register/Unsubscribe pairs,
+ hence the use of <!> event reshuffling */
+COORDINATE $r1: Register FROM Publisher,
+ <!> $r2: Register FROM Subscribers
+ DO SHARE $r1 $r2; OD;
+
+COORDINATE $u1: Unsubscribe FROM Publisher,
+ <!> $u2: Unsubscribe FROM Subscribers
+ DO SHARE $u1 $u2; OD;
+
+/* the following coordination is performed
+ for each valid permutation of Register/Unsubscribe */
+COORDINATE $client: Client FROM Subscribers
+ DO COORDINATE $reg: Register FROM $client,
+ $uns: Unsubscribe FROM $client
+
+ /* For Send event selection to coordinate with a particular
+ Client event, the SUCH THAT thread condition is used.
+ Client will Receive all and only Send between his Register and Unsubscribe */
+ DO COORDINATE $r: Receive FROM $client,
+ $s: Send FROM Publisher
+ SUCH THAT $s AFTER $reg AND $s BEFORE $uns
+
+ /* Register and Unsubscribe events have been shared and now can be used
+ to select appropriate Receive events from the Client and
+ Send events from the Publisher for coordination */
+
+ DO ADD $s PRECEDES $r; OD;
+ OD;
+ OD;
+
+/**** A query ******/
+/* It might be interesting to find out whether there are
+ Send events received by several Clients.
+ MARK traces containing such event configuration, and place
+ annotation pointing to the Send event of interest*/
+COORDINATE $s: Send
+DO
+ IF (#Receive FOLLOWS $s > 1) THEN
+ MARK;
+ ADD SAY("this Send is received by " #Receive FOLLOWS $s " Clients")
+ PRECEDES $s;
+ FI;
+OD;
diff --git a/models/Legacy_examples/Example12_network_topology_ring.mp b/models/Legacy_examples/Example12_network_topology_ring.mp
new file mode 100644
index 0000000000000000000000000000000000000000..d3dcba336d47cf365b1ea1017c60c6ae41bf21c8
--- /dev/null
+++ b/models/Legacy_examples/Example12_network_topology_ring.mp
@@ -0,0 +1,75 @@
+/* ring.mp
+ ring topology
+ an example of user-defined relation use
+
+ The following is a model of network ring,
+ where each node interacts with its left and right neighbors only.
+------------------------------------------*/
+
+SCHEMA ring
+/* model of networking ring, where each node sends/receives
+to/from its left and right neighbor.
+*/
+
+Node: (* ( send_left | send_right |
+ receive_from_left | receive_from_right ) *);
+
+ROOT Ring: {+ Node +}
+
+/* The following coordinations are done over the root Ring,
+ the ring may contain one or more Nodes */
+BUILD{
+
+COORDINATE $x1: Node,/* This thread produces a default set */
+<SHIFT_LEFT> $x2: Node
+
+/* SHIFT_LEFT reshuffling, means that when the default set
+of Node events is selected (all Node events from THIS),
+it takes the first event from the
+beginning and puts it to the end of sequence.
+This adjusted thread is used to produce the ring topology */
+
+DO
+/* The COORDINATE loop proceeds to set up new relations between $x1 and its neighbor */
+ ADD $x1 left_neighbor_of $x2,
+ $x2 right_neighbor_of $x1;
+OD;
+
+/*-----------------------------------------------------
+We assert the single ring property.
+^R yields a transitive closure of the relation R.
+Ring topology means that every node can be reached from any node in both directions.
+Although it is possible to prove that the previous coordination sets the ring properly,
+the following assertion check is provided for clarity to demonstrate how such
+properties can be expressed in MP.
+If uncommented, it will increase the trace generation time.
+Assertions are mostly used for model testing/debugging.
+You can uncomment it and try to run.
+--------------------------------------------------------*/
+
+/*----------------------------------------------------
+CHECK FOREACH $a: Node, $b: Node
+( $a ^left_neighbor_of $b AND
+ $a ^right_neighbor_of $b )
+ONFAIL SAY("ring property violation detected!");
+-----------------------------------------------------*/
+
+/* After the ring topology has been created,
+we can coordinate message exchange between neighbors,
+i.e. define the behavior of the ring */
+
+COORDINATE $m: Node /* Default set, do the following for each Node */
+
+DO COORDINATE $left: Node SUCH THAT $left left_neighbor_of $m
+
+ DO
+ COORDINATE $s1: send_left FROM $m,
+ $r1: receive_from_right FROM $left
+ DO ADD $s1 PRECEDES $r1; OD;
+
+ COORDINATE $s1: send_right FROM $left,
+ $r1: receive_from_left FROM $m
+ DO ADD $s1 PRECEDES $r1; OD;
+ OD;
+OD;
+}; /* end of the BUILD block for the root Ring */
diff --git a/models/Legacy_examples/Example13_FiniteStateDiagram.mp b/models/Legacy_examples/Example13_FiniteStateDiagram.mp
new file mode 100644
index 0000000000000000000000000000000000000000..90b775634588e05da0c86ff492d65dc9b3949e01
--- /dev/null
+++ b/models/Legacy_examples/Example13_FiniteStateDiagram.mp
@@ -0,0 +1,80 @@
+/* Example13_FiniteStateDiagram.mp
+
+ example of finite state diagram behavior model,
+ contains non-deterministic transitions (from S1 with symbol a),
+ and a single state loop (S3 with a).
+
+ The finite state transition diagram:
+
+ Start -> S1
+ S1 -> a -> S3
+ S1 -> a -> S4
+ S1 -> b -> S4
+ S2 -> b -> S1
+ S2 -> End
+ S3 -> a -> S3
+ S3 -> b -> S4
+ S4 -> a -> S2
+
+ Direct modeling of the state diagram including state visits
+ and actions triggering state transitions. Only paths starting
+ with Start and ending with End are valid.
+
+ Behavior of each state Si is represented by a separate
+ root event Si_behavior.
+
+ Each transition in the diagram Si -> Sj is modeled by a
+ composite event Si_to_Sj.
+
+ 1) Event Si_to_Sj contains the symbol triggering the transition.
+ 2) Si_to_Sj is shared by corresponding state behavior roots.
+
+ run for:
+ scope 1 (4 traces),
+ scope 2 (30 traces),
+ scope 3 (258 traces)
+*/
+
+SCHEMA FiniteStateDiagram
+
+S1_to_S3: a;
+S1_to_S4: (a | b);
+
+ROOT S1_behavior: Start S1
+ (* (S1_to_S3 | S1_to_S4) S2_to_S1 S1 *)
+ (S1_to_S3 | S1_to_S4);
+
+S2_to_S1: b;
+
+ROOT S2_behavior: (* S4_to_S2 S2 S2_to_S1 *)
+ S4_to_S2 S2 End;
+
+S1_behavior, S2_behavior SHARE ALL S2_to_S1;
+
+/* coordination should be done as soon as possible,
+ in order to prune the search,
+ but only after both root S1_behavior and S2_behavior
+ traces are available */
+
+S3_to_S3: a;
+S3_to_S4: b;
+
+ROOT S3_behavior: (* S1_to_S3 S3
+ (* S3_to_S3 S3 *)
+ S3_to_S4 *) ;
+
+S3_behavior, S1_behavior SHARE ALL S1_to_S3;
+
+S4_to_S2: a;
+
+ROOT S4_behavior: (* (S1_to_S4 | S3_to_S4) S4
+ S4_to_S2 *) ;
+
+S4_behavior, S1_behavior SHARE ALL S1_to_S4;
+S4_behavior, S2_behavior SHARE ALL S4_to_S2;
+S4_behavior, S3_behavior SHARE ALL S3_to_S4;
+
+SAY("The path: ");
+/* Sort state visits and transition events according to the BEFORE relation and then show them */
+COORDINATE <SORT> $a: (S1 | S2 | S3 | S4 | a | b | Start | End)
+ DO SAY($a); OD;
diff --git a/models/Legacy_examples/Example14_microwave_oven.mp b/models/Legacy_examples/Example14_microwave_oven.mp
new file mode 100644
index 0000000000000000000000000000000000000000..fa6ad1cab52efde09ccde8b0361c9edc2bd051fc
--- /dev/null
+++ b/models/Legacy_examples/Example14_microwave_oven.mp
@@ -0,0 +1,93 @@
+/* Example14, microwave_oven.mp
+
+ example of finite state diagram behavior model,
+ CTL formula representation in MP, and model checking for a small scope.
+
+ Microwave oven example from E.Clarke, O.Grumberg, D.Peled
+ "Model Checking". MIT Press, 1999, pp. 38-39.
+
+ S1 - start & end state
+
+ Transitions:
+ S1 -> start_oven -> S2
+ S1 -> close_door -> S3
+ S2 -> close_door -> S5
+ S3 -> open_door -> S1
+ S3 -> start_oven -> S6
+ S4 -> open_door -> S1
+ S4 -> done -> S3
+ S4 -> cook -> S4
+ S5 -> open_door -> S2
+ S5 -> reset -> S3
+ S6 -> warm_up -> S7
+ S7 -> start_cooking -> S4
+
+ State diagram converted into regular expressions,
+ or paths, including state visits
+ and commands triggering state transitions,
+ following well known algorithm NFA -> RE.
+
+ run for:
+ scope 1 (28 traces, 2 counterexamples, 1.75 sec.)
+*/
+
+SCHEMA oven
+
+ROOT Microwave: S1 (* R7 S1 *);
+
+/* regular expressions, or paths, including state visits
+ and actions triggering state transitions
+========================================================*/
+/* eliminating S7, paths from S6 to S4 via S7 */
+R1: warm_up S7 start_cooking;
+
+/* eliminating S6, paths from S3 to S4 via S6 */
+R2: start_oven S6 R1;
+
+/* eliminating S5, paths from S2 to S3 via S5 */
+R3: close_door S5 reset;
+
+/* eliminating S5, paths from S2 to S2 via S5 */
+R4: close_door S5 open_door;
+
+/* eliminating S2, paths from S1 to S3 via S2 */
+R5: start_oven S2 (* R4 S2 *) R3;
+
+/* eliminating S4, paths from S3 to S1 via S4 */
+R6: R2 S4 (* cook S4 *) open_door;
+
+/* eliminating S3, paths from S1 to S1 via S3 */
+R7: (close_door | R5) S3
+ (* R2 (* S4 cook *) S4 done S3 *)
+ (open_door | R6);
+
+/* States with atomic propositions represented as inner events,
+ absence of atomic proposition implies its negation
+===============================================================*/
+S1:; /* ~Start, ~Close, ~Heat, ~Error */
+
+S2: {Start, Error}; /* Start, ~Close, ~Heat, Error */
+
+S3: Close; /* ~Start, Close, ~Heat, ~Error */
+
+S4: {Close, Heat}; /* ~Start, Close, Heat, ~Error */
+
+S5: {Start, Close, Error}; /* Start, Close, ~Heat, Error */
+
+S6: {Start, Close}; /* Start, Close, ~Heat, ~Error */
+
+S7: {Start, Close, Heat}; /* Start, Close, Heat, ~Error */
+
+/* MP assertion to check CTL formula AG(Start -> AF Heat)
+==========================================================*/
+CHECK (FOREACH $s: Start EXISTS $h: Heat $h AFTER $s)
+ ONFAIL SAY("no Heat after Start detected");
+
+
+/************** create Path view ***********************/
+/* show the sequence of states and commands in precedence order */
+/*==============================================================*/
+COORDINATE <SORT> $a: (S1 | S2 | S3 | S4 | S5 | S6 | S7 |
+ warm_up | start_cooking | start_oven |
+ close_door | reset | open_door | cook | done)
+ DO SAY($a); OD;
diff --git a/models/Legacy_examples/Example15_Petri_net.mp b/models/Legacy_examples/Example15_Petri_net.mp
new file mode 100644
index 0000000000000000000000000000000000000000..b0ecf3becf6a41206e611e1fb1438a76fad6f5f5
--- /dev/null
+++ b/models/Legacy_examples/Example15_Petri_net.mp
@@ -0,0 +1,111 @@
+/* Example15_Petri_net.mp
+ modeling Petri net behavior
+ see the Petri net diagram in Sec. 2.16.2 in the MP v.4 Language Manual
+ scope 1 (2 traces, 0.02 sec.)
+ scope 2 (4 traces, 6.23 sec.)
+
+ to obtain in the Global view Petri net diagram
+ extracted from the event traces, run scope 2
+=======================================================*/
+
+SCHEMA petri_net
+/* behavior of each place and transition
+ is modeled by a separate root event */
+
+P1_sends_to_T1: send_token;
+P1_receives_from_T2: get_token;
+
+ROOT P1_behavior: get_token (* (* P1_receives_from_T2 *)
+ P1_sends_to_T1 *)
+ BUILD{ ENSURE FOREACH $s: P1_sends_to_T1
+ #get_token BEFORE $s > #send_token BEFORE $s;};
+
+ROOT T1_behavior: (* T1_receives_from_P1 T1_fires
+ {T1_sends_to_P2, T1_sends_to_P3} *);
+T1_sends_to_P2: send_token;
+T1_sends_to_P3: send_token;
+
+COORDINATE $s: P1_sends_to_T1,
+ $r: T1_receives_from_P1
+ DO ADD $s PRECEDES $r; OD;
+
+ROOT P2_behavior: (* (* P2_receives_from_T1 *)
+ P2_sends_to_T2 *)
+ BUILD{ ENSURE FOREACH $s: P2_sends_to_T2
+ #get_token BEFORE $s > #send_token BEFORE $s;};
+P2_receives_from_T1: get_token;
+P2_sends_to_T2: send_token;
+
+COORDINATE $s: T1_sends_to_P2,
+ $r: P2_receives_from_T1
+ DO ADD $s PRECEDES $r; OD;
+
+ROOT P3_behavior: get_token get_token
+ (* (* P3_receives_from_T1 *)
+ P3_sends_to_T2 *)
+ BUILD{ ENSURE FOREACH $s: P3_sends_to_T2
+ #get_token BEFORE $s > #send_token BEFORE $s;};
+P3_receives_from_T1: get_token;
+P3_sends_to_T2: send_token;
+
+COORDINATE $s: T1_sends_to_P3,
+ $r: P3_receives_from_T1
+ DO ADD $s PRECEDES $r; OD;
+
+ROOT T2_behavior: (* {T2_receives_from_P2, T2_receives_from_P3} T2_fires
+ [{T2_sends_to_P1, T2_sends_to_P4}] *);
+/* T2_sends_to events are made optional to terminate the loop from T2 to P1*/
+T2_sends_to_P1: send_token;
+T2_sends_to_P4: send_token;
+
+COORDINATE $s: P2_sends_to_T2,
+ $r: T2_receives_from_P2
+ DO ADD $s PRECEDES $r; OD;
+
+COORDINATE $s: P3_sends_to_T2,
+ $r: T2_receives_from_P3
+ DO ADD $s PRECEDES $r; OD;
+
+COORDINATE $s: T2_sends_to_P1,
+ $r: P1_receives_from_T2
+ DO ADD $s PRECEDES $r; OD;
+
+ROOT P4_behavior: get_token (* P4_receives_from_T2 *);
+P4_receives_from_T2: get_token;
+
+COORDINATE $s: T2_sends_to_P4,
+ $r: P4_receives_from_T2
+ DO ADD $s PRECEDES $r; OD;
+
+COORDINATE $b: (P1_behavior | P2_behavior | P3_behavior | P4_behavior)
+ DO SAY("At the end of simulation place " $b " has "
+ #get_token FROM $b - #send_token FROM $b " tokens");
+ OD;
+/*================================================================
+ Building Petri net diagram
+=================================================================*/
+GRAPH Diagram { TITLE ("Petri net diagram");};
+ATTRIBUTES {number initial_tokens;};
+
+WITHIN Diagram{
+ COORDINATE $a: $$ROOT DO
+ Node$f: LAST($a);
+
+ $a.initial_tokens :=
+ #{$t: get_token FROM $a SUCH THAT #send_token BEFORE $t == 0};
+
+ IF $a.initial_tokens > 0 THEN
+ ADD LAST("Start") ARROW("initial " $a.initial_tokens " tokens") Node$f;
+ FI;
+
+ COORDINATE $b: $$ROOT DO
+ IF $a != $b AND
+ /* looking for $c: A_sends_to_B and $d: B_receives_from_A events */
+ EXISTS $c: $$COMPOSITE FROM $a, $d: $$EVENT FROM $b ($c PRECEDES $d)
+ THEN ADD Node$f ARROW(1) LAST($b); FI;
+ OD;
+ OD;
+}; /* end WITHIN */
+
+GLOBAL
+SHOW Diagram;
diff --git a/models/Legacy_examples/Example16_software_spiral_process.mp b/models/Legacy_examples/Example16_software_spiral_process.mp
new file mode 100644
index 0000000000000000000000000000000000000000..f8d21425998fbfe8c472101decf9945a3ff8bc6d
--- /dev/null
+++ b/models/Legacy_examples/Example16_software_spiral_process.mp
@@ -0,0 +1,82 @@
+/* Example 16, model of the spiral software process
+
+ 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."
+
+ run scope up to 5
+======================================*/
+
+SCHEMA spiral
+
+ROOT Stakeholders:
+ Initial_communication_with_stakeholders
+ Prototype_demonstration_to_stakeholders
+ (* Stakeholders_are_not_satisfied
+ Prototype_demonstration_to_stakeholders *)
+ Stakeholders_are_satisfied;
+
+ROOT Spiral_process:
+ Initial_communication_with_stakeholders
+ Initial_requirements
+ Initial_design
+ Prototype_demonstration_to_stakeholders
+ (* One_iteration *)
+ Stakeholders_are_satisfied
+ Delivery_of_the_system;
+
+One_iteration:
+ Stakeholders_are_not_satisfied
+ Adjust_requirements
+ Redesign
+ Prototype_demonstration_to_stakeholders;
+
+Initial_design:
+ Architecture_design
+ Detailed_design
+ Coding
+ Testing;
+
+Redesign:
+ [ Architecture_redesign ] /* not always needed */
+ Detailed_redesign
+ Coding
+ Testing;
+
+Stakeholders, Spiral_process SHARE ALL
+ Initial_communication_with_stakeholders,
+ Prototype_demonstration_to_stakeholders,
+ Stakeholders_are_not_satisfied,
+ Stakeholders_are_satisfied;
+
+ROOT Architect:
+ Initial_communication_with_stakeholders
+ Initial_requirements
+ Architecture_design
+ Prototype_demonstration_to_stakeholders
+ (* Adjust_requirements
+ [ Architecture_redesign ]
+ Prototype_demonstration_to_stakeholders *);
+
+Architect, Spiral_process SHARE ALL
+ Initial_communication_with_stakeholders,
+ Initial_requirements,
+ Architecture_design,
+ Prototype_demonstration_to_stakeholders,
+ Adjust_requirements,
+ Architecture_redesign;
+
+ROOT Developers:
+ Detailed_design
+ Coding
+ Testing
+ (* Detailed_redesign
+ Coding
+ Testing *);
+
+Developers, Spiral_process SHARE ALL
+ Detailed_design,
+ Detailed_redesign,
+ Coding,
+ Testing;
diff --git a/models/Legacy_examples/Example17_Dining_Philosophers.mp b/models/Legacy_examples/Example17_Dining_Philosophers.mp
new file mode 100644
index 0000000000000000000000000000000000000000..6a2330a892b959217997c816aae07682034f5340
--- /dev/null
+++ b/models/Legacy_examples/Example17_Dining_Philosophers.mp
@@ -0,0 +1,90 @@
+/* Example 17, Dining_Philosophers.mp
+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.
+(from Wikipedia: http://en.wikipedia.org/wiki/Dining_philosophers_problem )
+
+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.
+
+scope 1 yields zero traces, because Philosopher cannot eat with a single fork.
+scope 2 yields 2 traces in approx. 0.01 sec.
+scope 3 yields 6 traces in approx. 0.05 sec.
+scope 4 yields 14 traces in approx. 0.44 sec.
+scope 5 yields 30 traces in approx. 1.6 sec.
+
+============================================================================*/
+SCHEMA Dining_Philosophers
+
+ROOT Philosophers: {+<$$scope> Philosopher +};
+
+Philosopher: (+ <1> think eat +)
+/* Philosopher eats at least once, but is limited to reduce the number of traces */ ;
+
+eat: { left_fork, right_fork };
+
+ROOT Forks: {+ <$$scope> Fork +};
+
+Fork: (* <2> (left_fork | right_fork) *)
+/* limit the number of fork use to reduce the number of traces,
+ this in fact limits each Philosopher to one "eat" event */
+
+/* Each fork is used at least once by each neighbor */
+BUILD{ ENSURE #left_fork > 0 AND #right_fork > 0;};
+
+/* Assign forks to the Philosophers.
+ Philosophers $p1 and $p2 share fork $f.
+
+ Shift_left reshuffling takes the first event
+ from the beginning and puts it to the end of sequence.
+ This adjusted thread is used to produce the ring topology,
+ and to assign two neighbors $p1 and $p2 for sharing fork $f */
+
+COORDINATE $p1: Philosopher,
+ <SHIFT_LEFT> $p2: Philosopher,
+ $f: Fork
+DO /* Default sequence is adequate here:
+ the order of fork use in Philosopher and in Fork are the same. */
+ $p1, $f SHARE ALL right_fork;
+ $p2, $f SHARE ALL left_fork;
+OD;
+
+/* to avoid deadlocks 'eat' events competing for resources are put in order. */
+COORDINATE $e1: eat
+DO COORDINATE $e2: eat
+ DO
+ IF EXISTS $f1: (left_fork | right_fork) FROM $e1,
+ $f2: (left_fork | right_fork) FROM $e2
+ ($f1 PRECEDES $f2)
+ THEN
+ ADD $e1 PRECEDES $e2;
+ FI;
+ OD;
+OD;
+
+/* Ensure that both forks can be used simultaneously */
+COORDINATE $e: eat
+DO COORDINATE $l: left_fork FROM $e,
+ $r: right_fork FROM $e
+ DO
+ /* MAY_OVERLAP $x $y is an abbreviation for NOT($x BEFORE $y OR $y BEFORE $x) */
+ ENSURE MAY_OVERLAP $l $r;
+ OD;
+OD;
diff --git a/models/Legacy_examples/Example18_Workflow_pattern.mp b/models/Legacy_examples/Example18_Workflow_pattern.mp
new file mode 100644
index 0000000000000000000000000000000000000000..6c3b9601b4316f26231d0145cbcb7db6601c78e7
--- /dev/null
+++ b/models/Legacy_examples/Example18_Workflow_pattern.mp
@@ -0,0 +1,30 @@
+/* Example18 Workflow pattern
+
+the web site
+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
+
+When handling a cardiac arrest, the check_breathing and check_pulse tasks
+run in parallel. Once the first of these has completed, the triage task
+is commenced. Completion of the other task is ignored and does not result
+in a second instance of the triage task.
+
+run for scope 1
+*/
+
+SCHEMA Cardiac_Arrest
+
+ROOT Phase1: { check_breathing [finish_first],
+ check_pulse [finish_first] }
+
+BUILD{ ENSURE #finish_first == 1; };
+
+ROOT Triage: identify_the_patient
+ record_assessment_findings
+ identify_the_priority;
+
+COORDINATE $a: finish_first, $b: identify_the_patient
+ DO ADD $a PRECEDES $b; OD;
diff --git a/models/Legacy_examples/Example19_Consumers_Suppliers.mp b/models/Legacy_examples/Example19_Consumers_Suppliers.mp
new file mode 100644
index 0000000000000000000000000000000000000000..95c01d138963dfe400fed287a3335d6f5569f012
--- /dev/null
+++ b/models/Legacy_examples/Example19_Consumers_Suppliers.mp
@@ -0,0 +1,101 @@
+/* Example 19, Consumers/Suppliers
+
+Asynchronous coordination and dependency definition example.
+
+user-defined relation related_to connects events within each
+single Request_delivery -> Consume chain
+
+on Gryphon:
+ scope 1, 2 traces, in less than 1 sec.
+ scope 2, 213 traces, approx. time 19 sec.
+*/
+
+SCHEMA Suppliers
+
+/*=========================================*/
+ROOT Consumers: {+ Consumer +};
+
+Consumer: (* Request_delivery
+
+ ( Receive_supply |
+
+ Not_available )
+ *)
+;
+
+/*=======================================================================
+ Supply_Office communicates asynchronously with Producers and Suppliers
+=========================================================================*/
+ROOT Supply_Office: (*<1.. $$scope * $$scope>
+ /* Supply_Office serves several Consumers,
+ hence the iteration should be increased */
+ Receive_order_and_buy
+ *);
+
+/*======== coordination ===================================================*/
+COORDINATE <!> $request: Request_delivery FROM Consumers,
+ $receive_request: Receive_order_and_buy FROM Supply_Office
+ DO
+ ADD $request PRECEDES $receive_request;
+ ADD $request related_to $receive_request;
+ OD;
+
+/*==========================================*/
+ROOT Producers: {+ Producer +};
+
+Producer: (* ( Sell | Not_available ) *);
+
+/*======== coordination ===================================================*/
+COORDINATE $receive_order: Receive_order_and_buy FROM Supply_Office,
+ /* Receive_order_and_buy and Sell/Not_available events
+ may be asynchronous */
+ <!> $sell: (Sell | Not_available) FROM Producers
+ DO ADD $receive_order PRECEDES $sell;
+ ADD $receive_order related_to $sell;
+ OD;
+
+COORDINATE $sell: Sell FROM Producers,
+ /* Sell and Receive_supply may be asynchronous */
+ <!> $receive: Receive_supply FROM Consumers
+DO ADD $sell PRECEDES $receive;
+ ADD $sell related_to $receive;
+OD;
+
+ENSURE FOREACH $request: Request_delivery,
+ $receive: Receive_supply
+ ( $request ^related_to $receive -> $request BEFORE $receive);
+
+/* preventing mismatched delivery */
+ENSURE
+ NOT EXISTS DISJ $c1: Consumer, $c2: Consumer
+ EXISTS $request: Request_delivery FROM $c1,
+ $receive: Receive_supply FROM $c2,
+ $order: Receive_order_and_buy FROM Supply_Office
+
+ ( $request ^related_to $order AND
+ $order ^related_to $receive );
+
+COORDINATE <!>$refusal1: Not_available FROM Producers,
+ $refusal2: Not_available FROM Consumers
+ DO SHARE $refusal1 $refusal2; OD;
+
+/* preventing mismatched refusals */
+ENSURE
+NOT EXISTS DISJ $c1: Consumer, $c2: Consumer
+ EXISTS $request: Request_delivery FROM $c1,
+ $receive: Not_available FROM $c2,
+ $order: Receive_order_and_buy FROM Supply_Office
+
+ ( $request ^related_to $order AND
+ $order ^related_to $receive );
+
+/**** add yet another relation for Supplier/Consumer ****/
+COORDINATE $c: Consumer
+ DO COORDINATE $p: Producer
+ DO
+ IF EXISTS $request: Request_delivery FROM $c,
+ $sell: Sell FROM $p
+ ( $request ^related_to $sell )
+ THEN ADD $p Is_supplier_for $c; FI;
+ OD;
+OD;
diff --git a/models/Legacy_examples/Example20_MP_model__reuse.mp b/models/Legacy_examples/Example20_MP_model__reuse.mp
new file mode 100644
index 0000000000000000000000000000000000000000..c09d654b8a85e7deac2951b79e8f5049c06ed9b2
--- /dev/null
+++ b/models/Legacy_examples/Example20_MP_model__reuse.mp
@@ -0,0 +1,89 @@
+SCHEMA Reuse_of_a_system
+
+/* Example 20.
+ Authentication system's behavior for reuse with MAP operation.
+
+ run for scope 3 or more to see attempts_exhausted event
+ you may hide the Requestor node in the event trace graph,
+ since the User will copy all Requestor's behavior
+
+============== reused MP code starts here ==================*/
+ROOT Data_Base: (* check_ID *);
+
+ROOT Authentication_Service:
+ request_ID
+ (* creds_invalid request_ID *)
+
+ ( creds_invalid
+ [ attempts_exhausted ]
+ cancel_access_request |
+
+ creds_valid
+ access_granted )
+
+BUILD{ /*--- constraints for this root ---*/
+ ENSURE #creds_invalid <= 3; /* no more than 3 attempts to get access */
+ ENSURE #attempts_exhausted == 1 <-> #creds_invalid == 3;
+ IF #attempts_exhausted > 0 THEN SAY(" attempts exhausted!");FI; }
+;
+
+request_ID: check_ID;
+
+Authentication_Service, Data_Base SHARE ALL check_ID;
+
+ROOT Requester:
+ request_access
+ provide_ID
+ (* creds_invalid request_access provide_ID *)
+
+ ( creds_valid
+ ( access_granted | abandon_access_request) |
+
+ creds_invalid
+ ( attempts_exhausted | abandon_access_request ) )
+;
+
+Requester, Authentication_Service SHARE ALL
+ creds_valid, creds_invalid,
+ attempts_exhausted, access_granted;
+
+COORDINATE $a: request_access FROM Requester,
+ $b: request_ID FROM Authentication_Service,
+ $c: provide_ID FROM Requester
+ DO ADD $a PRECEDES $b;
+ ADD $b PRECEDES $c;
+ OD;
+/*================= end of reused MP code =======================*/
+
+
+/*===============================================================*/
+/* new system, which will reuse authentication system's behavior */
+/*---------------------------------------------------------------*/
+ROOT User:
+
+ ( login_succeeds
+ ( work |
+ /* User may change their mind and cancel login */
+ cancel ) |
+
+ login_fails )
+;
+
+
+/*================================================================*/
+/* the following adjustments of the new model and the reused one
+ are needed to integrate their behaviors.
+
+ reuse of authentication system's behavior:
+ mapping actions of the Requestor from Authentication_Service
+ on actions of the User.
+ User will copy/reuse all activities of Requestor
+------------------------------------------------------------------*/
+/* Requester's behavior is included into the behavior of User */
+ MAP Requester ON User;
+
+/* synchronizing particular events from the authentication
+ system's behavior with events in the new system */
+COORDINATE $ready: access_granted FROM Requester,
+ $go: login_succeeds FROM User
+ DO ADD $ready PRECEDES $go; OD;
diff --git a/models/Legacy_examples/Example21_compiler1.mp b/models/Legacy_examples/Example21_compiler1.mp
new file mode 100644
index 0000000000000000000000000000000000000000..371f385233024744bdf39fae36ce112121a6f447
--- /dev/null
+++ b/models/Legacy_examples/Example21_compiler1.mp
@@ -0,0 +1,86 @@
+/* Example 21
+ Compiler front end,
+ bottom-up parser
+ Lexer and parser in batch mode
+
+run for
+scope 1, 2 traces, less than 1 sec.
+scope 2, 147 traces, approx. time 0.87 sec.
+scope 3, 11988 traces, approx. time 148 sec.
+====================================================*/
+
+SCHEMA compiler1
+
+ROOT Source_code: (* get_characters
+ unget_some_characters *)
+;
+
+/*----------- lexical analysis ----------------*/
+RegExpr_match: match_string
+ [ largest_successful_match
+ put_token ]
+;
+
+Token_recognition:
+ get_characters
+ {+ RegExpr_match +}
+ unget_some_characters
+BUILD{
+ /* only one RegExpr_match succeeds */
+ ENSURE #largest_successful_match == 1;
+};
+
+ROOT Lexer:
+ (+ Token_recognition +)
+;
+
+Source_code, Lexer SHARE ALL get_characters, unget_some_characters;
+
+/*--------- intermediate token list ----------*/
+ROOT Token_list:
+ (+ put_token +) (+ get_token +)
+BUILD{
+ ENSURE #put_token >= #get_token;
+};
+
+Token_list, Lexer SHARE ALL put_token;
+
+/* ----- bottom-up parsing -------------------*/
+Shift: Push
+ get_token
+;
+
+Reduce: (+<1..2> Pop +)
+/* to tame the combinatorial explosion for nested iterations */
+ Push
+;
+
+Shift_Reduce:
+ Push /* push the start non-terminal symbol */
+ get_token
+ (+ ( Shift |
+ Reduce Put_node )
+ +)
+
+ ( Reduce
+ Put_node
+ Parsing_complete |
+
+ Report_syntax_error )
+;
+
+Stack: (*<2 .. 2 * $$scope + 3 > (Push | Pop) *)
+ /* extended iteration to provide
+ sufficient numbers of Pop and Push events */
+BUILD{ ENSURE FOREACH $x: Pop
+ #Pop BEFORE $x < #Push BEFORE $x;
+};
+
+ROOT Parser: {Shift_Reduce, Stack}
+BUILD{ COORDINATE $s1: Shift_Reduce,
+ $s2: Stack
+ DO $s1, $s2 SHARE ALL Pop, Push; OD;
+};
+
+/*------ lexer and parser in the batch mode -------*/
+Token_list, Parser SHARE ALL get_token;
diff --git a/models/Legacy_examples/Example22_compiler2.mp b/models/Legacy_examples/Example22_compiler2.mp
new file mode 100644
index 0000000000000000000000000000000000000000..b18d9af47f41bf5a8b60a61f6f7e72744f52c7c3
--- /dev/null
+++ b/models/Legacy_examples/Example22_compiler2.mp
@@ -0,0 +1,80 @@
+/* Example 22
+ Compiler front end,
+ bottom-up parser
+ Lexer and parser in interaction mode
+
+run for
+scope 1, 2 traces, less than 1 sec.
+scope 2, 111 traces, approx. time 0.65 sec.
+scope 3, 4860 traces, approx. time 55 sec.
+====================================================*/
+
+SCHEMA compiler2
+
+ROOT Source_code: (* get_characters
+ unget_some_characters *)
+;
+
+/*----------- lexical analysis ----------------*/
+RegExpr_match: match_string
+ [ largest_successful_match
+ put_token ]
+;
+
+Token_recognition:
+ get_characters
+ {+ RegExpr_match +}
+ unget_some_characters
+BUILD{
+ /* only one RegExpr_match succeeds */
+ ENSURE #largest_successful_match == 1;
+};
+
+ROOT Lexer:
+ (+ Token_recognition +)
+;
+
+Source_code, Lexer SHARE ALL get_characters, unget_some_characters;
+
+/* ----- bottom-up parsing -------------------*/
+Shift: Push
+ get_token
+;
+
+Reduce: (+<1..2> Pop +)
+ /* to tame the combinatorial explosion for nested iterations */
+ Push
+;
+
+Shift_Reduce:
+ Push /* push the start non-terminal symbol */
+ get_token
+ (+ ( Shift |
+ Reduce
+ Put_node )
+ +)
+
+ ( Reduce
+ Put_node
+ Parsing_complete |
+
+ Report_syntax_error )
+;
+
+Stack: (*<2 .. 2 * $$scope + 3 > (Push | Pop) *)
+ /* extended iteration to provide
+ sufficient numbers of Pop and Push events */
+BUILD{ ENSURE FOREACH $x: Pop
+ #Pop BEFORE $x < #Push BEFORE $x;
+};
+
+ROOT Parser: {Shift_Reduce, Stack}
+BUILD{ COORDINATE $s1: Shift_Reduce,
+ $s2: Stack
+ DO $s1, $s2 SHARE ALL Pop, Push; OD;
+};
+
+/*------ lexer and parser in the interactive mode -------*/
+COORDINATE $produce_token: put_token FROM Lexer,
+ $consume_token: get_token FROM Parser
+ DO ADD $produce_token PRECEDES $consume_token; OD;
diff --git a/models/Legacy_examples/Example23_number_attributes.mp b/models/Legacy_examples/Example23_number_attributes.mp
new file mode 100644
index 0000000000000000000000000000000000000000..a0405536bb737d65c41b996e273fcf80c12c5037
--- /dev/null
+++ b/models/Legacy_examples/Example23_number_attributes.mp
@@ -0,0 +1,38 @@
+/* Example23.mp number attribute test */
+
+SCHEMA Shopping_spree
+
+ROOT Buyer: (*<0.. 2 * $$scope> Buy *);
+/* Increase the iteration to ensure enough Buy events to coordinate with both Shops */
+
+ATTRIBUTES{number price, total_cost;};
+
+ROOT Shop_A: (* (Sell_Item_1 | Sell_Item_2) *)
+/* Initializing attribute values in a context of composite event where these are used */
+BUILD{ COORDINATE $s: Sell_Item_1 DO $s.price:= 8; OD;
+ COORDINATE $s: Sell_Item_2 DO $s.price:= 20; OD;
+};
+
+ROOT Shop_B: (* (Sell_Item_2 | Sell_Item_3) *)
+
+/* In Shop_B the cost of Item_2 may be different */
+BUILD{ COORDINATE $s: Sell_Item_2 DO $s.price:= 22; OD;
+ COORDINATE $s: Sell_Item_3 DO $s.price:= 30; OD;
+};
+
+/* Schema’s attribute total_cost is automatically initialized by 0.0.
+ Absence of event reference means THIS by default */
+COORDINATE $sell: (Sell_Item_1 | Sell_Item_2 | Sell_Item_3),
+ $buy: Buy
+ DO /* to render the dependency between sell and buy events */
+ ADD $buy PRECEDES $sell;
+ OD;
+
+/* example of pre-defined attribute use */
+SAY(" Trace #" trace_id);
+
+/* use of aggregate operation to calculate total_cost as an attribute of the whole schema */
+total_cost := SUM{ $item: (Sell_Item_1 | Sell_Item_2 | Sell_Item_3) APPLY $item.price};
+
+SAY("Bought " #Buy " items. Total purchase cost is: " total_cost
+ " average cost: " total_cost/#Buy);
diff --git a/models/Legacy_examples/Example24_Bayesian_probability.mp b/models/Legacy_examples/Example24_Bayesian_probability.mp
new file mode 100644
index 0000000000000000000000000000000000000000..5353b1d802c4978317ec5897dec3712014df0a71
--- /dev/null
+++ b/models/Legacy_examples/Example24_Bayesian_probability.mp
@@ -0,0 +1,82 @@
+/* Example24.mp Bayesian attribute example
+
+ Suppose there are 3 red and 2 green balls in a box.
+ We pick at random three balls, one at a time.
+ The result of the process can be denoted as RRR, RRG, or RGG,
+ representing sets of selected balls.
+
+ The following MP schema demonstrates how to obtain all valid traces
+ and to calculate probabilities for the results.
+ Bar chart in GLOBAL section summarizes the probabilities of all outcomes.
+
+ Please notice that the trace Type 1 probability is calculated as 1/7 ~ 0.142857,
+ since Type 1 assumes that probability of selecting an alternative is
+ constant for the whole derivation process.
+
+ run for scope 1
+*/
+SCHEMA RedGreen
+
+ATTRIBUTES{ number selection_probability,
+ RRR_probability,
+ RRG_probability,
+ RGG_probability; };
+
+ROOT Selection:
+ /* there are precisely three ball selections */
+ (+ <3> ( Select_Red | Select_Green ) +)
+
+ /* possible selection configurations */
+ ( RRR | RRG | RGG )
+;
+
+/* Constraints to shape the valid traces */
+ENSURE (#RRR == 1 <-> #Select_Red == 3) AND
+ (#RRG == 1 <-> #Select_Red == 2) AND
+ (#RGG == 1 <-> #Select_Red == 1);
+
+/* Attribute calculations are done here */
+COORDINATE $res: ( RRR | RRG | RGG )
+DO
+ /* prepare for further calculations */
+ selection_probability:= 1;
+
+ COORDINATE $s: ( Select_Red | Select_Green )
+ DO
+ /* Probability of the result depends on the ball selection order */
+ IF $s IS Select_Red THEN
+ /* probability to select Red ball is:
+ (number of Red balls available / total number of available balls) */
+ selection_probability *:=
+ (3 - #Select_Red BEFORE $s)/(5 - #( Select_Red | Select_Green ) BEFORE $s);
+ ELSE
+ /* probability to select Green ball */
+ selection_probability *:=
+ (2 - #Select_Green BEFORE $s)/(5 - #( Select_Red | Select_Green ) BEFORE $s);
+ FI;
+ OD;
+
+ /* Report the results */
+ SAY( "Probability of result " $res " was " selection_probability);
+OD;
+
+ IF #Select_Red == 1 THEN GLOBAL.RGG_probability +:= selection_probability; FI;
+ IF #Select_Red == 2 THEN GLOBAL.RRG_probability +:= selection_probability; FI;
+ IF #Select_Red == 3 THEN GLOBAL.RRR_probability +:= selection_probability; FI;
+
+GLOBAL
+TABLE t1{
+ TABS string s1, number n1;
+ };
+
+/* fill the Table with probabilities collected in GLOBAL attributes */
+t1 <| s1: SAY("RRR"), n1: RRR_probability;
+t1 <| s1: SAY("RRG"), n1: RRG_probability;
+t1 <| s1: SAY("RGG"), n1: RGG_probability;
+
+
+BAR CHART b{ TITLE ("Total outcome probabilities in all " #$$TRACE " traces");
+ FROM t1; X_AXIS s1;
+ };
+
+SHOW b;
diff --git a/models/Legacy_examples/Example25_interval_attributes.mp b/models/Legacy_examples/Example25_interval_attributes.mp
new file mode 100644
index 0000000000000000000000000000000000000000..cfef3eb3d82e9c64579cae0d7288b7571e4e0aa5
--- /dev/null
+++ b/models/Legacy_examples/Example25_interval_attributes.mp
@@ -0,0 +1,28 @@
+/* Example 25, Use of interval attributes.
+ The task is to load a backpack with items not exceeding
+ the total weight of 30 units.
+ There may be several instances of the same item.
+
+ run for scopes 1 and up
+==========================================================*/
+SCHEMA backpack
+
+ATTRIBUTES{ interval weight; };
+
+/* Composite event is used to define attribute value for
+ all instances of a particular event */
+item1: BUILD{ weight := [2..5];};
+item2: BUILD{ weight := [10..16];};
+
+ROOT Backpack: (+ (item1 | item2) +)
+BUILD{
+ COORDINATE $item: (item1 | item2)
+ DO SAY("selected " $item " with weight " $item.weight);
+ /* interval weight is initialized by [0..0] */
+ weight +:= $item.weight;
+ OD;
+ /* ensure that the backpack's weight does not exceed maximum */
+ ENSURE weight > 0 AND weight <= 30; };
+
+SAY("selected " #(item1 | item2) " items");
+SAY("backpack weight is within interval " Backpack.weight);
diff --git a/models/Legacy_examples/Example26_timing_attributes.mp b/models/Legacy_examples/Example26_timing_attributes.mp
new file mode 100644
index 0000000000000000000000000000000000000000..65df381f75de10949a8bd56f80d22c734145cab4
--- /dev/null
+++ b/models/Legacy_examples/Example26_timing_attributes.mp
@@ -0,0 +1,42 @@
+/* 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
+*/
+SCHEMA Delays
+
+Work:
+BUILD{
+ SET duration AT LEAST 1;
+ /* The new default value for the Work event duration
+ attribute is set as an interval [1..1] */
+};
+
+
+Visitor:
+ /* set new default duration for Visitor */
+BUILD{ SET duration AT LEAST [2..3]; };
+
+Get_distracted: (+ Visitor +) ;
+
+ROOT Worker: (+ ( Work | Get_distracted) +);
+
+ATTRIBUTES{ interval total_delay; };
+/* delay is THIS.delay, or attribute of the whole schema event,
+ and is used to hold specific data extracted from the trace */
+
+COORDINATE $distraction: Get_distracted
+ DO total_delay +:= $distraction.duration; OD;
+
+/* show all events present in the trace with timing attributes,
+ preserving the order of derivation, top-down, left-to-right */
+COORDINATE $x: $$EVENT
+ DO SAY(" " $x " start " $x.start
+ " duration " $x.duration
+ " end " $x.end);
+ OD;
+
+SAY(" Delay created by " #Visitor " visitors is " total_delay);
diff --git a/models/Legacy_examples/Example27_Railroad_Crossing.mp b/models/Legacy_examples/Example27_Railroad_Crossing.mp
new file mode 100644
index 0000000000000000000000000000000000000000..c6c9332e8e18764433ef3a5a683e02a1988d8e57
--- /dev/null
+++ b/models/Legacy_examples/Example27_Railroad_Crossing.mp
@@ -0,0 +1,71 @@
+/*
+Example 27. Timing attribute use.
+
+Railroad crossing example from [Formal Methods for Real-Time Computing, 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.
+
+*/
+
+SCHEMA Railroad_Crossing
+
+ROOT Train:
+ (+
+ Enter_Restricted_Region
+ Goes_through_Restricted_Region
+ Enter_Crossing_Region
+ Goes_through_Crossing_Region
+ Leaves_Crossing_Region
+ +) ;
+
+ROOT Crossing:
+ (+
+ Move_Down
+ Down
+ Move_Up
+ Up
+ +) ;
+
+/* Set values for duration attributes */
+/*================================================*/
+Goes_through_Crossing_Region: BUILD{ SET duration AT LEAST 10; };
+
+Move_Down: BUILD{ SET duration AT LEAST 5; };
+
+Move_Up: BUILD{ SET duration AT LEAST 2; };
+
+COORDINATE $enter: Enter_Restricted_Region FROM Train,
+ $down: Move_Down FROM Crossing
+ DO ADD $enter PRECEDES $down; OD;
+
+COORDINATE $enter: Enter_Crossing_Region FROM Train,
+ $down: Down FROM Crossing
+ DO ADD $down PRECEDES $enter; OD;
+
+COORDINATE $leaves: Leaves_Crossing_Region FROM Train,
+ $up: Move_Up FROM Crossing
+ DO ADD $leaves PRECEDES $up; OD;
+
+/* The main safety condition */
+CHECK FOREACH $enter: Goes_through_Crossing_Region FROM Train
+ NOT EXISTS $up: Up FROM Crossing
+ MAY_OVERLAP $enter $up
+ ONFAIL SAY("Crossing is open when train is passing through!");
+
+COORDINATE
+ $goes_through: Goes_through_Crossing_Region FROM Train,
+ $down: Down FROM Crossing,
+ $bar_is_up: Move_Up FROM Crossing
+DO
+ SAY("Bar moved down by " $down.end );
+ SAY("Train starts go through crossing at " $goes_through.start);
+ SAY("Train ends go through crossing at " $goes_through.end);
+ SAY("Bar starts go up at " $bar_is_up.start);
+ IF $goes_through.start < $down.end THEN
+ SAY("Not enough time to close crossing");
+ ELSE SAY("Crossing was successfully closed");
+ FI;
+OD;
diff --git a/models/Legacy_examples/Example28_MP_model_of_MP_architecture.mp b/models/Legacy_examples/Example28_MP_model_of_MP_architecture.mp
new file mode 100644
index 0000000000000000000000000000000000000000..36264184995df0d7cc631065432f261384f703c3
--- /dev/null
+++ b/models/Legacy_examples/Example28_MP_model_of_MP_architecture.mp
@@ -0,0 +1,148 @@
+/* Example 28
+ MP compiler/trace generator architecture model
+
+ run for scope 1 or more
+
+===================================================*/
+SCHEMA MP_architecture
+
+ROOT User:
+ (+ [ load_MP_file ]
+ ( MP_model_editing | browsing_MP_code )
+ press_RUN_button
+ ( browse_event_trace |
+ syntax_errors_detected )
+ [ save_MP_file ]
+ +)
+ end_of_session
+;
+/*--------------------------------------------------*/
+
+ROOT MP_code_editor:
+ (+
+ ( MP_model_editing |
+ browsing_MP_code )
+ +)
+;
+
+User, MP_code_editor SHARE ALL MP_model_editing, browsing_MP_code;
+
+/*--------------------------------------------------*/
+
+ROOT MP_GUI:
+ (+ [ load_MP_file ]
+ press_RUN_button
+ input_MP_code
+ /* trace visualization happens only if there are no syntax errors,
+ and trace generator has been called */
+ ( receive_json_file
+ visualize_trace |
+
+ syntax_errors_detected )
+ [ save_MP_file ]
+ +)
+;
+
+User, MP_GUI SHARE ALL load_MP_file, save_MP_file,
+ press_RUN_button;
+
+COORDINATE $v: visualize_trace,
+ $b: browse_event_trace
+ DO ADD $v PRECEDES $b; OD;
+
+/*--------------------------------------------------*/
+
+ROOT MP_parser:
+ (+ input_MP_code
+ perform_syntax_analysis
+ ( write_abstract_syntax_tree |
+ syntax_errors_detected )
+ +)
+;
+
+MP_parser, MP_GUI SHARE ALL input_MP_code;
+
+User, MP_parser, MP_GUI SHARE ALL syntax_errors_detected;
+
+COORDINATE $p: press_RUN_button,
+ $r: input_MP_code
+ DO ADD $p PRECEDES $r; OD;
+/*--------------------------------------------------*/
+
+ROOT Abstract_syntax_tree:
+ (* write_abstract_syntax_tree
+ read_abstract_syntax_tree
+ *);
+
+MP_parser, Abstract_syntax_tree SHARE ALL write_abstract_syntax_tree;
+/*--------------------------------------------------*/
+
+ROOT Trace_generator:
+ (* read_abstract_syntax_tree
+ generate_Cpp_file
+ run_Cpp_compiler
+ run_executable
+ produce_json_file
+ *);
+
+Abstract_syntax_tree, Trace_generator SHARE ALL read_abstract_syntax_tree;
+
+COORDINATE $p: produce_json_file,
+ $r: receive_json_file
+ DO ADD $p PRECEDES $r; OD;
+/*--------------------------------------------------*/
+
+/* trace annotations */
+SAY(" Scope " $$scope " Trace #" trace_id );
+
+/*================================================================
+ Processing event trace to find dependencies between components.
+ Produces a UML-like Component Diagram. This code is reusable,
+ and can be copied/pasted into any other MP model.
+ See Sec. 5.3 in MP v.4 Manual
+ ================================================================*/
+GRAPH Diagram { TITLE ("main component interactions");};
+
+ COORDINATE $E1: ($$ROOT | $$COMPOSITE) DO
+ COORDINATE $E2: ($$ROOT | $$COMPOSITE) DO
+ WITHIN Diagram{
+ /* For each valid event trace find all root and composite
+ event instances within the event trace and add them to the graph. */
+ Node$a: LAST ($E1);
+ Node$b: LAST ($E2);
+ /* LAST option in the node constructors ensures
+ there will be only a single instance of a node
+ in the graph for each root and composite event
+ found in the event trace */
+
+ /* If event E1 is IN another event E2, add an arrow “E2 calls E1†*/
+ IF $E1 IN $E2 THEN
+ ADD Node$b ARROW("calls") Node$a;
+ FI;
+
+ /* We look for interactions between components and data structures.
+
+ Interactions between components, usually are represented by coordination of
+ events in the interacting components (presence of PRECEDES between events
+ in different threads).
+
+ Interactions between components and data structures are modeled by shared events,
+ since data structures are usually modeled as a set of operations performed on them. */
+
+ IF $E1 != $E2 AND
+ NOT ($E1 IN $E2 OR $E2 IN $E1) AND
+ ( ( EXISTS $E3: $$EVENT ($E3 IN $E1 AND $E3 IN $E2) ) OR
+
+ ( EXISTS $E3: $$EVENT FROM $E1,
+ $E4: $$EVENT FROM $E2 ($E3 PRECEDES $E4) ) ) THEN
+ ADD Node$a LINE("interacts with") Node$b;
+ FI;
+ }; /* end WITHIN Diagram */
+ OD;
+ OD; /* end of $E1 and $E2 loops */
+
+GLOBAL
+/* When trace derivation is completed, data from the traces has been accumulated in
+ the graph and is ready to be shown */
+SHOW Diagram;
+
diff --git a/models/Legacy_examples/Example29_stack1_Bayesian_probability.mp b/models/Legacy_examples/Example29_stack1_Bayesian_probability.mp
new file mode 100644
index 0000000000000000000000000000000000000000..b0fc26dbd9263b07ec7b73467da1566e9f259b92
--- /dev/null
+++ b/models/Legacy_examples/Example29_stack1_Bayesian_probability.mp
@@ -0,0 +1,95 @@
+/* Example 29
+
+ An example of Bayesian probability calculation.
+
+ run for scopes 1, 2, 3, and up.
+
+ This example illustrates the main parts in probabilistic MP model construction:
+
+ 1) selection of the search space - the finite number of event instances,
+ including the event trace, which is an event by itself.
+ 2) Rules for event attribute p2 calculation.
+ 3) The p2 attribute represents the probability for a particular event
+ instance (including the trace) to appear on the MP output.
+
+ When run on Firebird, the output also shows Type 1 trace probability
+ (p=nnnn on the right scroll bar),
+ which will be different from the calculated Type 2 values.
+
+ Note. For this simple example it is possible to run more than 5 iterations
+ of push/pop (beyond the max standard scope of 5) by using the explicit iteration option,
+ where M is the desired number of iterations.
+
+ ROOT Stack: (*<0..M> ( <<0.75>> push | <<0.25>> pop ) *)
+ this will require to update the first step in p2 assignment (line 57)
+ it will become p2 := 1/(M + 1);
+==================================================================*/
+
+SCHEMA stack1
+
+ROOT Stack: (* ( <<0.75>> push | <<0.25>> pop ) *)
+ /* probabilities for alternatives are here to enable also
+ the default Type 1 trace probability calculation, in order
+ to compare it with the Bayesian */
+ BUILD {
+ /* if an element is retrieved, it should have been stored before */
+ ENSURE FOREACH $x: pop FROM Stack
+ ( #pop BEFORE $x < #push BEFORE $x );
+ }
+;/* end BUILD for Stack */
+
+/*==============================================================*/
+/* here starts the part of model responsible for Bayesian logic */
+/*==============================================================*/
+ATTRIBUTES{ number p2;};
+/* the attribute p2 represents a probability of event
+ to be included in the current trace.
+ Since the whole trace also is an event,
+ attribute p2 for it specifies the trace probability -
+ the target of all this example */
+
+/* first, let's bring the probability to select the number of iterations.
+ For scope $$scope there may be 0, 1, 2, ... $$scope iterations.
+ Total ($$scope + 1) choices.
+ Hence: assuming that each choice has equal probability 1/($$scope + 1)
+ stand alone p2 is attribute of the whole event trace */
+
+ p2:= 1/($$scope + 1);
+/* here the default is THIS.p2 := 1/($$scope + 1);
+ p2 is an attribute of the whole trace.
+ The interpretation: "the probability of getting the trace segment so far" */
+
+/* by now the valid trace has been derived
+ and we can proceed with decorating its events with attribute values.
+ COORDINATE traverses its thread in order of derivation (the default) */
+COORDINATE $e: (pop | push)
+DO
+ IF #pop BEFORE $e == #push BEFORE $e THEN
+ /* if the condition above holds, the choice of event $e
+ is unambiguous: it should be 'push',
+ and its probability is the same as for the previous event */
+ ELSE
+ /* otherwise we have to choose one of the pop/push
+ with corresponding probability.
+ Notice that the option #pop BEFORE $e > #push BEFORE $e has been eliminated
+ by ENSURE filter during the valid trace derivation */
+ IF $e IS pop THEN p2 *:= 0.25;
+ ELSE p2 *:= 0.75; /* for 'push' */
+ FI;
+ FI;
+
+ /* Now we can set the probability for $e,
+ this is done for the purpose to show the sequence of pop/push later.
+ This $e.p2 attribute is not actually needed in order
+ to calculate p2 for the trace */
+ $e.p2 := p2;
+OD;
+
+/*=================================================*/
+/* for debugging purposes let's show the sequence
+ of pop/push with their probabilities in order of derivation */
+COORDINATE $x: (pop | push)
+ DO SAY($x " with probability " $x.p2); OD;
+
+/**** final report ****/
+SAY("Trace " trace_id " for scope " $$scope " has probability " p2);
diff --git a/models/Legacy_examples/Example30_Local_Report.mp b/models/Legacy_examples/Example30_Local_Report.mp
new file mode 100644
index 0000000000000000000000000000000000000000..0271dd2c88233d5fb169237fedbaa2204edc6ee4
--- /dev/null
+++ b/models/Legacy_examples/Example30_Local_Report.mp
@@ -0,0 +1,29 @@
+
+/* Example 30. Local Report within a trace.
+ run for scope 1 and up.
+*/
+SCHEMA Data_flow
+
+ROOT Writer: (* ( working | writing ) *);
+
+ROOT File: (+ writing +) (* reading *);
+Writer, File SHARE ALL writing;
+
+ROOT Reader: (* ( reading | working ) *);
+Reader, File SHARE ALL reading;
+
+REPORT basic_statistics {
+ TITLE ("scope= " $$scope " trace " trace_id);};
+
+/* Clear the contents after a trace derivation has been completed */
+CLEAR basic_statistics;
+
+/* fill the Report with data from the current event trace */
+SAY("#writing= " #writing) => basic_statistics;
+SAY("#reading= " #reading) => basic_statistics;
+SAY("#working= " #working) => basic_statistics;
+
+
+/* In order to make it visible together with the event trace, the SHOW command is needed */
+SHOW basic_statistics;
+
diff --git a/models/Legacy_examples/Example31_Global_report.mp b/models/Legacy_examples/Example31_Global_report.mp
new file mode 100644
index 0000000000000000000000000000000000000000..ad102ee91a6a0220854021bff9da9e385119ee92
--- /dev/null
+++ b/models/Legacy_examples/Example31_Global_report.mp
@@ -0,0 +1,31 @@
+/* Example 31. Global report.
+ run for scope 1 and up
+-----------------------------*/
+SCHEMA simple_message_flow
+
+ROOT Sender: (* send *);
+
+ROOT Receiver: (* (receive | does_not_receive) *);
+
+COORDINATE $x: send FROM Sender,
+ $y: (receive | does_not_receive) FROM Receiver
+ DO ADD $x PRECEDES $y; OD;
+
+REPORT statistics { TITLE ("scope= " $$scope);};
+
+/* for each valid trace add report records */
+IF #does_not_receive > 0 THEN
+ SAY( "trace " trace_id " sent " #send
+ " received " #receive
+ " ratio " #receive/#send ) => statistics;
+FI;
+/* Since no CLEAR operation is present, the contents of Report is preserved
+ and augmented for each valid event trace */
+
+GLOBAL
+
+SAY( "total traces " #$$TRACE) => statistics;
+/* Global expression #$$TRACE provides number of valid event traces derived
+ for the current scope */
+
+SHOW statistics;
diff --git a/models/Legacy_examples/Example32_Local_graph.mp b/models/Legacy_examples/Example32_Local_graph.mp
new file mode 100644
index 0000000000000000000000000000000000000000..625c9e85a465c6f0d4788fc17751d37aa2da2ccb
--- /dev/null
+++ b/models/Legacy_examples/Example32_Local_graph.mp
@@ -0,0 +1,67 @@
+/* Example 32. Local graph within the event trace.
+ run for scope 1 and up
+------------------------------------------------*/
+SCHEMA Car_Race
+
+Car: Start
+ (* drive_lap *)
+ ( finish [ winner ] | break);
+
+ROOT Cars: {+ Car +}
+ BUILD{
+ /* everybody who finishes drives the same number of laps */
+ ENSURE FOREACH DISJ $c1: Car, $c2: Car
+ (#finish FROM $c1 == 1 AND #finish FROM $c2 == 1 ->
+ #drive_lap FROM $c1 == #drive_lap FROM $c2) AND
+ /* if it breaks, then earlier */
+ (#finish FROM $c1 == 1 AND #break FROM $c2 == 1 ->
+ #drive_lap FROM $c1 >= #drive_lap FROM $c2);
+
+ /* there always will be at most one winner */
+ ENSURE #winner <= 1;
+
+ /* if at least one car finishes, there should be a winner */
+ENSURE #finish > 0 -> #winner > 0; };
+
+
+ROOT Judge: provide_start_signal
+ watch
+ (* finish *);
+
+COORDINATE $a: provide_start_signal FROM Judge
+ DO COORDINATE $b: Start FROM Cars
+ DO ADD $a PRECEDES $b; OD;
+ OD;
+Cars, Judge SHARE ALL finish;
+
+COORDINATE $w: winner
+ DO ENSURE #finish BEFORE $w == 1; OD;
+
+/* =======================================================
+ Here starts the trace view graph construction.
+ Operations are performed after a valid event trace has been
+ successfully derived.
+=========================================================*/
+GRAPH Winner_trace {
+ TITLE( "winner trace " trace_id " for scope " $$scope);};
+
+/* We want to render a graph extracted from each valid event trace,
+so the graph is cleared before the trace processing starts. */
+
+ COORDINATE $car_event: Car SUCH THAT #winner FROM $car_event > 0
+ DO
+
+/* the following WITHIN command provides a context for performing
+ operations on the Winner_trace graph */
+WITHIN Winner_trace{
+ Node$laps: NEW(#drive_lap FROM $car_event " laps");
+ ADD NEW("Start") ARROW("followed by") Node$laps;
+ ADD Node$laps ARROW("followed by") NEW("finish");
+ ADD LAST("finish") ARROW("followed by") NEW("winner");
+}; /* end of WITHIN Winner_trace body */
+
+ OD; /* end of Car loop */
+
+SHOW Winner_trace;
+CLEAR Winner_trace ;
+
diff --git a/models/Legacy_examples/Example33_Component_Diagram.mp b/models/Legacy_examples/Example33_Component_Diagram.mp
new file mode 100644
index 0000000000000000000000000000000000000000..5c1236ec9fc52bff59c61e00fa75594f76fedc25
--- /dev/null
+++ b/models/Legacy_examples/Example33_Component_Diagram.mp
@@ -0,0 +1,132 @@
+/* Example 33
+ Compiler front end, bottom-up parser
+ Lexer and parser in interactive mode.
+
+ Example of UML-like Component Diagram extracted
+ from the set of valid event traces
+ The MP code for constructing UML-like Component Diagram
+ is reusable and can be copied/pasted into any MP model.
+
+ run for
+ scope 1, 20 traces, approx. 5 sec.
+
+====================================================*/
+SCHEMA compiler_example
+
+ROOT Source_code: (+<1.. $$scope + 1>
+ get_characters
+ unget_some_characters +)
+;
+
+/*============= lexical analysis ===============*/
+RegExpr_match: match_string
+ [ put_token ]
+;
+
+Token_recognition:
+ get_characters
+ {+ RegExpr_match +}
+ unget_some_characters
+BUILD{
+ /* only one RegExpr_match succeeds */
+ ENSURE #put_token == 1;
+};
+
+ROOT Lexer: (+<1..2 * $$scope> Token_recognition +) ;
+
+Source_code, Lexer SHARE ALL get_characters, unget_some_characters;
+
+/*================ bottom-up parsing ===============*/
+Shift: Push
+ get_token
+;
+
+Reduce: (*<0..3> Pop *)
+ /* <0..3> is needed to tame the combinatorial explosion for nested iterations */
+ Push
+;
+
+ROOT Parser:
+ Push /* push the start non-terminal symbol */
+
+ /* Shift_Reduce */
+ (+<1..$$scope + 1>
+ get_token
+ [ Shift ]
+ Reduce
+ [ Put_node]
+ +)
+ ( Parsing_complete |
+ Report_syntax_error )
+;
+
+/*--- lexer and parser in the interactive mode ---*/
+COORDINATE $produce_token: put_token FROM Lexer,
+ $consume_token: get_token FROM Parser
+ DO ADD $produce_token PRECEDES $consume_token; OD;
+
+/*==================================================*/
+ROOT Stack: (*<2 .. 2 * $$scope + 1 > (Push | Pop) *)
+ /* extended iteration to provide
+ sufficient number of Pop and Push events */
+BUILD{ ENSURE FOREACH $x: Pop
+ #Pop BEFORE $x < #Push BEFORE $x; }
+;
+
+Parser, Stack SHARE ALL Pop, Push;
+
+/*==================================================*/
+ROOT Abstract_syntax_tree: (*<0..2 * $$scope> Put_node *);
+
+Parser, Abstract_syntax_tree SHARE ALL Put_node;
+
+/*================================================================
+ Processing event trace to find dependencies between components.
+ Produces a UML-like Component Diagram. This code is reusable,
+ and can be copied/pasted into any other MP model.
+ ================================================================*/
+GRAPH Diagram { TITLE ("main component interactions");};
+
+ COORDINATE $E1: ($$ROOT | $$COMPOSITE) DO
+ COORDINATE $E2: ($$ROOT | $$COMPOSITE) DO
+ WITHIN Diagram{
+ /* For each valid event trace find all root and composite
+ event instances within the event trace and add them to the graph. */
+ Node$a: LAST ($E1);
+ Node$b: LAST ($E2);
+ /* LAST option in the node constructors ensures
+ there will be only a single instance of a node
+ in the graph for each root and composite event
+ found in the event trace */
+
+ /* If event E1 is IN another event E2, add an arrow “E2 calls E1†*/
+ IF $E1 IN $E2 THEN
+ ADD Node$b ARROW("calls") Node$a;
+ FI;
+
+ /* We look for interactions between components and data structures.
+
+ Interactions between components, usually are represented by coordination of
+ events in the interacting components (presence of PRECEDES between events
+ in different threads).
+
+ Interactions between components and data structures are modeled by shared events,
+ since data structures are usually modeled as a set of operations performed on them. */
+
+ IF $E1 != $E2 AND
+ NOT ($E1 IN $E2 OR $E2 IN $E1) AND
+ ( ( EXISTS $E3: $$EVENT ($E3 IN $E1 AND $E3 IN $E2) ) OR
+
+ ( EXISTS $E3: $$EVENT FROM $E1,
+ $E4: $$EVENT FROM $E2 ($E3 PRECEDES $E4) ) ) THEN
+ ADD Node$a LINE("interacts with") Node$b;
+ FI;
+ }; /* end WITHIN Diagram */
+ OD;
+ OD; /* end of $E1 and $E2 loops */
+
+GLOBAL
+/* When trace derivation is completed, data from the traces has been accumulated in
+ the graph and is ready to be shown */
+SHOW Diagram;
+
diff --git a/models/Legacy_examples/Example34_Graph_as_data_structure.mp b/models/Legacy_examples/Example34_Graph_as_data_structure.mp
new file mode 100644
index 0000000000000000000000000000000000000000..873759c781757149f84a0b2642b20dc4adcd44b8
--- /dev/null
+++ b/models/Legacy_examples/Example34_Graph_as_data_structure.mp
@@ -0,0 +1,50 @@
+/* Example 34.
+ Accumulating and rendering statistics from event traces.
+ Graphs as container data structures
+============================================================*/
+SCHEMA Statistics
+ROOT A: (* ( a | b) *);
+ROOT B: (+ c +);
+
+GRAPH Stat{ TITLE("Total event count as graph for scope " $$scope);};
+
+ATTRIBUTES { number count;};
+
+COORDINATE $x: $$EVENT DO
+ WITHIN Stat{
+ Node$e: LAST ($x); /* creates new node with label $x if needed,
+ or finds the existing one */
+ Node$e.count +:= 1;
+ /* add more data to the node */
+ ADD Node$e ARROW("in trace") LAST("trace " trace_id);
+ };
+OD;
+
+GLOBAL
+/* Render the accumulated statistics as Report.
+ The Stat graph is used as a data structure. */
+REPORT Total_event_statistics{ TITLE("Total event count as Report"); };
+
+ WITHIN Stat{
+ FOR Node$a DO
+ IF Node$a.count > 0 THEN
+ /* Nodes with “trace†labels have count attribute 0.
+ Create and connect new node with the total count to each event node */
+ ADD Node$a ARROW("total count") NEW (Node$a.count);
+ /* graph loop works only with the initial graph contents,
+ new nodes added within the loop body
+ don’t participate in the iterations.
+ That prevents from infinite looping. */
+
+ /* Add to the Report as well.
+ Use the graph as a source of accumulated data. */
+ SAY(Node$a " event count: " Node$a.count)
+ => Total_event_statistics;
+ FI;
+ OD; /* end FOR */
+ }; /* end WITHIN */
+
+ /* render statistics as a graph */
+ SHOW Stat;
+ /* show the Report */
+ SHOW Total_event_statistics;
diff --git a/models/Legacy_examples/Example35_Finite_State_Diagram.mp b/models/Legacy_examples/Example35_Finite_State_Diagram.mp
new file mode 100644
index 0000000000000000000000000000000000000000..ff0ca8160c4696f5154ba4491eac0ad2b88b95d3
--- /dev/null
+++ b/models/Legacy_examples/Example35_Finite_State_Diagram.mp
@@ -0,0 +1,97 @@
+/* Example 35.
+
+ Adding path and state transition diagrams to
+ the Finite Automaton behavior model.
+
+ run for scope 2
+==========================================================*/
+SCHEMA Finite_State_Diagram_with_path
+
+ROOT S1_behavior:
+ Start Start_to_S1 S1
+ (* (S1_to_S3 | S1_to_S4) S2_to_S1 S1 *)
+ (S1_to_S3 | S1_to_S4);
+Start_to_S1: empty;
+S1_to_S3: a;
+S1_to_S4: (a | b);
+
+ROOT S2_behavior:
+ (* S4_to_S2 S2 S2_to_S1 *)
+ S4_to_S2 S2
+ S2_to_End End;
+S2_to_S1: b;
+S2_to_End: empty;
+
+S1_behavior, S2_behavior SHARE ALL S2_to_S1;
+
+ROOT S3_behavior:
+ (* S1_to_S3 S3
+ (* S3_to_S3 S3 *)
+ S3_to_S4 *);
+S3_to_S3: a;
+S3_to_S4: b;
+
+S3_behavior, S1_behavior SHARE ALL S1_to_S3;
+
+ROOT S4_behavior:
+ (* (S1_to_S4 | S3_to_S4) S4
+ S4_to_S2 *);
+S4_to_S2: a;
+
+S4_behavior, S1_behavior SHARE ALL S1_to_S4;
+S4_behavior, S2_behavior SHARE ALL S4_to_S2;
+S4_behavior, S3_behavior SHARE ALL S3_to_S4;
+
+GRAPH Path { TITLE("Path for the event trace"); };
+/* The following coordination extracts all triples State-Symbol-State
+ from the trace and accumulates corresponding nodes/transitions
+ in the Path graph. */
+
+CLEAR Path; /* Path graph is cleared before a new event trace derivation begins. */
+
+WITHIN Path{
+ COORDINATE
+ /* SORT (plain synchronous coordination) performs topological sort
+ on the selected event set with respect to the transitive closure of
+ PRECEDES (BEFORE relation), and the coordination will follow this ordering.
+ If A BEFORE B holds for events A and B, event A will appear in the sorted
+ sequence before B. This way pairs of states and transitions between them
+ are synchronized. */
+ <SORT> $state1: (Start | S1 | S2 | S3 | S4),
+ <SORT> $symbol: (a | b | empty),
+ <SORT> $state2: (S1 | S2 | S3 | S4 | End)
+
+ DO
+ Node$s1: LAST ($state1);
+ /* Assigns to the node variable Node$s1 the last instance of node
+ with the event name stored in $state1 in this graph, or creates a new node,
+ if such instance does not yet exist */
+ Node$s2: NEW ($state2);
+ /* Creates a new instance of node with name $state2. As a result,
+ nodes with the same label (representing the same state in the diagram)
+ may appear repeatedly in the Path graph. */
+ ADD Node$s1 ARROW($symbol) Node$s2;
+ OD;
+
+ /* show Path graph for each event trace */
+ SHOW Path;
+}; /* end WITHIN Path */
+
+GRAPH Diagram { TITLE("State transition diagram"); };
+
+WITHIN Diagram{
+ /* The following coordination extracts all triples State-Symbol-State from
+ the trace and accumulates corresponding nodes/transitions in the graph */
+ COORDINATE
+ <SORT> $state1: (Start | S1 | S2 | S3 | S4),
+ <SORT> $symbol: (a | b | empty),
+ <SORT> $state2: (S1 | S2 | S3 | S4 | End)
+ DO
+ ADD LAST ($state1) ARROW($symbol) LAST ($state2);
+ /* this time nodes with the same label will be unique */
+ OD;
+}; /* end WITHIN Diagram */
+
+GLOBAL
+/* After all valid traces have been derived, show the accumulated diagram */
+SHOW Diagram;
diff --git a/models/Legacy_examples/Example36_Statechart.mp b/models/Legacy_examples/Example36_Statechart.mp
new file mode 100644
index 0000000000000000000000000000000000000000..f41f30f641c63d9521dfe27e34c1781395d4d882
--- /dev/null
+++ b/models/Legacy_examples/Example36_Statechart.mp
@@ -0,0 +1,83 @@
+/* Example 36.
+
+ Extracting Statechart view from MP model.
+
+ run for scope 1 and up
+==========================================================*/
+SCHEMA ATM_withdrawal_with_Statechart_view
+
+ROOT Customer: (* insert_card
+ ( identification_succeeds
+ request_withdrawal
+ (get_money | not_sufficient_funds) |
+
+ identification_fails )
+ retrieve_card
+ *);
+
+ROOT ATM_system: (* Idle
+ read_card
+ validate_id
+ ( id_successful
+ check_balance
+ ( sufficient_balance
+ dispense_money |
+ unsufficient_balance ) |
+
+ id_failed )
+ *)
+ Idle;
+
+ROOT Data_Base: (* validate_id [ check_balance ] *);
+
+/* Interactions */
+Data_Base, ATM_system SHARE ALL validate_id, check_balance;
+
+COORDINATE $x: insert_card FROM Customer,
+ $y: read_card FROM ATM_system
+DO ADD $x PRECEDES $y; OD;
+
+COORDINATE $x: request_withdrawal FROM Customer,
+ $y: check_balance FROM ATM_system
+DO ADD $x PRECEDES $y; OD;
+
+COORDINATE $x: identification_succeeds FROM Customer,
+ $y: id_successful FROM ATM_system
+DO ADD $y PRECEDES $x; OD;
+
+COORDINATE $x: get_money FROM Customer,
+ $y: dispense_money FROM ATM_system
+DO ADD $y PRECEDES $x; OD;
+
+COORDINATE $x: not_sufficient_funds FROM Customer,
+ $y: unsufficient_balance FROM ATM_system
+DO ADD $y PRECEDES $x; OD;
+
+COORDINATE $x: identification_fails FROM Customer,
+ $y: id_failed FROM ATM_system
+DO ADD $y PRECEDES $x; OD;
+
+GRAPH Diagram{ TITLE("ATM state transition diagram"); };
+
+/*=====================================
+ Building a graph proceeds here
+=======================================*/
+COORDINATE
+ <CUT_END> $state1: /* these are ATM system’s states */
+ ( Idle | id_successful | id_failed |
+ sufficient_balance | unsufficient_balance),
+
+ $user: /* these are User’s inputs that trigger ATM state transitions */
+ (insert_card | request_withdrawal | retrieve_card),
+
+ <CUT_FRONT> $state2: /* these are ATM system’s states */
+ ( Idle | id_successful | id_failed |
+ sufficient_balance | unsufficient_balance)
+ DO
+ WITHIN Diagram{
+ ADD LAST ($state1) ARROW($user) LAST ($state2); };
+ OD;
+
+GLOBAL
+
+SHOW Diagram;
diff --git a/models/Legacy_examples/Example37_GLOBAL_query.mp b/models/Legacy_examples/Example37_GLOBAL_query.mp
new file mode 100644
index 0000000000000000000000000000000000000000..d6f37e17a2f685fa129f560b3cae2711caae5099
--- /dev/null
+++ b/models/Legacy_examples/Example37_GLOBAL_query.mp
@@ -0,0 +1,61 @@
+/* Example 37 GLOBAL query
+
+Unreliable message flow.
+Assuming that probability for a message to get lost is 0.2,
+find probability of a trace with more than 75% successfully received messages.
+
+Since we are interested only in traces with at least one 'send' event,
+the (+ ... +) iteration is used.
+
+This example is small enough to try scopes larger than 5.
+That can be done using explicit iteration limit (running for instance,
+for scope 1), like:
+
+ROOT Sender: (+<1..7> send +);
+ROOT Receiver: (+<1..7> (receive |<<0.2>> does_not_receive) +);
+
+ Run for scopes 1 and up.
+*/
+SCHEMA unreliable_message_flow
+
+ROOT Sender: (+ send +);
+ROOT Receiver: (+ (receive |<<0.2>> does_not_receive) +);
+
+COORDINATE $x: send FROM Sender,
+ $y: (receive | does_not_receive) FROM Receiver
+ DO ADD $x PRECEDES $y; OD;
+
+ATTRIBUTES {number trace_unique_id,
+ summary_probability,
+ count; };
+
+GRAPH good_traces{ }; /* To accumulate data about traces of interest */
+
+IF #receive / #send > 0.75 THEN
+ WITHIN good_traces {
+ Node$x: NEW(trace_id);
+ Node$x.trace_unique_id := trace_id; };
+ MARK; /* MARK this trace */
+FI;
+
+GLOBAL
+REPORT R{TITLE("Scope " $$scope);};
+
+WITHIN good_traces{
+ FOR Node$a DO
+ /* sum up probabilities of traces stored in the 'good_traces'.
+ Please notice that trace's probability can be estimated only
+ after all valid trace derivation has been completed,
+ i.e. should be postponed to the GLOBAL section,
+ using the #$$TP( ) function. */
+ summary_probability +:= #$$TP(Node$a.trace_unique_id);
+ count +:=1;
+ OD;
+ };
+
+ SAY( "Total " #$$TRACE " traces") => R;
+ SAY("In "count " of traces at least 75% of sent messages have been received") => R;
+ SAY("At the given scope probability for at least 75% messages to pass through is " summary_probability) => R;
+
+ SHOW R;
+
diff --git a/models/Legacy_examples/Example38_knapsack.mp b/models/Legacy_examples/Example38_knapsack.mp
new file mode 100644
index 0000000000000000000000000000000000000000..ebe7c4de00ebb093a0cf5f545cb2b2153068062b
--- /dev/null
+++ b/models/Legacy_examples/Example38_knapsack.mp
@@ -0,0 +1,81 @@
+/* Example 38 Knapsack
+
+ 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),
+ see https://en.wikipedia.org/wiki/Knapsack_problem
+
+ 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).
+
+ Run for scope 1 and up to 5
+*/
+SCHEMA Knapsack
+
+ATTRIBUTES { number limit, accumulated_total, current_max,
+ A_count, B_count, C_count;};
+
+GLOBAL.limit := 11;
+
+ROOT A: (* Item_A *)
+ BUILD{ accumulated_total := #Item_A * 2;
+ };
+
+accumulated_total +:= A.accumulated_total;
+IF accumulated_total > GLOBAL.limit THEN REJECT; FI;
+
+ROOT B: (* Item_B *)
+ BUILD{ accumulated_total := #Item_B * 3;
+ };
+
+accumulated_total +:= B.accumulated_total;
+IF accumulated_total > GLOBAL.limit THEN REJECT; FI;
+
+ROOT C: (* Item_C *)
+ BUILD{ accumulated_total := #Item_C * 5;
+ };
+
+accumulated_total +:= C.accumulated_total;
+IF accumulated_total > GLOBAL.limit THEN REJECT; FI;
+
+/* if got so far, check whether accumulated_total can be stored as result */
+GRAPH candidates{};
+
+IF accumulated_total >= GLOBAL.current_max THEN
+ GLOBAL.current_max := accumulated_total;
+
+ /* add potential candidate to the list */
+ WITHIN candidates{
+ Node$a: NEW(trace_id);
+ Node$a.accumulated_total := accumulated_total;
+ Node$a.A_count := #Item_A;
+ Node$a.B_count := #Item_B;
+ Node$a.C_count := #Item_C;
+ SAY("Best result so far: " accumulated_total);
+ };
+
+ ELSE REJECT;
+FI;
+
+GLOBAL
+REPORT best_knapsack{TITLE("Best knapsack");};
+
+SAY("Weight limit " limit) => best_knapsack;
+SAY("Single item's weight: A= 2 B= 3 C= 5" ) => best_knapsack;
+SAY("For scope " $$scope " best packing is " current_max) => best_knapsack;
+
+WITHIN candidates{
+ FOR Node$x DO
+ IF Node$x.accumulated_total == current_max THEN
+ SAY("Pack "
+ Node$x.A_count " of A, "
+ Node$x.B_count " of B, "
+ Node$x.C_count " of C" ) => best_knapsack;
+ FI;
+ OD;
+ };
+
+SHOW best_knapsack;
diff --git a/models/Legacy_examples/Example39_turtles.mp b/models/Legacy_examples/Example39_turtles.mp
new file mode 100644
index 0000000000000000000000000000000000000000..bedbdb0b29519d639f1fa1bff8dfaf9a88d42b88
--- /dev/null
+++ b/models/Legacy_examples/Example39_turtles.mp
@@ -0,0 +1,132 @@
+/* Example39 turtles.mp
+
+ Demonstration of the benefits for complete
+ example set generation in MP.
+
+
+ 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,
+ or all three of them. It becomes too complicated...."
+
+ Now it is time to use MP to obtain all possible scenarios for that story.
+
+ Here it is. Run for scope 1.
+ There are 13 possible scenarios, and none when all three
+ are telling the truth.
+
+ ==================================*/
+SCHEMA Turtles
+
+neighbors: { (nobody_before | one_before | two_before ),
+ (nobody_behinds | one_behinds | two_behinds) }
+BUILD{
+ /* no more than one of two_before or two_behinds */
+ ENSURE (#two_before + #two_behinds) < 2 AND
+ (#two_before == 1 -> #nobody_behinds == 1) AND
+ (#two_behinds == 1 -> #nobody_before == 1) ;
+ };
+
+ROOT Turtle_1: neighbors (Lying | Telling_the_truth)
+BUILD{
+ ENSURE (#Telling_the_truth == 1 <->
+ #nobody_before == 1 AND #two_behinds == 1);
+ };
+
+ROOT Turtle_2: neighbors (Lying | Telling_the_truth)
+BUILD{
+ ENSURE (#Telling_the_truth == 1 <->
+ #one_before == 1 AND #one_behinds == 1);
+ };
+
+ROOT Turtle_3: neighbors (Lying | Telling_the_truth)
+BUILD{
+ ENSURE (#Telling_the_truth == 1 <->
+ #one_before == 1 AND #one_behinds == 1);
+ };
+
+/*===============================
+ global constraints
+=================================*/
+/* ensure the shape of the pack
+---------------------------------*/
+ENSURE FOREACH $t1: $$ROOT
+ (#two_before FROM $t1 > 0 -> EXISTS DISJ $t2: $$ROOT, $t3: $$ROOT
+ $t1 != $t2 AND $t1 != $t3 AND
+
+ /* $t1 is the root of upward fork */
+ ( (#one_behinds FROM $t2 == 1 AND #one_behinds FROM $t3 == 1) OR
+
+ /* $t1 is the bottom of vertical line */
+ (#one_behinds FROM $t2 == 1 AND #one_behinds FROM $t2 == 1 AND
+ #two_behinds FROM $t3 == 1 )
+ )
+ );
+
+ENSURE FOREACH $t1: $$ROOT
+ (#two_behinds FROM $t1 > 0 -> EXISTS DISJ $t2: $$ROOT, $t3: $$ROOT
+ $t1 != $t2 AND $t1 != $t3 AND
+
+ /* $t1 is the top of downward fork */
+ ( (#one_before FROM $t2 == 1 AND #one_before FROM $t3 == 1) OR
+
+ /* $t1 is the top of vertical line */
+ (#one_behinds FROM $t2 == 1 AND #one_behinds FROM $t2 == 1 AND
+ #two_before FROM $t3 == 1 )
+ )
+ );
+
+/* turtles form either a fork or a line */
+/*======================================*/
+ENSURE /* fork upward */
+ #two_before == 1 AND
+ #one_behinds == 2 AND
+ #one_before == 0 AND
+ #two_behinds == 0 AND
+ #nobody_before == 2 AND
+ #nobody_behinds == 1 OR
+
+ /* fork downward */
+ #two_behinds == 1 AND
+ #one_before == 2 AND
+ #one_behinds == 0 AND
+ #two_before == 0 AND
+ #nobody_before == 1 AND
+ #nobody_behinds == 2 OR
+
+ /* vertical */
+ #two_behinds == 1 AND
+ #one_before == 1 AND
+ #one_behinds == 1 AND
+ #two_before == 1 OR
+
+ /* parallel */
+ #nobody_behinds == 3 AND
+ #nobody_before == 3
+;
+/*-------------------------------------------------------*/
+IF #two_before == 1 AND #one_behinds == 2 AND #one_before == 0 THEN
+ SAY("form fork upward"); FI;
+
+IF #two_behinds == 1 AND #one_before == 2 AND #one_behinds == 0 THEN
+ SAY("form fork downward"); FI;
+
+
+IF #two_behinds == 1 AND #one_before == 1 AND
+ #one_behinds == 1 AND #two_before == 1 THEN
+ SAY("form vertical line"); FI;
+
+IF #nobody_behinds == 3 THEN
+ SAY("moving parallel"); FI;
+
+IF #Lying == 0 THEN SAY("All three are telling truth!"); MARK;
+ELSE SAY( #Lying " are lying"); FI;
diff --git a/models/Legacy_examples/Example40_web_browsers.mp b/models/Legacy_examples/Example40_web_browsers.mp
new file mode 100644
index 0000000000000000000000000000000000000000..5c6181c2b66620c1dbe23fbebf301592c0f564b2
--- /dev/null
+++ b/models/Legacy_examples/Example40_web_browsers.mp
@@ -0,0 +1,107 @@
+/* Example 40. MP Web browsers formal security model.
+
+based on the papers by:
+
+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
+
+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.
+
+In particular, we've found very inspiring the sentences from the
+Akhave et al.:
+
+"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
+form the “backbone†of the model" (page 292)
+
+This has motivated to design the MP behavior model of the web activities
+in order to model the vulnerabilities explained in the papers above.
+
+ run for scope 1: 3 traces, no counterexamples for Property1, in less than 0.001 sec.
+ run for scope 2: 7 traces, 1 counterexample for Property1, in 0.13 sec.
+ run for scope 3: 52 traces, 16 counterexamples for Property1, in 15 sec.
+
+ This example borrowed from Daniel Jackson's paper demonstrates
+ how MP can check whether Client's web query may
+ be indirectly affected by Bad Server's Redirect intervention.
+
+==============================================================================*/
+SCHEMA Web_browser
+
+/* Response may embed some Request events,
+ Only Responses from Bad_Server contain Redirect */
+Response: {* Request *} [ Redirect ] Send_Response
+BUILD{
+ COORDINATE $r: Request
+ DO
+ ADD THIS causes $r;
+ OD;
+};
+
+/* Client starts interactions */
+ROOT Client: Request (+ (Request | Process_Response | Response ) +)
+BUILD{
+ ENSURE #Redirect == 0;
+
+ ENSURE #Request == #Process_Response; };
+
+
+ROOT Good_Server: (*<0 .. $$scope + 1> (Request | Process_Response | Response ) *)
+BUILD{
+ ENSURE #Redirect == 0;
+
+ ENSURE #Request == #Process_Response; };
+
+
+ROOT Bad_Server: (*<0 .. $$scope + 1> (Request | Process_Response | Response ) *)
+BUILD{
+ ENSURE #Response == #Redirect;
+
+ ENSURE #Request == #Process_Response; };
+
+
+COORDINATE $a: Request,
+ $b: Response,
+ $c: Process_Response
+ DO
+ /* No Server should respond to its own Request */
+ ENSURE FOREACH $s: $$ROOT NOT ($a FROM $s AND $b FROM $s);
+
+ /* allow only pairs Request/Process_Request from the same Server */
+ ENSURE EXISTS $s: $$ROOT ($a FROM $s AND $c FROM $s);
+
+ ADD $a PRECEDES $b;
+ ADD $a causes $b;
+
+ /* to make the correspondence between Request/Process_Response more visible */
+ ADD $b is_response_to $a;
+
+ COORDINATE $d: Send_Response FROM $b
+ DO
+ ADD $d PRECEDES $c;
+ ADD $d causes $c;
+ OD;
+ OD;
+
+/* Client never does directly interact with Bad_Server */
+ENSURE NOT EXISTS $r1: Request FROM Client, $r2: Response FROM Bad_Server ($r1 causes $r2);
+
+/*=================== Property1 =========================
+ Check whether Client's Process_Response may
+ be indirectly affected by Bad_Server's Redirect intervention
+=========================================================*/
+IF EXISTS $r1: Process_Response FROM Client, $r2: Redirect ($r2 BEFORE $r1)
+THEN SAY("Response to Client may be affected by Bad Server");
+ MARK;
+FI;
diff --git a/models/Legacy_examples/Example41_Replay_Attack.mp b/models/Legacy_examples/Example41_Replay_Attack.mp
new file mode 100644
index 0000000000000000000000000000000000000000..5749bbec43b43fc58ccc58c29120d8ca58160316
--- /dev/null
+++ b/models/Legacy_examples/Example41_Replay_Attack.mp
@@ -0,0 +1,63 @@
+/* Example 41. The description of Replay Attack
+ is available at
+ https://en.wikipedia.org/wiki/Replay_attack
+
+ run scope up to 5
+======================================*/
+
+SCHEMA Replay_Attack
+
+ROOT Alice:
+ sends_password_to_Bob
+
+ (* presents_Alice_password
+ talks *)
+;
+
+/*---------------------------------------*/
+ROOT Network:
+ message_in_transit
+;
+
+COORDINATE $a: sends_password_to_Bob FROM Alice,
+ $n: message_in_transit FROM Network
+ DO ADD $a PRECEDES $n; OD;
+
+/*---------------------------------------*/
+/* Eavesdropper */
+ROOT Eve:
+ eavesesdrops_message
+ (+ presents_Alice_password
+ talks +)
+;
+
+COORDINATE $n: message_in_transit FROM Network,
+ $e: eavesesdrops_message FROM Eve
+ DO ADD $n PRECEDES $e; OD;
+
+/*---------------------------------------*/
+
+ROOT Bob:
+ requests_password_from_Alice
+ receives_password_from_Alice
+
+ (*<1.. 2 * $$scope> asks_for_password
+ talks *)
+;
+
+COORDINATE $a1: requests_password_from_Alice FROM Bob,
+ $r1: sends_password_to_Bob FROM Alice
+ DO ADD $a1 PRECEDES $r1; OD;
+
+COORDINATE $n: message_in_transit FROM Network,
+ $b: receives_password_from_Alice FROM Bob
+ DO ADD $n PRECEDES $b; OD;
+
+COORDINATE $a: asks_for_password FROM Bob,
+ $p: presents_Alice_password /* not necessary to give the FROM owner,
+ just the event name is sufficient */
+ DO ADD $a PRECEDES $p; OD;
+
+COORDINATE $t1: talks SUCH THAT NOT $t1 FROM Bob,
+ $t2: talks FROM Bob
+ DO SHARE $t1 $t2; OD;
diff --git a/models/Legacy_examples/Example42_Bar_Chart.mp b/models/Legacy_examples/Example42_Bar_Chart.mp
new file mode 100644
index 0000000000000000000000000000000000000000..dade7edfb50152ab420057c88fe4d2ebbb1150ae
--- /dev/null
+++ b/models/Legacy_examples/Example42_Bar_Chart.mp
@@ -0,0 +1,53 @@
+/*
+ Example42
+ Assembling statistics about a current trace in a TABLE and rendering it.
+ Table and bar chart example, run for scope 1
+*/
+
+SCHEMA Example
+ROOT A: a b c a;
+
+TABLE trace_stats {
+ TITLE ("Trace " trace_id);
+TABS string event_name,
+number total_number;
+};
+
+BAR CHART chart_states {
+ TITLE( "Trace " trace_id " chart");
+ FROM trace_stats;
+/* contents of the bar chart is derived from
+ the table trace_stats */
+ X_AXIS event_name;
+};
+
+GRAPH event_counters { };
+/* This graph container is used as an associative array
+ data structure to accumulate event count
+ for each event in the trace via node attributes */
+ATTRIBUTES {number count;};
+
+/* Collect event data and store it in the graph container */
+WITHIN event_counters{
+ COORDINATE $e: $$EVENT /* loop over all events within the trace */
+ DO Node$a: LAST ($e);
+ Node$a.count +:=1; /* increment node’s attribute value */
+ OD;
+ /* Second loop - now fill the table, see loop_over_graph (105) */
+ FOR Node$n /* variable Node$n is traversing event_counters node set */
+ DO
+ trace_stats <| /* store tuple in the table trace_stats */
+ event_name : SAY(Node$n),
+ /* here (Node$n) is a string_constructor(87)
+ converting node’s name (label) into a character string */
+ total_number: Node$n.count ;
+ OD;
+}; /* end WITHIN */
+
+SHOW trace_stats;
+SHOW chart_states;
+/* contents of the related table provides data source for the bar chart */
+
+
+
+
diff --git a/models/Legacy_examples/Example43_Histogramm.mp b/models/Legacy_examples/Example43_Histogramm.mp
new file mode 100644
index 0000000000000000000000000000000000000000..ad5a2c6f7c3dcbf88a18309f449bf9172366d36a
--- /dev/null
+++ b/models/Legacy_examples/Example43_Histogramm.mp
@@ -0,0 +1,45 @@
+/* Example43
+ Histogram example, run for scopes 1, 2, 3, and up
+*/
+SCHEMA Example
+ROOT A: (<<0.2>> a1 | <<0.3>> a2 | (* a3 *));
+ATTRIBUTES { number count; };
+
+GLOBAL
+/* this GRAPH is used as a container to collect data about valid trace probabilities */
+GRAPH Data { };
+
+WITHIN Data{
+ /* numerical_loop_header(40) is used to perform required interval calculations. */
+ FOR Num$t: [1.. #$$TRACE] STEP 1
+ DO FOR Num$n: [0 .. 1] STEP 0.1
+ DO
+ Node$x: LAST("[" Num$n ".." Num$n + 0.1 ")");
+ /* p - pre-defined trace probability attribute */
+ IF Num$n <= #$$TP(Num$t) AND
+ #$$TP(Num$t) < Num$n + 0.1 THEN
+ Node$x.count +:= 1;
+ FI;
+ OD;
+ OD;
+}; /* end of WITHIN Data */
+
+TABLE probability_histogram {
+TABS string probability_interval,
+ number trace_count; };
+
+BAR CHART probability_chart { TITLE("Trace probabilities");
+ FROM probability_histogram;
+ X_AXIS probability_interval; };
+WITHIN Data{
+ FOR Node$n
+ DO probability_histogram <|
+ probability_interval: SAY(Node$n),
+ trace_count: Node$n.count;
+ OD;
+};
+
+SHOW probability_chart SORT;
+/* The contents of the chart is sorted by X_AXIS string values, since the order of adding rows to the
+ TABLE may be arbitrary */
+
diff --git a/models/Legacy_examples/Example44_Gantt_Chart.mp b/models/Legacy_examples/Example44_Gantt_Chart.mp
new file mode 100644
index 0000000000000000000000000000000000000000..fe4483df5b9e157783ebab43411f026c402a9199
--- /dev/null
+++ b/models/Legacy_examples/Example44_Gantt_Chart.mp
@@ -0,0 +1,39 @@
+/* Example44
+ Gantt chart example
+*/
+SCHEMA S
+ROOT A: a1 a2;
+
+ROOT B: b1 a2 b2;
+
+A, B SHARE ALL a2;
+
+COORDINATE $a1: a1, $a2: a2, $b1: b1, $b2: b2
+ DO
+ SET $a1.duration AT LEAST 3;
+ SET $a2.duration AT LEAST 5;
+ SET $b1.duration AT LEAST 1;
+ SET $b2.duration AT LEAST 2;
+ OD;
+
+TABLE gantt_1{
+ TABS string event_name,
+ number start_time,
+ number duration_time;
+};
+
+BAR CHART gantt_2 { TITLE("Example of Gantt Chart");
+ FROM gantt_1;
+ X_AXIS event_name;
+ ROTATE; /* to place the X_AXIS vertical */
+};
+
+COORDINATE $e: $$EVENT
+ DO /* add this event to the Table */
+ gantt_1 <|
+ event_name: SAY($e),
+ start_time: $e.start.smallest,
+ duration_time: $e.duration.largest;
+ OD;
+
+SHOW gantt_2;
diff --git a/models/Legacy_examples/Example45_Martian_Lander.mp b/models/Legacy_examples/Example45_Martian_Lander.mp
new file mode 100644
index 0000000000000000000000000000000000000000..10b3b3a4fc8ad6e14215d21f31e284fd1b61b052
--- /dev/null
+++ b/models/Legacy_examples/Example45_Martian_Lander.mp
@@ -0,0 +1,163 @@
+/* Example 45. Real time system behavior modeling.
+ Landing system for Martian Lander.
+
+ MP model written by M.Auguston following example 1 and Appendix B from
+ 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
+
+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
+ADJM Adjust motor thrust
+TDP Transmit info to display panel
+IEM Initiate emergency mode
+ETC Other housekeeping function,
+IVEL Input measured velocity
+IALT Input measured altitude
+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
+
+Action Time in ms
+RACC 10
+STMR 10
+ADJM 20
+TDP 10
+IEM 10
+ETC 10
+IVEL 20
+IALT 20
+CKDT 10
+RRM 10
+
+ run for scope 1 and up.
+*/
+SCHEMA Martian_Lander
+
+ROOT Measure_and_display:
+ /* runs Timer1 */
+ STMR1
+ (+ {IVEL, IALT}
+ CKDT
+ TDP
+ +)
+ stop_Timer1
+;
+
+ROOT Landing:
+ START
+/* Phase 1 */
+ { RACC,
+ STMR1, /* starts Timer1 */
+ STMR2 /* starts Timer2 */
+ }
+
+ (+ { ADJM, ETC } +)
+
+/* Phase 2 */
+ (IOINT | /* normal landing */
+
+ TMRINT /* Timer2 sets interrupt */
+ IEM /* initiate emergency mode */
+ Emergency_Landing )
+
+ Lands
+ {stop_Timer1, stop_Timer2}
+;
+
+Emergency_Landing:
+ (* fire_RRM *)
+;
+
+ROOT Timer2:
+/* responsible for switching on Emergency_landing after 100 msec */
+ STMR2
+ [ TMRINT ]
+ stop_Timer2
+;
+
+Landing, Measure_and_display SHARE ALL STMR1, stop_Timer1;
+Landing, Timer2 SHARE ALL STMR2, TMRINT, stop_Timer2;
+
+/*=== set timing for events, in ms ===*/
+COORDINATE $a: RACC DO SET $a.duration AT LEAST 10; OD;
+COORDINATE $a: STMR1 DO SET $a.duration AT LEAST 10; OD;
+COORDINATE $a: STMR2 DO SET $a.duration AT LEAST 10; OD;
+COORDINATE $a: ADJM DO SET $a.duration AT LEAST 20; OD;
+COORDINATE $a: TDP DO SET $a.duration AT LEAST 10; OD;
+COORDINATE $a: IEM DO SET $a.duration AT LEAST 10; OD;
+COORDINATE $a: ETC DO SET $a.duration AT LEAST 10; OD;
+COORDINATE $a: IVEL DO SET $a.duration AT LEAST 20; OD;
+COORDINATE $a: IALT DO SET $a.duration AT LEAST 20; OD;
+COORDINATE $a: CKDT DO SET $a.duration AT LEAST 10; OD;
+COORDINATE $a: fire_RRM DO SET $a.duration AT LEAST 10; OD;
+
+/*=== arrange trace annotations ===*/
+ADD SAY("Running Timer1") alert Measure_and_display;
+
+COORDINATE $a: TMRINT DO
+ SET $a.start AT LEAST 101;
+ ADD SAY("Emergency landing started at " $a.start) alert $a;
+OD;
+
+COORDINATE $a: Lands DO
+ ADD SAY("Landing complete at " $a.end) alert $a;
+OD;
+
+/* measurement and display continue till the landing is complete */
+ENSURE FOREACH $a: IVEL (Measure_and_display.start - $a.start) >= 40 ->
+ EXISTS $b: IVEL $a PRECEDES $b;
+
+/*====== main timing constraint ======*/
+/* normal landing completes before the deadline 100 msec. */
+ENSURE FOREACH $a: IOINT $a.start <= 100;
+
+/*===== table for some event timings =====*/
+TABLE Time_table{ TITLE("Event timings");
+ TABS string event_name, number start_time,
+ number event_duration, number end_time;
+ };
+
+CLEAR Time_table; /* prepare for the new event trace */
+
+/* pick up timing for some events */
+COORDINATE $x: (IVEL | IALT | TDP | ADJM | fire_RRM |
+ Emergency_Landing | Lands | stop_Timer1) DO
+ Time_table <| event_name: SAY($x),
+ start_time: $x.start.smallest,
+ event_duration: $x.duration.smallest,
+ end_time: $x.end.smallest;
+OD;
+
+SHOW Time_table;
+
+/* show Gantt Chart for some event timing */
+BAR CHART Timing{ TITLE("Event timings");
+ FROM Time_table;
+ X_AXIS event_name;
+ TABS start_time, event_duration; /* show these values only */
+ ROTATE; /* show as Gantt chart */
+};
+
+SHOW Timing;
diff --git a/models/Legacy_examples/Example46_CargoScreening.mp b/models/Legacy_examples/Example46_CargoScreening.mp
new file mode 100644
index 0000000000000000000000000000000000000000..13fe2283d993b66b14f1d52881729320e9936a03
--- /dev/null
+++ b/models/Legacy_examples/Example46_CargoScreening.mp
@@ -0,0 +1,61 @@
+/* Cargo Screening process model
+May 6, 2011, draft written by Mikhail Auguston, NPS, Monterey, CA
+source:
+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
+
+Error found: 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"
+
+*/
+
+SCHEMA CargoScreening
+
+ROOT CargoScreeningProcess: Screening Targeting ;
+
+Screening: CBP_Officers_analyze_shipping_information_to_identify_high_risk_cargo;
+
+Targeting : CBP_Officers_review_the_shipping_information
+ CBP_Officers_select_high_risk_cargo_to_be_presented_for_inspection
+ ( High_risk_cargo_selected Inspection |
+ No_high_risk_cargo_selected Loading
+ );
+
+Inspection: ( selection_has_been_accepted
+ the_cargo_is_scanned_using_large_scale_NII_equipment
+ Anomaly_detection_and_processing |
+
+ /*this branch is missing in the originalal document! */
+ selection_has_not_been_accepted
+ PhysicalExamination
+ AnomalyResolution );
+
+Anomaly_detection_and_processing: AnomalyDetection
+ ( ThreatIsNotFound Loading |
+ AnomalyIsFound
+ PhysicalExamination
+ AnomalyResolution );
+
+AnomalyDetection: CBP_Officers_or_host_country_officials_identify_anomalies_in_the_x_ray_image;
+
+PhysicalExamination: CBP_Officers_or_host_country_officials_open_containers_to_locate_anomaly;
+
+AnomalyResolution: Officials_determine_if_the_anomaly_presents_a_threat
+ ( ThreatIsNotFound Loading |
+ ThreatIsFound Resolution );
+
+Resolution: Officials_take_appropriate_steps_to_resolve_the_threat;
+
+Loading: The_container_is_loaded_onto_the_cargo_ship;
+
diff --git a/models/Legacy_examples/Example47_Elevator.mp b/models/Legacy_examples/Example47_Elevator.mp
new file mode 100644
index 0000000000000000000000000000000000000000..48189b3b39099220fadc227d6a12035c8bf38aab
--- /dev/null
+++ b/models/Legacy_examples/Example47_Elevator.mp
@@ -0,0 +1,43 @@
+/*Elevator Model
+
+K.Giammarco circa 2011
+
+This model demonstrates the modeling of situations and consequential events
+in MP. The pattern is:
+
+( SituationA do_one_thing |
+ SituationB do_another_thing )
+
+in the case of this model,
+
+( Elevator_works_fine Get_Off |
+ Emergency_Situation Call_for_help )
+
+*/
+
+SCHEMA ELEVATOR
+
+ROOT Passenger : Request_Up_Service
+ ( Available
+ Enter_Elevator
+ Request_floor
+ ( Elevator_works_fine Get_Off |
+ Emergency_Situation Call_for_help ) |
+ Non_Available Elevator_works_fine Wait );
+
+ROOT Elevator : (Available | Non_Available);
+
+ROOT Maintenance_Personnel : ( Emergency_Situation
+ Instant_Response
+ Provide_Exit_Opportunity |
+ Elevator_works_fine
+ Do_Nothing );
+
+COORDINATE $a: Call_for_help FROM Passenger,
+ $b: Instant_Response FROM Maintenance_Personnel
+ DO ADD $a PRECEDES $b; OD;
+
+Passenger, Elevator SHARE ALL Available, Non_Available;
+Passenger, Maintenance_Personnel SHARE ALL Emergency_Situation, Elevator_works_fine;
+
+
\ No newline at end of file
diff --git a/models/Legacy_examples/Example48_Manufacturing_Process.mp b/models/Legacy_examples/Example48_Manufacturing_Process.mp
new file mode 100644
index 0000000000000000000000000000000000000000..6eeb2831553b74ab0df671fb8de519ca3cf5d1f0
--- /dev/null
+++ b/models/Legacy_examples/Example48_Manufacturing_Process.mp
@@ -0,0 +1,80 @@
+/*
+
+Application of Monterey Phoenix Modeling to Manufacturing Product Systems
+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.
+Created by: John Palmer
+August 2014
+
+*/
+
+SCHEMA Manufacturing_System
+
+ROOT SYSTEM: (* Incoming_Material
+ Multi_Axis_Machine
+ Media_Finish
+ Send_to_Inspector
+
+ (* Rejected
+ Rework
+ Send_to_Inspector
+ *)
+
+ Accepted
+
+ ( ( Turning_Machine_1
+ Milling_Machine_1
+ Turning_Machine_2
+ Milling_Machine_2 ) |
+
+ ( Multitask_1 Multitask_2 )
+ )
+
+ Send_to_Inspector2
+
+ (* Rejected2
+ Rework2
+ Send_to_Inspector2
+ *)
+
+ Accepted2
+
+ Surface_Treatment
+ Package_Part
+ Ship_Part
+ *);
+
+ROOT INSPECTOR: (* <0..3> Inspect
+ ( Accept | Reject )
+ *);
+
+ Inspect: CheckPart ProvideAnswer;
+
+ROOT INSPECTOR2: (* <0..3> Inspect2
+ ( Accept2 | Reject2 )
+ *);
+
+ Inspect2: CheckPart2 ProvideAnswer2;
+
+
+
+ROOT SysInsp: (* <1..3> Send_to_Inspector
+ Inspect
+ ( Reject Rejected | Accept Accepted )
+ *);
+
+
+INSPECTOR, SysInsp SHARE ALL Inspect, Accept, Reject;
+SysInsp, SYSTEM SHARE ALL Send_to_Inspector, Accepted, Rejected;
+
+
+ROOT SysInsp2: (*<1..3> Send_to_Inspector2
+ Inspect2
+ ( Reject2 Rejected2 | Accept2 Accepted2 )
+ *);
+
+
+SysInsp2, SYSTEM SHARE ALL Send_to_Inspector2, Accepted2, Rejected2;
+INSPECTOR2, SysInsp2 SHARE ALL Inspect2, Accept2, Reject2;
+
diff --git a/models/Legacy_examples/Example49_Swarm_UAV.mp b/models/Legacy_examples/Example49_Swarm_UAV.mp
new file mode 100644
index 0000000000000000000000000000000000000000..b7dcb004945e04a0aa77340182afb1f01afd7c6c
--- /dev/null
+++ b/models/Legacy_examples/Example49_Swarm_UAV.mp
@@ -0,0 +1,141 @@
+/*
+ Kristin Giammarco and Mikhail Auguston
+ MP Model based on "Swarm CONOPs" Draft 11 February 2015
+ 11 February 2015 - Initial Model Started by KGiammarco
+ 25 May 2015 - M.Auguston Merged several COORDINATE, SHARE ALL to speed up
+ trace generation
+ 22 July 2015 - added a few more coordinate statements to capture dependencies
+
+ 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).
+*/
+
+SCHEMA Swarm_UAV
+
+ROOT Flight_Crew: Conduct_PreMission_Briefing
+ (+ PreFlight_UAV +)
+ Confirm_Staging_Plans
+ (+ Confirm_Launch_Permission
+ Launch_UAV
+ Assess_Flight_Behavior
+ Confirm_Nominal_Flight_Behavior
+ Stage_UAV_for_Ingress +)
+
+ Alert_All_UAVs_Staged
+
+ (* [ Receive_Recovery_Prioritization_List ]
+ /* above optional event will always occur because it is
+ COORDINATEd with a mandatory event */
+
+ Observe_New_UAV_in_Recovery_List
+ Recover_UAV
+ Retrieve_UAV
+ Alert_RC_UAV_Landing *)
+
+ Confirm_UAVs_Recovered_Retrieved
+ Conduct_PostMission_Hotwash;
+
+ROOT Swarm: {+ UAV +};
+
+ UAV: Undergo_PreFlight
+ Launch
+ Report_Flight_Status
+ Confirm_Staged_for_Ingress
+ Store_Ingress_SubSwarm_ID
+ Perform_Mission
+ Store_Egress_SubSwarm_ID
+ Confirm_Staged_for_Egress
+ Land;
+
+COORDINATE $a: PreFlight_UAV FROM Flight_Crew,
+ $b: Undergo_PreFlight FROM Swarm
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Launch_UAV FROM Flight_Crew,
+ $b: Launch FROM Swarm
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Report_Flight_Status FROM Swarm,
+ $b: Assess_Flight_Behavior FROM Flight_Crew
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Stage_UAV_for_Ingress FROM Flight_Crew,
+ $b: Confirm_Staged_for_Ingress FROM Swarm
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Confirm_Staged_for_Egress FROM Swarm,
+ $b: Observe_New_UAV_in_Recovery_List FROM Flight_Crew
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Recover_UAV FROM Flight_Crew,
+ $b: Land FROM Swarm
+ DO ADD $b PRECEDES $a; OD;
+
+ROOT Mission_Commander: Conduct_PreMission_Briefing
+ Confirm_Staging_Plans
+ Confirm_Swarm_Mission_Plan
+ (* Confirm_Launch_Permission *)
+ Conduct_PostMission_Hotwash;
+
+Flight_Crew, Mission_Commander SHARE ALL Confirm_Staging_Plans, Confirm_Launch_Permission;
+
+
+COORDINATE $a: Confirm_UAVs_Recovered_Retrieved FROM Flight_Crew,
+ $b: Conduct_PostMission_Hotwash FROM Mission_Commander
+ DO ADD $a PRECEDES $b; OD;
+
+
+ROOT Swarm_Operator: Conduct_PreMission_Briefing
+ Confirm_Swarm_Mission_Plan
+ Receive_Swarm_Mission_Plan_Approval
+ (+ Assign_Ingress_SubSwarmID +)
+ Confirm_All_UAVs_Staged
+ Command_Swarm_to_Commence_Mission
+ (* Assign_Egress_SubSwarmID *)
+ Provide_Recovery_Prioritization_List
+ Conduct_PostMission_Hotwash;
+
+Mission_Commander, Swarm_Operator SHARE ALL Confirm_Swarm_Mission_Plan;
+
+COORDINATE $a: Confirm_Staged_for_Ingress FROM Swarm,
+ $b: Assign_Ingress_SubSwarmID FROM Swarm_Operator,
+ $c: Store_Ingress_SubSwarm_ID FROM Swarm
+
+ DO ADD $a PRECEDES $b;
+ ADD $b PRECEDES $c;
+ OD;
+
+COORDINATE $a: Store_Ingress_SubSwarm_ID FROM Swarm
+ DO COORDINATE $b: Alert_All_UAVs_Staged FROM Flight_Crew
+ DO ADD $a PRECEDES $b; OD;
+ OD;
+
+COORDINATE $a: Alert_All_UAVs_Staged FROM Flight_Crew,
+ $b: Confirm_All_UAVs_Staged FROM Swarm_Operator
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Command_Swarm_to_Commence_Mission FROM Swarm_Operator
+ DO COORDINATE $b: Perform_Mission FROM Swarm
+ DO ADD $a PRECEDES $b; OD;
+ OD;
+
+COORDINATE $a: Assign_Egress_SubSwarmID FROM Swarm_Operator,
+ $b: Store_Egress_SubSwarm_ID FROM Swarm
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Provide_Recovery_Prioritization_List FROM Swarm_Operator,
+ $b: Receive_Recovery_Prioritization_List FROM Flight_Crew
+ DO ADD $a PRECEDES $b; OD;
+
+ROOT Range_Control: (* Receive_UAV_Landing_Notification *);
+
+COORDINATE $a: Alert_RC_UAV_Landing FROM Flight_Crew,
+ $b: Receive_UAV_Landing_Notification FROM Range_Control
+ DO ADD $a PRECEDES $b; OD;
+
+ROOT Safety_Coordinator: Conduct_PreMission_Briefing
+ Conduct_PostMission_Hotwash;
+
+Flight_Crew, Mission_Commander, Swarm_Operator, Safety_Coordinator SHARE ALL
+ Conduct_PreMission_Briefing, Conduct_PostMission_Hotwash;
diff --git a/models/Legacy_examples/Example50_Flight.mp b/models/Legacy_examples/Example50_Flight.mp
new file mode 100644
index 0000000000000000000000000000000000000000..ff64ab55e84b04e1869deb021d9870a80a1a5b60
--- /dev/null
+++ b/models/Legacy_examples/Example50_Flight.mp
@@ -0,0 +1,234 @@
+/* Model of a commercial flight, November 27, 2013
+
+This model demonstrates the interlacing of root events as Phases
+and as Actors. 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.
+
+*/
+
+/*-----------------------------------------------------
+ Phases
+-----------------------------------------------------*/
+
+SCHEMA Flight
+
+
+
+ROOT Preflight: BoardAircraft
+ FlightCheck
+ DepartureClearance
+ Pushback
+ IssueGroundInstruction
+ Taxi ;
+
+ROOT Takeoff: Clear_for_takeoff
+ Liftoff
+ Handoff_to_TRACon ;
+
+ROOT Departure: ChangeFrequency
+ IssueClearances
+ Handoff_to_ARTCC ;
+
+ROOT EnRoute: IssueInstruction
+ ( OceanicExtension | Follow_route )
+ ChangeFrequency2
+ Handoff_to_TRACon2 ;
+
+ROOT Descent: Clear_descent
+ Maneuver_toward_Airport ;
+
+ROOT Approach: [ Hold ]
+ Clear_approach
+ Enter_approach_line
+ Handoff_to_tower ;
+
+ROOT Landing: Clear_landing
+ Land
+ Taxi_instruction
+ Taxi_to_gate
+ Disembark ;
+
+/*-----------------------------------------------------
+ Actors
+-----------------------------------------------------*/
+
+ROOT Passenger: BoardAircraft
+ InsideCabin
+ Disembark ;
+
+ROOT Pilot: FlightCheck
+ Pushback
+ Taxi
+ Liftoff
+ ChangeFrequency
+ ( OceanicExtension | Follow_route )
+ ChangeFrequency2
+ Maneuver_toward_Airport
+ [ Hold ]
+ Enter_approach_line
+ Land
+ Taxi_to_gate ;
+
+ROOT Controller: DepartureClearance
+ IssueGroundInstruction
+ Clear_for_takeoff
+ Handoff_to_TRACon
+ IssueClearances
+ Handoff_to_ARTCC
+ IssueInstruction
+ Handoff_to_TRACon2
+ Clear_descent
+ Clear_approach
+ Handoff_to_tower
+ Clear_landing
+ Taxi_instruction ;
+
+/*-----------------------------------------------------
+ Overlapping between actors and process phases
+-----------------------------------------------------*/
+
+Passenger, Preflight SHARE ALL BoardAircraft;
+
+Passenger, Landing SHARE ALL Disembark;
+
+Pilot, Preflight SHARE ALL FlightCheck,
+ Pushback,
+ Taxi;
+
+Pilot, Takeoff SHARE ALL Liftoff;
+
+Pilot, Departure SHARE ALL ChangeFrequency;
+
+Pilot, EnRoute SHARE ALL OceanicExtension,
+ Follow_route,
+ ChangeFrequency2;
+
+Pilot, Descent SHARE ALL Maneuver_toward_Airport;
+
+Pilot, Approach SHARE ALL Hold,
+ Enter_approach_line;
+
+Pilot, Landing SHARE ALL Land,
+ Taxi_to_gate;
+
+Controller, Preflight SHARE ALL DepartureClearance,
+ IssueGroundInstruction;
+
+Controller, Takeoff SHARE ALL Clear_for_takeoff,
+ Handoff_to_TRACon;
+
+Controller, Departure SHARE ALL IssueClearances,
+ Handoff_to_ARTCC;
+
+Controller, EnRoute SHARE ALL IssueInstruction,
+ Handoff_to_TRACon2;
+
+Controller, Descent SHARE ALL Clear_descent;
+
+
+Controller, Approach SHARE ALL Clear_approach,
+ Handoff_to_tower;
+
+Controller, Landing SHARE ALL Clear_landing,
+ Taxi_instruction;
+
+/*---------------------------------------------------------
+ Coordination between phases
+---------------------------------------------------------*/
+
+COORDINATE $a: BoardAircraft FROM Passenger,
+ $b: FlightCheck FROM Pilot,
+ $c: DepartureClearance FROM Controller,
+ $d: Pushback FROM Pilot,
+ $e: IssueGroundInstruction FROM Controller,
+ $f: ( Taxi | Hold ) FROM Pilot,
+ $g: Clear_for_takeoff FROM Controller,
+ $h: Liftoff FROM Pilot,
+ $i: Handoff_to_TRACon FROM Controller,
+ $j: ChangeFrequency FROM Pilot,
+ $k: IssueClearances FROM Controller
+
+ DO ADD $a PRECEDES $b,
+ $b PRECEDES $c,
+ $c PRECEDES $d,
+ $d PRECEDES $e,
+ $e PRECEDES $f,
+ $f PRECEDES $g,
+ $g PRECEDES $h,
+ $h PRECEDES $i,
+ $i PRECEDES $j,
+ $j PRECEDES $k; OD;
+
+
+COORDINATE $a: IssueInstruction FROM Controller,
+ $b: ( OceanicExtension | Follow_route ) FROM Pilot,
+ $c: ChangeFrequency2 FROM Pilot,
+ $d: Handoff_to_TRACon2 FROM Controller,
+ $e: Clear_descent FROM Controller,
+ $f: ( Maneuver_toward_Airport | Hold ) FROM Pilot,
+ $g: Clear_approach FROM Controller,
+ $h: Enter_approach_line FROM Pilot,
+ $i: Handoff_to_tower FROM Controller,
+ $j: Clear_landing FROM Controller,
+ $k: Land FROM Pilot,
+ $l: Taxi_instruction FROM Controller,
+ $m: Taxi_to_gate FROM Pilot,
+ $n: Disembark FROM Passenger
+
+ DO ADD $a PRECEDES $b,
+ $b PRECEDES $c,
+ $c PRECEDES $d,
+ $d PRECEDES $e,
+ $e PRECEDES $f,
+ $f PRECEDES $g,
+ $g PRECEDES $h,
+ $h PRECEDES $i,
+ $i PRECEDES $j,
+ $j PRECEDES $k,
+ $k PRECEDES $l,
+ $l PRECEDES $m,
+ $m PRECEDES $n; OD;
+
+/*
+
+ROOT Preflight_Takeoff: Taxi
+ Clear_for_takeoff ;
+
+COORDINATE $x: Taxi FROM Preflight,
+ $y: Clear_for_takeoff FROM Takeoff
+ DO ADD $x PRECEDES $y; OD;
+
+ROOT Takeoff_Departure: Handoff_to_TRACon
+ ChangeFrequency ;
+
+COORDINATE $x: Handoff_to_TRACon FROM Takeoff,
+ $y: ChangeFrequency FROM Departure
+ DO ADD $x PRECEDES $y; OD;
+
+/* Departure and EnRoute are coordinated within Controller */
+
+/* EnRoute and Descent are coordinated within Controller */
+
+/*ROOT Descent_Approach: Maneuver_toward_Airport
+ [ Hold ]
+ Clear_approach ;
+
+COORDINATE $x: Handoff_to_TRACon FROM Descent,
+ $y: ChangeFrequency FROM Approach
+ DO ADD $x PRECEDES $y; OD;
+
+/* Approach and Landing are coordinated within Controller */
+
+/*Preflight, Preflight_Takeoff SHARE ALL Taxi;
+
+Preflight_Takeoff, Takeoff SHARE ALL Clear_for_takeoff;
+
+Takeoff, Takeoff_Departure SHARE ALL Handoff_to_TRACon;
+
+Takeoff_Departure, Departure SHARE ALL ChangeFrequency;
+
+Descent, Descent_Approach SHARE ALL Maneuver_toward_Airport;
+
+Descent_Approach, Approach SHARE ALL Hold, Clear_approach;
+
diff --git a/models/Legacy_examples/Example51_Autonomous_Car.mp b/models/Legacy_examples/Example51_Autonomous_Car.mp
new file mode 100644
index 0000000000000000000000000000000000000000..7d88365fed2f335c382f1060ca51badd16f2cbce
--- /dev/null
+++ b/models/Legacy_examples/Example51_Autonomous_Car.mp
@@ -0,0 +1,58 @@
+/* A model of an autonomous car that was used to support a failure mode
+analysis of autonomous automobile technology (student project).
+Created by G. Kaminski, November 2015
+*/
+
+SCHEMA Autonomous_Car
+
+/*Actors*/
+
+ROOT Car: Search_for_Destination
+
+ ( Prompt_for_New_Destination |
+ Find_Destination )
+
+ Begin_Trip
+ Drive
+ Reach_Destination
+ Confirm_Trip_Complete
+
+ ( End_Trip |
+ Start_New_Trip);
+
+ Find_Destination: Confirm_Destination_Found;
+
+
+ROOT User: Enter_Car
+ Enter_Desired_Destination
+
+ ( Enter_New_Destination |
+ Confirm_Destination )
+
+ ( Confirm_Destination_Reached |
+ Destination_Not_Reached );
+
+
+/*Interactions*/
+
+COORDINATE $a: Enter_Desired_Destination FROM User,
+ $b: Search_for_Destination FROM Car
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Prompt_for_New_Destination FROM Car,
+ $b: Enter_New_Destination FROM User
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Confirm_Trip_Complete FROM Car,
+ $b: ( Confirm_Destination_Reached |
+ Destination_Not_Reached ) FROM User
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Confirm_Destination_Found FROM Car,
+ $b: Confirm_Destination FROM User
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: ( Enter_New_Destination |
+ Confirm_Destination ) FROM User,
+ $b: Begin_Trip FROM Car
+ DO ADD $a PRECEDES $b; OD;
\ No newline at end of file
diff --git a/models/Legacy_examples/Example52_Swarm_Search_and_Track.mp b/models/Legacy_examples/Example52_Swarm_Search_and_Track.mp
new file mode 100644
index 0000000000000000000000000000000000000000..5677443d7c03c84ca544bc2728b6dcc34e16f02a
--- /dev/null
+++ b/models/Legacy_examples/Example52_Swarm_Search_and_Track.mp
@@ -0,0 +1,79 @@
+/*
+Michael Revill
+22 February 2016
+Incorporating Failure Modes and Failsafe Behaviors
+MP model Swarm_Search_and_Track elaborates on
+"Perform_Mission" event in Swarm2-v8.mp
+
+Edited by K.Giamamrco on 26 Feb 2016
+Established naming convention:
+Noun-oriented events are actors (root events)
+Verb-oriented events in sentence case are activities
+Verb-oriented events in title case are states
+
+This model demonstrates the found unexpected behavior for
+object discovery after bingo fuel (trace 6)
+
+*/
+
+SCHEMA Swarm_Search_and_Track
+
+ROOT Swarm_Operator: Command_swarm_to_commence_mission
+ Monitor_mission
+ Issue_recovery_command;
+
+ Monitor_mission: (* Receive_target_alert
+ Assess_detected_object
+ ( Object_is_Valid_Target |
+ Object_is_Not_Target )
+ *);
+
+ROOT Swarm: {+ UAV +};
+
+ UAV: Commence_mission
+ Search_and_track_objects
+ Return_to_base
+ End_mission;
+
+ Search_and_track_objects:
+
+ (* ( Detect_object
+ Evaluate_object
+ ( Target_Found
+ Alert_operator
+ Track_target |
+
+ Non_Target_Found
+ Resume_target_search ) |
+
+ Bingo_Fuel
+ Reassess_environment
+ [ ( Target_Found
+ Alert_operator
+ Track_target |
+
+ Non_Target_Found
+ ) ]
+
+ )
+ *);
+
+COORDINATE $a: Command_swarm_to_commence_mission FROM Swarm_Operator
+ DO COORDINATE $b: Commence_mission FROM Swarm
+ DO ADD $a PRECEDES $b; OD;
+ OD;
+
+COORDINATE $a: Alert_operator FROM Swarm,
+ $b: Receive_target_alert FROM Swarm_Operator
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Issue_recovery_command FROM Swarm_Operator
+ DO COORDINATE $b: Return_to_base FROM Swarm
+ DO ADD $a PRECEDES $b; OD;
+ OD;
+
+ROOT Environment: (* Present_object_signature *);
+
+COORDINATE $a: Present_object_signature FROM Environment,
+ $b: Detect_object FROM Swarm
+ DO ADD $a PRECEDES $b; OD;
diff --git a/models/Legacy_examples/Example53_First_Responder.mp b/models/Legacy_examples/Example53_First_Responder.mp
new file mode 100644
index 0000000000000000000000000000000000000000..0f25d9d0a75cfc706c9c575a6a9fe8cdb0277c7a
--- /dev/null
+++ b/models/Legacy_examples/Example53_First_Responder.mp
@@ -0,0 +1,59 @@
+/* A first responder scenario involving the administation of a rescue
+medication (Narcan) to an overdose victim by a First Responder or a
+Bystander.
+
+Create by J. Bryant, May 2016
+
+The model was developed to compare response times, but unexpected
+scenarios emerged that was previously not considered. Trace 6 and others
+show a double administration of Narcan by both the bystander and the first
+responder.
+
+*/
+
+SCHEMA Narcan_Administration
+
+ROOT OverdoseVictim:
+ overdose_on_and_opioid
+ (breathing_is_supressed | stops_breathing)
+ lose_consiousness
+ receives_Narcan
+ (recovers_in_hospital | dies);
+
+ROOT Bystander:
+ takes_notice
+
+ (call_911|have_another_bystander_call_911)
+
+ (Carrying_Narcan | Not_Carrying_Narcan);
+ Carrying_Narcan:
+ administer_Narcan_while_on_line;
+ Not_Carrying_Narcan:
+ follow_the_operators_instructions;
+
+ROOT FirstResponder:
+ receives_911_call
+ responds_to_scene
+
+ (Narcan_was_administered|Narcan_was_not_administered);
+ Narcan_was_administered:
+ get_the_patient_to_hospital;
+ Narcan_was_not_administered:
+ administer_Narcan
+ get_the_patient_to_hospital;
+
+COORDINATE
+ $a:(administer_Narcan_while_on_line | Narcan_was_administered) FROM Bystander,
+ $b:receives_Narcan FROM OverdoseVictim
+ DO ADD $a PRECEDES $b; OD;
+
+
+COORDINATE
+ $a:(call_911|have_another_bystander_call_911) FROM Bystander,
+ $b:receives_911_call FROM FirstResponder
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE
+ $a:get_the_patient_to_hospital FROM FirstResponder,
+ $b:recovers_in_hospital FROM OverdoseVictim
+ DO ADD $a PRECEDES $b; OD;
diff --git a/models/Legacy_examples/Example54_Unmanned_Spacecraft_Comms.mp b/models/Legacy_examples/Example54_Unmanned_Spacecraft_Comms.mp
new file mode 100644
index 0000000000000000000000000000000000000000..710b2de7af357fa04c29451b6c228a478470eb5e
--- /dev/null
+++ b/models/Legacy_examples/Example54_Unmanned_Spacecraft_Comms.mp
@@ -0,0 +1,60 @@
+/* Heartbeat.mp
+October 4, 2015
+Created by: C. Nelson
+
+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.
+
+Run for scope 1 and up.
+
+*/
+
+/*—————————————————————————————
+ Actors
+———————————————————————————————*/
+
+SCHEMA Heartbeat
+
+ROOT Spacecraft: Receive_Heartbeat
+ (+ Echo_Heartbeat
+ Receive_Incremented_Heartbeat
+ Compare_Received_Heartbeat_Values
+ ( SC_HB_Valid | SC_HB_Invalid ) +);
+
+ SC_HB_Valid: ( Continue_Approach | Switch_to_Redundant_Comm_System );
+
+ SC_HB_Invalid: Abort_Operations;
+
+
+ROOT ISS: Generate_Heartbeat
+ Send_Heartbeat
+ (+ Receive_Echoed_Heartbeat
+ Increment_Heartbeat Send_Incremented_Heartbeat
+ Compare_Sent_and_Received_HB
+ ( HB_Valid | HB_Invalid ) +);
+
+ HB_Valid: ( Continue_Approach | Abort_Operations );
+
+ HB_Invalid: ( Switch_to_Redundant_Comm_System | Abort_Operations );
+
+/*—————————————————————————————
+ Interactions
+———————————————————————————————*/
+
+ISS, Spacecraft SHARE ALL Abort_Operations,
+ Switch_to_Redundant_Comm_System,
+ Continue_Approach;
+
+COORDINATE $a: Send_Heartbeat FROM ISS,
+ $b: Receive_Heartbeat FROM Spacecraft
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Echo_Heartbeat FROM Spacecraft,
+ $b: Receive_Echoed_Heartbeat FROM ISS
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Send_Incremented_Heartbeat FROM ISS,
+ $b: Receive_Incremented_Heartbeat FROM Spacecraft
+ DO ADD $a PRECEDES $b; OD;
diff --git a/models/Legacy_examples/Example55_UAV_Ingress.mp b/models/Legacy_examples/Example55_UAV_Ingress.mp
new file mode 100644
index 0000000000000000000000000000000000000000..9d7d5db3f7ee6f3dc00e437f1069522c34450c49
--- /dev/null
+++ b/models/Legacy_examples/Example55_UAV_Ingress.mp
@@ -0,0 +1,114 @@
+/*******************************************************************
+
+UAV HADR Mission
+
+The following 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.
+
+This model contains an unexpected behavior in which the UAV status
+is acceptable but the operator aborts the ingress (trace 2).
+
+ created by A. Constable May 2017
+
+********************************************************************/
+
+
+SCHEMA UAV_Ingress
+
+/*-----------------------
+ JTF C2
+-------------------------*/
+
+ROOT JTF_C2: Provide_launch_command;
+
+
+/*-----------------------
+ GCS OPERATOR
+-------------------------*/
+
+ROOT GCS_Operator: (* Receive_launch_command
+ Check_launch_parameters_for_safety
+ Recieve_launch_clearence_from_host_ship
+ Provide_launch_command
+ Receive_UAV_status_and_position
+ Assess_UAV_status_and_position
+ Status_acceptable
+ (Command_UAV_to_proceed_on_ingress
+ Receive_UAV_position |
+ Command_UAV_abort)
+ *);
+
+
+/*-----------------------
+ GROUND CREW
+-------------------------*/
+
+ROOT Ground_Crew: (* Receive_launch_command
+ Provide_launch_command
+ *);
+
+
+/*-----------------------
+ UAV
+-------------------------*/
+
+ROOT UAV: (* Receive_launch_command
+ Launch
+ Execute_climb
+ Maneuver_to_clear_obstacles
+ Maneuver_to_ingress_altitude
+ Level_off_at_ingress_altitude
+ Transmit_status_and_position
+ (Receive_command_to_proceed
+ Follow_flight_path_to_reach_onstation_area_and_altitude
+ Reach_onstation_waypoint
+ Report_status |
+ Receive_command_to_abort
+ Abort_mission)
+ Apply_status_decision
+ *);
+
+
+/*-----------------------
+ NAV REFERENCE
+-------------------------*/
+
+ROOT Navigation_Reference: ;
+
+
+
+/*---------------------------------------------
+ COORDINATION
+-----------------------------------------------*/
+
+COORDINATE $a: Provide_launch_command FROM JTF_C2,
+ $b: Receive_launch_command FROM GCS_Operator
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Provide_launch_command FROM GCS_Operator,
+ $b: Receive_launch_command FROM Ground_Crew
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Provide_launch_command FROM Ground_Crew,
+ $b: Receive_launch_command FROM UAV
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Transmit_status_and_position FROM UAV,
+ $b: Receive_UAV_status_and_position FROM GCS_Operator
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Command_UAV_to_proceed_on_ingress FROM GCS_Operator,
+ $b: Receive_command_to_proceed FROM UAV
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Command_UAV_abort FROM GCS_Operator,
+ $b: Receive_command_to_abort FROM UAV
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Report_status FROM UAV,
+ $b: Receive_UAV_position FROM GCS_Operator
+ DO ADD $a PRECEDES $b; OD;
+
+
+
diff --git a/models/Legacy_examples/Example56_Small_Package_Delivery.mp b/models/Legacy_examples/Example56_Small_Package_Delivery.mp
new file mode 100644
index 0000000000000000000000000000000000000000..578f4d30360565601b1893a84ebe5cca0ab0114d
--- /dev/null
+++ b/models/Legacy_examples/Example56_Small_Package_Delivery.mp
@@ -0,0 +1,208 @@
+/* Small Package Delivery
+
+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?"
+
+Non-combatant Scenario 1 authored by N. Roberts (Engility)
+MP model authored by K. Giammarco (NPS) and D. Shifflett (NPS)
+
+This model shows only two scenarios due to overloading constraints
+(constraints that suppress entire branches of execution that a user
+intended to permit).
+
+Removing everything except the SCHEMA definition and the Air_Vehicle
+root (line 36 and lines 114-128) and running that model subset, one can
+see 6 event traces, one of which is unexpected: the Air_Vehicle drops
+the payload with no vessel in sight (trace 6).
+
+*/
+
+SCHEMA Small_Package_Delivery
+
+
+/*-----------------------
+ RESCUEE BEHAVIORS
+-------------------------*/
+ROOT Rescuee: { Victim, EPIRB };
+
+ Victim: ( Receive_Payload
+ Emergency_Averted |
+ Payload_Not_Received
+ Diabetic_Coma );
+
+ EPIRB:;
+
+
+/*-----------------------------
+ MISSION COMMANDER BEHAVIORS
+-------------------------------*/
+ROOT Mission_Commander: ( Confirm_Vessel
+ ( Confirms_Drop_via_Video_Feed |
+
+ Confirms_Payload_Misses_Target ) |
+
+ Confirm_Not_Found )
+ Authorized_UAV_Return;
+
+
+
+/*-----------------------------
+ UAV OPERATOR BEHAVIORS
+-------------------------------*/
+ROOT UAV_Operator: [ Command_UAV_To_Drop_Payload ]
+ [ Release_UAV_to_Second_Location ]
+ Command_UAV_Return
+ Transfer_to_LOS_Communication
+ Command_UAV_to_Land
+ Turn_Off_UAV;
+
+/***INTERACTIONS***/
+
+COORDINATE $a: Confirm_Vessel FROM Mission_Commander,
+ $b: Command_UAV_To_Drop_Payload FROM UAV_Operator
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: ( Confirms_Drop_via_Video_Feed |
+ Confirms_Payload_Misses_Target ) FROM Mission_Commander,
+ $b: Release_UAV_to_Second_Location FROM UAV_Operator
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Authorized_UAV_Return FROM Mission_Commander,
+ $b: Command_UAV_Return FROM UAV_Operator
+ DO ADD $a PRECEDES $b; OD;
+
+
+
+/*-----------------------------
+ INMARSAT BEHAVIORS
+-------------------------------*/
+ROOT INMARSAT: Relay_Data_and_Comm_UAV_Communication;
+
+
+
+/*-----------------------------
+ Control Station BEHAVIORS
+-------------------------------*/
+ROOT Control_Station: Receive_Video;
+
+
+/***INTERACTIONS***/
+
+COORDINATE $a: Receive_Video FROM Control_Station,
+ $b: ( Confirm_Vessel | Confirm_Not_Found ) FROM Mission_Commander
+ DO ADD $a PRECEDES $b; OD;
+
+
+/*-----------------------------
+ Air Vehicle BEHAVIORS
+-------------------------------*/
+ROOT Air_Vehicle: Start_GPS_Navigation
+ Transit_to_Mission_Location
+ Detect_Beacon
+ ( <<0.90>> Locate_Vessel
+ Holds_over_Vessel |
+ <<0.10>> Vessel_Not_Found )
+ Transmit_Video
+ [ Receive_Command
+ Drop_Payload
+ ( <<0.98>> Payload_on_Target |
+ <<0.02>> Payload_Misses_Target )
+ ]
+
+ Return_to_Hold_Point
+ Shut_Down;
+
+
+/***INTERACTIONS***/
+
+COORDINATE $a: Relay_Data_and_Comm_UAV_Communication FROM INMARSAT,
+ $b: Start_GPS_Navigation FROM Air_Vehicle
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Transmit_Video FROM Air_Vehicle,
+ $b: Receive_Video FROM Control_Station
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Command_UAV_To_Drop_Payload FROM UAV_Operator,
+ $b: Receive_Command FROM Air_Vehicle
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Payload_on_Target FROM Air_Vehicle,
+ $b: Receive_Payload FROM Rescuee
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Payload_on_Target FROM Air_Vehicle,
+ $b: Confirms_Drop_via_Video_Feed FROM Mission_Commander
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Payload_Misses_Target FROM Air_Vehicle,
+ $b: Payload_Not_Received FROM Rescuee
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Payload_Misses_Target FROM Air_Vehicle,
+ $b: Confirms_Payload_Misses_Target FROM Mission_Commander
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Command_UAV_Return FROM UAV_Operator,
+ $b: Return_to_Hold_Point FROM Air_Vehicle
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Return_to_Hold_Point FROM Air_Vehicle,
+ $b: Transfer_to_LOS_Communication FROM UAV_Operator
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Turn_Off_UAV FROM UAV_Operator,
+ $b: Shut_Down FROM Air_Vehicle
+ DO ADD $a PRECEDES $b; OD;
+
+
+/***CONSTRAINTS***/
+
+ENSURE #Locate_Vessel > 0 -> #Confirm_Vessel > 0;
+
+ENSURE #Vessel_Not_Found > 0 -> #Confirm_Not_Found > 0;
+
+
+/*-------------------------------------
+ Launch and Recovery System BEHAVIORS
+---------------------------------------*/
+
+ROOT Launch_and_Recovery_System: { UCARS, RAST };
+
+ UCARS: Guide_UAV_To_Landing;
+
+ RAST: Grab_UAV;
+
+
+/***INTERACTIONS***/
+
+COORDINATE $a: Command_UAV_to_Land FROM UAV_Operator,
+ $b: Guide_UAV_To_Landing FROM Launch_and_Recovery_System
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Guide_UAV_To_Landing FROM Launch_and_Recovery_System,
+ $b: Grab_UAV FROM Launch_and_Recovery_System
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Grab_UAV FROM Launch_and_Recovery_System,
+ $b: Turn_Off_UAV FROM UAV_Operator
+ DO ADD $a PRECEDES $b; OD;
+
diff --git a/models/Legacy_examples/Example57_Authentication.mp b/models/Legacy_examples/Example57_Authentication.mp
new file mode 100644
index 0000000000000000000000000000000000000000..c9b6910a2f419ed793249dc98cedc1ad1e6efb93
--- /dev/null
+++ b/models/Legacy_examples/Example57_Authentication.mp
@@ -0,0 +1,56 @@
+/*******************************************************************************
+
+A Model for Simple Authentication
+
+A demonstration that shows how to reject unwanted behaviors with ENSURE
+constraints.
+
+ created by K.Giammarco on 05/16/2017
+ modified by K.Giammarco on 08/07/2017 for capitalization of state events
+ modified by K.Giammarco on 08/07/2017 for ENSURE constraints
+
+********************************************************************************/
+
+SCHEMA Authentication
+
+/*-----------------------
+ USER BEHAVIORS
+-------------------------*/
+
+ROOT User: Provide_credentials
+ (* CREDS_INVALID Reenter_credentials *)
+ [ CREDS_VALID Access_system ];
+
+/*-----------------------
+ SYSTEM BEHAVIORS
+-------------------------*/
+
+ROOT System: Verify_credentials
+ (+ ( CREDS_INVALID Deny_access |
+ CREDS_VALID Grant_access ) +)
+ [ Lock_account ]
+ ;
+
+/*-----------------------
+ INTERACTION CONSTRAINTS
+-------------------------*/
+
+User, System SHARE ALL CREDS_VALID, CREDS_INVALID;
+
+COORDINATE $a: Provide_credentials FROM User,
+ $b: Verify_credentials FROM System
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Deny_access FROM System,
+ $b: Reenter_credentials FROM User
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Grant_access FROM System,
+ $b: Access_system FROM User
+ DO ADD $a PRECEDES $b; OD;
+
+ENSURE #CREDS_INVALID <= 3;
+
+ENSURE #Deny_access >= 3 <-> #Lock_account == 1;
+
+ENSURE #Grant_access >= 1 -> #Lock_account == 0;
\ No newline at end of file
diff --git a/models/Legacy_examples/Example58_UAV_OnStation.mp b/models/Legacy_examples/Example58_UAV_OnStation.mp
new file mode 100644
index 0000000000000000000000000000000000000000..b0a4843a6de5b0aa90def20feb3aee5dea139043
--- /dev/null
+++ b/models/Legacy_examples/Example58_UAV_OnStation.mp
@@ -0,0 +1,148 @@
+/*********************************************************************************************
+
+A Model for an Unmanned Aerial Vehicle in the OnStation Phase of an ISR Mission
+
+Demonstrates use of concurrent events within a root and annotations with
+SAY and MARK
+
+"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
+
+ created by K.Giammarco on 02-03-2017
+ modified by K.Giammarco on 02-04-2017 to remove normal events from failure mode scenarios
+ modified by K.Giammarco on 02-05-2017 to add normal events back to failure mode scenarios
+ and added annotations
+
+*********************************************************************************************/
+
+
+SCHEMA UAV_OnStation
+
+
+/*-----------------------
+ GCS OPERATOR MODEL
+-------------------------*/
+
+ROOT GCS_Operator: (+ Receive_status
+ [ Receive_UAV_video ]
+ [ Assess_target
+ ( Target_is_not_of_interest Command_to_resume_search |
+
+ Target_is_of_Interest Command_target_monitoring ) ]
+ [ Receive_bingo_fuel_status_message ]
+ +)
+ Command_end_of_mission End_search;
+
+
+/*------------------------------------------------------------------
+ UAV MODEL
+--------------------------------------------------------------------*/
+
+ROOT UAV: /*Reach_OnStation_area*/
+
+ { Stream_video, Search, Monitor_status };
+
+ Stream_video: (* Send_UAV_video *);
+
+ Search: Follow_search_pattern
+ (* ( Target_detected
+ Send_target_info
+ ( Resume_search_pattern |
+
+ Monitor_target ) |
+
+ No_target_detected Continue_search )
+ *)
+
+ End_search;
+
+ Monitor_status: ( Health_normal [ Detect_bingo_fuel ] |
+ Failure_mode Failsafe_behavior );
+
+
+/*-----------------------
+ ENVIRONMENT MODEL
+-------------------------*/
+
+ROOT Environment: (* Present_target_signature *);
+
+
+/*-----------------------
+ INTERACTIONS
+-------------------------*/
+
+UAV, GCS_Operator SHARE ALL End_search;
+
+COORDINATE $a: ( Health_normal | Failure_mode ) FROM UAV,
+ $b: Receive_status FROM GCS_Operator
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Send_UAV_video FROM UAV,
+ $b: Receive_UAV_video FROM GCS_Operator
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Send_target_info FROM UAV,
+ $b: Assess_target FROM GCS_Operator
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Command_to_resume_search FROM GCS_Operator,
+ $b: Resume_search_pattern FROM UAV
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Command_target_monitoring FROM GCS_Operator,
+ $b: Monitor_target FROM UAV
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Detect_bingo_fuel FROM UAV,
+ $b: Receive_bingo_fuel_status_message FROM GCS_Operator
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Present_target_signature FROM Environment,
+ $b: ( Target_detected | No_target_detected ) FROM UAV
+ DO ADD $a PRECEDES $b; OD;
+
+/*-----------------------
+ GENERAL CONSTRAINTS
+-------------------------*/
+
+ENSURE #Health_normal > 0 -> #Send_UAV_video > 0;
+
+
+/*-----------------------
+ ANNOTATIONS
+-------------------------*/
+
+COORDINATE $s: Stream_video
+
+ DO IF #Send_UAV_video IN $s == 0 THEN MARK;
+ FI;
+ OD;
+
+IF #Health_normal > 0 THEN
+ SAY("UAV health was normal");
+FI;
+
+IF #Failure_mode > 0 THEN
+ SAY("UAV had a failure mode");
+FI;
+
+IF #Send_UAV_video == 0 THEN
+ SAY("No streaming video");
+FI;
+
+IF #Detect_bingo_fuel > 0 THEN
+ SAY("UAV had bingo fuel condition");
+FI;
+
+IF #Monitor_target > 0 THEN
+ SAY("Target of interest was detected");
+FI;
+
+IF #Resume_search_pattern > 0 THEN
+ SAY("Target was not mission-related");
+FI;
+
+IF #No_target_detected > 0 THEN
+ SAY("UAV missed a target signature");
+FI;
diff --git a/models/Legacy_examples/Example59_Cycle_Pattern.mp b/models/Legacy_examples/Example59_Cycle_Pattern.mp
new file mode 100644
index 0000000000000000000000000000000000000000..8d75d0f4292bc25b24a8237c9ab0f2a8f9832482
--- /dev/null
+++ b/models/Legacy_examples/Example59_Cycle_Pattern.mp
@@ -0,0 +1,57 @@
+/***************************************
+ 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
+
+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
+discinyms (discipline-specific synonyms) as they
+may appear in the preferred domain taxonomy.
+
+Run the model for scopes 2, and 3 and inspect
+the different possible patterns for Cycle.
+Running at scope 1 will generate zero traces because
+of the ENSURE constraint on line 29.
+
+****************************************/
+
+SCHEMA Cycle_ISP_v2
+
+ROOT Cycle: (+ Initial_condition
+ (+ ( Step_forward | Step_backward ) +)
+ End_condition +);
+
+ENSURE #( Step_forward | Step_backward ) > 1;
+
+
+
+/*Check for Positive Reinforcement Template */
+IF EXISTS DISJ $a: Step_forward, $b: Step_forward
+ $a PRECEDES $b THEN
+ SAY("Positive Reinforcement Detected"); FI;
+
+/*Check for Negative Reinforcement Template */
+IF EXISTS DISJ $a: Step_backward, $b: Step_backward
+ $a PRECEDES $b THEN
+ SAY("Negative Reinforcement Detected"); FI;
+
+/*Check for Oscillation Template */
+IF EXISTS $a: Step_forward, $b: Step_backward
+ $a PRECEDES $b OR
+ $b PRECEDES $a THEN
+ SAY("Oscillation Detected"); FI;
+
+/*Note Lifecycle Completion */
+COORDINATE $a: End_condition
+ DO ADD SAY("Lifecycle Complete") PRECEDES $a; OD;
+
+/*Check for Recycle Template */
+IF #Initial_condition > 1 THEN
+ SAY("Recycle Detected"); FI;
+
+
diff --git a/models/Legacy_examples/Example60_Surgery.mp b/models/Legacy_examples/Example60_Surgery.mp
new file mode 100644
index 0000000000000000000000000000000000000000..624cc75c1045624d994b5a39bee607b7274e9c43
--- /dev/null
+++ b/models/Legacy_examples/Example60_Surgery.mp
@@ -0,0 +1,86 @@
+/* Surgery example
+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.
+"Identifying decision patterns using Monterey Phoenix" by Quartuccio, John,
+Kristin Giammarco, and Mikhail Auguston.
+Available at https://ieeexplore.ieee.org/abstract/document/7994952
+
+Created by: J. Quartuccio (2017)
+Naval Postgraduate School
+*/
+
+/*Actors*/
+SCHEMA Surgery
+
+ROOT Physician: Routine_procedure
+ Perception
+ Leadership_context
+ Decision;
+
+ Perception: ( Recognize_environment |
+ Not_recognize_environment );
+
+ Leadership_context: ( Receive_input |
+ Not_receive_input );
+ Decision: ( Correct_decision |
+ Incorrect_decision );
+
+ROOT Nurses: {+ Nurse +};
+
+ Nurse: Routine_procedure
+ Perception
+ Communication;
+
+ Communication: ( Communicate_observation |
+ Not_communicate_observation );
+
+ROOT Environment: Routine_procedure
+ Problem_state
+ Outcome_state;
+
+ Problem_state: ( Problem |
+ No_problem );
+
+ Outcome_state: ( Successful_outcome |
+ Failed_outcome );
+
+/*Interactions*/
+
+COORDINATE
+$a: Leadership_context FROM Physician
+DO COORDINATE
+$b: ( Communicate_observation
+| Not_communicate_observation ) FROM Nurses
+DO ADD $b PRECEDES $a; OD;
+OD;
+
+COORDINATE
+$a: Decision FROM Physician,
+$b: Outcome_state FROM Environment
+DO ADD $a PRECEDES $b; OD;
+
+Physician, Nurses, Environment SHARE ALL Routine_procedure;
+
+ENSURE (#No_problem FROM Environment == 1 ->
+#Successful_outcome
+FROM Environment == 1);
+
+ENSURE(#Not_communicate_observation FROM
+Nurses - #Nurse == 0 ->
+#Not_receive_input FROM Physician == 1);
+
+ENSURE(#Recognize_environment FROM Physician
+- #Not_receive_input == 0 ->
+#Correct_decision == 1);
+
+ENSURE (#Receive_input FROM Physician == 1 ->
+#Correct_decision FROM Physician == 1);
+ENSURE (#Not_receive_input FROM Physician == 1 ->
+#Incorrect_decision FROM Physician == 1);
+
+ENSURE (#Correct_decision FROM Physician == 1 ->
+#Successful_outcome FROM Environment
+==1);
+ENSURE (#Incorrect_decision FROM Physician == 1 ->
+#Failed_outcome FROM Environment ==1);
\ No newline at end of file
diff --git a/models/Legacy_examples/Example61_Spent_Fuel_Cooling_and_Cleanup.mp b/models/Legacy_examples/Example61_Spent_Fuel_Cooling_and_Cleanup.mp
new file mode 100644
index 0000000000000000000000000000000000000000..de834307bf8ff094a53a2febec99c72c546df38c
--- /dev/null
+++ b/models/Legacy_examples/Example61_Spent_Fuel_Cooling_and_Cleanup.mp
@@ -0,0 +1,203 @@
+/* Cooling Pool
+
+created by K.Giammarco 5/4/2020
+modified by K.Giammarco 5/8/2020 with D.VanBossuyt
+modified by K.Giammarco 5/13/2020 with D.VanBossuyt
+
+The purpose of this model is to identify the components of and
+interactions among a spent nuclear fuel cooling pool and its environment.
+
+*/
+
+
+/*—————————————————————————————
+ Actors
+———————————————————————————————*/
+SCHEMA Spent_Fuel_Cooling_and_Cleanup_System
+
+
+ROOT External_Systems: { Operator, Ext_Cooling_Loop };
+
+
+ Operator: Monitor_Spent_Fuel_Pool;
+
+ Monitor_Spent_Fuel_Pool: [ Receive_Low_Water_Alert ]
+ [ Receive_Critically_Low_Water_Alarm ]
+ [ Receive_High_Temperature_Alarm ]
+ ;
+
+
+ Ext_Cooling_Loop: Supply_Cold_Water
+ Remove_Warm_Water;
+
+
+ROOT Heat_Exchanger: Remove_Decay_Heat;
+
+
+ROOT Cooling_Loop: Pump_Pool_Water_into_Cooling_Loop
+ Deliver_Pool_Water_to_Heat_Exchanger
+ Return_Pool_Water_to_Cooling_Pool;
+
+
+ROOT Spent_Fuel_Pool: Store_Spent_Fuel_Rods
+ { Circulate_Water_for_Cooling,
+ Circulate_Water_for_Cleanup,
+ Monitor_Pool_Water
+ };
+
+ Circulate_Water_for_Cooling: Provide_Heated_Water_for_Cooling
+ Accept_Cooled_Pool_Water;
+
+ Circulate_Water_for_Cleanup: Provide_Radioactive_Water_for_Cleanup
+ Accept_Cleaned_Pool_Water;
+
+ Monitor_Pool_Water: ( Water_Level_Normal |
+
+ Water_Level_Low
+ Notify_Operator_Low_Water
+ Accept_Low_Volume_Makeup_Water
+
+ [ Water_Level_Critically_Low
+ Notify_Operator_Critically_Low_Water
+ Accept_High_Volume_Makeup_Water ] )
+
+ ( Temperature_Normal |
+ Temperature_High
+ Notify_Operator_High_Temperature )
+ ;
+
+
+ROOT Purification_Subsystem: { Purification_Loop, Water_Make_Up_System };
+
+ Purification_Loop: Pump_Pool_Water_into_Purification_Subsystem
+ Filter_Pool_Water
+ Demineralize_Pool_Water
+ Return_Pool_Water;
+
+ Water_Make_Up_System: [ Add_Water ];
+
+
+
+ROOT Emergency_Water_Tank: [ Add_Water ];
+
+
+/*—————————————————————————————
+ Interactions
+———————————————————————————————*/
+
+COORDINATE $a: Store_Spent_Fuel_Rods FROM Spent_Fuel_Pool,
+ $b: Circulate_Water_for_Cooling FROM Spent_Fuel_Pool,
+ $c: Circulate_Water_for_Cleanup FROM Spent_Fuel_Pool,
+ $d: Monitor_Pool_Water FROM Spent_Fuel_Pool
+
+ DO ADD $a radioactive_particles $b;
+ ADD $a thermal_energy $b;
+ ADD $a radioactive_particles $c;
+ ADD $a thermal_energy $c;
+ ADD $a radioactive_particles $d;
+ ADD $a thermal_energy $d;
+OD;
+
+
+COORDINATE $a: Provide_Heated_Water_for_Cooling FROM Spent_Fuel_Pool,
+ $b: Pump_Pool_Water_into_Cooling_Loop FROM Cooling_Loop
+ DO ADD $a PRECEDES $b;
+ ADD $a hot_radioactive_pool_water $b;
+ OD;
+
+
+COORDINATE $a: Deliver_Pool_Water_to_Heat_Exchanger FROM Cooling_Loop,
+ $b: Remove_Decay_Heat FROM Heat_Exchanger
+ DO ADD $a PRECEDES $b;
+ ADD $a hot_radioactive_pool_water $b;
+ OD;
+
+
+COORDINATE $a: Supply_Cold_Water FROM External_Systems,
+ $b: Remove_Decay_Heat FROM Heat_Exchanger,
+ $c: Remove_Warm_Water FROM External_Systems
+ DO ADD $a PRECEDES $b;
+ ADD $b PRECEDES $c;
+ ADD $a cold_water $b;
+ ADD $b hot_water $c;
+OD;
+
+
+
+COORDINATE $a: Provide_Radioactive_Water_for_Cleanup FROM Spent_Fuel_Pool,
+ $b: Pump_Pool_Water_into_Purification_Subsystem FROM Purification_Subsystem
+ DO ADD $a PRECEDES $b;
+ ADD $a hot_radioactive_pool_water $b;
+OD;
+
+
+
+COORDINATE $a: Remove_Decay_Heat FROM Heat_Exchanger,
+ $b: Return_Pool_Water_to_Cooling_Pool FROM Cooling_Loop
+ DO ADD $a PRECEDES $b;
+ ADD $a cooled_radioactive_pool_water $b;
+OD;
+
+
+COORDINATE $a: Return_Pool_Water_to_Cooling_Pool FROM Cooling_Loop,
+ $b: Accept_Cooled_Pool_Water FROM Spent_Fuel_Pool
+ DO ADD $a PRECEDES $b;
+ ADD $a cooled_radioactive_pool_water $b;
+ OD;
+
+
+COORDINATE $a: Return_Pool_Water FROM Purification_Subsystem,
+ $b: Accept_Cleaned_Pool_Water FROM Spent_Fuel_Pool
+ DO ADD $a PRECEDES $b;
+ ADD $a hot_cleaned_pool_water $b;
+ OD;
+
+
+/* If Water Level Low */
+
+COORDINATE $a: Water_Level_Low FROM Spent_Fuel_Pool,
+ $b: Add_Water FROM Purification_Subsystem
+ DO ADD $a PRECEDES $b;
+ ADD $a set_point_1_trigger $b;
+
+ OD;
+
+COORDINATE $a: Notify_Operator_Low_Water FROM Spent_Fuel_Pool,
+ $b: Receive_Low_Water_Alert FROM External_Systems
+ DO ADD $a PRECEDES $b;
+ ADD $a set_point_1_alert $b;
+ OD;
+
+
+COORDINATE $a: Water_Level_Critically_Low FROM Spent_Fuel_Pool,
+ $b: Add_Water FROM Emergency_Water_Tank
+ DO ADD $a PRECEDES $b;
+ ADD $a set_point_2_trigger $b;
+ OD;
+
+COORDINATE $a: Notify_Operator_Critically_Low_Water FROM Spent_Fuel_Pool,
+ $b: Receive_Critically_Low_Water_Alarm FROM External_Systems
+ DO ADD $a PRECEDES $b;
+ ADD $a set_point_2_alarm $b;
+ OD;
+
+
+COORDINATE $a: Add_Water FROM Purification_Subsystem,
+ $b: Accept_Low_Volume_Makeup_Water FROM Spent_Fuel_Pool
+ DO ADD $a PRECEDES $b;
+ ADD $a clean_cool_water $b;
+ OD;
+
+
+COORDINATE $a: Add_Water FROM Emergency_Water_Tank,
+ $b: Accept_High_Volume_Makeup_Water FROM Spent_Fuel_Pool
+ DO ADD $a PRECEDES $b;
+ ADD $a clean_cool_water $b;
+ OD;
+
+
+COORDINATE $a: Notify_Operator_High_Temperature FROM Spent_Fuel_Pool,
+ $b: Receive_High_Temperature_Alarm FROM External_Systems
+ DO ADD $a PRECEDES $b;
+ ADD $a high_temp_alarm $b;
+ OD;
diff --git a/models/Legacy_examples/Example62_Prisoners_Dilemma.mp b/models/Legacy_examples/Example62_Prisoners_Dilemma.mp
new file mode 100644
index 0000000000000000000000000000000000000000..c9e7f0a5a7954584c82e333cf091311aed42827d
--- /dev/null
+++ b/models/Legacy_examples/Example62_Prisoners_Dilemma.mp
@@ -0,0 +1,86 @@
+/* The Prisoner's Dilemma
+Michael Collins
+August 10, 2020.
+https://en.wikipedia.org/wiki/Prisoner%27s_dilemma
+https://plato.stanford.edu/entries/prisoner-dilemma/#Symm2t2PDOrdiPayo
+
+In this case, the classic model is the output in the traces
+of the model with the payouts as documented in
+"Game Theory and Strategy" by Philip D. Straffin
+Mathematical Association of America 1993
+isbn: 0-88385-637-9
+Chapter 12, page 73.
+
+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,
+is computed from
+"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.
+
+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
+from different stores.
+
+A related version of the prisoners dilemma to shopping is
+documented at the Wikipedia article cited above. "The donation game."
+
+This model is only meant to be run at scope 1.
+
+From Alice's viewpoint: (in this case the selfish view point).
+the payoff for Alice when she confesses = 1.
+the payoff for Alice when Bob does not confess = 2.
+in all other circumstances the payoff for Alice = 0.
+
+From Bob's viewpoint: (in this case the selfish view point)
+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.
+
+*/
+
+
+/*—————————————————————————————
+ Actors
+———————————————————————————————*/
+SCHEMA Prisoners_Dilemma
+
+ATTRIBUTES { number utility1, utility2, payout_alice, payout_bob ;};
+
+
+do_not_confess_alice: BUILD{ utility1:= 0 ; utility2:= 2 ;};
+confess_alice: BUILD{ utility1:= 1 ; utility2:= 0 ;};
+do_not_confess_bob : BUILD{ utility1:= 2 ; utility2:= 0 ;};
+confess_bob: BUILD{ utility1:= 0 ; utility2:= 1 ;};
+
+
+ROOT Alice: ( do_not_confess_alice | confess_alice );
+
+ROOT Bob: ( do_not_confess_bob | confess_bob );
+
+payout_alice:= SUM{ $act:( do_not_confess_alice | confess_alice | do_not_confess_bob | confess_bob ) APPLY $act.utility1 } - 2 ;
+payout_bob := SUM{ $act:( do_not_confess_alice | confess_alice | do_not_confess_bob | confess_bob ) APPLY $act.utility2 } - 2 ;
+
+
+/*—————————————————————————————
+ Interactions
+———————————————————————————————*/
+SAY( "Payout Alice = " payout_alice);
+SAY( "Payout Bob = " payout_bob );
\ No newline at end of file
diff --git a/models/Legacy_examples/Example63_Find_Advisor.mp b/models/Legacy_examples/Example63_Find_Advisor.mp
new file mode 100644
index 0000000000000000000000000000000000000000..dfd51aee5a9d74b131abb4ef77bc1ca188c6ea98
--- /dev/null
+++ b/models/Legacy_examples/Example63_Find_Advisor.mp
@@ -0,0 +1,65 @@
+/* example63_Find_Advisor.mp
+ modeling human interactions
+
+Human interaction and organizational processes can be modeled as well as technological
+system and subsystem interactions.
+
+In this example, the process of a student finding an advisor for a potentially
+MP-related research topic is modeled. Alternate behaviors for humans are described in
+terms of possible decisions they could make.
+
+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.
+
+Run for scope 1 (there is no iteration in this example, so increaasing the scope will not
+produce more scenarios).
+
+The "Sequence" or "Swim Lanes" layouts are the most appropriate for browsing traces here.
+The "Sequence" mode yields views very similar to the UML or SysML Sequence Diagrams.
+
+*/
+
+
+/*—————————————————————————————
+ Actors
+———————————————————————————————*/
+SCHEMA FindAdvisor
+
+ROOT Student: Hear_about_MP
+ Get_intrigued
+ Check_out_website
+ Try_out_MP_modeling
+ ( Like_MP | Decide_MP_not_for_me );
+
+ Like_MP: Email_Advisor
+ Discuss_research_interests
+ ( Do_an_awesome_MP_project | Find_another_approach );
+
+ROOT Advisor: ( Set_up_meeting
+ Discuss_research_interests
+ ( Assess_MP_as_a_good_fit Advise_an_awesome_MP_project |
+ Recommend_another_approach ) |
+ Does_something_else );
+
+/*—————————————————————————————
+ Interactions
+———————————————————————————————*/
+
+COORDINATE $a: Email_Advisor FROM Student,
+ $b: Set_up_meeting FROM Advisor
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Discuss_research_interests FROM Student,
+ $b: ( Assess_MP_as_a_good_fit | Recommend_another_approach ) FROM Advisor
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Assess_MP_as_a_good_fit FROM Advisor,
+ $b: Do_an_awesome_MP_project FROM Student
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Recommend_another_approach FROM Advisor,
+ $b: Find_another_approach FROM Student
+ DO ADD $a PRECEDES $b; OD;
+
+Student, Advisor SHARE ALL Discuss_research_interests;
\ No newline at end of file
diff --git a/models/Legacy_examples/x_Default_Example_Beginner_Use_of_MP.mp b/models/Legacy_examples/x_Default_Example_Beginner_Use_of_MP.mp
new file mode 100644
index 0000000000000000000000000000000000000000..3f610381547febae925d6287c78eef0813bd955e
--- /dev/null
+++ b/models/Legacy_examples/x_Default_Example_Beginner_Use_of_MP.mp
@@ -0,0 +1,89 @@
+/* A Simple Model of Beginner MP-Firebird Use
+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.
+
+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
+
+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
+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. */
+
+
+SCHEMA Beginner_Use_of_MP
+
+
+/* Actor Behaviors */
+
+ROOT User: ( Import_existing_model |
+
+ Define_problem_of_interest
+ Create_new_MP_model
+ Save_model )
+
+ Run_the_model
+ Inspect_scenarios
+ (* Find_issue
+ Edit_MP_model
+ Save_model_copy
+ Rerun_the_model
+ Reinspect_scenarios *)
+
+ Find_all_scenarios_acceptable;
+
+
+ROOT MP_Firebird_Tool: { User_Interface, NPS_Server };
+
+ User_Interface:
+ (* Receive_run_command
+ Send_model_for_processing
+ Display_scenarios *);
+
+ NPS_Server: (* Generate_scenarios
+ Send_scenarios *);
+
+
+/* Interactions */
+
+COORDINATE $a: ( Run_the_model | Rerun_the_model ),
+ $b: Receive_run_command
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Send_model_for_processing, $b: Generate_scenarios
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Send_scenarios, $b: Display_scenarios
+ DO ADD $a PRECEDES $b; OD;
+
+COORDINATE $a: Display_scenarios,
+ $b: ( Inspect_scenarios | Reinspect_scenarios )
+ DO ADD $a PRECEDES $b; OD;
+
+
+/*Additional Constraints */
+
+/*Assumption that existing model has no verification issues. */
+ENSURE #Import_existing_model >=1 -> #Find_issue == 0;
+
+
+/* Trace annotations */
+
+IF #Find_issue >1 THEN
+ SAY( #Find_issue " issues were discovered");
+
+ ELSE IF #Find_issue ==1 THEN
+ SAY( #Find_issue " issue was discovered");
+ FI;
+FI;
\ No newline at end of file