package gestionProc;
import java.util.LinkedList;
import java.util.Iterator;

/**
 * Gere les processus avec une file
 */
public class ProcessusFIFO implements ProcessusList
{
    private LinkedList maListe; /*@ in plist; @*/
    /*@ private represents plist <- maListe; @*/
    
    /**
     * Construit une file de processus vide 
     */
    /*@
      @ ensures plist.size() == 0;
      @*/
    public ProcessusFIFO()
    {
	maListe = new LinkedList();
    }
    
    /** Ajoute le processus p a la tete de la file */
    /*@ also
      @ requires \same;
      @
      @ ensures plist.get(0) == p;
      @ ensures (\forall int i; 0 <= i && i < \old(plist.size()) - 1; \old(plist.get(i)) == plist.get(i+1));
      @*/
    public void ajouterProcessus(Processus p)
    {
	maListe.addFirst(p);
    }
    
    /**
     * Test si le processus p appartient a la file de processus 
     */
    public boolean contientProcessus(Processus p)
    {
	return maListe.contains(p);
    }
    
    /**
     * Test si la file de processus est vide ou non
     */
    public boolean empty()
    {
	return maListe.isEmpty();
    }
    
    /** 
     * Retourne le nombre d'elements (Processus) de la file 
     */
    public int nbElem()
    {
	return maListe.size();
    }
    
    /** Retire la tete de la file */
    /*@ also
      @
      @ requires \same;
      @
      @ ensures \result == \old(plist.get(plist.size())); // Impossible d'utiliser un \old dans un \old : on utilise 
      @                                                   // donc le fait qu'on a une postcondition qui assure que la
      @                                                   // taille sera d'un élément de moins qu'en entrée.
      @ ensures (\forall int i; 0 <= i && i < plist.size(); plist.get(i) == \old(plist.get(i+1)));
      @*/
    public Processus retirerProcessus()
    {
	return (Processus)maListe.removeLast();
    }

    /** Affiche le contenu de la file */
    /*@ also
      @ ensures \result != null && \result.length() > 0;
      @*/
    public String toString()
    {
	if (maListe.isEmpty())
	    return "file vide";

	String res = "";	
	Iterator it = maListe.iterator();

	while(it.hasNext())
	    res += ((Processus)it.next()).toString() + "\n";

	return res;
    }
}