Debido al problema de contaminación priónica en vacas, el número de sacrificios está causando escasez de recintos que puedan ser dedicados a almacenarlas. El gobierno decide autorizar el uso de salas de mataderos para almacenar reses sanas y enfermas, con la restricción de que una sala sólo debe albergar, en cada momento, vacas de una clase.
Con objeto de optimizar el uso de las salas no se hace una asignación
estricta de salas a tipos de vacas, sino que cuando una sala queda
vacía (porque todas las vacas que había allí ha sido llevada a cremar
o a una carnicería) se puede reutilizar para guardar indistintamente
vacas sanas o contaminadas (tras una desinfección de la que no tenemos
que ocuparnos). Previendo la posibilidad de fallos humanos, se decide
automatizar el sistema de asignación de salas con un sistema de
control. El funcionamiento del sistema es el siguiente: se señala, al
llegar, si se quiere depositar o retirar una vaca y si ésta está
contaminada o no. El sistema asignará una sala de la que extraer o
recoger.
El diseño del recurso al que se ha llegado es el siguiente:
C-TADSOL AlmacenVacas
C-Operaciones
ACCION DejarLoca:TipoAlmTipoNumSala
ACCION RetirarLoca:TipoAlmTipoNumSala
ACCION DejarNormal:TipoAlmTipoNumSala
ACCION RetirarNormal:TipoAlmTipoNumSala
Operaciones
ACCION Iniciar:TipoAlm
CONCURRENCIA:
ninguna
TRANSACCIONES:
DejarLoca
RetirarLoca
DejarNormal
RetirarNormalDominio:
Tipo: TipoAlm = Secuencia(TipoSala)
TipoNumSala = {1..NumSalas}
Donde:
TipoSala = (nvacas: TipoTamtipo:TipoVaca)
TipoVaca = locanormal
TipoTam = {0..TamSala}
TamSala = ...
NumSalas = ...
Invariante:![]()
CPRE: cierto
Iniciar(alm)
POST: Todas las salas estan inicialmente vac'ias
POST:![]()
CPRE: Hay una sala de vacas locas con espacio u otra cualquiera vac'ia
CPRE:![]()
DejarLoca(alm, sala)
POST: Se utiliza la sala de vacas locas o la sala vac'ia
POST:![]()
![]()
CPRE: Hay una sala con vacas locas
CPRE:![]()
RetirarLoca(alm, sala)
POST: Se retira una vaca de una sala con vacas locas
POST:![]()
![]()
CPRE: Hay una sala de vacas normales con espacio u otra cualquiera vac'ia
CPRE:![]()
DejarNormal(alm, sala)
POST: Se utiliza la sala de vacas normales o la sala vac'ia
POST:![]()
![]()
CPRE: Hay una sala con vacas normales
CPRE:![]()
RetirarNormal(alm, sala)
POST: Se retira una vaca de una sala con vacas normales
POST:![]()
![]()
Operación | CPRE informal | CPRE codificada | Condition | ||
---|---|---|---|---|---|
DejarLoca(alm, sala) |
|
|
dejaresperando[loca] | ||
RetirarLoca(alm, sala) |
|
|
retiraresperando[loca] | ||
DejarNormal(alm, sala) |
|
|
dejaresperando[normal] | ||
RetirarNormal(alm, sala) |
|
|
retiraresperando[normal] |
|
|
|
|
||||||
|
|
|
|
|
|||||
|
|
|
|
|
|||||
|
|
|
|
|
|||||
|
|
|
|
|
Para asegurar la vivacidad se debe respetar en todo momento la restricción introducida en la primera nota. Esta restricción se respetará si en todo momento el número de salas dedicadas a un tipo de vaca es menor o igual a NumSalas - 1. Como el número de salas dedicadas a un tipo de vaca puede aumentar como consecuencia de ejecutar un operación Dejar, debemos modificar las CPREs de las operaciones Dejar de manera que recojan la restricción. Al modificar las CPREs, vamos a introducir dos contadores en el estado del recurso, nosalaslocas y nosalasnormales, que indicarán el número de salas dedicadas a vacas locas y a vacas normales, respectivamente. Lógicamente, estos contadores deben ser inicializados a cero. Dado que estos dos contadores deben formar parte del tipo TipoAlm, tenemos que modificar la definición del tipo TipoAlm:
Las CPREs de las operaciones Dejar quedarán así:
Dado que estas operaciones pueden incrementar el número de salas dedicadas a las vacas de un tipo, debemos también modificar las postcondiciones de las operaciones Dejar:
Asimismo, también debemos modificar las postcondiciones de las operaciones Retirar, ya que puede suceder que tras retirar una vaca de un tipo, una sala se queda vacía, y por lo tanto se decremente el número de salas dedicadas a dicho tipo.
Estos cambios introducidos en las CPREs y las postcondiciones
de las operaciones Dejar, y en las postcondiciones de
las operaciones Retirar van a afectar a dos condiciones de desbloqueo.
Si al retirar una vaca de un tipo, se queda vacía la sala, entonces
para poder desbloquear una operación Dejar del otro
tipo de vacas, debemos comprobar
.
CONST
normal = 1;
loca = 2;
NUMSALAS = ...;
TAMSALA = ...;
(* Tipos de uso general *)
TYPE
TipoVaca = [normal..loca];
TipoNumSala = [1..NUMSALAS];
(***********************************************************************)
(* Implementacion del gestor del almacen *)
(***********************************************************************)
TYPE TipoGestorAlmacen = MONITOR
(* Constantes, tipos y nombres de procedimientos a usar dentro del monitor *)
IMPORT
normal, loca, TipoVaca, TipoNumSala, NUMSALAS, TAMSALA;
(* Procedimientos p'ublicos *)
PUBLIC
DejarNormal,
DejarLoca,
RetirarNormal,
RetirarLoca;
(* Tipos y variables privadas del monitor. *)
TYPE
TipoTamSala = [0..TAMSALA];
TipoSala = RECORD
npiezas : TipoTamSala;
tipo : TipoVaca;
END;
VAR (* Estas variables se utilizan en la inicializaci'on *)
i: TipoNumSala;
j: TipoVaca;
(* Variables que definen el estado interno del recurso *)
STATE
almacen: ARRAY TipoNumSala OF TipoSala;
nodejaresperando: ARRAY TipoVaca OF CARDINAL;
dejaresperando: ARRAY TipoVaca OF CONDITION;
retiraresperando: ARRAY TipoVaca OF CONDITION;
saladisponible: TipoNumSala;
nosalas: ARRAY TipoVaca OF CARDINAL;
(* Implementaci'on de las operaciones del recurso *)
PROCEDURE BuscarSalaNoLlena (tipo: TipoVaca) : CARDINAL;
(**
* PRE: nosalas(tipo)NUMSALAS - 1
BuscarSalaNoLlena (almacen, sala, nosalas)
POST: Devuelve la sala no llena que contiene m'as vacas de la clase "tipo".
* Si no existe ninguna sala con vacas de la clase "tipo",
* se devuelve cualquier sala vac'ia siempre que el n'umero de salas asignadas a
* las vacas de la clase "tipo" no supere el tope NUMSALAS-1. Si tampoco
* existe una sala vac'ia que satisfaga el requisito anterior, se devuelve
* cero.
* POST:
* resultado =![]()
**)
END BuscarSalaNoLlena;
PROCEDURE BuscarSalaOcupada (tipo: TipoVaca): CARDINAL;
(**
* PRE: cierto
BuscarSalaOcupada (almacen, sala)
POST: Devuelve la sala que contenga un menor numero de vacas de la clase
* SPMgt;"tipo". Si no existe ninguna sala con vacas de la clase "tipo",
* se devuelve cero.
* POST: resultado =![]()
**)
END BuscarSalaOcupada;
PROCEDURE ElOtro(tipo: TipoVaca):TipoVaca;
(**
* PRE: cierto
* ElOtro (tipo)
* POST: resultado =![]()
**)
END ElOtro;
PROCEDURE Dejar (tipo : TipoVaca; sala:TipoNumSala);(**
* PRE: almacen(sala).npiezasTAMSALA
* Dejar (tipo, sala, almacen, nosalas)
* POST: Deja una vaca en la sala indicada actualizando el almac'en y el contador de salas
* POST:almacen
(i) =
![]()
(almacen
(sala) = 0
(almacen
(sala) = tipo
nosalas
(tipo) = nosalas
(tipo) + 1))
**)
END Dejar;
PROCEDURE Retirar (tipo : TipoVaca, sala:TipoNumSala);(**
* PRE: almacen(sala).npiezas0
* Dejar (tipo, sala, almacen, nosalas)
* POST: Deja una vaca en la sala indicada actualizando el almac'en y el contador de salas
* POST:![]()
(almacen
(sala) = 1)
nosalas
(tipo) = nosalas
(tipo) - 1)
**)
END Retirar;
PROCEDURE DejarNormal (VAR sala: TipoNumSala);
BEGIN
(* Sincronizaci'on de entrada *)
sala := BuscarSalaNoLlena(normal);
IF sala = 0 THEN
INC(nodejaresperando[normal]);
Delay(dejaresperando[normal]);
DEC(nodejaresperando[normal]);
sala := saladisponible;
END;
*(* Actualizaci'on del almacen *)
Dejar (normal, sala);
(* Sincronizaci'on de salida *)
saladisponible := sala;
IF nodejaresperando[normal]0 AND (almacen[sala].npiezas
TAMSALA) THEN
Continue(dejaresperando[normal]); (* despertar en cascada *)
ELSE
Continue(retiraresperando[normal]);
END;END DejarNormal;PROCEDURE DejarLoca (VAR sala: TipoNumSala);
BEGIN
(* Sincronizaci'on de entrada *)
sala := BuscarSalaNoLlena(loca);
IF sala = 0 THEN
INC(nodejaresperando[loca]);
Delay(dejaresperando[loca]);
DEC(nodejaresperando[loca]);
sala := saladisponible;
END;
(* Actualizaci'on del almacen *)
Dejar (loca, sala);
(* Sincronizaci'an de salida *)
saladisponible := sala;
IF nodejaresperando[loca]0 AND (almacen[sala].npiezas
TAMSALA) THEN
Continue(dejaresperando[loca]); (* despertar en cascada *)
ELSE
Continue(retiraresperando[loca]);
END;
END DejarNormal;
PROCEDURE RetirarNormal (VAR sala: TipoNumSala);
BEGIN
(* Sincronizaci'on de entrada *)
sala := BuscarSalaOcupada(normal);
IF sala = 0 THEN
(* No es necesario notificar el bloqueo *)
Delay(retiraresperando[normal]);
sala := saladisponible;
END;
(* Actualizaci'on del almacen *)
Retirar (normal, sala);
(* Sincronizaci'on de salida *)
saladisponible := sala;
IF nodejaresperando[loca]0 AND (almacen[sala].npiezas = 0) AND
(nosalas[loca]NUMSALAS-2) THEN
Continue(dejaresperando[loca]);
ELSE
Continue(dejaresperando[normal]);
END;
END RetirarNormal;
PROCEDURE RetirarLoca (VAR sala: TipoNumSala);
BEGIN
(* Sincronizaci'on de entrada *)
sala := BuscarSalaOcupada(loca);
IF sala = 0 THEN
(* No es necesario notificar el bloqueo *)
Delay(retiraresperando[loca]);
sala := saladisponible;
END;
(* Actualizaci'on del almacen *)
Retirar (loca, sala);
(* Sincronizaci'on de salida *)
saladisponible := sala;
IF nodejaresperando[normal]0 AND (almacen[sala].npiezas = 0) AND
(nosalas[normal] < NUMSALAS-2) THEN
Continue(dejaresperando[normal]);
ELSE
Continue(dejaresperando[loca]);
END;
END RetirarLoca;
BEGIN
(* El almac'en est'a inicialmente vac'io *)
FOR i := 1 TO NUMSALAS DO
almacen[i].npiezas := 0
END ;
FOR j := normal TO loca DO
nodejaresperando[j] := 0; (* No hay operaciones bloqueadas *)
nosalas[j] := 0;
END;
END (* MONITOR TipoGestorAlmacen *);