Given the set of all people <#1229#> P<#1229#>, a floor is a set of ordered pairs of
People, where each ordered pair suggests a directional communication channel
from the first of the pair to the second. Of course the floor should only be
made up of the users currently in the conference, and we keep track of the
users of the system. Then all this information is captured by:
<#1230#>FLOOR<#1230#>
floor :
(P
P)
users :
P
floor
users
users
by+
By way of example we define some types of floor. Firstly the floor where
everybody has a communication channel with everyone else - except
themselves.
<#1232#>OPENFLOOR<#1232#>
FLOOR
floor =
{
x,y : P
\
|
\
x,y
users
(x,y)
}
-
{
x : P
\
|
\
x
users
(x,x)
}
by+
Then the (we imagine) very common floor where one speaker talks to all the
other people in the conference:
<#1233#>SPEAKERFLOOR<#1233#>
FLOOR
p,q : P
\
|
\
p,q
floor
fst
\
p = fst
\
q
#
floor
\
=
\
#
users - 1
by+