(****************************************************************************** * S C S I - 2 *----------------------------------------------------------------------------- * INRIA - Unite de Recherche Rhone-Alpes * 655, avenue de l'Europe * 38330 Montbonnot Saint Martin * FRANCE *----------------------------------------------------------------------------- * Module : SCSI-2 * Auteurs : Hubert Garavel et Massimo Zendri * Version : 1.1 * Date : 99/04/19 12:37:29 *****************************************************************************) specification SCSI_BUS [ARB,CMD,REC] : noexit library BOOLEAN, NATURAL endlib type SCSI_NUMBER is BOOLEAN sorts NUM opns 0 (*! constructor *), 1 (*! constructor *), #ifdef TOTAL 2 (*! constructor *), 3 (*! constructor *), 4 (*! constructor *), 5 (*! constructor *), 6 (*! constructor *), #endif 7 (*! constructor *) : -> NUM _==_, _<>_ : NUM, NUM -> BOOL eqns forall N1, N2 : NUM ofsort BOOL N1 == N1 = true; N1 == N2 = false; (* assuming priority *) ofsort BOOL N1 <> N2 = not (N1 == N2); endtype type SCSI_WIRE is BOOLEAN sorts WIRE opns WIRE (*! constructor *) : BOOL, BOOL, #ifdef TOTAL BOOL, BOOL, BOOL, BOOL, BOOL, #endif BOOL -> WIRE endtype type SCSI_LENGTH is NATURAL, SCSI_NUMBER opns MAX_LENGTH_0 : -> NAT MAX_LENGTH_1 : -> NAT MAX_LENGTH_2 : -> NAT MAX_LENGTH_3 : -> NAT MAX_LENGTH_4 : -> NAT MAX_LENGTH_5 : -> NAT MAX_LENGTH_6 : -> NAT MAX_LENGTH_7 : -> NAT AVAILABLE : NAT, NUM -> BOOL eqns ofsort NAT MAX_LENGTH_0 = 8; MAX_LENGTH_1 = 8; MAX_LENGTH_2 = 8; MAX_LENGTH_3 = 8; MAX_LENGTH_4 = 8; MAX_LENGTH_5 = 8; MAX_LENGTH_6 = 8; MAX_LENGTH_7 = 8; ofsort BOOL forall L:NAT AVAILABLE (L, 0) = (L < MAX_LENGTH_0); AVAILABLE (L, 1) = (L < MAX_LENGTH_1); #ifdef TOTAL AVAILABLE (L, 2) = (L < MAX_LENGTH_2); AVAILABLE (L, 3) = (L < MAX_LENGTH_3); AVAILABLE (L, 4) = (L < MAX_LENGTH_4); AVAILABLE (L, 5) = (L < MAX_LENGTH_5); AVAILABLE (L, 6) = (L < MAX_LENGTH_6); #endif AVAILABLE (L, 7) = (L < MAX_LENGTH_7); endtype type CONTENTS is NATURAL, SCSI_NUMBER, SCSI_LENGTH sorts CONTENTS opns TUPLE (*! constructor *) : NAT, NAT -> CONTENTS ZERO : -> CONTENTS NOT_FULL : CONTENTS, NUM -> BOOL ALL_FULL : CONTENTS -> BOOL INCR : CONTENTS, NUM -> CONTENTS DECR : CONTENTS, NUM -> CONTENTS eqns forall L0, L1:NAT ofsort CONTENTS ZERO = TUPLE (0, 0); ofsort BOOL ALL_FULL (TUPLE (L0, L1)) = not (AVAILABLE (L0, 0)) and not (AVAILABLE (L1, 1)) ; ofsort BOOL NOT_FULL (TUPLE (L0, L1), 0) = AVAILABLE (L0, 0); NOT_FULL (TUPLE (L0, L1), 1) = AVAILABLE (L1, 1); ofsort CONTENTS INCR (TUPLE (L0, L1), 0) = TUPLE (L0 + 1, L1); INCR (TUPLE (L0, L1), 1) = TUPLE (L0, L1 + 1); ofsort CONTENTS DECR (TUPLE (L0, L1), 0) = TUPLE (L0 - 1, L1); DECR (TUPLE (L0, L1), 1) = TUPLE (L0, L1 - 1); endtype type ACCESS is NATURAL, SCSI_NUMBER, SCSI_WIRE opns P : WIRE, NUM -> BOOL (* pas de demande de bus *) A : WIRE, NUM -> BOOL (* demande acceptee *) eqns forall r0, r1, (* ... *) r7: Bool, N:NUM ofsort BOOL (* P (WIRE (r0, r1, ..., r7), N) = not (rN) *) P (WIRE (r0, r1, (* ... *) r7), 0) = not (r0); P (WIRE (r0, r1, (* ... *) r7), 1) = not (r1); #ifdef TOTAL P (WIRE (r0, r1, (* ... *) r7), 2) = not (r2); P (WIRE (r0, r1, (* ... *) r7), 3) = not (r3); P (WIRE (r0, r1, (* ... *) r7), 4) = not (r4); P (WIRE (r0, r1, (* ... *) r7), 5) = not (r5); P (WIRE (r0, r1, (* ... *) r7), 6) = not (r6); #endif P (WIRE (r0, r1, (* ... *) r7), 7) = not (r7); ofsort BOOL (* A (WIRE (r0, r1, ..., r7), N) = rN and not (rN+1 or ... or r7) *) A (WIRE (r0, r1, (* ... *) r7), 0) = r0 and not (r1 (* or r3 or r4 or r5 or r6 *) or r7); A (WIRE (r0, r1, (* ... *) r7), 1) = r1 and not ((* r3 or r4 or r5 or r6 or r7 or *) r7); #ifdef TOTAL (* ... *) #endif A (WIRE (r0, r1, (* ... *) r7), 7) = r7; endtype behaviour ( DISK [ARB,CMD,REC] (0 of NUM, 0 of NAT) |[ARB]| DISK [ARB,CMD,REC] (1 of NUM, 0 of NAT) #ifdef TOTAL |[ARB]| DISK [ARB,CMD,REC] (2 of NUM, 0 of NAT) |[ARB]| DISK [ARB,CMD,REC] (3 of NUM, 0 of NAT) |[ARB]| DISK [ARB,CMD,REC] (4 of NUM, 0 of NAT) |[ARB]| DISK [ARB,CMD,REC] (5 of NUM, 0 of NAT) |[ARB]| DISK [ARB,CMD,REC] (6 of NUM, 0 of NAT) #endif ) |[ARB, CMD, REC]| CONTROLLER [ARB,CMD, REC] (7 of NUM, ZERO) where process CONTROLLER [ARB,CMD,REC] (NC : NUM, C: CONTENTS) : noexit := choice N:NUM [] [N <> NC] -> [NOT_FULL (C, N)] -> ( ARB ?W:WIRE [A (W, NC)]; (* il demande le bus et il l'obtient *) CMD !N ; CONTROLLER [ARB, CMD, REC] (NC, INCR (C, N)) [] ARB ?W:WIRE [not (A (W, NC)) and not (P (W, NC))]; (* il demande le bus et il ne l'obtient pas *) CONTROLLER [ARB, CMD, REC] (NC, C) ) [] REC ?N:NUM [N <> NC] ; CONTROLLER [ARB,CMD,REC] (NC, DECR (C,N)) [] (* [ALL_FULL (C)] -> *) ARB ?W:WIRE [P (W, NC)]; CONTROLLER [ARB, CMD, REC] (NC, C) endproc process DISK [ARB, CMD, REC](N:NUM, L:NAT) : noexit := [L > 0 of NAT] -> ( ARB ?W:WIRE [A (W, N)]; (* il demande le bus et l'obtient *) REC !N; DISK [ARB, CMD, REC] (N, L-1) [] ARB ?W:WIRE [not (P (W, N)) and not (A (W, N))]; (* il demande le bus et ne l'obtient pas *) DISK [ARB, CMD, REC] (N, L) ) [] [L = 0 of NAT] -> ARB ?W:WIRE [P (W, N)]; (* il ne demande pas le bus *) DISK [ARB, CMD, REC] (N, L) [] CMD !N; DISK [ARB, CMD, REC] (N, L+1) endproc endspec