The ASIDE schema

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+