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+