[sc34wg3] Tau: The role in operator

[Robert Barta]

On Sat, Jul 31, 2004 at 07:00:04PM -0400, Lars Marius Garshol wrote:
> When going through the Tau model at the RM workshop today we found one
> strange thing that we couldn't quite account for.
> 
> The role in operator is defined as
> 
>   a upm r = ...
...
> We discussed this at the RM workshop when Ann presented the model and
> agreed that there are two possible interpretations:
> 
>   1) m up r = {a | a element-of m ^ exists p | <r, p> element-of a}
>   
>   2) m up <r, p> = {a | a element-of m ^ <r, p> element-of a}
> 
> 
> Did we miss something, or is there a problem with the notation here?
> Also, which of the two interpretations is the intended one?

Lars (et.al),

This is clearly a typo. It should read

  p -> r = {a element-of m | exists p : <r, p> element-of a}

It basically delivers ALL assertions in the map where p is a player of
the role r.

\rho