An aside is where any user sets up a private one way link with any other
user. The analogy is sitting next to someone at a conference and whispering
in their ear. We stipulate that any user may only have one aside where they
are the speaker, and one where they are the listener. That is for a given
u?, the most asides allowed would be a (u?, p) and a (q, u?), of course, if
p=q, then we would have a conversation in progress, since both the channels
(u?, p) and (p, u?) would be open. This is, of course, merely a design
decision and is used for the purposes of exposition.
Here is the ASIDE schema:
<#1255#>ASIDE<#1255#>
users :
P
asides :
(P
P)
asides
users
users
p,q : P
P
\
|
\
p,q
asides
\
p
q
(fst
\
p
fst
\
q
snd
\
p
snd
\
q)
by+
Now some of the operations we wish to perform on our ASIDES schema are as
follows: a user may, at any time, set up an aside with another user, if the
initiating user does not have an aside with someone else or the recipient of
the requested aside is not the ``hearer'' in another aside. That is:
<#1256#>ASIDE1<#1256#>
u?,p? : P
ASIDE
u?
users
p?
users
u?
(fst*
asides)
p?
(snd*
asides)
asides' = asides
{
(u?,p?)
}
by+
Or a request for a two way aside- the pre-conditions for this are even
stronger- that neither user is involved in any asides:
<#1257#>ASIDE2<#1257#>
u?,p? : P
ASIDE
u?
users
p?
users
u?
(fst*
asides)
p?
(fst*
asides)
u?
(snd*
asides)
p?
(snd*
asides)
asides' = asides
{
(u?,p?)
}
{
(p?,u?)
}
by+
And similarly the operations of removing the aside are straightforward. Here
is the operation of removing a unidirectional aside (which was originally
set up by the same user):
<#1258#>REMOVE-ASIDE1<#1258#>
u?,p? : P
ASIDE
u?
users
p?
users
{
(u?,p?)
}
asides
asides' = asides -
{
(u?,p?)
}
by+
And of course if we could specify a REMOVE-ASIDE2 similarly to get rid of a
two-way aside.
If we extend the analogy of the aside in a conference, then a user may wish
to remove an aside channel that they didn't initiate, by moving somewhere
else or by telling the person initiating the aside to shut up in the real
conference. So we define a <#1259#> Remove-Unwanted-Aside operator<#1259#>. The only
difference here being that the aside <#1260#> (p?,u?)<#1260#> is removed rather than
<#1261#> (u?,p?)<#1261#>:
<#1262#>REMOVE-UNWANTED-ASIDE<#1262#>
u?,p? : P
ASIDE
u?
users
p?
users
{
(p?,u?)
}
asides
asides' = asides -
{
(p?,u?)
}
by+
When someone leaves the conferencing system then any asides they are
involved in must be removed.
<#1263#>LEAVE-A<#1263#>
u? : P
ASIDE
u?
users
asides' = asides -
{ p : P
\
|
\
(u?, p)
asides
(u?,p)
}
-
{ p : P
\
|
\
(p, u?)
asides
(p, u?)
}
users' = users -
{
u?
}
by+