Operations on the FLOOR schema

The first operation we define, is that of a new user joining the conference system. And by default we join them to the listeners of any maximal speaker, so: <#1243#>ADDUSER<#1243#> u? : P FLOOR u? users users' = users { u? } floor' = floor { q : P \ | \ (q \ maximal \ floor) (q, u?) } by+ (Note in all examples u? represents the person initiating the operation.) Of course the user may not be very happy about this, and so we define operations where they can stop having to listen to a speaker. So if a user <#1244#> u?<#1244#> wishes to stop hearing the speaker <#1245#> p?<#1245#>, we have: <#1246#>REMOVE-LISTEN-SPEAKER<#1246#> u?,p? : P FLOOR u?, p? users (p?,u?) floor floor' = floor - { (p?,u?) } users' = users by+ And, correspondingly, any user should be able to get to hear any speaker of a floor: (This operation is optional, it may not be allowed.) <#1247#>REQUEST-LISTEN-SPEAKER<#1247#> u?,p? : P FLOOR u?, p? users speaker \ floor \ p? ;SPM_gt; 0 floor' = floor { (p?, u?) } users' = users by+ The first predicate in the above schema states that p? is already speaking- there is not much point listening to them if they are not. If the speaker wasn't specified, then the default would be for a channel to be set up from the maximal speaker of the current floor to the user <#1248#> u?<#1248#>. Next, we give the converse of the operation of a user joining a conferencing system, namely leaving it. We suggest at this point that in order for a user to leave a conference they must <#1249#> not<#1249#> be a speaker of the current floor. If that is true, then we close any open channels involving the user and remove the user from the variable <#1250#> users<#1250#>. <#1251#>LEAVE-F<#1251#> u? : P FLOOR speaker \ u? \ floor = 0 floor' = floor - { p : P \ | \ (p, u?) floor (p, u?) } users' = users - { u? } by+ Then finally, we specify an ``I've finished operation''. That is, when a speaker has finished what they wanted to say. If there are other speakers as well as the person finishing, we just close all the open channels for which P is the speaker: <#1252#>FINISHED1<#1252#> u? : P FLOOR speaker \ floor \ u? ;SPM_gt; 0 p:P \ | \ p u? speaker \ floor \ u? ;SPM_gt; 0 floor' = floor - { p : P \ | \ (u?, p) floor (u?, p) } users' = users by+ However if the ``I've finished'' operation is engaged where the initiator is the only current speaker, then the floor becomes empty (i.e. there is a special case of finishing). (In fact the floor becomes what the highest ranked bid requests- we shall see this later) so we write, for the time being: <#1253#>FINISHED2<#1253#> u? : P FLOOR speaker \ floor \ u? ;SPM_gt; 0 p:P \ | \ p u? speaker \ floor \ u? ;SPM_gt; 0 floor = users' = users by+