(******************************************************************************
 *   			  S C S I - 2
 *-----------------------------------------------------------------------------
 *   INRIA - Unite de Recherche Rhone-Alpes
 *   655, avenue de l'Europe
 *   38330 Montbonnot Saint Martin
 *   FRANCE
 *-----------------------------------------------------------------------------
 *   Module		:	SCSI-2
 *   Auteur		:	Claude Chaudet
 *   Version		:	1.2
 *   Date		: 	00/02/17 19:31:20
 *****************************************************************************)

-- Specification du protocole SCSI-2
-- Cas avec 4 disques (ID0, 1, 2, 3 et un controleur ID7)

module SCSI_TYPES is

-- IDs SCSI des disques / controleurs

type SCSI_NUMBER is
 id0,id1,id2,id3,id7
 with ==, !=
end type

-- Etat de la nappe de fils pour demande de bus

type SCSI_WIRE is
   array [SCSI_NUMBER] of bool
end type

-- Tailles maximales des files d'attentes

function MAX_LENGTH(in id : SCSI_NUMBER) : nat is
  case id is
    id7 -> return 0 
	| any -> return 8
  end case
end function

-- La file d'attente du periph id est elle pleine si elle a lg messages ? 

function AVAILABLE (in lg : nat, id : SCSI_NUMBER) : bool is
  return (lg < MAX_LENGTH(id))
end function

-- Remplissage des files d'attente

type CONTENTS is
  array [SCSI_NUMBER] of nat
end type

-- Cte : files d'attentes vides

function ZERO : CONTENTS is
  return [0,0,0,0,0,0,0]
end function

-- Renvoie vrai si la file d'attente du id eme disque n'est pas saturee
-- Dans l'etat q de remplissage

function NOT_FULL(in q : CONTENTS, in id : SCSI_NUMBER) : bool is
  return AVAILABLE(q[id], id)
end function

-- Renvoie vrai si toutes les files d'attente sont saturees
-- Dans l'etat q de remplissage

function ALL_FULL(in q : CONTENTS) : bool is
  return (not(AVAILABLE(q[id0], id0)) and 
         not(AVAILABLE(q[id1], id1)) and 
         not(AVAILABLE(q[id2], id2)) and 
         not(AVAILABLE(q[id3], id3)))
end function

-- place un message dans une file d'attente
function INCR(inout q : CONTENTS, in id : SCSI_NUMBER) : void is
  q[id] := q[id] + 1
end function

-- ote un message d'une file d'attente

function DECR(inout q : CONTENTS, in id : SCSI_NUMBER) is
  q[id] := q[id] - 1
end function

-- vrai si le id eme periph ne veut pas acceder au bus dans l'etat de fils w
function P(in w : SCSI_WIRE, in id : SCSI_NUMBER) : bool  is
  return not(w[id])
end function

-- Le id eme periph peut-t-il acceder au bus dans l'etat de nappe w? 
          
function A(in w : SCSI_WIRE, in id : SCSI_NUMBER) : bool  is
  case id is
    id0 ->  return (w[0] and not(w[7] or w[1] or w[2] or w[3]))
  | id1 ->  return (w[1] and not(w[7] or w[2] or w[3]))
  | id2 ->  return (w[2] and not(w[7] or w[3]))
  | id3 ->  return (w[3] and not(w[7]))
  | id7 ->  return w[7] 
  end case
end function

-- Comportement du controleur
-- idc = ID du controleur

process CONTROLLER [CMD, REC : SCSI_NUMBER , ARB : SCSI_WIRE] (in idc : SCSI_NUMBER) is
	var q : CONTENTS := ZERO, w : SCSI_WIRE := WIRE(false, false, false, false, false) in
		loop
		-- envoyer une commande a un disque
			choice id : SCSI_NUMBER [] 
				if ( (id != idc) and NOT_FULL(q,id) )			
				then
					ARB ?w [A(w, id)] ;
					CMD !id ;
					INCR(?q, !id)
				[]
	   			ARB ?w [not(A(w, idc)) and not(P(w,idc))]
				end if
			end choice
		[] -- recevoir un resultat d'un disque
			var id : SCSI_NUMBER in
				REC ? id [id != idc] ;
				DECR(?q, !id)
			end var
		[] -- permet aux disques d'utiliser le bus
			ARB ? w [P(w, idc)]
		end loop
	end var
end process

-- Comportement d'un disque
-- id = ID du disque

process DISK [CMD, REC : SCSI_NUMBER , ARB:SCSI_WIRE] (in id : SCSI_NUMBER) is
	var lgq : nat := 0, w : SCSI_WIRE := WIRE(false, false, false, false, false) in 
		loop
		-- Il y a des messages dans la file d'entree => demande de bus et traitement
			if (lgq > 0) then
				ARB ?w [A(w,id)];
				REC !id; 
				lgq := lgq - 1
			[]
				ARB ?w [not(P(w,id)) and not(A(w, id))]
			end if
	[] -- La file d'entree est vide
			if (lgq == 0) then
				ARB ? w [P(w, id)]
			end if
	[] -- Reception d'une commande (value matching)
			CMD ! id ;
			lgq := lgq + 1
		end loop
  end var
end process

end module

specification SCSI2 import SCSI_TYPES is
  gates CMD, REC : SCSI_NUMBER , ARB : SCSI_WIRE
  (* CMD : requete ctrl -> disque de transfert (r|w)
     REC : reconnect : un disque a fini de traiter une requete
     ARB : arbitrage : valeur des fils pour l'attribution du bus *)
  behaviour 
      ( 
                DISK [ ... ] (id0)
        |[ARB]| DISK [ ... ] (id1)
        |[ARB]| DISK [ ... ] (id2)
        |[ARB]| DISK [ ... ] (id3)
      ) |[ ARB, CMD, REC ]| 
                CONTROLLER [ ... ] (id7)
end specification