-- 1. An example specification of a simplified NFS-protocol
-- ========================================================

SERVER_MACHINES = {1..m}
CLIENT_MACHINES = {1..n}

datatype DIR_NAME = D0 | D1 | ....

datatype STATES = S0 | S1 | ...

-- The MOUNT-file of client i
-- where Dij is the set of directories on server j, which are mount by client i
MOUNT(i) = {(1,Di1), (2,Di2), ...}

datatype ACK = OK | ERR
ACKS ={OK,ERR,S0,S1,...} -- union(ACK,STATES)

-- permission
-- 0: none
-- 1: read
-- 2: wirte
-- 3: read-write 
RIGHTS = {0,1,2,3}

-- Channel declarations
channel read: CLIENT_MACHINES.SERVER_MACHINES.DIR_NAME
channel write: CLIENT_MACHINES.SERVER_MACHINES.DIR_NAME.STATES
channel ack: CLIENT_MACHINES.SERVER_MACHINES.ACKS
channel perm: DIR_NAME.CLIENT_MACHINES.RIGHTS
channel read_state, write_state: DIR_NAME.STATES

-- System specification
-- suppose: PERM defines the set of access permissions of the whole system
-- suppose: S0 is the initial state of all directories
SYSTEM = 
	(|||c:CLIENT_MACHINES @ CLIENT(c))
	[| {| read,write,ack |} |]
	(((
	(|||s:SERVER_MACHINES @ SERVER(s))
	[| {| read_state,write_state |} |]
	(|||d:DIR_NAME @ DIRECTORY(d,S0)))
	[| {| perm |} |]
	RIGHT(PERM))
	\ {| read_state,write_state,perm |})


-- Specification of a client
CLIENT(i) =
	[](j,ds):MOUNT @  ([]d:ds @ (
	read.i.j.d -> (ack.i.j?x  -> CLIENT(i)
		       []
		       ack.i.j.ERR -> CLIENT(i)
		       )
	[]
	([]y:STATES @ (write.i.j.d!y -> 
			(ack.i.j.OK  -> CLIENT(i)
		         []
		         ack.i.j.ERR -> CLIENT(i)
		        )))))

-- Specification of a server
SERVER(i) = 
	read?c!i?d -> perm.d.c?p ->
		(if (p==1 or p==3) 
		 then read_state.d?x -> ack.c.i!x -> SERVER(i)
		 else ack.c.i!ERR -> SERVER(i))
	[]
	write?c!i?d?x -> perm.d.c?p ->
		(if (p==2 or p==3) 
		 then write_state.d!x -> ack.c.i!OK -> SERVER(i)
		 else ack.c.i!ERR -> SERVER(i))

-- Specification of a directory
DIRECTORY(i,s) = 
	read_state.i!s -> DIRECTORY(i,s)
	[]
	write_state.i?y -> DIRECTORY(i,y)

-- rs has the type: set of (DIR_NAME,CLIENT_MACHINES,RIGHTS)
RIGHT(rs) = 
	[](d,c,x):rs @ (perm.d.c.x -> RIGHT(rs))

-- 2. To do
-- ========

-- Specification of catching with write-through
-- Determination of various parameters 
	(at least 2 servers and 2 clients)
-- Proof of deadlock and livelock situations with FDR
	(at least 3 sets of parameters)
-- Documentation of your specification and test results


-- 3. Deadline: 05.08.2002
-- =======================