Parser error: Unclear scoping - decision needed

[pjljvandelaar]

The following model is accepted by TorXakis:

PROCDEF p [Input1, Input2 :: Int; Output :: Int] () ::=
        Input1 ? x 
    >-> Input2 ? y [[ x <> y ]] 
    >-> Output ! x + y | Input1 ?x | Input2 ?y [[ x == y ]]
    >-> Output ! x + y
    >-> STOP
ENDDEF

CHANDEF chans ::= Input1,Input2, Output :: Int ENDDEF

MODELDEF M ::=
    CHAN IN Input1, Input2
    CHAN OUT Output
    SYNC {Input1},{Input2},{Output},{Output | Input1 | Input2}
    BEHAVIOUR
        p[Input1, Input2, Output]()
ENDDEF

However when doing

stepper M
step 2
menu

one obtains [].

The scoping rules according to Jan should be:

PROCDEF p [Input1, Input2 :: Int; Output :: Int] () ::=
        Input1 ? x'  
    >-> Input2 ? y' [[ x' <> y' ]] 
    >-> Output ! x' + y' | Input1 ?x | Input2 ?y [[ x == y ]]
    >-> Output ! x + y
    >-> STOP
ENDDEF

I don't know whether I agree: I think an act offer should be a single data structure. Furthermore, we often use the following transformation as well:

A ! x <==> A ? A$1 [[ A$1 == x]]

Applying this in p yields

PROCDEF p [Input1, Input2 :: Int; Output :: Int] () ::=
        Input1 ? x  
    >-> Input2 ? y [[ x <> y ]] 
    >-> Output ? Output$1 | Input1 ?x | Input2 ?y [[ (Output$1 == x + y) /\ (x == y) ]]
    >-> Output ! x + y
    >-> STOP
ENDDEF

making it even stranger that the x and y should be different (due to their scope)!

I think we should make a decision that is also clear to our users. I have no problems with even forbidding this construct (declaring variable using ? and communicating its value using ! in a single ActOffer).

[tretmans]

1. in any language you can write bullshit by reusing same names for different things. If you think this is confusing, and I think it is, then use a different name for the second use of x. In other words: these are these typical constructions that you should not use, but which, if used, should be well defined. And in TXS they are.
2. the alternative of having the x' in Output ! x' + y' refer to the x in the same line has also disadvantages: it would mean use before declaration which other people consider as counter-intuitive (in particular if you spread Output ! x + y | Input1 ?x | Input2 ?y [[ x == y ]] over many lines). Moreover, it is consistent with the use of assignment in STAUTDEF: { x := x +1 } The first x is the new value; the second x refers to the old value.
3. Conclusion: I am not so much in favour of changing the static semantics on this aspect.
4. Apparently this is a bug in the new compiler. V0.6.0 gives the right answer:

   
   TXS >>  TorXakis :: Model-Based Testing

TXS >> txsserver starting: "PC-31093.tsn.tno.nl" : 55355 TXS >> Solver "z3" initialized : Z3 [4.6.0] TXS >> TxsCore initialized TXS >> input files parsed: TXS >> p1.txs TXS >> info TXS >> TorXakis version : 0.6.0 (commit: 6f02370) TXS >> Build time : Thu 04/05/2018 9:05:20.97 TXS >> stepper M TXS >> Stepper started TXS >> step 10 TXS >> .....1: Act { { ( Input1, [ 0 ] ) } } TXS >> .....2: Act { { ( Input2, [ 1 ] ) } } TXS >> .....3: Act { { ( Input1, [ 0 ] ) ( Input2, [ 0 ] ) ( Output, [ 1 ] ) } } TXS >> .....4: Act { { ( Output, [ 0 ] ) } } TXS >> no state or deadlock TXS >> FAIL: No Output (Quiescence) TXS >>

Note that I had to change the model:

CHAN IN
CHAN OUT Input1, Input2, Output SYNC {Input1},{Input2},{Output},{Output | Input1 | Input2}

is not allowed with combinations of inputs and outputs. A set of SYNC actions must be input or output (what should a tester otherwise do with it?).  Another bug in the new compiler.

[pjljvandelaar]

So according to Jan, in a multi action,

• All variables in exclamation marks refer to variables defined before this multi action (the old context).
• All variables in the constraint refer to the new context.
• All variables in question marks introduce new variables, which are known in the rest of the action prefix (including the constraint) and which hide variables with the same name in the old context.

