module ebay

sig Client {
        bids : Auction -> Bid,
        auctions : set Auction
}
sig Product {}
sig Auction {
        product : lone Product
}
sig Bid {}

fact tables {
        -- all the auctions are in the product table (one)
        Auction in product.Product
        -- there is no Product table (note that the Product table "dies" without Product being a key)
        -- if we didn't "kill" the table, it would persist as a non-standard reference to a non-key
        Product in Auction.product
        -- there is no Bid table (same as for Product)
        Bid in Auction.(Client.bids)
}

fact refs {
        auctions in Client lone -> Auction
        {a : Auction, b : Bid, c : Client | c -> a -> b in bids} in Client.auctions -> Bid -> lone Client
}

pred inv {
        -- auction creators cannot bid for products that they are selling
        -- SQL: check before insertion on bids
        no bids.Bid.product & auctions.product
}