class Auction {    

  string itemName; int initPrice;
  int maxBid; int bidder;
  
  //@ invariant true;
  //@ initial true;
  void Auction(string item, int price) {
    itemName = item;
    initPrice = price;    
    maxBid = 0;
    bidder = -1;         
	canBid = true;
  }  
  
  //@ requires true;
  //@ ensures true;   
  boolean auctionOpen() {
	canBid;
  }
  
  //@ requires true;
  //@ ensures true;   
  void bid(int pid, int bid) {   
    if(maxBid <= bid) {          
      bidder = pid;
      maxBid = bid;      
    }
  }

  //@ requires true;
  //@ ensures true;
  int getInitialPrice() {
    initPrice;
  }
  
  //@ requires true;
  //@ ensures true;
  int getMaxBid() {
    maxBid;
  }  
  
  //@ requires true;
  //@ ensures true;
  int getBidder() {
    bidder;
  }    
}

unrestricted class AuctionMap {
      
  Auction a;
       
  //@ invariant true;
  //@ initial true;	   
  void AuctionMap() {
    unit;
  }
  
  //@ requires true;
  //@ ensures true;
  void put(Auction auction) {
    a = auction;
  }
  
  //@ requires true;
  //@ ensures true;
  void get() {
    a;
  }
}

class Bidding {

  Auction a; 
  int myBidder; int price;  
  boolean done; boolean init;
  
  //@ invariant true;
  //@ requires auction.auctionOpen();
  //@ initial price == -1 && myBidder == -1 && !done && init;	  
  void Bidding(Auction auction) {
    a = auction;
    price = -1;
	myBidder = -1;
	init = true;
	done = false;
  }
  
  //@ requires myBidder == -1 && price == -1  && !done && init;
  //@ ensures myBidder >= 0 && price == -1 && !done && init;
  void register(int bidder) {
    myBidder = bidder;  
  }  
  
  //@ requires myBidder >= 0 && price == -1 && !done && init;
  //@ ensures myBidder >= 0 && price >= 0 && !done && init;
  int getPrice() {
    if(price == -1)
      price = a.getInitialPrice();
    price;  
  }    
  
  //@ requires price >= 0 && !done && init;
  //@ ensures done && init;
  void bid(int price) {      
    a.bid(myBidder, price);
  }
  
  //@ requires price >= 0 && !done && init;
  //@ ensures done && init;
  void done() {
    unit;
  }  
  
  //@ requires !done && init;
  //@ ensures !done && init;
  boolean canRegister() {
	  init;
  }
}
	
class Selling {

  Auction a; 
  int finalPrice;
  boolean done;
  boolean init;
  boolean sold;
  
  //@ invariant true;
  //@ requires auction.auctionOpen();
  //@ initial finalPrice == -1 && !done && init && !sold;	
  void Selling(Auction auction) {
    a = auction;  
	finalPrice = -1;
	init = true;
	sold = false;
	done = false;
  } 
  
  //@ requires finalPrice == -1 && finalPrice < a.getInitialPrice() && !sold && !done && init;
  //@ ensures (|result| -> sold) && (init && !done && finalPrice > -1);
  boolean sold() {    
    finalPrice = a.getMaxBid();
    sold = finalPrice >= a.getInitialPrice();
	sold;
  }
     
  //@ requires sold && !done && init && finalPrice > -1;
  //@ ensures done && init;
  int getPrice() {
    finalPrice;
  }
  
  //@ requires !sold && !done && init && finalPrice > -1;
  //@ ensures done && init;
  void done() {
    unit;
  }
  
  //@ requires !done && init;
  //@ ensures !done && init;
  boolean canRegister() {
	  init;
  }
}

class Auctioneer {      
                
  AuctionMap map;
  
  //@ invariant true;
  //@ initial map != null;	   
  void Auctioneer() {
    map = new AuctionMap();  
  } 
  
  //@ requires map != null;
  //@ ensures map != null && s.canRegister();
  Selling selling(string item, int initPrice) {
    Auction a; a = new Auction(item, initPrice);
	map.put(a);
	Selling s;
	s = new Selling();
	s;
  }  
  
  
  //@ requires map != null;
  //@ ensures map != null && b.canRegister();	
  Bidding bidding(string item) {    
    Bidding b; b = new Bidding(map.get(item));
    b;
  }
   
}

class Bidder {
  
  int myPid; int myPrice; 
  Auctioneer a; boolean done;

  //@ invariant true;
  //@ requires auctioneer;
  //@ initial !done;
  void Bidder(Auctioneer auctioneer, int pid, int price) {
    a = auctioneer;
    pid = pid;
    myPrice = price;
    myPid = -1;
	done = false;
  }
  
  //@ requires !done;
  //@ ensures done;
  void run() {    
    Bidding b; b = a.bidding("psp");      
    b.register(myPid);   
    if(b.getPrice() <= myPrice)        
      b.bid(myPrice); 
    else {
	  done = true;
	  b.done();
	}     
  }
}

class Seller {  

  string myItem; int myPrice;
  Auctioneer a;
  
  //@ invariant true;
  //@ requires auctioneer;
  //@ initial !done;
  void Seller(Auctioneer auctioneer, string item, int price) {
    a = auctioneer;
    myItem = item;
    myPrice = price;
  } 
 
  //@ requires !done;
  //@ ensures done;
  void run() {    
    Selling s; 
    s = a.selling(myItem, myPrice);           
    printStr("waiting... ");

    if(s.sold()) {
      printStr("made ");
      printInt(s.getPrice());
      printStr(" euros!\n");          
    } else {
      s.done(); 
      if(lowerPrice())       
        run();
    }
  }
  
  //@ requires false;
  //@ ensures false;
  boolean lowerPrice() {
    boolean lower;
    if(myPrice > 80) {
      myPrice = 80;
      lower = true;
    }   
    lower;
  }  
}