(******************************************************************************
 *   			  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.1
 *   Date		: 	99/04/19 12:37:29
 *****************************************************************************)

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

module SCSI_TYPES is

function NB_PERIPH : nat is return 8 end function

function ID_CONTROLLER : nat is return 7 end function

function QUEUE_LENGTH : nat is return 8 end function

-- IDs SCSI des disques / controleurs

type SCSI_NUMBER is
 { id : nat, id < NB_PERIPH }
 with =, !=
end type

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

type SCSI_WIRE is
  list of bool
end type

-- La file d'attente du periph id est elle saturee
-- si elle comporte lg messages ? 

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

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

-- Remplissage des files d'attente

type CONTENTS is
  list of nat
end type

-- Cte : files d'attentes vides

function ZERO : CONTENTS is
  var j : nat, tmp : CONTENTS := empty in 
    for j:=0 while j<=NB_PERIPH by j := j + 1 do
      tmp := cons(0, tmp)
    end for;
    return tmp
  end var
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(nth(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
  var j : nat := 0 in 
    while j < NB_PERIPH do
      if AVAILABLE(nth(q,j), j) 
      then 
        return false
      end if
    end while; 
    return true
  end var
end function

-- place un message dans une file d'attente
function INCR(in q : CONTENTS, in id : SCSI_NUMBER) : CONTENTS is
  if (id == 0)
  then
    return cons(head(q) + 1, tail(q))
  else
    return cons(head(q), INCR(tail(q), id - 1))
  end if
end function

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

function DECR(in q : CONTENTS, in id : SCSI_NUMBER) : CONTENTS is
  if (id == 0)
  then
    return cons(head(q) - 1, tail(q))
  else
    return cons(head(q), INCR(tail(q), id - 1))
  end if
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(nth(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
    if empty(w)
    then 
      return true
    elsif (NB_PERIPH - length(w) >= id)
    then 
      return (head(w) and A(tail(w, id)))
    else 
      return A(tail(w, id))
    end if
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 ;
					q := 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] ;
				q := 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
  behaviour 
  par ARB#8, CMD#2, REC#2 in
     [ARB, CMD, REC] -> par ID : SCSI_NUMBER in [0,1,2,3,4,5,6] 
                          |[ARB]| DISK [ ... ] (ID) 
			end par 
  || [ARB, CMD, REC] -> CONTROLLER [ ... ] (ID_CONTROLLER)
  end par
end specification