From 2bea2d8eadb0ae83ff076c9a723cc30643f45b9d Mon Sep 17 00:00:00 2001
From: Pamela Dyer <pamela.dyer@uconn.edu>
Date: Fri, 25 Jun 2021 19:55:17 +0000
Subject: [PATCH] Pamela's 2nd Merge Request - FIXED
---
...e01_SimpleMessageFlow_EventCoordination.mp | 6 +-
...01a_UnreliableMessageFlow_VirtualEvents.mp | 5 +-
Example02_DataFlow_EventSharing.mp | 8 +-
...e03_ATMWithdrawal_BehaviorOfEnvironment.mp | 10 +--
Example04_StackBehavior_EnsureCondition.mp | 12 ++-
...e04a_StackBehavior_UserDefinedRelations.mp | 74 +++++++++++--------
...e04b_QueueBehavior_UserDefinedRelations.mp | 69 ++++++++---------
Example05_CarRace_NestedComposition.mp | 8 +-
...e06_UnreliableChannel_AssertionChecking.mp | 5 +-
...le07_UnconstrainedStack_TraceAnnotation.mp | 5 +-
...loyer_CoordinationAcrossHierarchyLevels.mp | 10 +--
...ple09_PipeFilter_TraceAnnotationQueries.mp | 5 +-
...ple10_PublishSubscribe_EventReshuffling.mp | 11 ++-
...ple11_RingTopology_UserDefinedRelations.mp | 5 +-
...e12_CardiacArrestWorkflow_VirtualEvents.mp | 4 +-
...3_ConsumersSuppliers_DependencyTracking.mp | 7 +-
Example14_ShoppingSpree_NumberAttributes.mp | 4 +-
...ple15_BackpackWeight_IntervalAttributes.mp | 5 +-
...ckBehavior_ProbabilityCalculationsType1.mp | 9 ++-
...aredEvents_ProbabilityCalculationsType1.mp | 9 ++-
...en_BayesianProbabilityCalculationsType2.mp | 8 +-
...or_BayesianProbabilityCalculationsType2.mp | 8 +-
Example20_Activity_Diagram.mp | 8 +-
Example21_DataFlow_LocalReport.mp | 10 ++-
Example22_SimpleMessageFlow_GlobalReport.mp | 6 +-
Example23_CarRace_LocalGraph.mp | 5 +-
Example24_Compiler_ComponentDiagram.mp | 11 +--
Example25_Graph_as_Data_Structure.mp | 10 ++-
...ple26_UnreliableMessageFlow_GlobalQuery.mp | 8 +-
...ssemblingStatistics_Table_and_Bar_Chart.mp | 6 +-
Example28_AssemblingStatistics_Histogram.mp | 10 ++-
Example29_AssemblingStatistics_Gantt_Chart.mp | 8 +-
...e30_MicrowaveOven_ModelingModelChecking.mp | 8 +-
Example31_Aspect_Oriented_Paradigm.mp | 8 +-
Example32_Petri_Net.mp | 7 +-
Example33_ATMWithdrawal_StatechartView.mp | 7 +-
...ple34_FiniteStateDiagram_PathAnnotation.mp | 10 +--
Example35_FiniteStateDiagram_PathDiagram.mp | 8 +-
Example36_Authentication_SystemReuse.mp | 10 +--
Example37_Compiler1_ComponentReuse.mp | 8 +-
Example38_Compiler2_ComponentReuse.mp | 8 +-
..._Merging_Root_Events_to_Reduce_Run_Time.mp | 7 +-
...titioningLargeSchemaIntoSeparateSchemas.mp | 11 ++-
43 files changed, 258 insertions(+), 203 deletions(-)
diff --git a/Example01_SimpleMessageFlow_EventCoordination.mp b/Example01_SimpleMessageFlow_EventCoordination.mp
index 9b604dd..2e0f661 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 207b96a..d7a23e6 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 47d18b6..6459a5d 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 245fcae..c343378 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 1ddf8bc..23db197 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 196b587..0264da3 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 b22b82e..61b342a 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 766eda9..3c2c096 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 5a021fe..5bb6667 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 2587453..270ca31 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 92d6736..436259d 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 2a59ae8..e66badb 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 45a0b63..a3ce1cd 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 0ce9061..bc83e67 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 a29f138..24768d3 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 f1a8117..a35ac24 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 f6ce753..d429ae8 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 c596c95..a291d6a 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 f35fec7..849e948 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 c08f59d..44b8550 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 a7c160f..a7b421b 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 d8c8db1..0173c2b 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 8091ca5..3aeeb31 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 01c847f..e3a7524 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 6bbc765..0a65ba2 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 6ec84f2..eb55913 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 f8c2322..4a98981 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 019fea3..40edc33 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 84f651d..5acf62d 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 c3f18e0..19bcfec 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 908ca95..d7fdc6e 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 dc1ad1b..305baa0 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 a8c23e4..ddbf74f 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 63efa4a..e52b875 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 01ef7c7..a13f23b 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 79a8340..b720314 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 6946cd0..06e7dfa 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 7b6af2b..c2a67b0 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 993b889..d7c98e6 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 1b90df9..e1282ad 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 1c2fc02..01d78de 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 28cf824..c585ce4 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 38c2edc..a51fdfb 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;
--
GitLab