package lect1_coding;

import java.lang.String;

import utils.DomainConstraint;
import utils.NotPossibleException;
import utils.OptType;
import utils.AttrRef;
import utils.DOpt;

/**
 * @overview An armored vehicle used in the game
 * 
 * @attributes
 *  hitPoint    Integer     int
 *  damage      Integer     int
 *  armor       Integer     int
 *  price       Integer     int
 * 
 * @object
 *  A typical Tank is <hp, d, a, p> where hitPoint(hp), damage(d), armor(a), price(p)
 * 
 * @abstract_property
 *  mutable(hitPoint) = true /\ optional(hitPoint) = false /\ min(hitPoint) = 1
 *  mutable(damage) = true /\ optional(damage) = false /\ min(damage) = 1
 *  mutable(armor) = true /\ optional(armor) = false /\ min(armor) = 0
 *  mutable(price) = false /\ optional(price) = false /\ min(price) = 1
 * 
 * @author namhv
 */
public class Tank {
    @DomainConstraint(type="Integer", mutable=true, optional=false, min=1)
    private int hitPoint;

    @DomainConstraint(type="Integer", mutable=true, optional=false, min=1)
    private int damage;
    
    @DomainConstraint(type="Integer", mutable=true, optional=false, min=0)
    private int armor;
    
    @DomainConstraint(type="Integer", mutable=false, optional=false, min=1)
    private int price;

    /**
     * @effects
     *  if hp, d, a, p are valid
     *      initialize this as <tt><hp, d, a, p></tt>
     *  else
     *      throws NotPossibleException
     */
    public Tank(@AttrRef("hitPoint") int hp, @AttrRef("damage") int d, 
                @AttrRef("armor") int a, @AttrRef("price") int p) 
                throws NotPossibleException {
        if (!validateHitPoint(hp)) {
            throw new NotPossibleException(
                "Tank.init: Invalid Tank HP: " + hp
            );
        }

        if (!validateDamage(d)) {
            throw new NotPossibleException(
                "Tank.init: Invalid Tank damage: " + d
            );
        }

        if (!validateArmor(a)) {
            throw new NotPossibleException(
                "Tank.init: Invalid Tank armor: " + a
            );
        }

        if (!validatePrice(p)) {
            throw new NotPossibleException(
                "Tank.init: Invalid Tank price: " + p
            );
        }

        this.hitPoint = hp;
        this.damage = d;
        this.armor = a;
        this.price = p;
    }

    /**
     * @effects
     *      return hitPoint
     */
    @DOpt(type=OptType.Observer) @AttrRef("hitPoint")
    public int getHitPoint() {
        return hitPoint;
    }

    /**
     * @effects
     *      return damage
     */
    @DOpt(type=OptType.Observer) @AttrRef("damage")
    public int getDamage() {
        return damage;
    }

    /**
     * @effects
     *      return armor
     */
    @DOpt(type=OptType.Observer) @AttrRef("armor")
    public int getArmor() {
        return armor;
    }

    /**
     * @effects
     *      return price
     */
    @DOpt(type=OptType.Observer) @AttrRef("price")
    public int getPrice() {
        return price;
    }

    /**
     * @effects
     *      if hp is valid
     *          set this.hitPoint = hp
     *          return true
     *      else
     *          return false
     */
    @DOpt(type=OptType.Mutator) @AttrRef("hitPoint")
    public boolean setHitPoint(int hp) {
        if (validateHitPoint(hp)) {
            this.hitPoint = hp;
            return true;
        } else {
            return false;
        }
    }

    /**
     * @effects
     *      if d is valid
     *          set this.damage = d
     *          return true
     *      else
     *          return false
     */
    @DOpt(type=OptType.Mutator) @AttrRef("damage")
    public boolean setDamage(int d) {
        if (validateDamage(d)) {
            this.damage = d;
            return true;
        } else {
            return false;
        }
    }

    /**
     * @effects
     *      if a is valid
     *          set this.armor = a
     *          return true
     *      else
     *          return false
     */
    @DOpt(type=OptType.Mutator) @AttrRef("armor")
    public boolean setArmor(int a) {
        if (validateArmor(a)) {
            this.armor = a;
            return true;
        } else {
            return false;
        }
    }

    @Override
    public String toString() {
        // return "Tank: <" + hitPoint + "," + daƯmage + "," + armor + "," + price + ">";
        return String.format("Tank: <%d,%d,%d,%d>", hitPoint, damage, armor, price);
    }

    /**
     * @effects <pre>
     *      if this satisfies abstract properties
     *          return true
     *      else
     *          return false
     *      </pre>
     */
    public boolean repOK() {
        if (!validateHitPoint(hitPoint) || !validateDamage(damage) || !validateArmor(armor) || !validatePrice(price)) {
            return false;
        }

        return true;
    }

    /**
     * @effects <pre>
     *      if hp is valid
     *          return true
     *      else
     *          return false
     *      </pre>
     */
    private boolean validateHitPoint(int hp) {
        if (hp < 1) {
            return false;
        }
        return true;
    }

    /**
     * @effects <pre>
     *      if d is valid
     *          return true
     *      else
     *          return false
     *      </pre>
     */
    private boolean validateDamage(int d) {
        if (d < 1) {
            return false;
        }
        return true;
    }

    /**
     * @effects <pre>
     *      if a is valid
     *          return true
     *      else
     *          return false
     *      </pre>
     */
    private boolean validateArmor(int a) {
        if (a < 0) {
            return false;
        }
        return true;
    }

    /**
     * @effects <pre>
     *      if p is valid
     *          return true
     *      else
     *          return false
     *      </pre>
     */
    private boolean validatePrice(int p) {
        if (p < 1) {
            return false;
        }
        return true;
    }
}