diff --git a/Example01_simple_message_flow.mp b/Example01_simple_message_flow.mp
new file mode 100644
index 0000000000000000000000000000000000000000..0ea964f0c5e1a5d3a3606c2f1e02bec47ca3fad6
--- /dev/null
+++ b/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/Example01a_unreliable_message_flow.mp b/Example01a_unreliable_message_flow.mp
new file mode 100644
index 0000000000000000000000000000000000000000..d714bd0c5ba15a37e7cebecd62e4b7ba4df54d5a
--- /dev/null
+++ b/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/Example02_Data_flow.mp b/Example02_Data_flow.mp
new file mode 100644
index 0000000000000000000000000000000000000000..811e1de5c05900631a534383e10924fd91038d20
--- /dev/null
+++ b/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/Example03_ATM_withdrawal.mp b/Example03_ATM_withdrawal.mp
new file mode 100644
index 0000000000000000000000000000000000000000..0c33381eeedc80f433f26581a87f283271eb48f1
--- /dev/null
+++ b/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/Example04_Stack_behavior.mp b/Example04_Stack_behavior.mp
new file mode 100644
index 0000000000000000000000000000000000000000..0c660075f65c5c6248d423abf77219494b29c336
--- /dev/null
+++ b/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/Example04a_Queue_behavior.mp b/Example04a_Queue_behavior.mp
new file mode 100644
index 0000000000000000000000000000000000000000..3aed579e46c93823948700930d49e3ef8b7bcbcf
--- /dev/null
+++ b/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/Example05_Car_Race.mp b/Example05_Car_Race.mp
new file mode 100644
index 0000000000000000000000000000000000000000..4f6a8fd1696640cb494f27500d720ebb288be6c6
--- /dev/null
+++ b/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/Example06_Assertion_Checking.mp b/Example06_Assertion_Checking.mp
new file mode 100644
index 0000000000000000000000000000000000000000..61d2cdd5ddbcfc7abbdceb49229fa295b8a4fb03
--- /dev/null
+++ b/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/Example07_Unconstrained_Stack.mp b/Example07_Unconstrained_Stack.mp
new file mode 100644
index 0000000000000000000000000000000000000000..817cee81c00edf2727d9cdd9a669b80d280eb5bb
--- /dev/null
+++ b/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/Example08_Operational_Process.mp b/Example08_Operational_Process.mp
new file mode 100644
index 0000000000000000000000000000000000000000..e930176a2b7dbc5bc020ee3929f3a03147a92e4b
--- /dev/null
+++ b/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/Example09_Employee_Employer.mp b/Example09_Employee_Employer.mp
new file mode 100644
index 0000000000000000000000000000000000000000..b4423996067a0807558a1252a928e9d1aae4e2d7
--- /dev/null
+++ b/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/Example10_Pipe_Filter.mp b/Example10_Pipe_Filter.mp
new file mode 100644
index 0000000000000000000000000000000000000000..63896c93432204eb441999ce30cdc279d45a82f6
--- /dev/null
+++ b/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/Example11_Publish_Subscribe.mp b/Example11_Publish_Subscribe.mp
new file mode 100644
index 0000000000000000000000000000000000000000..b885a2ed08874cd27fd08df23391baf5caf8dbfd
--- /dev/null
+++ b/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/Example12_network_topology_ring.mp b/Example12_network_topology_ring.mp
new file mode 100644
index 0000000000000000000000000000000000000000..d3dcba336d47cf365b1ea1017c60c6ae41bf21c8
--- /dev/null
+++ b/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/Example13_FiniteStateDiagram.mp b/Example13_FiniteStateDiagram.mp
new file mode 100644
index 0000000000000000000000000000000000000000..90b775634588e05da0c86ff492d65dc9b3949e01
--- /dev/null
+++ b/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/Example14_microwave_oven.mp b/Example14_microwave_oven.mp
new file mode 100644
index 0000000000000000000000000000000000000000..fa6ad1cab52efde09ccde8b0361c9edc2bd051fc
--- /dev/null
+++ b/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/Example15_Petri_net.mp b/Example15_Petri_net.mp
new file mode 100644
index 0000000000000000000000000000000000000000..b0ecf3becf6a41206e611e1fb1438a76fad6f5f5
--- /dev/null
+++ b/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/Example16_software_spiral_process.mp b/Example16_software_spiral_process.mp
new file mode 100644
index 0000000000000000000000000000000000000000..f8d21425998fbfe8c472101decf9945a3ff8bc6d
--- /dev/null
+++ b/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/Example17_Dining_Philosophers.mp b/Example17_Dining_Philosophers.mp
new file mode 100644
index 0000000000000000000000000000000000000000..6a2330a892b959217997c816aae07682034f5340
--- /dev/null
+++ b/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/Example18_Workflow_pattern.mp b/Example18_Workflow_pattern.mp
new file mode 100644
index 0000000000000000000000000000000000000000..6c3b9601b4316f26231d0145cbcb7db6601c78e7
--- /dev/null
+++ b/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/Example19_Consumers_Suppliers.mp b/Example19_Consumers_Suppliers.mp
new file mode 100644
index 0000000000000000000000000000000000000000..cb771e90ffca161946487229e76e2359ff87cc8a
--- /dev/null
+++ b/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, 670 traces, approx. time 2.5 min.
+*/
+
+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/Example20_MP_model__reuse.mp b/Example20_MP_model__reuse.mp
new file mode 100644
index 0000000000000000000000000000000000000000..c09d654b8a85e7deac2951b79e8f5049c06ed9b2
--- /dev/null
+++ b/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/Example21_compiler1.mp b/Example21_compiler1.mp
new file mode 100644
index 0000000000000000000000000000000000000000..371f385233024744bdf39fae36ce112121a6f447
--- /dev/null
+++ b/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/Example22_compiler2.mp b/Example22_compiler2.mp
new file mode 100644
index 0000000000000000000000000000000000000000..b18d9af47f41bf5a8b60a61f6f7e72744f52c7c3
--- /dev/null
+++ b/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/Example23_number_attributes.mp b/Example23_number_attributes.mp
new file mode 100644
index 0000000000000000000000000000000000000000..a0405536bb737d65c41b996e273fcf80c12c5037
--- /dev/null
+++ b/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/Example24_Bayesian_probability.mp b/Example24_Bayesian_probability.mp
new file mode 100644
index 0000000000000000000000000000000000000000..5022d189337f73d5b9c6343a766ba09eeb0aeeab
--- /dev/null
+++ b/Example24_Bayesian_probability.mp
@@ -0,0 +1,56 @@
+/* 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.
+ 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; };
+
+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;
diff --git a/Example25_interval_attributes.mp b/Example25_interval_attributes.mp
new file mode 100644
index 0000000000000000000000000000000000000000..cfef3eb3d82e9c64579cae0d7288b7571e4e0aa5
--- /dev/null
+++ b/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/Example26_timing_attributes.mp b/Example26_timing_attributes.mp
new file mode 100644
index 0000000000000000000000000000000000000000..65df381f75de10949a8bd56f80d22c734145cab4
--- /dev/null
+++ b/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/Example27_Railroad_Crossing.mp b/Example27_Railroad_Crossing.mp
new file mode 100644
index 0000000000000000000000000000000000000000..c6c9332e8e18764433ef3a5a683e02a1988d8e57
--- /dev/null
+++ b/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/Example28_MP_model_of_MP_architecture.mp b/Example28_MP_model_of_MP_architecture.mp
new file mode 100644
index 0000000000000000000000000000000000000000..36264184995df0d7cc631065432f261384f703c3
--- /dev/null
+++ b/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/Example29_stack1_Bayesian_probability.mp b/Example29_stack1_Bayesian_probability.mp
new file mode 100644
index 0000000000000000000000000000000000000000..b0fc26dbd9263b07ec7b73467da1566e9f259b92
--- /dev/null
+++ b/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/Example30_Local_Report.mp b/Example30_Local_Report.mp
new file mode 100644
index 0000000000000000000000000000000000000000..0271dd2c88233d5fb169237fedbaa2204edc6ee4
--- /dev/null
+++ b/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/Example31_Global_report.mp b/Example31_Global_report.mp
new file mode 100644
index 0000000000000000000000000000000000000000..ad102ee91a6a0220854021bff9da9e385119ee92
--- /dev/null
+++ b/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/Example32_Local_graph.mp b/Example32_Local_graph.mp
new file mode 100644
index 0000000000000000000000000000000000000000..625c9e85a465c6f0d4788fc17751d37aa2da2ccb
--- /dev/null
+++ b/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/Example33_Component_Diagram.mp b/Example33_Component_Diagram.mp
new file mode 100644
index 0000000000000000000000000000000000000000..5c1236ec9fc52bff59c61e00fa75594f76fedc25
--- /dev/null
+++ b/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/Example34_Graph_as_data_structure.mp b/Example34_Graph_as_data_structure.mp
new file mode 100644
index 0000000000000000000000000000000000000000..873759c781757149f84a0b2642b20dc4adcd44b8
--- /dev/null
+++ b/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/Example35_Finite_State_Diagram.mp b/Example35_Finite_State_Diagram.mp
new file mode 100644
index 0000000000000000000000000000000000000000..ff0ca8160c4696f5154ba4491eac0ad2b88b95d3
--- /dev/null
+++ b/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/Example36_Statechart.mp b/Example36_Statechart.mp
new file mode 100644
index 0000000000000000000000000000000000000000..f41f30f641c63d9521dfe27e34c1781395d4d882
--- /dev/null
+++ b/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/Example37_GLOBAL_query.mp b/Example37_GLOBAL_query.mp
new file mode 100644
index 0000000000000000000000000000000000000000..d6f37e17a2f685fa129f560b3cae2711caae5099
--- /dev/null
+++ b/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/Example38_knapsack.mp b/Example38_knapsack.mp
new file mode 100644
index 0000000000000000000000000000000000000000..ebe7c4de00ebb093a0cf5f545cb2b2153068062b
--- /dev/null
+++ b/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/Example39_turtles.mp b/Example39_turtles.mp
new file mode 100644
index 0000000000000000000000000000000000000000..bedbdb0b29519d639f1fa1bff8dfaf9a88d42b88
--- /dev/null
+++ b/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/Example40_web_browsers.mp b/Example40_web_browsers.mp
new file mode 100644
index 0000000000000000000000000000000000000000..5c6181c2b66620c1dbe23fbebf301592c0f564b2
--- /dev/null
+++ b/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/Example41_Replay_Attack.mp b/Example41_Replay_Attack.mp
new file mode 100644
index 0000000000000000000000000000000000000000..5749bbec43b43fc58ccc58c29120d8ca58160316
--- /dev/null
+++ b/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/Example42_Bar_Chart.mp b/Example42_Bar_Chart.mp
new file mode 100644
index 0000000000000000000000000000000000000000..dade7edfb50152ab420057c88fe4d2ebbb1150ae
--- /dev/null
+++ b/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/Example43_Histogram.mp b/Example43_Histogram.mp
new file mode 100644
index 0000000000000000000000000000000000000000..c40bdfa07024449cf9eaed6019578d65aafe051f
--- /dev/null
+++ b/Example43_Histogram.mp
@@ -0,0 +1,48 @@
+/* Example 43
+ 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.
+ The following MP code can be reused for any MP model just by Copy/Paste. */
+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) OR
+ /* special case when the only single trace with probability 1 exists */
+ ( #$$TRACE == 1 AND Num$n == 0.9 ) 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/Example44_Gantt_Chart.mp b/Example44_Gantt_Chart.mp
new file mode 100644
index 0000000000000000000000000000000000000000..fe4483df5b9e157783ebab43411f026c402a9199
--- /dev/null
+++ b/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/Example45_Martian_Lander.mp b/Example45_Martian_Lander.mp
new file mode 100644
index 0000000000000000000000000000000000000000..10b3b3a4fc8ad6e14215d21f31e284fd1b61b052
--- /dev/null
+++ b/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;