The predicate that decides whether to dequeue a high priority item included a negation operator, but this reversed the correct sense.
Tested on x86_64-pc-linux-gnu, committed on trunk 2011-10-24 Matthew Heaney <hea...@adacore.com> * a-cuprqu.adb, a-cbprqu.adb (Dequeue_Only_High_Priority): Predicate had wrong sense.
Index: a-cbprqu.adb =================================================================== --- a-cbprqu.adb (revision 180365) +++ a-cbprqu.adb (working copy) @@ -51,8 +51,31 @@ Success : out Boolean) is begin + -- This operation dequeues a high priority item if it exists in the + -- queue. By "high priority" we mean an item whose priority is equal + -- or greater than the value At_Least. The generic formal operation + -- Before has the meaning "has higher priority than". To dequeue an + -- item (meaning that we return True as our Success value), we need + -- as our predicate the equivalent of "has equal or higher priority + -- than", but we cannot say that directly, so we require some logical + -- gymnastics to make it so. + + -- If E is the element at the head of the queue, and symbol ">" + -- refers to the "is higher priority than" function Before, then we + -- derive our predicate as follows: + + -- original: P(E) >= At_Least + -- same as: not (P(E) < At_Least) + -- same as: not (At_Least > P(E)) + -- same as: not Before (At_Least, P(E)) + + -- But that predicate needs to be true in order to successfully + -- dequeue an item. If it's false, it means no item is dequeued, and + -- we return False as the Success value. + if List.Length = 0 - or else not Before (At_Least, Get_Priority (List.First_Element)) + or else Before (At_Least, + Get_Priority (List.Container.First_Element)) then Success := False; return; Index: a-cuprqu.adb =================================================================== --- a-cuprqu.adb (revision 180365) +++ a-cuprqu.adb (working copy) @@ -72,8 +72,29 @@ Success : out Boolean) is begin + -- This operation dequeues a high priority item if it exists in the + -- queue. By "high priority" we mean an item whose priority is equal + -- or greater than the value At_Least. The generic formal operation + -- Before has the meaning "has higher priority than". To dequeue an + -- item (meaning that we return True as our Success value), we need + -- as our predicate the equivalent of "has equal or higher priority + -- than", but we cannot say that directly, so we require some logical + -- gymnastics to make it so. + + -- If E is the element at the head of the queue, and symbol ">" + -- refers to the "is higher priority than" function Before, then we + -- derive our predicate as follows: + -- original: P(E) >= At_Least + -- same as: not (P(E) < At_Least) + -- same as: not (At_Least > P(E)) + -- same as: not Before (At_Least, P(E)) + + -- But that predicate needs to be true in order to successfully + -- dequeue an item. If it's false, it means no item is dequeued, and + -- we return False as the Success value. + if List.Length = 0 - or else not Before (At_Least, Get_Priority (List.First.Element)) + or else Before (At_Least, Get_Priority (List.First.Element)) then Success := False; return;