updating state using operations vs updating directly in an action

[JeremyBryans]

Hi,

In the process below, action Go2 updates a map in state directly; action Go3 updates it via an operation.

I would have expected both to have the same effect, but the operation loses the original maplet in mem in favour of the second, even though the two maplets are not compatible.

Any ideas? I'm on Symphony 0.3.3.

Thanks, Jeremy

channels

DebugMem : map nat to nat

process TEST = begin

state
  mem : map nat to nat := {|->}

  operations

  write:(nat) ==> ()
   write(m) ==  
    mem := mem ++ {m|->3}

   actions

  Go2 = for all i in set {2,3} do
   (mem := mem ++ {i|->3});
    DebugMem!mem -> Skip   --- [DebugMem.{2 |-> 3, 3 |-> 3}]

  Go3 = for all i in set {2,3} do 
   (write(3));
  DebugMem!mem -> Skip --- [DebugMem.{3 |-> 3}]
  @
  Go3

 end

[alvarohm]

You are calling the operation on 3. I think it should be on i.

[JeremyBryans]

Thanks Alvaro, You're right. My mistake.