So the rewrite rule

A ! x <==> A ? A$1 [[ A$1 == x ]]

is more complicated

A ! x | B ? x [[ x>0 ]] >-> p <==> A ? A$1 | B ? B$1 [[ (A$1 == x) /\ (B$1 > 0) ]] >-> p [x/B$1]

And the context can change back and forth, like in the following example

 Input1 ?x 
| Input2 ?y
| Output ! x + y 
[[ x == y ]] 

For single actions, I could easily accept these rules. For multi-actions, I have my doubts whether these are the easiest ones for our users (both in the TorXakis language and at our API where you first make an ActOffer and then combine it into an ActionPref and use it in a large behaviour).

[pjljvandelaar]

At 2. you state use before declaration which other people consider as counter-intuitive. I have no problem with forbidding using newly defined variables in exclamation marks, since one could easily write the more clear statement Output ? z | Input1 ?x | Input2 ?y [[ (x == y) /\ (z == x+y) ]]

[pjljvandelaar]

I agree that the syntax should be clearly defined in the corner cases. Since one can put curly brackets around the actions to create a single multi action, for me a multi action hints at a shared scope. See e.g.

{ Input1 ?x 
| Input2 ?y
| Output ! x + y 
} [[ x == y ]]

Implementing the current behaviour of torxakis is easy given the name and a unique id that distinguished the one x from the other x. However, in the new implementation, we removed this unique id and want to rely on the name only. Since the code is bad / difficult to read anyway, it is insufficient reason for me to go back and add the unique id.

Discussed with Corado. He came up with

1. Sequence operator suggest change of scope to him. Note that this is inline with a stautdef that also assigns values on a whole transition (set of actions) and not on a part (single action).
2. This seemed correct to him (which is an error in current TorXakis):

   A ? y [[y >0]] >-> { B ?x | C !x } [[ x > 5]] >-> ....

We have now five choices

1. Use the original TorXakis scoping (and maybe have to reintroduce unique id for this reason only)
2. Internally use a different scope than in the TorXakis language and let the compiler handle the different scopes. Increase complexity and might be a source of bugs.
3. Change the scoping rules of TorXakis (and check all models for this change).
4. Forbidding this scoping confusion. I.e. it is an error to write A!x | B?x.
5. Make communication internally into two steps. First, communicate (with constraints) use old context and channel variables only. Second, pass communicate values on wards: assign the values of the channel variables to the newly declared variables (i.e. create the new context).

Let's discuss on monday!

[pjljvandelaar]

Note LPE handles it fine (some small changes for readability):

PROCDEF LPE_proxyProcess [ Input1 :: Int; Input2 :: Int; Output :: Int ] ( pc :: Int; x1 :: Int; x2 :: Int; y1 :: Int; x3 :: Int; y2 :: Int; x4 :: Int; y3 :: Int )
::=
( { Input1 ? Input1$1 :: Int } [[ ( 0 == pc ) ]]
>-> ( LPE_proxyProcess [Input1,Input2,Output] ( 1, Input1$1, x2, y1, x3, y2, x4, y3 )
) )
##
( { Input2 ? Input2$1 :: Int } [[ ( IF ( 1 == pc ) THEN (not (( Input2$1 == x1 )) ) ELSE False FI ) ]]
>-> ( LPE_proxyProcess [Input1,Input2,Output] ( 2, x1, x1, Input2$1, x3, y2, x4, y3 )
) )
##
( { Input1 ? Input1$1 :: Int | Input2 ? Input2$1 :: Int | Output ? Output$1 :: Int } [[ ( IF ( 2 == pc ) THEN ( IF ( Input1$1 == Input2$1 ) THEN ( Output$1 == ( x2 + y1 ) ) ELSE False FI ) ELSE False FI ) ]]
>-> ( LPE_proxyProcess [Input1,Input2,Output] ( 3, x1, x2, y1, x2, y1, Input1$1, Input2$1 )
) )
##
( { Output ? Output$1 :: Int } [[ ( IF ( 3 == pc ) THEN ( Output$1 == ( x4 + y3 ) ) ELSE False FI ) ]]
>-> ( LPE_proxyProcess [Input1,Input2,Output] ( -1, (ANY :: Int), (ANY :: Int), (ANY :: Int), (ANY :: Int), (ANY :: Int), (ANY :: Int), (ANY :: Int) )
) )
ENDDEF