#include <vcc.h>

typedef enum {
  METRO,
  INTERM,
  RURAL
} addrtype;

_(pure) int max(int a, int b)
_(ensures \result == (a > b ? a : b))
{
  if (a > b) return a;
  return b;
}

int calculate_price(int actual_weight, int v_s, int v_p, addrtype address_type)
{
  int price = -1;
  int effective_weight;
    
  switch(address_type) {
  case METRO:
    if (actual_weight <= 5 && v_s <= 5) { // small package
      effective_weight = max(actual_weight, v_s);
      price = 300 + 100 * max(0, effective_weight - 2);
    } else { //parcel
      effective_weight = max(actual_weight, v_p);
      price = 100 + 75 * max(0, effective_weight - 1);
    }
    break;
  case INTERM:
    if (actual_weight <= 5 && v_s <= 5) { // small package
      effective_weight = max(actual_weight, v_s);
      price = 500 + 150 * max(0, effective_weight - 2);
    } else { //parcel
      effective_weight = max(actual_weight, v_p);
      price = 225 + 125 * max(0, effective_weight - 1);
    }
    break;
  case RURAL:
    if (actual_weight <= 5 && v_s <= 5) { // small package
      effective_weight = max(actual_weight, v_s);
      price = 1000 + 250 * max(0, effective_weight - 2);
    } else { //parcel
      effective_weight = max(actual_weight, v_p);
      if (v_s <= 5) { // Special offer
	price = 225 + 125 * max(0, effective_weight - 1);
      } else { // regular price
	price = 500 + 275 * max(0, effective_weight - 1);
      }
    }
    break;
  }
  
  return price;
}