package gestionProc;


public class Processus
{
    /*@ public invariant prio >= 0 && prio <= PRIO_MAX;
      @ invariant myid.matches("[0-9]*");
      @ invariant myid.length() == TAILLE_IDENT;
      @
      @*/

    public static int PRIO_MAX = 25;
    public static int TAILLE_IDENT = 4;

    private /*@ spec_public @*/ int prio;
    private /*@ spec_public @*/ String myid;

    /**
     * Construit un processus
     * @param p La priorite
     * @param id L'identifiant
     */
    /*@ requires p >= 0 && p <= PRIO_MAX;
      @ requires id != null;
      @ requires id.length() == TAILLE_IDENT;
      @ requires id.matches("[0-9]*");
      @
      @ ensures myid.equals(id);
      @ ensures prio == p;
      @*/
    public Processus(int p, String id)
    {
	prio = p;
	myid = id;
    }

    /**
     * Retourne la priorite du processus
     * @return la priorite
     */
    /*@ ensures \result == prio;
      @*/
    public /*@ pure @*/ int getPriorite()
    {
	return prio;
    }

    /**
     * Retourne l'identifiant du processus
     * @return l'identifiant
     */
    /*@ ensures \result.equals(myid);
      @*/
    public /*@ pure @*/ String getIdent()
    {
	return myid;
    }

    /*@ also
      @
      @ ensures \result <==> (o instanceof Processus && ((Processus)o).getIdent().equals(myid));
      @*/
    public boolean equals(/*@ nullable @*/ Object o)
    {
	Processus p = (Processus)o;

	return myid.equals(p.getIdent());
    }

    /**
     * Affiche les infos concernant processus 
     */
    /*@ also
      @ ensures \result != null && \result.length() > 0;
      @*/
    public String toString()
    {
	return "[id : "+ getIdent() +", priorite : "+ getPriorite() +" ]";
    }


}