/* Results
 * Author: qzy
 * Creation date: ÐÇÆÚ¶þ ÈýÔÂ 23 2010
 */
MACHINE
    Results
SETS
    RUNNER
VARIABLES
    finish
INVARIANT
    finish : iseq(RUNNER)
INITIALISATION
    finish := []
OPERATIONS
    finished(rn) =
    PRE
        rn : RUNNER & rn /: ran(finish)
    THEN
        finish := finish <- rn
    END;
    
    rn <-- query(pos) =
    PRE
        pos : NAT1 & pos <= size(finish)
    THEN
        rn := finish(pos)
    END;
    
    dequalify(pos) =
    PRE
        pos : NAT1 & pos <= size(finish)
    THEN
        finish := finish /|\ (pos - 1) ^ (finish \|/ pos)
    END;
    
    ss <-- medals =
    BEGIN
        ss := finish /|\ 3
    END
    
END