monitoreh

// Grupo: Santiago Canabal Ramos (z170221), Rafael Navarro Atienza (z170149)

/*ERRORES:
- invariante mal definido (hay que considerar tambien los colores y trenes[3])
+ esta bien definida
- puede desbloquear mas de un proceso
+ ¿?
- no deberia usar ninguna otra clase mas que Enclavamiento y Control
+ puede ser lo del los throws que ya hemos quitado
 */
import es.upm.babel.cclib.Monitor;

public class EnclavamientoMonitor implements Enclavamiento {
    //declaracion de variables tipo
    private boolean presencia;
    private Control.Color [] color = new Control.Color [4];
    private int [] trenes = new int [4];
    //declaracion de monitores y condiciones de barrera
    private Monitor mutex;
    private Monitor.Cond [] freno = new Monitor.Cond [2]; //1 condition por cada posible estado de freno
    private Monitor.Cond [] barrera = new Monitor.Cond [2]; //1 condition por cada posible estado de barrera
    private Monitor.Cond [][] semaforo = new Monitor.Cond [4][4]; //1 condition por cada posible estado de semaforo

    //Contructor
    public EnclavamientoMonitor() {
        //Inicializacion de variables tipo
        presencia=false;
        for(int i=0;i<4;i++) {
            color[i]=Control.Color.VERDE;
            trenes[i]=0;
        }
        //Inicializacion de monitores y condiciones de barrera
        mutex = new Monitor();
        for(int i=0;i<2;i++) {	//condicion[0]=false;
        						//condicion[1]=true
            freno[i] = mutex.newCond();
            barrera[i] = mutex.newCond();
        }
        for(int j=0;j<4;j++) {//j=numero del semaforo
            for(int k=0;k<4;k++) {//k=color del semaforo
                semaforo[j][k] = mutex.newCond();
                //[j][k=1]=>ROJO
                //[j][k=2]=>AMARILLO
                //[j][k=3]=>VERDE
            }
        }

    }

    //Metodo para corregir los colores en los diferentes semaforos
    //de acuerdo al numero de trenes en cada segmento
    private void coloresCorrectos() {

        if(trenes[1]>0) {
            color[1] = Control.Color.ROJO;
        }
        else if(trenes[1]==0) {

            if((trenes[2]>0 || presencia==true)) {
                color[1] = Control.Color.AMARILLO;
            }
            else if(trenes[2]==0 && presencia==false) {
                color[1] = Control.Color.VERDE;
            }
        }

        if(trenes[2]>0 || presencia==true) {
            color[2] = Control.Color.ROJO;
        }

        else if(trenes[2]==0 && presencia==false) {
            color[2] = Control.Color.VERDE;
        }

        color[3] = Control.Color.VERDE;
    }

    //Metodo que comprueba la invariante
    private boolean invariante() {
    	coloresCorrectos();
        return (trenes[1]>=0 && trenes[2]>=0);
    }

    //Metodo que valora la posibilidad de
    //desbloquear algun proceso
    private void desbloquear() {
        boolean res = true;

        if ((trenes[1]+trenes[2]==0) && res) {
            if (barrera[0].waiting()>0) {
                barrera[0].signal();
                res=false;
            }
        }
        else if (barrera[1].waiting()>0) {
            barrera[1].signal();
            res=false;
        }

        if (trenes[1]>1 || trenes[2]>1 || trenes[2]==1 && presencia) {
            if (freno[0].waiting()>0) {
                freno[0].signal();
                res=false;
            }
        }
        else if (freno[1].waiting()>0) {
            freno[1].signal();
            res=false;
        }
        //[j][k=1]=>ROJO
        //[j][k=2]=>AMARILLO
        //[j][k=3]=>VERDE
        if (color[1]==Control.Color.VERDE && res) {
            if (semaforo[1][1].waiting()>0 && res) {
                semaforo[1][1].signal();
                res=false;
            }
            if (semaforo[1][2].waiting()>0 && res) {
                semaforo[1][2].signal();
                res=false;
            }
        }
        else if (color[1]==Control.Color.AMARILLO && res) {
            if (semaforo[1][1].waiting()>0 && res) {
                semaforo[1][1].signal();
                res=false;
            }
            if (semaforo[1][3].waiting()>0 && res) {
                semaforo[1][3].signal();
                res=false;
            }
        }
        else if (color[1]==Control.Color.ROJO && res) {
            if (semaforo[1][2].waiting()>0 && res) {
                semaforo[1][2].signal();
                res=false;
            }
            if (semaforo[1][3].waiting()>0 && res) {
                semaforo[1][3].signal();
                res=false;
            }
        }

        if (color[2]==Control.Color.VERDE && res) {
            if (semaforo[2][1].waiting()>0 && res) {
                semaforo[2][1].signal();
                res=false;
            }
            if (semaforo[2][2].waiting()>0 && res) {
                semaforo[2][2].signal();
                res=false;
            }
        }
        else if (color[2]==Control.Color.AMARILLO && res) {
            if (semaforo[2][1].waiting()>0 && res) {
                semaforo[2][1].signal();
                res=false;
            }
            if (semaforo[2][3].waiting()>0 && res) {
                semaforo[2][3].signal();
                res=false;
            }
        }
        else if (color[2]==Control.Color.ROJO && res) {
            if (semaforo[2][2].waiting()>0 && res) {
                semaforo[2][2].signal();
                res=false;
            }
            if (semaforo[2][3].waiting()>0 && res) {
                semaforo[2][3].signal();
                res=false;
            }
        }

        if (color[3]==Control.Color.VERDE && res) {
            if (semaforo[3][1].waiting()>0 && res) {
                semaforo[3][1].signal();
                res=false;
            }
            if (semaforo[3][2].waiting()>0 && res) {
                semaforo[3][2].signal();
                res=false;
            }
        }
        else if (color[3]==Control.Color.AMARILLO && res) {
            if (semaforo[3][1].waiting()>0 && res) {
                semaforo[3][1].signal();
                res=false;
            }
            if (semaforo[3][3].waiting()>0 && res) {
                semaforo[3][3].signal();
                res=false;
            }
        }
        else if (color[3]==Control.Color.ROJO && res) {
            if (semaforo[3][2].waiting()>0 && res) {
                semaforo[3][2].signal();
                res=false;
            }
            if (semaforo[3][3].waiting()>0 && res) {
                semaforo[3][3].signal();
                res=false;
            }
        }
    }

