Interpreter: bug in parallel action and assignment?

[richardpaynea55]

This is related to an earlier bug about replicated parallelism. When I use an action with replicated parallelism, only one of the replications allows state to be updated. In the model below:

channels
  inA : nat * nat
  outA : nat * nat

process p = 
begin
  state
    a: nat :=0

  operations
    updateA : nat ==> ()
    updateA(newA) == 
      a := newA

  @ ||| n in set {1,...,3} @ [{}] inA.n!a -> updateA(n); outA!n!a -> Skip

end

I obtain various trace options, including:

[inA.3.0, outA.3.3, inA.1.0, outA.1.0, inA.2.0, outA.2.0]
[inA.1.0, outA.1.0, inA.3.0, outA.3.3, inA.2.0, outA.2.0]

It appears that the state variable a is updated only when n=3. I am assuming there is no shared state (which would result in a=6), and it seems that only one of the replication branches allows assignments to hold.

[lausdahl]

Is this what you expected:

inA.2.0,inA.3.0,inA.1.0,outA.1.1,outA.3.3,outA.2.2

[joey-coleman]

I doubt it's what Richard expected, but that is one (of perhaps 8) possible valid traces.

[richardpaynea55]

It was not what I'd hoped, but Kenneth and I discussed this and agree that this is the correct behaviour, where the action:

@ (||| n in set {1,...,3} @ [{a}] inA.n!a -> updateA(n); outA!n!a -> Skip); finalout!a -> Skip 

would result in a sample trace:

[inA.2.0,inA.3.0,inA.1.0,outA.1.1,outA.3.3,outA.2.2,finalout.0]

i.e. the local variable a is destroyed. We assume that there is no way to obtain the value a at the end of the replication.

[lausdahl]

Currently the value finalout.x will be the a state of the last one executed. This is because no delayed context is wrapped around the last branch of of the replicated AST.