Promoting all the operations to act on the CONFERENCE Schema

Let us complete our conference schema, by adding all the operations to the schema (this is really just an example of modularisation and locality). <#1283#>CONFERENCE<#1283#> FLOOR ASIDES QUEUE-BIDS ALLOWED asides floor = floor allowed f : Bid \ | \ f queue f.floor allowed by+ (Note that asides are independent of floors. The predicate #tex2html_wrap_inline4186# states that no channel can be an aside as well as part of the current floor. This also says that we need only one two-way channel between each pair of users. It allows us as well to know easily which channels of the system are open at any time by considering the value of #tex2html_wrap_inline4188#.) So we now we write down our operations, and because of our modularity, a lot of this promotion is trivial. For example the operation of asking to be able to hear another speaker in the current floor is just written. <#1284#>CONF-REQUEST-LISTEN-SPEAKER<#1284#> Request-Listen-Speaker ASIDES QUEUE-BIDS ALLOWED floor { (p?,u?) } allowed by+ And we can do this precisely because this operation doesn't affect any of the other part of the conference system. Here is another example. Consider what happens when a new aside is requested- does this affect any of the other Schema? No, of course not. All we must do is make sure that the requested aside is not an existing channel in the current floor (since we must have that the intersection of <#1285#> asides<#1285#> and <#1286#> floor<#1286#> is empty). Thus: <#1287#>CONF-ASIDE1<#1287#> FLOOR ASIDE1 QUEUE-BIDS ALLOWED (u?, p?) floor by+ And just one more example, making a bid merely changes the state of the QUEUE-BIDS schema, so promoting the operator to act on the whole conference is again trivial: <#1288#>CONF-NEW-BID<#1288#> FLOOR ASIDE NEW-BID ALLOWED by+ Many operators will promote just as easily. Now though, we must describe the operations that effect more than just one part of the Conferencing system, for example let us start with what happens when the lifetime of a floor comes to an end. Remember how this happens? Well a speaker stops talking and if he is the last speaker of that floor than the current floor will be replaced by the floor requested by the highest ranked bid. We do not, in any way though wish this change of floor to interrupt existing asides- why should it? Here goes, we use the FINISHED2 schema defined before. Note that an aside is over-written in the channel is part of the new floor. (This is to maintain the truth of the predicate #tex2html_wrap_inline4190#). <#1289#>CONF-NEWFLOOR<#1289#> FINISHED2 ASIDES QUEUE-BIDS ALLOWED # queue ;SPM_gt; 0 queue' = (tl \ queue) floor' = (hd \ queue) floor asides' = asides - (hd \ queue).floor users' = (hd \ queue).users by+ This only really leaves us to clear up what happens when a users joins or leaves the conferencing system. First let us describe what happens when they join. We suggest at this time that a new user not only becomes an audience for all the maximal speakers of the present floor, but also for all the maximal speakers in all the floors of the requested bids. <#1290#>CONF-ADD-USER<#1290#> ADDUSER ASIDES QUEUE-BIDS ALLOWED n : 1.. # queue ( { n } queue').users = ({ n } queue).users { u? } \ n : 1.. # queue ( { n } queue').floor = ({ n } queue).floor \ \ \ \ \ \ \ \ \ \ \ \ \ { q : P \ | \ q \ maximal \ ( { n } queue). floor (q,u?) } asides' = asides by+ If a user wishes to leave a conference then they should first remove all the bids they have made which are currently in the queue of requested bids. This operation was described in section 4.6 (<#1291#> REMOVE-ALL-BIDS)<#1291#>, and is easily promoted. <#1292#>CONF-REMOVE-ALL-BIDS<#1292#> FLOOR ASIDE REMOVE-ALL-BIDS ALLOWED by+ Once this has succeeded and the user has no bids in the queue, they may leave the system. In other words a pre-condition of leaving the conference is that no bids are currently in the queue which have been made by the person wishing to leave the conference. <#1293#>CONF-LEAVE<#1293#> LEAVE-F LEAVE-A QUEUE-BIDS ALLOWED b : Bid \ | \ b queue b.requestor = u? n : 1.. # queue ( { n } queue').users = ({ n } queue).users - { u? } n : 1.. # queue ( { n } queue').floor = ( { n } queue).floor \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ - { x,y : P \ | \ (x = u? y = u? (x,y) } by+