    @Override
    public void avisarPresencia(boolean presencia) {
        if(invariante()) {
            mutex.enter();
            // chequeo de la PRE (no existe PRE)
            // chequeo de la CPRE y posible bloqueo (no existe posibilidad de bloqueo)
            // implementacion de la POST
            this.presencia=presencia;
            coloresCorrectos();
            // codigo de desbloqueo
            desbloquear();
            mutex.leave();
        }

    }

    @Override
    public boolean leerCambioBarrera(boolean actual) {
        boolean resultado=false;
        if(invariante()) {
            mutex.enter();
            // chequeo de la PRE (no existe PRE)
            // chequeo de la CPRE y posible bloqueo
            if(actual==(trenes[1]+trenes[2]==0)) {
                if(!actual) {
                    barrera[0].await();
                }
                else {
                    barrera[1].await();
                }
            }
            // implementacion de la POST
            if(trenes[1]+trenes[2]==0) {
                resultado=true;
            }
            // codigo de desbloqueo
            desbloquear();
            mutex.leave();
        }
        return resultado;
    }

    @Override
    public boolean leerCambioFreno(boolean actual) {
        boolean resultado=false;
        if(invariante()) {
            mutex.enter();
            // chequeo de la PRE (no existe PRE)
            // chequeo de la CPRE y posible bloqueo
            if(actual==(trenes[1]>1 || trenes[2]>1 || trenes[2]==1 && presencia==true)) {
                if(!actual) {
                    freno[0].await();
                }
                else {
                    freno[1].await();
                }
            }
            // implementacion de la POST
            if(trenes[1]>1 || trenes[2]>1 || trenes[2]==1 && presencia==true) {
                resultado=true;
            }
            // codigo de desbloqueo
            desbloquear();
            mutex.leave();
        }
        return resultado;
    }

    @Override
    public Control.Color leerCambioSemaforo(int i, Control.Color actual) {
        // chequeo de la PRE
        if(i==0)
            throw new PreconditionFailedException();
        if(invariante()) {
            mutex.enter();
            // chequeo de la CPRE y posible bloqueo
            if(actual.equals(color[i])) {
                if(color[i].equals(Control.Color.ROJO)) {
                    semaforo[i][1].await();
                }
                else if(color[i].equals(Control.Color.AMARILLO)) {
                    semaforo[i][2].await();
                }
                else if(color[i].equals(Control.Color.VERDE)) {
                    semaforo[i][3].await();
                }
            }
            // implementacion de la POST
            // codigo de desbloqueo
            desbloquear();
            mutex.leave();
        }
        return color[i];
    }

    @Override
    public void avisarPasoPorBaliza(int i) {
        // chequeo de la PRE
        if(i==0)
            throw new PreconditionFailedException();
        if(invariante()) {
            mutex.enter();
            // chequeo de la CPRE y posible bloqueo (no existe posibilidad de bloqueo)
            // implementacion de la POST
            trenes[i-1]--;
            trenes[i]++;
            coloresCorrectos();
            // codigo de desbloqueo
            desbloquear();
            mutex.leave();
        }
    }

}