diff --git a/Example01_SimpleMessageFlow_EventCoordination.mp b/Example01_SimpleMessageFlow_EventCoordination.mp
index 9b604dda1cc74f22d4dd49e386405b745399a643..2e0f661857d142468eb10561fd2bc0f79e81a925 100644
--- a/Example01_SimpleMessageFlow_EventCoordination.mp
+++ b/Example01_SimpleMessageFlow_EventCoordination.mp
@@ -1,4 +1,4 @@
-/* Example 01. Model of [Simple_Message_Flow]
+/* Example 01. Model of Simple Message Flow
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.
@@ -8,8 +8,8 @@ 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.
+Instructions: Run for Scopes 1 and up. Viewing of traces also includes a
+"Swim Lanes" option.
==========================================================*/
diff --git a/Example01a_UnreliableMessageFlow_VirtualEvents.mp b/Example01a_UnreliableMessageFlow_VirtualEvents.mp
index 207b96aadbf147c2a0633db89901d9fbd79704ba..d7a23e6b5f1144b4783f4a509031829118e4b2e3 100644
--- a/Example01a_UnreliableMessageFlow_VirtualEvents.mp
+++ b/Example01a_UnreliableMessageFlow_VirtualEvents.mp
@@ -1,9 +1,10 @@
-/* Example 01a. Model of [Unreliable_Message_Flow]
+/* Example 01a. Model of 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.
+Instructions: Run for Scopes 1 and up. Viewing of traces also includes a "Swim
+Lanes" option.
==========================================================*/
diff --git a/Example02_DataFlow_EventSharing.mp b/Example02_DataFlow_EventSharing.mp
index 47d18b6e276ae9354eba0feb9c5b97b8f0a43b6b..6459a5d3b677f0631b0d74722a8612a7a88dbacc 100644
--- a/Example02_DataFlow_EventSharing.mp
+++ b/Example02_DataFlow_EventSharing.mp
@@ -1,4 +1,4 @@
-/* Example 02. Model of [Data_Flow]
+/* Example 02. Model of Data Flow
data items as behaviors
@@ -18,10 +18,10 @@ 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.
+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.
+Instructions: Run for Scopes 1 and up. Viewing of traces also includes a
+"Swim Lanes" option.
==========================================================*/
diff --git a/Example03_ATMWithdrawal_BehaviorOfEnvironment.mp b/Example03_ATMWithdrawal_BehaviorOfEnvironment.mp
index 245fcaeb0080d63c5164d87b504529c49e103c32..c3433783b448bbdd55064e2685be235d43e17c1f 100644
--- a/Example03_ATMWithdrawal_BehaviorOfEnvironment.mp
+++ b/Example03_ATMWithdrawal_BehaviorOfEnvironment.mp
@@ -1,4 +1,4 @@
-/* Example 03. Model of [ATM_Withdrawal]
+/* Example 03. Model of ATM Withdrawal
Integrated system and environment behaviors
@@ -17,15 +17,13 @@ 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.
+Instructions: Run for Scopes 1 and up. "Sequence" mode yields views very similar to the UML or SysML
+Sequence Diagrams. Viewing of traces also includes a "Swim Lanes" option.
+
==========================================================*/
SCHEMA ATM_Withdrawal
diff --git a/Example04_StackBehavior_EnsureCondition.mp b/Example04_StackBehavior_EnsureCondition.mp
index 1ddf8bc4ea0e8a63783298761fbe318918476557..23db1978f378ebf1401c87681cf6e61fa71fc9e1 100644
--- a/Example04_StackBehavior_EnsureCondition.mp
+++ b/Example04_StackBehavior_EnsureCondition.mp
@@ -1,4 +1,4 @@
-/* Example04_StackBehavior_EnsureCondition.mp
+/* Example 04. Model of Stack Behavior
The event trace is a set of events and the Boolean expressions
in MP can embrace the traditional predicate calculus notation. A set
@@ -27,12 +27,16 @@ and demonstrates an example of combining imperative (event grammar)
and declarative (Boolean expressions) constructs for behavior
specification.
-*/
-SCHEMA Stack_behavior
+Instructions: Run for Scopes 1 and up. Viewing of traces also
+includes a "Swim Lanes" option.
+
+==========================================================*/
+
+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 );
-};
\ No newline at end of file
+};
diff --git a/Example04a_StackBehavior_UserDefinedRelations.mp b/Example04a_StackBehavior_UserDefinedRelations.mp
index 196b5878e4b4ec1319cf760d6fa392fb31523255..0264da3061a11b16261533489e387ed56bc3f86f 100644
--- a/Example04a_StackBehavior_UserDefinedRelations.mp
+++ b/Example04a_StackBehavior_UserDefinedRelations.mp
@@ -1,45 +1,55 @@
-/* Example4a_Queue_behavior.mp
+/* Example 04a. Model of Stack Behavior
-run for scopes 1, 2, 3, and up.
-*/
+The event trace is a set of events and the Boolean expression constructs in MP
+can support the traditional first order predicate calculus notation.
-/* This rule specifies the behavior of a queue in terms of queue operations
-enqueue and dequeue. It is assumed that initially Queue is empty.
+A set of behaviors (event traces) may be defined by the event
+grammar rules, composition operations, and some additional constraints –
+ENSURE conditions.
+
+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
-dequeue events inside Queue trace.
+pop events inside Stack trace. The FROM Stack part is optional, by default it is
+assumed to be FROM THIS.
-The function #dequeue BEFORE $x yields the number of dequeue events preceding $x.
+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 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 */
+(Boolean expressions) constructs for behavior specification.
+
+Instructions: Run for Scopes 1 and up. Viewing of traces also includes a
+"Swim Lanes" option.
+
+==========================================================*/
+
+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/Example04b_QueueBehavior_UserDefinedRelations.mp b/Example04b_QueueBehavior_UserDefinedRelations.mp
index b22b82ef05b93e533f7b6b526f88439a54d1109c..61b342ad269cb83bf62ac9f723c146e76dc42f37 100644
--- a/Example04b_QueueBehavior_UserDefinedRelations.mp
+++ b/Example04b_QueueBehavior_UserDefinedRelations.mp
@@ -1,53 +1,48 @@
-/* Example 04b. Model of [Queue_Behavior]
+/* Example 04b. Model of Queue Behavior
-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.
+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
-pop events inside Stack trace. The FROM Stack part is optional, by default it is
-assumed to be FROM THIS.
+dequeue events inside Queue trace.
-The function #pop BEFORE $x yields the number of pop events preceding $x.
+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.
+Instructions: Run for Scopes 1 and up. Viewing of traces also includes a "Swim
+Lanes" option.
+
==========================================================*/
-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 */
+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_CarRace_NestedComposition.mp b/Example05_CarRace_NestedComposition.mp
index 766eda91bccf7545f6c952f49c9f090d06a8c77f..3c2c0968df3f26ee30368b06dbe0b583882fedb4 100644
--- a/Example05_CarRace_NestedComposition.mp
+++ b/Example05_CarRace_NestedComposition.mp
@@ -1,13 +1,13 @@
-/* Example 05. Model of [Car_Race]
+/* Example 05. Model of Car Race
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.
+
+Instructions: Run for Scopes 1 and up. Viewing of traces also
+includes a "Swim Lanes" option.
==========================================================*/
diff --git a/Example06_UnreliableChannel_AssertionChecking.mp b/Example06_UnreliableChannel_AssertionChecking.mp
index 5a021feabe7963a6faaa1897361f5592fca79683..5bb6667aced8e06846fe7476bb8b702d51a76dca 100644
--- a/Example06_UnreliableChannel_AssertionChecking.mp
+++ b/Example06_UnreliableChannel_AssertionChecking.mp
@@ -1,4 +1,4 @@
-/* Example 06. Model of [Unreliable_Channel]
+/* Example 06. Model of Unreliable Channel
Assertion checking, Communicating via unreliable channel.
@@ -20,6 +20,9 @@
if the property should always hold, it makes sense to convert it
into the ENSURE condition.
+ Instructions: Run for Scopes 1 and up. Viewing of traces also
+ includes a "Swim Lanes" option.
+
==========================================================*/
SCHEMA Unreliable_Channel
diff --git a/Example07_UnconstrainedStack_TraceAnnotation.mp b/Example07_UnconstrainedStack_TraceAnnotation.mp
index 258745355c1180ebf82c62ba6a303e33f77c266d..270ca3141e365f67e6dd835b0c29144964c998c3 100644
--- a/Example07_UnconstrainedStack_TraceAnnotation.mp
+++ b/Example07_UnconstrainedStack_TraceAnnotation.mp
@@ -1,4 +1,4 @@
-/* Example 07. Model of [Unconstrained_Stack]
+/* Example 07. Model of Unconstrained Stack
Trace annotation techniques
@@ -17,6 +17,9 @@ 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.
+Instructions: Run for Scopes 1 and up. Viewing of traces also includes a
+"Swim Lanes" option.
+
==========================================================*/
SCHEMA Unconstrained_Stack
diff --git a/Example08_EmployeeEmployer_CoordinationAcrossHierarchyLevels.mp b/Example08_EmployeeEmployer_CoordinationAcrossHierarchyLevels.mp
index 92d6736d9baeebdeac72b31e0cf12d0b08da2064..436259dc5b0c76d4c77773d0a524d66bdfaa6264 100644
--- a/Example08_EmployeeEmployer_CoordinationAcrossHierarchyLevels.mp
+++ b/Example08_EmployeeEmployer_CoordinationAcrossHierarchyLevels.mp
@@ -1,4 +1,4 @@
-/* Example 08. Model of [Employee_Employer]
+/* Example 08. Model of Employee Employer
The web site http://www.infoq.com/articles/bpelbpm
“Why BPEL is not the holy grail for BPM “
@@ -18,11 +18,9 @@ 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.
+parallel workflow [in BPEL] that is equivalent to this one ..."
+
+Instructions: Run for Scopes 1 and up. Viewing of traces also includes a "Swim Lanes" option. Some box reshuffling may be needed to improve the trace layout.
==========================================================*/
diff --git a/Example09_PipeFilter_TraceAnnotationQueries.mp b/Example09_PipeFilter_TraceAnnotationQueries.mp
index 2a59ae8a69a96e3cce51f8dba94c3ee3de626623..e66badbd3f31ccce7da7d28776251ec6e724fde2 100644
--- a/Example09_PipeFilter_TraceAnnotationQueries.mp
+++ b/Example09_PipeFilter_TraceAnnotationQueries.mp
@@ -1,4 +1,4 @@
-/* Example 09. Model of [Pipe_Filter]
+/* Example 09. Model of Pipe Filter
pipe/filter architecture model with 2 filters
@@ -8,6 +8,9 @@
3) received message can stay in the Filter for while,
before being sent (if at all).
+ Instructions: Run for Scopes 1, 2, 3, and 4. Viewing of traces also includes a "Swim Lanes" option.
+ Scope 4: 959 traces in approx. 6.1 sec.
+
==========================================================*/
SCHEMA Pipe_Filter
diff --git a/Example10_PublishSubscribe_EventReshuffling.mp b/Example10_PublishSubscribe_EventReshuffling.mp
index 45a0b63acc70847e5fe23d5ba129785674c29b53..a3ce1cdc4dd409122f8a60381bfe572396362cac 100644
--- a/Example10_PublishSubscribe_EventReshuffling.mp
+++ b/Example10_PublishSubscribe_EventReshuffling.mp
@@ -1,11 +1,10 @@
-/* Example 10. Model of [Publish_Subscribe]
+/* Example 10. Model of Publish Subscribe
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.
+ when new information is available.
+
+ Instructions: Run for Scopes 1, 2, and 3. Viewing of traces also includes a "Swim Lanes" option.
+ Scope 3: 3813 traces in approx. 7.4 min.
==========================================================*/
diff --git a/Example11_RingTopology_UserDefinedRelations.mp b/Example11_RingTopology_UserDefinedRelations.mp
index 0ce90612f833c3039cc743b5f0e4c66231867026..bc83e67d38fd54fe047346d0c7c9550c1f768a04 100644
--- a/Example11_RingTopology_UserDefinedRelations.mp
+++ b/Example11_RingTopology_UserDefinedRelations.mp
@@ -1,10 +1,13 @@
-/* Example 11. Model of [Ring_Topology]
+/* Example 11. Model of Ring Topology
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.
+
+ Instructions: Run for Scopes 1, 2, and 3. Viewing of traces also includes a "Swim Lanes" option.
+ Scope 3: 1570 traces in approx. 31 sec.
==========================================================*/
diff --git a/Example12_CardiacArrestWorkflow_VirtualEvents.mp b/Example12_CardiacArrestWorkflow_VirtualEvents.mp
index a29f138af7ff5fd806accba8353b1d0440554ff3..24768d332c373422d518d637a3e1dc4b2a7f093d 100644
--- a/Example12_CardiacArrestWorkflow_VirtualEvents.mp
+++ b/Example12_CardiacArrestWorkflow_VirtualEvents.mp
@@ -1,4 +1,4 @@
-/* Example 12. Model of [Cardiac_Arrest_Workflow]
+/* Example 12. Model of Cardiac Arrest Workflow
the web site
http://workflowpatterns.com/patterns/control/index.php
@@ -12,7 +12,7 @@ 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
+Instructions: Run for Scope 1. Viewing of traces also includes a "Swim Lanes" option.
==========================================================*/
diff --git a/Example13_ConsumersSuppliers_DependencyTracking.mp b/Example13_ConsumersSuppliers_DependencyTracking.mp
index f1a8117f95741353bd72032f34dd60de899fa8af..a35ac2401b68ca0fcedc1b5526834be87ea75516 100644
--- a/Example13_ConsumersSuppliers_DependencyTracking.mp
+++ b/Example13_ConsumersSuppliers_DependencyTracking.mp
@@ -1,13 +1,12 @@
-/* Example 13. Model of [Consumers_Suppliers]
+/* Example 13. Model of 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.
+Instructions: Run for Scopes 1 and 2. Viewing of traces also includes a "Swim Lanes" option.
+ Scope 2: 110 traces in approx. 38 sec.
==========================================================*/
diff --git a/Example14_ShoppingSpree_NumberAttributes.mp b/Example14_ShoppingSpree_NumberAttributes.mp
index f6ce753b261f4f6aba37bc7a5472588e7e2f30d4..d429ae89f03df9bb0a9662e1dc3d1bfad1253597 100644
--- a/Example14_ShoppingSpree_NumberAttributes.mp
+++ b/Example14_ShoppingSpree_NumberAttributes.mp
@@ -1,4 +1,6 @@
-/* Example 14. Model of [Shopping_Spree]
+/* Example 14. Model of Shopping Spree
+
+Instructions: Run for Scopes 1 and up. Viewing of traces also includes a "Swim Lanes" option.
==========================================================*/
diff --git a/Example15_BackpackWeight_IntervalAttributes.mp b/Example15_BackpackWeight_IntervalAttributes.mp
index c596c95d38f88791bc64043fb189109a77ffba32..a291d6a1dbb2db660ec688cf3ace10d49a312e49 100644
--- a/Example15_BackpackWeight_IntervalAttributes.mp
+++ b/Example15_BackpackWeight_IntervalAttributes.mp
@@ -1,4 +1,4 @@
-/* Example 15. Model of [Backpack_Weight]
+/* Example 15. Model of Backpack Weight
Use of interval attributes.
@@ -6,9 +6,10 @@
the total weight of 30 units.
There may be several instances of the same item.
- run for scopes 1 and up
+ Instructions: Run for Scopes 1 and up. Viewing of traces also includes a "Swim Lanes" option.
==========================================================*/
+
SCHEMA Backpack_Weight
ATTRIBUTES{ interval weight; };
diff --git a/Example16_StackBehavior_ProbabilityCalculationsType1.mp b/Example16_StackBehavior_ProbabilityCalculationsType1.mp
index f35fec747f74f1fa279d92bf3a5f9802ca0fde99..849e9489bb84ac2411c5c9f9f5e47a8ba8a87893 100644
--- a/Example16_StackBehavior_ProbabilityCalculationsType1.mp
+++ b/Example16_StackBehavior_ProbabilityCalculationsType1.mp
@@ -1,4 +1,4 @@
-/* Example16_StackBehavior_ProbabilityCalculationsType1.mp
+/* Example 16. Model of Stack Behavior
Here is a simple stack behavior model. Valid behaviors don’t permit
a scenario when Pop operation is applied to the empty stack. For the
@@ -13,10 +13,13 @@ impossible in a real stack, so they are cut from the model.
By removing some scenarios, the remaining probabilities change.
-*/
+Instructions: Run for Scopes 1 and up. Viewing of traces also includes a "Swim Lanes" option.
+
+==========================================================*/
+
SCHEMA Stack_Behavior
ROOT Stack: (* (<<0.75>> Push | <<0.25>> 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 ); };
\ No newline at end of file
+( #Pop BEFORE $x < #Push BEFORE $x ); };
diff --git a/Example17_SharedEvents_ProbabilityCalculationsType1.mp b/Example17_SharedEvents_ProbabilityCalculationsType1.mp
index c08f59d00876241b87d0f5dc6b4bc2a2c9af8d67..44b8550f5c63760533ba07bd884ac07271041db7 100644
--- a/Example17_SharedEvents_ProbabilityCalculationsType1.mp
+++ b/Example17_SharedEvents_ProbabilityCalculationsType1.mp
@@ -1,13 +1,16 @@
-/* Example17_SharedEvents_ProbabilityCalculationsType1.mp
+/* Example 17. Model of Shared Events
A simple example of shared events. If one root has a, the other root
also has a. If neither root has a, then root 1 must have b, and root 2
must have c. Additionally, probabilities show how "SHARE ALL" increases
the chances of the shared event.
-*/
+Instructions: Run for Scope 1. Viewing of traces also includes a "Swim Lanes" option.
+
+==========================================================*/
+
SCHEMA Shared_Events
ROOT R1: (<<0.6>> a | b);
ROOT R2: (<<0.8>> a | c);
-R1, R2 SHARE ALL a;
\ No newline at end of file
+R1, R2 SHARE ALL a;
diff --git a/Example18_RedGreen_BayesianProbabilityCalculationsType2.mp b/Example18_RedGreen_BayesianProbabilityCalculationsType2.mp
index a7c160f6d67faf5f5ddeda736f347b8ec4484064..a7b421b3b8af3df13012e047558e2b082f949bbe 100644
--- a/Example18_RedGreen_BayesianProbabilityCalculationsType2.mp
+++ b/Example18_RedGreen_BayesianProbabilityCalculationsType2.mp
@@ -1,4 +1,4 @@
-/* Example 18. Model of [Red_Green]
+/* Example 18. Model of Red Green
Bayesian attribute example
@@ -13,8 +13,10 @@
since Type 1 assumes that probability of selecting an alternative is
constant for the whole derivation process.
- run for scope 1
-*/
+ Instructions: Run for Scope 1. Viewing of traces also includes a "Swim Lanes" option.
+
+==========================================================*/
+
SCHEMA Red_Green
ATTRIBUTES{ number selection_probability; };
diff --git a/Example19_StackBehavior_BayesianProbabilityCalculationsType2.mp b/Example19_StackBehavior_BayesianProbabilityCalculationsType2.mp
index d8c8db1ea87b6a41c24c9abae5f2a899c691eda5..0173c2bc8d9c05e638ae6263b41fe01babcc32a6 100644
--- a/Example19_StackBehavior_BayesianProbabilityCalculationsType2.mp
+++ b/Example19_StackBehavior_BayesianProbabilityCalculationsType2.mp
@@ -1,10 +1,8 @@
-/* Example 19. Model of [Stack_Behavior]
+/* Example 19. Model of Stack Behavior
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:
+ 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.
@@ -24,6 +22,8 @@
this will require to update the first step in p2 assignment (line 57)
it will become p2 := 1/(M + 1);
+ Instructions: Run for Scopes 1 and up. Viewing of traces also includes a "Swim Lanes" option.
+
==========================================================*/
SCHEMA Stack_Behavior
diff --git a/Example20_Activity_Diagram.mp b/Example20_Activity_Diagram.mp
index 8091ca50cdb23a2aa3f98290e2e6b0de6c3d80f8..3aeeb31a6fe7c3a916d0eae61dc68dc0e8b17b63 100644
--- a/Example20_Activity_Diagram.mp
+++ b/Example20_Activity_Diagram.mp
@@ -1,10 +1,12 @@
-/* Example20_Activity_Diagram.mp
+/* Example 20. Model of Activity Diagram
This model demonstrates how to use "SHOW ACTIVITY DIAGRAM" to
display the possible traces in flowchart form. Root A has 4 different
possible traces at scope 1, and the flowchart displays those possiblities.
-*/
+Instructions: Run for Scope 1. Viewing of traces also includes a "Swim Lanes" option.
+
+==========================================================*/
SCHEMA Activity_Diagram
@@ -15,4 +17,4 @@ ROOT A:
a6
( a7 | a8 );
-SHOW ACTIVITY DIAGRAM A;
\ No newline at end of file
+SHOW ACTIVITY DIAGRAM A;
diff --git a/Example21_DataFlow_LocalReport.mp b/Example21_DataFlow_LocalReport.mp
index 01c847f708b3f6494ce9f097d4a21cf5660a9812..e3a7524961a30d9c4562fd88b6b8b6eaa5bff040 100644
--- a/Example21_DataFlow_LocalReport.mp
+++ b/Example21_DataFlow_LocalReport.mp
@@ -1,7 +1,11 @@
+/* Example 21. Model of Data Flow
+
+Local Report within a trace.
+
+ Instructions: Run for Scopes 1 and up. Viewing of traces also includes a "Swim Lanes" option.
+
+==========================================================*/
-/* Example 30. Local Report within a trace.
- run for scope 1 and up.
-*/
SCHEMA Data_Flow
ROOT Writer: (* ( working | writing ) *);
diff --git a/Example22_SimpleMessageFlow_GlobalReport.mp b/Example22_SimpleMessageFlow_GlobalReport.mp
index 6bbc765738776eb451122404312d1c65c05d8bae..0a65ba22a38e440be9f3627748be4b8f386c39c7 100644
--- a/Example22_SimpleMessageFlow_GlobalReport.mp
+++ b/Example22_SimpleMessageFlow_GlobalReport.mp
@@ -1,6 +1,6 @@
-/* Example 22. Model of [Simple_Message_Flow]
-
- run for scope 1 and up
+/* Example 22. Model of Simple Message Flow
+
+ Instructions: Run for Scopes 1 and up. Viewing of traces also includes a "Swim Lanes" option.
==========================================================*/
diff --git a/Example23_CarRace_LocalGraph.mp b/Example23_CarRace_LocalGraph.mp
index 6ec84f2b0b5367ffe012f020364c61b994233202..eb5591339de7eeddbec0ff5668ef84674382330c 100644
--- a/Example23_CarRace_LocalGraph.mp
+++ b/Example23_CarRace_LocalGraph.mp
@@ -1,7 +1,8 @@
-/* Example 23. Model of [Car_Race]
+/* Example 23. Model of Car Race
Local graph within the event trace.
- run for scope 1 and up
+
+ Instructions: Run for Scopes 1 and up. Viewing of traces also includes a "Swim Lanes" option.
==========================================================*/
diff --git a/Example24_Compiler_ComponentDiagram.mp b/Example24_Compiler_ComponentDiagram.mp
index f8c232283d3d675238c3b3b939f18ce3441d18d0..4a98981cd26d4031243b3a8eaeaaa1ee88649f3f 100644
--- a/Example24_Compiler_ComponentDiagram.mp
+++ b/Example24_Compiler_ComponentDiagram.mp
@@ -1,4 +1,4 @@
-/* Example 24. Model of [Compiler]
+/* Example 24. Model of Compiler
Compiler front end, bottom-up parser
Lexer and parser in interactive mode.
@@ -7,11 +7,12 @@
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.
-====================================================*/
+ Instructions: Run for Scope 1. Viewing of traces also includes a "Swim Lanes" option.
+ Scope 1: 20 traces in approx. 3.1 sec.
+
+==========================================================*/
+
SCHEMA Compiler
ROOT Source_code: (+<1.. $$scope + 1>
diff --git a/Example25_Graph_as_Data_Structure.mp b/Example25_Graph_as_Data_Structure.mp
index 019fea311476321a730ac20a02352c45297f578b..40edc33eb8ce4b9eeb01921daf1b79e018a5eb04 100644
--- a/Example25_Graph_as_Data_Structure.mp
+++ b/Example25_Graph_as_Data_Structure.mp
@@ -1,8 +1,12 @@
-/* Example 25. Model of [Graph_as_Data_Structure]
+/* Example 25. Model of Graph as Data Structure
- Accumulating and rendering statistics from event traces.
+ Accumulating and rendering statistics from event traces.
Graphs as container data structures
-============================================================*/
+
+ Instructions: Run for Scopes 1 and up. Viewing of traces also includes a "Swim Lanes" option.
+
+==========================================================*/
+
SCHEMA Graph_as_Data_Structure
ROOT A: (* ( a | b) *);
ROOT B: (+ c +);
diff --git a/Example26_UnreliableMessageFlow_GlobalQuery.mp b/Example26_UnreliableMessageFlow_GlobalQuery.mp
index 84f651dd637e0fb0dc82cc707571c95018d0b8f1..5acf62d525c5564785d6555d8b85e7da0cc4b4ac 100644
--- a/Example26_UnreliableMessageFlow_GlobalQuery.mp
+++ b/Example26_UnreliableMessageFlow_GlobalQuery.mp
@@ -1,4 +1,4 @@
-/* Example 26. Model of [Unreliable_Message_Flow]
+/* Example 26. Model of Unreliable Message Flow
GLOBAL query
@@ -16,8 +16,10 @@ 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.
-*/
+Instructions: Run for Scopes 1 and up. Viewing of traces also includes a "Swim Lanes" option.
+
+==========================================================*/
+
SCHEMA Unreliable_Message_Flow
ROOT Sender: (+ send +);
diff --git a/Example27_AssemblingStatistics_Table_and_Bar_Chart.mp b/Example27_AssemblingStatistics_Table_and_Bar_Chart.mp
index c3f18e079016599ab10ee3487f24de4f78260941..19bcfec5ca2896288c0ec67ab67a9ca9851fedde 100644
--- a/Example27_AssemblingStatistics_Table_and_Bar_Chart.mp
+++ b/Example27_AssemblingStatistics_Table_and_Bar_Chart.mp
@@ -1,7 +1,9 @@
-/* Example 27. Model of [Table_and_Bar_Chart]
+/* Example 27. Model of Table and Bar Chart
Assembling statistics about a current trace in a TABLE and rendering it.
- Table and bar chart example, run for scope 1
+ Table and bar chart example.
+
+ Instructions: Run for Scope 1. Viewing of traces also includes a "Swim Lanes" option.
==========================================================*/
diff --git a/Example28_AssemblingStatistics_Histogram.mp b/Example28_AssemblingStatistics_Histogram.mp
index 908ca95543fca3c0e5e8472edfb4e475a7712866..d7fdc6e3f2d70b1a66235c6f1be9f0b21f8c3ab3 100644
--- a/Example28_AssemblingStatistics_Histogram.mp
+++ b/Example28_AssemblingStatistics_Histogram.mp
@@ -1,7 +1,11 @@
-/* Example 28. Model of [Histogram]
+/* Example 28. Model of Histogram
- Histogram example, run for scopes 1, 2, 3, and up
-*/
+ Histogram example
+
+ Instructions: Run for Scopes 1 and up. Viewing of traces also includes a "Swim Lanes" option.
+
+==========================================================*/
+
SCHEMA Histogram
ROOT A: (<<0.2>> a1 | <<0.3>> a2 | (* a3 *));
ATTRIBUTES { number count; };
diff --git a/Example29_AssemblingStatistics_Gantt_Chart.mp b/Example29_AssemblingStatistics_Gantt_Chart.mp
index dc1ad1b86d876f8023b3c341305cce0d8ca4e28d..305baa042e53481368cfa2d67aa8325058830d75 100644
--- a/Example29_AssemblingStatistics_Gantt_Chart.mp
+++ b/Example29_AssemblingStatistics_Gantt_Chart.mp
@@ -1,7 +1,11 @@
-/* Example 29. Model of [Gantt_Chart]
+/* Example 29. Model of Gantt Chart
Gantt chart example
-*/
+
+ Instructions: Run for Scope 1. Viewing of traces also includes a "Swim Lanes" option.
+
+==========================================================*/
+
SCHEMA Gantt_Chart
ROOT A: a1 a2;
diff --git a/Example30_MicrowaveOven_ModelingModelChecking.mp b/Example30_MicrowaveOven_ModelingModelChecking.mp
index a8c23e4deb2326556bd577ccca330268f8baa7fd..ddbf74f652ad6dd8bc59caae6051eceb18ef32f2 100644
--- a/Example30_MicrowaveOven_ModelingModelChecking.mp
+++ b/Example30_MicrowaveOven_ModelingModelChecking.mp
@@ -1,4 +1,4 @@
-/* Example 30. Model of [Microwave_Oven]
+/* Example 30. Model of Microwave Oven
example of finite state diagram behavior model,
CTL formula representation in MP, and model checking for a small scope.
@@ -26,9 +26,9 @@
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.)
+
+ Instructions: Run for Scope 1. Viewing of traces also includes a "Swim Lanes" option.
+ Scope 1: 28 traces (including 2 counterexamples) in approx. 1.4 sec.
==========================================================*/
diff --git a/Example31_Aspect_Oriented_Paradigm.mp b/Example31_Aspect_Oriented_Paradigm.mp
index 63efa4a0c0359b3661ef555f971e604f71d8548e..e52b8754f392a968ccf3327f592947740f13905a 100644
--- a/Example31_Aspect_Oriented_Paradigm.mp
+++ b/Example31_Aspect_Oriented_Paradigm.mp
@@ -1,4 +1,4 @@
-/* Example31_Aspect_Oriented_Paradigm.mp
+/* Example 31. Model of Aspect Oriented Paradigm
The COORDINATE operation supports a “cause-effect†refinement for
the behavior of two components and it bears a certain similarity
@@ -13,7 +13,9 @@ methods M1 and M2 as join points, and the aspect behavior requires
a call to Prolog before, and to Epilog after each method call as an
advice. The corresponding MP model may look like the following.
-*/
+Instructions: Run for Scopes 1 and up. Viewing of traces also includes a "Swim Lanes" option.
+
+==========================================================*/
SCHEMA Aspect_Oriented_Paradigm
@@ -29,4 +31,4 @@ COORDINATE
DO ADD
$a1 PRECEDES $jp,
$jp PRECEDES $a2;
-OD;
\ No newline at end of file
+OD;
diff --git a/Example32_Petri_Net.mp b/Example32_Petri_Net.mp
index 01ef7c726ba4fb6df7a2a67911faa645ad85cde5..a13f23b97dcfbc2d5ae2ad97c7b8f498b2d17fd0 100644
--- a/Example32_Petri_Net.mp
+++ b/Example32_Petri_Net.mp
@@ -1,13 +1,14 @@
-/* Example 32. Model of [Petri_Net]
+/* Example 32. Model of Petri Net
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
+ Instructions: Run for Scopes 1 and 2. Viewing of traces also includes a "Swim Lanes" option.
+ Scope 2: 4 traces in approx. 6.6 sec.
+
==========================================================*/
SCHEMA Petri_Net
diff --git a/Example33_ATMWithdrawal_StatechartView.mp b/Example33_ATMWithdrawal_StatechartView.mp
index 79a83402139cc4e988b74875c8f39d28be3c3536..b720314f2bd3b026f3a297a7cf23dffa0f0474be 100644
--- a/Example33_ATMWithdrawal_StatechartView.mp
+++ b/Example33_ATMWithdrawal_StatechartView.mp
@@ -1,10 +1,11 @@
-/* Example 33. Model of [ATM_Withdrawal]
+/* Example 33. Model of ATM Withdrawal
Extracting Statechart view from MP model.
-
- run for scope 1 and up
+
+ Instructions: Run for Scopes 1 and up. Viewing of traces also includes a "Swim Lanes" option.
==========================================================*/
+
SCHEMA ATM_Withdrawal
ROOT Customer: (* insert_card
diff --git a/Example34_FiniteStateDiagram_PathAnnotation.mp b/Example34_FiniteStateDiagram_PathAnnotation.mp
index 6946cd08910773cff2568782cece1a573bb64735..06e7dfa55e3f8e672d797a539ad17733760ead05 100644
--- a/Example34_FiniteStateDiagram_PathAnnotation.mp
+++ b/Example34_FiniteStateDiagram_PathAnnotation.mp
@@ -1,4 +1,4 @@
-/* Example 34. Model of [Finite_State_Diagram_with_Path_Annotation]
+/* Example 34. Model of Finite State Diagram with Path Annotation
example of finite state diagram behavior model,
contains non-deterministic transitions (from S1 with symbol a),
@@ -28,11 +28,9 @@
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)
+
+ Instructions: Run for Scopes 1 and 2. Viewing of traces also includes a "Swim Lanes" option.
+ Scope 2: 30 traces in approx. 9.4 sec.
==========================================================*/
diff --git a/Example35_FiniteStateDiagram_PathDiagram.mp b/Example35_FiniteStateDiagram_PathDiagram.mp
index 7b6af2b8227a651b3a9c6c1025ba5f4dfedfae63..c2a67b048de3f6440f44b4cb3318739e09b33e4b 100644
--- a/Example35_FiniteStateDiagram_PathDiagram.mp
+++ b/Example35_FiniteStateDiagram_PathDiagram.mp
@@ -1,11 +1,13 @@
-/* Example 35. Model of [Finite_State_Diagram_with_Path_Diagram]
+/* Example 35. Model of Finite State Diagram with Path Diagram
Adding path and state transition diagrams to
the Finite Automaton behavior model.
-
- run for scope 2
+
+ Instructions: Run for Scope 2. Viewing of traces also includes a "Swim Lanes" option.
+ Scope 2: 30 traces in approx. 11 sec.
==========================================================*/
+
SCHEMA Finite_State_Diagram_with_Path_Diagram
ROOT S1_behavior:
diff --git a/Example36_Authentication_SystemReuse.mp b/Example36_Authentication_SystemReuse.mp
index 993b889edf3882feae7e47550271038f8e39fc61..d7c98e61ceb4194251800be227b3fbe3926af711 100644
--- a/Example36_Authentication_SystemReuse.mp
+++ b/Example36_Authentication_SystemReuse.mp
@@ -1,14 +1,12 @@
-/* Example 36. Model of [Authentication_System]
+/* Example 36. Model of Authentication System
- Authentication system's behavior for reuse with MAP operation.
+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
+Instructions: Run for Scopes 1 and up. Viewing of traces also includes a "Swim Lanes" option. At Scope 3 and above, the attempts_exhausted event can be seen. 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 ==================*/
-SCHEMA Reuse_of_a_system
+SCHEMA Authentication_System
ROOT Data_Base: (* check_ID *);
diff --git a/Example37_Compiler1_ComponentReuse.mp b/Example37_Compiler1_ComponentReuse.mp
index 1b90df9d7c29ab0a5212e8166e92aba64e202706..e1282adb171a810d1215dd5d102db324531e1735 100644
--- a/Example37_Compiler1_ComponentReuse.mp
+++ b/Example37_Compiler1_ComponentReuse.mp
@@ -1,13 +1,11 @@
-/* Example 37. Model of [Compiler1]
+/* Example 37. Model of Compiler 1
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.
+Instructions: Run for Scopes 1 and 2. Viewing of traces also includes a "Swim Lanes" option.
+ Scope 2: 147 traces in approx. 1.8 sec.
==========================================================*/
diff --git a/Example38_Compiler2_ComponentReuse.mp b/Example38_Compiler2_ComponentReuse.mp
index 1c2fc025b06598e6ade7be5bdf3c19978a7c888a..01d78de382101b83293f8660f341b61b0f3acd40 100644
--- a/Example38_Compiler2_ComponentReuse.mp
+++ b/Example38_Compiler2_ComponentReuse.mp
@@ -1,13 +1,11 @@
-/* Example 38. Model of [Compiler2]
+/* Example 38. Model of Compiler 2
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.
+Instructions: Run for Scopes 1, 2, and 3. Viewing of traces also includes a "Swim Lanes" option.
+ Scope 3: 4860 traces in approx. 1.6 min.
==========================================================*/
diff --git a/Example39_Merging_Root_Events_to_Reduce_Run_Time.mp b/Example39_Merging_Root_Events_to_Reduce_Run_Time.mp
index 28cf824720516f298f5c3ae63df45fec9da66c2c..c585ce4d0dd8f3b9ca4eaefb0db2c8865888c88c 100644
--- a/Example39_Merging_Root_Events_to_Reduce_Run_Time.mp
+++ b/Example39_Merging_Root_Events_to_Reduce_Run_Time.mp
@@ -1,4 +1,4 @@
-/* Example39_Merging_Root_Events_to_Reduce_Run_Time.mp
+/* Example 39. Model of Merging Root Events to Reduce Run Time
Complex MP models may have large number of root events with several
coordination operations performed on clusters of roots. This may be
@@ -26,7 +26,10 @@ derivation task we introduce a separate root event B_and_C to
encapsulate the trace segment derivation (including the coordination)
for B and C.
-*/
+Instructions: Run for Scopes 1 and 2. Viewing of traces also includes a "Swim Lanes" option.
+
+==========================================================*/
+
SCHEMA Merging_Root_Events_to_Reduce_Run_Time
ROOT A: (* ( work | send_to_B) *);
ROOT B: (*<1.. $$scope + 1>
diff --git a/Example40_ApplicationProcess_partitioningLargeSchemaIntoSeparateSchemas.mp b/Example40_ApplicationProcess_partitioningLargeSchemaIntoSeparateSchemas.mp
index 38c2edccb15bd8554720fe9a5729e511818ba4db..a51fdfb36b837223e16671238cd66a81824488f3 100644
--- a/Example40_ApplicationProcess_partitioningLargeSchemaIntoSeparateSchemas.mp
+++ b/Example40_ApplicationProcess_partitioningLargeSchemaIntoSeparateSchemas.mp
@@ -1,4 +1,4 @@
-/* Example40_ApplicationProcess_partitioningLargeSchemaIntoSeparateSchemas.mp
+/* Example 40. Model of Application Process
An applicant submits application and needs to get it approved by
the bureaucratic chain of two officials. If the first official approves,
@@ -8,8 +8,11 @@ approve/reject the application or request it reworked and resubmitted.
Rework and resubmit events may be repeated several times. Each rejection
is final and cannot be followed by rework and resubmit events.
-*/
-SCHEMA Application_approval_process
+Instructions: Run for Scopes 1 and up. Viewing of traces also includes a "Swim Lanes" option.
+
+==========================================================*/
+
+SCHEMA Application_Process
ROOT Applicant:
prepare_application
@@ -54,4 +57,4 @@ DO ADD $r PRECEDES $rr; OD;
COORDINATE $a: approves_and_forwards_to_Applicant FROM Official_2,
$aa: application_is_approved FROM Applicant
-DO ADD $a PRECEDES $aa; OD;
\ No newline at end of file
+DO ADD $a PRECEDES $aa; OD;