Sequencing Composition with Model Programs

Question

Hi All,

Using the sequencing composition operator on model programs might often not be a good idea.
Anyway I would like to understand, how the definition is applied to this case.
Let's assume we have two scenarios Z1 and Z2 and a model program. A simple example is this

machine S2() : Actions 
{
  (Z1;Z2) || ModelProgram
}

machine S1() : Actions 
{
   (Z1 || ModelProgram );(Z2 || ModelProgram )
}

Using the "Chat"-example with the scenarios below shows:
* S1 and S2 both use the sequencing operator.
* S1 and S2 have different results.
* S1 sequences programs, S2 sequences scenarios.
* Machine S2 is often seen in the examples - S1 not.
* Machine S2 is understood easily, since the transitions in the two scenarios are just sequenced.
* Machine S1 has the problem, that identical states are not necessarily merged.
* Machine S1 : the right operand of the sequencing operator is empty, if explored alone, but not if used in S1.

How can the sequencing operator be defined now?
Thank You again!

P.S. "Chat"-example scenarios:

machine Z1() : Actions
{
    (LogonRequest(1);(!call LogonRequest* |?| _* ))
}

machine Z2() : Actions
{
    (LogoffRequest(1);(!call LogonRequest* |?| _* ))
}

My idea is currently something like this:

Explore states of the left operand. Go to accepting states. Make all these states non-accepting. Uses exactly these states as initial state in the right operand. Explore now with these initial states the right operand.
If identical transitions from these states exist in both operands, create a new state and cut all transitions to existing states from left operand.

Answer 1

Hi, sorry for the late reply.

Can you paste full code of Z1 and Z2?

I am trying machines like

machine Z1() : Actions where ForExploration = true
{
    (LogonRequest(1);(!call LogonRequest* |?| _* )) || BoundModelProgram
}

machine Z2() : Actions where ForExploration = true
{
    (LogonRequest(1) || BoundModelProgram); ((!call LogonRequest* |?| _* )||BoundModelProgram )
}

but I hit state bound.

 

Answer 2

Hi Xiang,

If I use "BoundModelProgram" instead of "ModelProgram" the exploration is very big.
So let's disable BroadcastRequest in this case.

To make my question clearer-if I look at both graph views (machine 1, 2) below:
Why do I get in case of machine 1 not the return from state9 to state3 (as in machine 2).

The definition of sequencing model programs seems to extend the sequencing to all steps in the right operand? Always new states are generated for every step in the right operand, right?

Thank you for your help!

========================
                                   Machine 1:
========================

========================
                                   Machine 2:
========================

Answer 3

That is correct. The meaning of "A ; B" is "all behaviors consisting of a behavior from A followed by a behavior from B". If you would go back to state 3 in your machine 2, you would get action sequences that don't match the above definition. So, as you well explain, once the exploration graph transitions to the second operand, it must stay there, which requires a new set of states.

Answer 4

Thank you Nico,

This explains all the effects:

* No transition back to state 3 in machine 1
* Two identical "LogoffRequests" from state 3, but only one "ListRequest" in machine 1.
* The repeating behavior in machine 1.

Thank you very much again for explaining the example to me!