Page tree
Skip to end of metadata
Go to start of metadata
  1. Does MP check to make sure that every behavior listed under actors section appears in at least one interaction?
    1. The event trace generator code does not currently check for that condition, or vice versa.  Not all events will have an interaction, but all events specified in an interaction need to be present in some root event.  It is a common bug in student models due to misspellings or deletions.
    2. Yes, MP trace generator guarantees that all valid traces within given scope will be produced.

      try to run the following example (for scope 1).

      SCHEMA s1

      ROOT A: a (b | c) d;

      ROOT B: e C;

      C: f (g | h);

      and see how all possible traces are produced.

      Please read carefully Sec. 3 of the MP Manual)

  • No labels


  1. From the guides: "Pattern (+ B +) may be used to denote a sequence of one or more events B, and {+ B +} denotes a set of one or more events B."  What is the difference between (+B+) and {+B+}? 

  2. (+ B +) yields ordered wrt PRECEDES sequence of Bs, {+ B +} denotes a set of unordered Bs, see Fig. 1 on page 7 of the MP Manual. It explains the difference between (* B *) and {* B *}, but (+ B +) and {+ B } are similar, the only difference is that ( +) and {+ +} should contain at least one event, where (* *) and {* *} may be empty.

  3. Thank you Mikhail.  I failed to match the explanation to the figure, or note the keyword "sequence" was missing... Presumably, ordered means sequence and implies PRECEDES and implies one at a time...  Does unordered imply that events could happen simultaneously or is that irrelevant/abstracted?

  4. Unordered (i.e. set vs sequence) implies that events can happen concurrently.   In MP sequences and sets of events can be combined.   A space between two events implies the PRECEDES relationship.    For example  "{a, b c}"   means that the event a and the event sequence (b c) are concurrent.   This is indicated syntactically by the comma between a and ( b c ) You can see this on the GUI because FOLLOWS (the reverse of PRECEDES) is shown only between events b and c on the picture by the dark arrow.  While a always happens, it could be either before or after c.   Also note that ( ) cannot be used (even with the comma) to indicate unordered.