This consists of an ordered sequence of ranked ``bids'' for desired floors.
The bids are ordered, or ranked, by a weighting function <#1265#> W<#1265#>, which
scores each Bid. Firstly let us describe a Bid:
<#1266#>BID<#1266#>
FLOOR
requester : P
id :
time-of-request : Time
s : SPEECH-ACT
request
FLOOR.users
by+
A bid can only be made if the <#1267#> users<#1267#> part of the <#1268#> FLOOR<#1268#> schema
contains the requester.
So now, we can give our schema for QUEUE-BIDS:
<#1269#>QUEUE-BIDS<#1269#>
W : Bid
queue :
[Bid]
users : P
p,q : Bid
\
|
\
p,q
queue
W
\
p
W
\
q
by+
Then we say that change of state of the <#1270#> QUEUE-BIDS<#1270#> schema does not affect
the Weighting function:
<#1271#> QUEUE-BIDS<#1271#>
QUEUE-BIDS
QUEUE-BIDS'
W' = W
by+
Default values of the bid would be that the <#1272#> FLOOR.users<#1272#> became equal
to the current variable <#1273#> users<#1273#>. That <#1274#> FLOOR<#1274#> is given the value
<#1275#> SPEAKERFLOOR<#1275#> with the requestor as the sole speaker, and that the type
of speech act, is an assertion.
Now there are two operations that affect this schema independently of the
other schemas mentioned. Firstly, requesting a bid:
<#1276#>NEW-BID<#1276#>
b? : Bid
QUEUE-BIDS
queue' =
queue
{
b?
}
by+
And that of removing a bid; of course a precondition for this will be that
the bid was actually made by the person removing the bid:
<#1277#>REMOVE-BID<#1277#>
u? : P
id :
QUEUE-BIDS
b : Bid
\
|
\
b
queue
b.id = id
b.requestor = u?
queue' =
queue -
{
b
}
by+
Then for completion (we shall use this operation later) the operation of
removing all one's own bids from the current queue of bids:
<#1278#>REMOVE-ALL-BIDS<#1278#>
u? : P
QUEUE-BIDS
queue' =
queue -
{
b: Bid
\
|
\
b
queue
b.requestor = u?
b
}
by+