Offline Team3 Benchmark1

AuctionBidding. This property is about bids on items on an online auction site.

Benchmark Data

The Trace Part

There are 4 traces in marq/offline/bench1

• auction_trace_valid
• auction_trace_invalid1
• auction_trace_invalid2
• auction_trace_invalid3

The first trace satisfies the property and is a long trace of 13,430,408 events with 484,416 create_auction events, 12,846,793 bid events, 98,199 sold events and 1000 endOfDay events.

The other three traces are relatively short traces capturing different ways in which the property can be violated.

• invalid1 sells an item for less than the minimum
• invalid2 sells an item after its period expires
• invalid3 sells an item twice

These are all based on a trace consisting of the first 6 days (84,780 events) of the valid trace. This consists of 3062 create_auction events, 80,742 bid events, 970 sold events and 6 endOfDay events. In the first two cases data values are altered to make the traces invalid and in the third case an additional sold event occurs.

The trace to be used in the competition is auction_trace_valid, other traces are for demonstration/testing.

The Property Part

Informal Description

When an item is being sold an auction is created and recorded using the create_auction(item,minimum,period) event where minimum is the minimum price the item can be sold for and period is the number of days the auction will last. Each bid on the item must be strictly larger than the previous bid; bids are recorded by the event bid(item,amount). The auction is over when the period is over or the item is sold. An item can only be and must be sold if the last bid amount is greater than the minimum price; the sold(item) event records when an item is sold. After the auction is over no events related to the item are allowed. An item can only be placed for auction once. The passing of days is recorded by a propositional endOfDay event; the period of an auction is over when there have been period number of endOfDay events.

Demonstration Traces

The following traces should be accepted

   create_auction(hat,4,10).bid(hat,1).bid(hat,3).bid(hat,4).sold(hat)
   create_auction(hat,4,10).endOfDay.endOfDay.bid(hat,3)
   create_auction(shoes,50,2).create_auction(hat,4,10).bid(shoes,50).bid(hat,3).sold(shoes)

The following traces should be rejected

   create_auction(hat,5,10).bid(hat,1).bid(hat,3).bid(hat,4).sold(hat)
   create_auction(hat,4,1).endOfDay.endOfDay.bid(hat,3)
   create_auction(shoes,50,2).create_auction(hat,4,10).bid(shoes,50).bid(hat,5).sold(shoes)

Each of these invalid traces are versions of the valid traces where a number has been changed to make the trace invalid. In the first trace the hat is sold for less than the minimum. In the second trace there is a bid on the hat after the period ends. In the third trace the hat has had a bid that takes it above the minimum but has not been sold.

Formal Specification

   qea(AuctionBidding){
     Forall(item)
      
     accept next(start){ 
         create_auction(item,minimum,period)  -> created 
         endOfDay -> start
     }
     accept next(created){
         endOfDay if[ period>1 ] do[ period:=period-1 ] -> created
         endOfDay if[ period=1 ] -> auctionOver
         bid(item,amount) if [ amount > last_amount and amount <  minimum ] 
                          do [ last_amount:=amount ] -> created
         bid(item,amount) if [ amount > last_amount and amount >= minimum ] 
                          do [ last_amount:=amount ] -> aboveMin
     }
     next(aboveMin){
         bind(item,amount) if[ amount > last_amount ] do [ last_amount:=amount ] -> aboveMin
         sold(item) -> auctionOver
         endOfDay if[ period>1 ] do[ period:=period-1 ] -> aboveMin
     }
     accept next(auctionOver){ endOfDay -> auctionOver }
   }

Clarification Requests

This is a space where other teams can ask for clarifications and the submitting team can answer. When a team requests a clarification, the team should be mentioned in the request and the request timestamped. The team submitting the benchmark should ensure they watch this page so that they get notifications of questions.