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+