package lect1_design;

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

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

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

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

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

    /**
     * @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)

    /**
     * @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)

    /**
     * @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)

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

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

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

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