Two local variables with the same name (XSTS)

[mondokm]

Declaring two local variables with the same name inside a transition causes both to appear in the trace output. Example code:

choice {
   local var a: integer = 1;
   x := x + a;
}
choice {
   local var a: integer = 2;
   x := x + a;
}

Resulting trace:

(XstsState post_init last_internal
  (ExplState
    (x 3)
    (a 1)
    (a 2)))
(XstsState post_init last_env
  (ExplState
    (x 3)
    (a 1)
    (a 2)))
(XstsState post_init last_internal
  (ExplState
    (x 6)
    (a 1)
    (a 2))))