/* http://www.cs.york.ac.uk/~andyg/filesystem/spinmodel.pml */


#define NoofNodes 5 /* Approx max depth of dir tree */
#define PathLength 6 /* Always NoofNodes+1 */
#define NoofNames 5 /* Approx max width of dir tree */

#if !defined(myverif)
chan STDIN;
#endif

typedef lock {
	bit islocked;
	unsigned lockedby : 1;
	unsigned waiting : 1
};

typedef superblock {
	unsigned s_root : 3;
	lock s_umount;
	lock s_lock
};

typedef hashlinks {
	unsigned next : 3;
	unsigned prev : 3
};

typedef rcu {
	bit pending;
	unsigned function : 3
};

typedef dentry {
	unsigned d_count : 3;
	lock d_lock;
	unsigned d_inode : 3;
	hashlinks d_hash;
	unsigned d_parent : 3;
	bit d_child [8]; 
	rcu d_rcu;
	bit d_subdirs [8];
	unsigned d_iname : 3
};

typedef filelock {
	unsigned locklist : 3;
	unsigned locktypes : 3;
	unsigned blocks : 3
};

typedef inode {
	unsigned i_dentry : 3;
	lock i_lock;
	lock i_mutex;
	lock i_alloc_sem;
	filelock i_flock;
	unsigned i_state : 2;
 	unsigned i_writecount : 3
};

typedef dentryref {
	unsigned ref :3
};


typedef dentrypool {
	dentry dentries [NoofNodes];
	bit available [8]
};

typedef inodepool {
	inode inodes [NoofNodes];
	bit available [8]
};


/* Base Functions */

inline alloc_dentry (dep,returnval, localvar,error) {
d_step{
	localvar=0;
	do
	:: localvar==NoofNodes -> break
	:: else {
		if 
		:: dep.available[localvar] != 0  -> localvar++
		:: else  {
			dep.available[localvar]=1;
			returnval=localvar;
			break
		}
		fi
	}
	od;
	if 
	:: localvar==NoofNodes -> error=1
	:: else error=0
	fi
} /*dstep */
	if
	:: error==1 ->
/* end_alloc_dentry:  Problem with redeclaration for now */
		goto end
	:: else
	fi
};

inline dealloc_dentry(dep,dent) {
d_step{
	assert (dent>=0 && dent<=NoofNodes-1 && dep.available[dent]==1); 
	dep.available[dent]=0
} /*dstep*/
};

inline alloc_inode (inp,returnval, localvar,error) {
d_step{
	localvar=0;
	do
	:: localvar==NoofNodes -> break
	:: else {
		if
		:: inp.available[localvar] != 0 -> localvar++
		:: else {
			inp.available[localvar]=1;
			returnval=localvar;
			break
		}
		fi
	}
	od;
	if 
	::localvar==NoofNodes -> error=1
	:: else error=0
	fi
} /*dstep */
	if
	:: error==1 ->
/* end_alloc_inode: problem with redeclaration  */
		goto end
	:: else
	fi
};

inline dealloc_inode(inp,in) {
	assert (in>=0 && in<=NoofNodes-1 && inp.available[in]==1);
	inp.available[in]=0
};

/***************************************************************************/

/* Low-level File system operations  */

inline allocate_dentry(dent,name,parent,lvplus1_4h,lvplus1_1) 
{
	alloc_dentry(dpool,dent,lvplus1_4h,lvplus1_1);
	/* init dentry defaults + parent + filename*/
	dpool.dentries[dent].d_count=1; /* Not marked for deletion */
	dpool.dentries[dent].d_lock.islocked=0;
	dpool.dentries[dent].d_lock.lockedby=0;
	dpool.dentries[dent].d_lock.waiting=0;
	dpool.dentries[dent].d_inode=0; /* initially 0 */
	/* Not bothering to set hash links (dcache gone) */
	dpool.dentries[dent].d_parent=parent; /* parent of root is root */
	dpool.dentries[dent].d_child[0]=0;
	dpool.dentries[dent].d_child[1]=0;
	dpool.dentries[dent].d_child[2]=0;
	dpool.dentries[dent].d_child[3]=0;
	dpool.dentries[dent].d_child[4]=0;
	dpool.dentries[dent].d_child[5]=0;
	dpool.dentries[dent].d_child[6]=0; 
	dpool.dentries[dent].d_child[7]=0; /* No siblings */
	/* Not bothering to set rcu for now */
	dpool.dentries[dent].d_subdirs[0]=0;
	dpool.dentries[dent].d_subdirs[1]=0;
	dpool.dentries[dent].d_subdirs[2]=0;
	dpool.dentries[dent].d_subdirs[3]=0;
	dpool.dentries[dent].d_subdirs[4]=0;
	dpool.dentries[dent].d_subdirs[5]=0;
	dpool.dentries[dent].d_subdirs[6]=0; 
	dpool.dentries[dent].d_subdirs[7]=0; /* No children (dirs) */
	dpool.dentries[dent].d_iname=name
}

inline allocate_inode(ind,dent,lvplus1_4h,lvplus1_1)
{
	alloc_inode(ipool,ind,lvplus1_4h,lvplus1_1);
	/* init dentry */
	ipool.inodes[ind].i_dentry=dent;
	ipool.inodes[ind].i_mutex.islocked=0;
	ipool.inodes[ind].i_lock.islocked=0
	/* not bothering to initialise other attributes yet */
}

inline init_superblock(dep,inp,sb,node,lvplus1_4h,lvplus1_1)
{
	allocate_dentry(node,0,0,lvplus1_4h,lvplus1_1); /* name 0, parent 0 */
	assert(node==0); /* node allocated should have been 0 */
	allocate_inode(node,0,lvplus1_4h,lvplus1_1); /* point to dentry 0 */
	assert(node==0); /* should have allocated inode 0 */
	/* init superblock */
	sb.s_root=0; /* dentry 0 */
	sb.s_umount.islocked=0;
	sb.s_umount.lockedby=0;
	sb.s_umount.waiting=0;
	/* important dentry fields */
	assert(dep.dentries[0].d_inode==0); /* corresponding inode is 0 */
	assert(dep.dentries[0].d_iname==0); /* Name 0 reserved for root */
	dep.dentries[0].d_subdirs[0]=1; /* Root is a directory (subdir of itself) */
	dep.dentries[0].d_child[0]=1; /* Root is a sibling of itself */
	/* important inode field */
	assert(inp.inodes[0].i_dentry==0) /* corresponding dentry is 0 */
}

inline modelfinddentry(name,parent,returndent,count)
{
	/* This should probably be atomic - but will assume dcache locked when called */
	assert(dcache_lock.islocked==1);
	if
	:: parent==NoofNodes -> { /*Parent Null*/
		assert(name==0); /* We should be looking for root */
		returndent=super.s_root /* And here's the root dentry */
	}
	:: else {
		/* This is the equivalent of the dcache operation to find the right name */
		/* No information in dentry unless name is a subdir */
		/* Since speed is not important for model, will search dpool rather than use subdirs */
		count=0;
		do
		:: count<NoofNodes -> {
			if 
			:: dpool.available[count]==1 && dpool.dentries[count].d_parent==parent &&
				dpool.dentries[count].d_iname==name  &&
				dpool.dentries[count].d_count!=0 -> { /* in use */
					returndent=count;
					break
			}
			:: else count++
			fi
		}
		:: count==NoofNodes -> {
			returndent=NoofNodes;
			break
		}
		od
	}
	fi
}

/* Lowest level sys calls */

inline is_prefix(patharray1,patharray2,return_flag)
{
	/* scratch variable ip_count */
  
	d_step {
		return_flag=0;
		ip_count=0;
		do
		:: patharray1[ip_count]==patharray2[ip_count] && patharray1[ip_count]!=NoofNodes -> {
			ip_count++;
			assert(ip_count<NoofNodes+1)
		}
		:: patharray1[ip_count]==NoofNodes -> {
			return_flag=1;
			break
		}
		:: patharray1[ip_count]!=patharray2[ip_count] && patharray1[ip_count]!=NoofNodes -> break
		od
	}
}

inline concat_element(patharray,name)
{
	/* scratch vars: ce_count */
	d_step{
		ce_count=0;
		do
		:: patharray[ce_count]!=NoofNodes -> ce_count++
		:: patharray[ce_count]==NoofNodes -> {
			assert(ce_count+1<=NoofNodes);
			patharray[ce_count]=name;
			patharray[ce_count+1]=NoofNodes;
			break
		}
		od
	}
}

inline prepend(patharray1,patharray2) { 
	/* A path array is array of 4bit unsigned, length NoofNodes+1, terminated by number NoofNodes */
	/*Note this is going to be too large a state space for any reasonable verification */
	/* Review later */

	/* scratch variables : pp_temparay, pp_count, pp_flag, pp_offset */

	d_step {
		pp_count=0;
		pp_flag=0; /*start with patharray2 */
		do
		:: pp_flag==0 -> {
			if 
			:: patharray2[pp_count]!=NoofNodes -> {
				pp_temparray[pp_count]=patharray2[pp_count];
				pp_count++
			}
			:: else {
				pp_offset=pp_count;
				pp_count=0;
				pp_flag=1
			}
			fi
		}
		:: pp_flag==1 -> {
			if
			:: patharray1[pp_count]!=NoofNodes -> {
				pp_temparray[pp_count+pp_offset]=patharray2[pp_count];
				pp_count++
			}		
			:: else {
				pp_temparray[pp_count+pp_offset]=patharray2[pp_count];
				break
			}
			fi
		}
		od;
		pp_count=0;
		do  /* Write result back to patharray1 */
		:: pp_temparray[pp_count]!=NoofNodes -> {
			patharray1[pp_count]=pp_temparray[pp_count];
			pp_count++
		}
		:: else {
			patharray1[pp_count]=pp_temparray[pp_count];
			break
		}
		od
	} /* d_step */
}

inline last_component (patharray,lastcomponent) {
	d_step {
		assert(patharray[0]==0 && patharray[1]!=NoofNodes); /* Absolute path (starts root) but not root */
		lc_count=1;
		lastcomponent=patharray[1];
		assert(lastcomponent!=0); /* shouldn't be root */
		do
		:: lc_count<NoofNodes+1 -> 
			if
			:: patharray[lc_count+1]!=NoofNodes -> {
				lc_count++;
				lastcomponent=patharray[lc_count];
				assert(lastcomponent!=0); /* shouldn't be root */
			}
			:: else break /* Finished */
			fi
		:: lc_count==NoofNodes+1 -> assert(false) /* Run out of path */
		od
	} /* d_step */
}

inline down(mutex){ /* Doesn't deal with lockedby, waiting etc. yet */
	if
	:: mutex.islocked==0 -> mutex.islocked=1 
	fi
}

inline up(mutex){ /* Doesn't deal with lockedby, waiting etc. yet */
	mutex.islocked=0;
}

inline spinlock_lock(spinlock){ /* Doesn't deal with lockedby, waiting etc. yet */
	if
	:: spinlock.islocked==0 -> spinlock.islocked=1 
	fi
}

inline spinlock_unlock(spinlock){ /* Doesn't deal with lockedby, waiting etc. yet */
	spinlock.islocked=0
}

inline dget(dent) { /* increase usage count on dentry */
	assert(dent!=NoofNodes); /* Replaces if structure in dget pseudocode dentry not null */
	spinlock_lock(dpool.dentries[dent].d_lock);
	if 
	:: dpool.dentries[dent].d_count != 0 -> /* not marked for deletion */
		dpool.dentries[dent].d_count++ /* Need to check for overflow */
	:: else
	fi;
	spinlock_unlock(dpool.dentries[dent].d_lock)
}

inline dput(dent) {
	assert(dent!=NoofNodes); /* Replaces if structure in dput pseudocode */
	spinlock_lock(dpool.dentries[dent].d_lock);
	if 
	:: dpool.dentries[dent].d_count > 1 -> /* not marked for deletion */
		dpool.dentries[dent].d_count-- /* Need to check for underflow (assert) */
	:: else
	fi;
	spinlock_unlock(dpool.dentries[dent].d_lock)
}

inline is_directory(dent,flag) {
	d_step {
		assert(dent!=NoofNodes); /* replaces part of if in pseudocode */
		id_count=0;
		flag=0;
		do
		:: id_count<NoofNodes -> {
			flag=flag | dpool.dentries[dent].d_subdirs[id_count];
			id_count++
		}
		:: id_count==NoofNodes -> break
		od
	} /* d_step */
}

inline get_dentry(name,parent,returndent,mfdlv_4_1) {
	spinlock_lock(dcache_lock);
	modelfinddentry(name,parent,returndent,mfdlv_4_1); /* specific find function */
	if
	:: returndent!=NoofNodes -> {  /* Found name */
		dget(returndent);
		assert(dpool.dentries[returndent].d_count != 0) /* replaces check for success in pseudocode */
	}
	:: else
	fi;
	spinlock_unlock(dcache_lock)
}

inline path_release(dent) {
	assert(dent!=NoofNodes); /* Not Null - replaces if branch in pseudocode */
	dput(dpool.dentries[dent].d_parent);
	dput(dent);
}

inline update_parent(dent,siblingslv,subdirslv,isdirectory_flag,count,count2)
{
	assert(dent!=NoofNodes);
	printf("Update parent called with dent = %u\n",dent);
	is_directory(dent,isdirectory_flag);
	assert(isdirectory_flag==1);

	count=0;
	do /* init siblings and subdirs */
	:: count<NoofNodes -> {
		siblingslv[count]=0;
		subdirslv[count]=0;
		count++;
	}
	:: count==NoofNodes -> break
	od;

	count=1; /* Don't take root into account */ 
	do /* calc subdirs and siblings */
	:: count<NoofNodes -> {
		if
		:: dpool.available[count]==1 && dpool.dentries[count].d_count!=0 /* in use */
			&& dpool.dentries[count].d_parent==dent -> { /* and parent is right one */
			siblingslv[count]=1; /* mark as sibling */
			is_directory(count,isdirectory_flag);
			if
			:: isdirectory_flag -> subdirslv[count]=1; /* mark as subdir */
			:: else
			fi;
			count++
		}
		:: else count++
		fi;
	}
	:: count==NoofNodes -> break
	od;
	subdirslv[dent]=1; /* dent is subdir of itself */

	count=1; /* Don't update root's siblings */  
	do /* update siblings */
	:: count<NoofNodes -> {
		if
		:: dpool.available[count]==1 && dpool.dentries[count].d_count!=0 /* in use */
			&& dpool.dentries[count].d_parent==dent -> { /* and parent is right one */
			count2=0;
			do /* write sibling array */
			:: count2<NoofNodes -> {
				dpool.dentries[count].d_child[count2]=siblingslv[count2];
				count2++
			}
			:: count2==NoofNodes -> break
			od
		}
		:: else
		fi;
		count++;
	}
	:: count==NoofNodes -> break
	od;
	
	count2=0;
	do /* write subdirs array */
	:: count2<NoofNodes -> {
		dpool.dentries[dent].d_subdirs[count2]=subdirslv[count2];
		count2++
	}
	:: count2==NoofNodes -> break
	od
}

/* Lower level sys calls */
/* Local vars TBD */
/* Assumes dpool,ipool,super,dcache_lock, inode_lock to be global */


inline path_lookup(patharray,cwd,parent,child,tmp,dtmp,pathindex,isdirectory_flag,mfdlv_4_1) {
	parent=NoofNodes; /* Null */
	if
	:: patharray[0]!=0 -> prepend(patharray,cwd)
	:: else
	fi;
	assert(patharray[0]==0); /*starts with root */
	tmp=0; /* first name is root */
	pathindex=0; /* current position in path */
	do
	:: tmp != NoofNodes -> { /* Not reached end of path (NoofNodes=NULL) */ 
		printf("tmp=%u, pathindex=%u\n",tmp,pathindex);
		get_dentry(tmp,parent,dtmp,mfdlv_4_1);
		printf("dtmp fetched as %u\n",dtmp);
		if
		:: dtmp==NoofNodes -> { /* current path extension doesn't exist */
			if 
			:: parent==NoofNodes -> {/* Never even found root */
				child=NoofNodes;
				break
			}
			:: else { /* Found root but got stuck later */
				if
				:: patharray[pathindex+1]!=NoofNodes -> { /* Got stuck before last component */
					dput(parent);
					parent=NoofNodes;
					child=NoofNodes;
					break
				}
				:: else { /* It was the last component in the path */
					child=NoofNodes;	
					printf("Last component in Path!!\n");
					break
				}
				fi
			}
			fi
		}
		:: else  { /* Current path extension does exist */
			if 
			:: patharray[pathindex+1]!=NoofNodes -> { /* Not last element in path */
				is_directory(dtmp,isdirectory_flag);
				if 
				:: isdirectory_flag -> {
					if 
					:: parent!=NoofNodes -> dput(parent) 
					/* First time through parent = NULL, no dget on parent, so no dput */
					:: else
					fi;
					parent=dtmp;
					pathindex++;
					tmp=patharray[pathindex]
				}
				:: else { /* can't go any further */
					if 
					:: parent!=NoofNodes -> dput(parent) 
					/* First time through parent = NULL, no dget on parent, so no dput */
					:: else
					fi;
					dput(dtmp);
					parent=NoofNodes;
					child=NoofNodes;
					break;
				}
				fi
			}
			:: else { /* Is last element */
				pathindex++;
				tmp=patharray[pathindex]
			}
			fi
		}
		fi
	}
	:: tmp == NoofNodes -> {
		child = dtmp;
		break /* parent and child set correctly */
	}
	od 
}


/* Sys calls */
/* Local vars TBD */

inline sys_creat(patharray,cwd,error,parent,file,isdirectory_flag,filename,plulv_4_1,plulv_4_2,plulv_4_3,plulv_1_1,
			up_lv1,up_lv2,mfdlv_4_1){
	error=0;
	path_lookup(patharray,cwd,parent,file,plulv_4_1,plulv_4_2,plulv_4_3,plulv_1_1,mfdlv_4_1);
	if
	:: parent!=NoofNodes -> { /* if parent exists */
		down(ipool.inodes[dpool.dentries[parent].d_inode].i_mutex);
		if 
		:: file!=NoofNodes -> is_directory(file,isdirectory_flag) /* Only check directory if file exists */
		:: else
		fi;
		if 
		:: file != NoofNodes && ! isdirectory_flag -> { /* File exists and isn't directory */
			up(ipool.inodes[dpool.dentries[parent].d_inode].i_mutex);
			path_release(file)
		}
		:: file != NoofNodes && isdirectory_flag -> { /* File exists but is directory */
			up(ipool.inodes[dpool.dentries[parent].d_inode].i_mutex);
			path_release(file);
			error=1
		}
		:: file == NoofNodes -> { /* File doesn't exist */
			spinlock_lock(dcache_lock);
			last_component(patharray,filename); /* Get filename */
			allocate_dentry(file,filename,parent,plulv_4_1,plulv_1_1); /* borrow the PLU locals! */ 
			assert(file!=NoofNodes && file!=0); /* replaces if structure - file not null or root */
					/* This check is redundant - root will never be reallocated
					   and allocate_dentry will terminate rather than return null */
			dget(file);
			spinlock_lock(inode_lock);
			allocate_inode(dpool.dentries[file].d_inode,file,plulv_4_1,plulv_1_1);
						/* Borrowing pathlookup lvs again! */
			spinlock_unlock(inode_lock);		
			assert(dpool.dentries[file].d_inode!=NoofNodes &&
				dpool.dentries[file].d_inode!=0); /* replaces if structure */
					/* This check is redundant - root will never be reallocated
					   and allocate_dentry will terminate rather than return null */
			update_parent(dpool.dentries[file].d_parent,up_lv1,up_lv2,plulv_1_1,
				plulv_4_1,plulv_4_2); /* Borrow the plu lvs */
			printf("Updated Parent!! \n");
			path_release(file);
			spinlock_unlock(dcache_lock);
			up(ipool.inodes[dpool.dentries[parent].d_inode].i_mutex);
		}
		fi
	}
	:: else { /* Either child and parent don't exist, or child is root (from path_lookup(root)) */ 
		error=1;
		if
		:: file!=NoofNodes -> {
			assert(file==0); /* can only happen for root */
			dput(file)
		}
		:: else
		fi
	}
	fi
}

inline sys_mkdir(patharray,cwd,error,parent,dir,isdirectory_flag,dirname,plulv_4_1,plulv_4_2,plulv_4_3,plulv_1_1,
			up_lv1,up_lv2,mfdlv_4_1){
	error=0;
	path_lookup(patharray,cwd,parent,dir,plulv_4_1,plulv_4_2,plulv_4_3,plulv_1_1,mfdlv_4_1);
	if 
	:: parent==NoofNodes -> { /* Either child and parent don't exist, or child is root (from path_lookup(root)) */ 
		error=1;
		if
		:: dir!=NoofNodes -> {
			assert(dir==0); /* can only happen for root */
			dput(dir)
		}
		:: else
		fi
	}
	:: else 
		if 
		:: dir!=NoofNodes ->  {/* directory exists */
			path_release(dir);
			error=1
		}
		:: else { /* parent exists but dir doesn't */
			spinlock_lock(dcache_lock);
			last_component(patharray,dirname); /* Get dirname */
			allocate_dentry(dir,dirname,parent,plulv_4_1,plulv_1_1); /* borrow the PLU locals! */ 
			assert(dir!=NoofNodes && dir!=0); /* replaces if structure - file not null or root */
					/* This check is redundant - root will never be reallocated
					   and allocate_dentry will terminate rather than return null */
			dget(dir);
			spinlock_lock(inode_lock);
			allocate_inode(dpool.dentries[dir].d_inode,dir,plulv_4_1,plulv_1_1);
						/* Borrowing pathlookup lvs again! */
			assert(dpool.dentries[dir].d_inode!=NoofNodes &&
				dpool.dentries[dir].d_inode!=0); /* replaces if structure */
					/* This check is redundant - root will never be reallocated
					   and allocate_dentry will terminate rather than return null */
			down(ipool.inodes[dpool.dentries[dir].d_inode].i_mutex);
			spinlock_unlock(inode_lock);
			dpool.dentries[dir].d_subdirs[dir]=1; /* directory is subdir of itself */
			update_parent(dpool.dentries[dir].d_parent,up_lv1,up_lv2,plulv_1_1,
				plulv_4_1,plulv_4_2); /* Borrow the plu lvs */
			path_release(dir);
			spinlock_unlock(dcache_lock);
			up(ipool.inodes[dpool.dentries[dir].d_inode].i_mutex);
		}
		fi
	fi
}

inline sys_unlink(patharray,cwd,error,parent,file,isdirectory_flag, plulv_4_1,plulv_4_2,plulv_4_3,plulv_1_1,
		up_lv1,up_lv2,mfdlv_4_1)
{
	error=0;
	path_lookup(patharray,cwd,parent,file,plulv_4_1,plulv_4_2,plulv_4_3,plulv_1_1,mfdlv_4_1);
	if 
	:: parent==NoofNodes -> { /* Either child and parent don't exist, or child is root (from path_lookup(root)) - 
				guards use of dput [with assertion] not required in pseudocode*/ 
		error=1;
		if
		:: file!=NoofNodes -> {
			assert(file==0); /* can only happen for root */
			dput(file)
		}
		:: else
		fi
	}
	:: else 
		if 
		:: file==NoofNodes ->  {/* parent exists but file doesn't */
			dput(parent);
			error=1
		}
		:: else { /* parent and file exist */
			is_directory(file,isdirectory_flag);
			if 
			:: isdirectory_flag -> { /* file to be deleted is a directory! */
				path_release(file);
				error=1
			}
			:: else { /* ok to delete */
				down(ipool.inodes[dpool.dentries[file].d_inode].i_mutex);
					/* This is NEVER released in this model cause the
					    inode will never get reassigned, just deallocated 
					    - need to check that this field in particular is cleaned up 
					    in alloc/dealloc */
				spinlock_lock(dcache_lock);
				
				/* The following is a fix to get around absence 
				   of i_count in inode structure and lack of reassignment
				    of nodes in alloc functions. Avoids need for 
				    clean up operation */
				
				do
				:: dpool.dentries[file].d_count!=0 -> {
					spinlock_lock(dpool.dentries[file].d_lock);
					if
					:: dpool.dentries[file].d_count==2 -> 
						dpool.dentries[file].d_count=0
					:: else
					fi;
					spinlock_unlock(dpool.dentries[file].d_lock)
				}
				:: dpool.dentries[file].d_count==0 -> break
				od;
				assert(dpool.dentries[file].d_count==0); 
					/* Nothing should have been able to interfere */
				spinlock_lock(ipool.inodes[dpool.dentries[file].d_inode].i_lock);
				dealloc_inode(ipool,dpool.dentries[file].d_inode);
				spinlock_lock(dpool.dentries[file].d_lock);
				dealloc_dentry(dpool,file);
				/* end of fix */
				
				update_parent(parent,up_lv1,up_lv2,plulv_1_1,
					plulv_4_1,plulv_4_2); /* Borrow the plu lvs */
				dput(parent);
				spinlock_unlock(dcache_lock)
			}
			fi
		}
		fi
	fi
}

inline sys_rmdir (patharray,cwd,error,parent,dir,isdirectory_flag,plulv_4_1,plulv_4_2,plulv_4_3,plulv_1_1,
	up_lv1,up_lv2,mfdlv_4_1) 
{
	error=0;
	path_lookup(patharray,cwd,parent,dir,plulv_4_1,plulv_4_2,plulv_4_3,plulv_1_1,mfdlv_4_1);	
	if 
	:: parent==NoofNodes -> { /* Either child and parent don't exist, or child is root (from path_lookup(root)) - 
				guards use of dput [with assertion] not required in pseudocode*/ 
		error=1;
		if
		:: dir!=NoofNodes -> {
			assert(dir==0); /* can only happen for root */
			dput(dir)
		}
		:: else
		fi
	}
 	:: else 
		if 
		:: dir == NoofNodes -> {
			dput(parent);
			error=1;
		}
		:: else {
			is_directory(dir,isdirectory_flag);
			if
			:: !isdirectory_flag -> {
				path_release(dir);
				error=1;
			}
			:: else { /* Ok to remove if dir empty */
				down(ipool.inodes[dpool.dentries[dir].d_inode].i_mutex);
					/* This is NEVER released in this model cause the
					    inode will never get reassigned, just deallocated 
					    (unless dir has children and remove fails)
					    - need to check that this field in particular is cleaned up 
					    in alloc/dealloc */
				spinlock_lock(dcache_lock);
				plulv_4_1=0;  /* borrow plu lvs */
				plulv_4_2=0;
				do
				:: plulv_4_1<NoofNodes -> {
					if
					:: dpool.available[plulv_4_1]==1 && /* allocated */
					   dpool.dentries[plulv_4_1].d_count !=0 && /* assigned */
					   dpool.dentries[plulv_4_1].d_parent==dir -> {/*ischild of dir*/
						plulv_4_2++
					}
					:: else
					fi;
					plulv_4_1++
				}
				:: plulv_4_1==NoofNodes -> break
				od;
				if 
				:: plulv_4_2 != 0 -> { /* has children */
					spinlock_unlock(dcache_lock);
					up(ipool.inodes[dpool.dentries[dir].d_inode].i_mutex);
					path_release(dir);
					error=1
				}
				:: else { /* ok to remove  */
					/* The following is a fix that deals with lack of 
					   i_count field in inodes and non-reassignment in
					   allocation functions. Avoids need for cleanup operation.*/
					do
					:: dpool.dentries[dir].d_count!=0 -> {
						spinlock_lock(dpool.dentries[dir].d_lock);
						if
						:: dpool.dentries[dir].d_count==2 ->
							dpool.dentries[dir].d_count=0
						:: else
						fi;
						spinlock_unlock(dpool.dentries[dir].d_lock);
					}
					:: dpool.dentries[dir].d_count==0 -> break
					od;
					assert(dpool.dentries[dir].d_count==0); 
					/* Nothing should have been able to interfere */
					spinlock_lock(ipool.inodes[dpool.dentries[dir].d_inode].i_lock);
					dealloc_inode(ipool,dpool.dentries[dir].d_inode);
					spinlock_lock(dpool.dentries[dir].d_lock);
					dealloc_dentry(dpool,dir);
					/* end of fix */

					update_parent(parent,up_lv1,up_lv2,
						plulv_1_1,plulv_4_1,plulv_4_2); /* Borrow the plu lvs */
					dput(parent);
					spinlock_unlock(dcache_lock)
				}
				fi
			}
			fi
		}
		fi
	fi
}

inline sys_rename2(patharray1,patharray2,cwd,error,parent_src,child_src,parent_dest,child_dest,
	isdirectory_flag,plulv_4_1,plulv_4_2,plulv_4_3,plulv_1_1,up_lv1,up_lv2,mfdlv_4_1)
{
	printf("Entered rename2 ok\n");
	printf("0's mutex currently %u\n",ipool.inodes[0].i_mutex.islocked);
	if
	:: child_dest!=NoofNodes -> {
		is_directory(child_dest,isdirectory_flag); 
		if 
		:: isdirectory_flag -> { /* destination is directory - move source child into it */
			if 
			:: parent_dest != NoofNodes -> /* might be root */
				dput(parent_dest)
			:: else
			fi;
			parent_dest=child_dest;
			last_component(patharray1,plulv_4_1) ; /* borrow plu lv */
			get_dentry(plulv_4_1,parent_dest,child_dest,mfdlv_4_1);  /* Note no dget!! */
			/* concat last component of src onto patharray2 */
			concat_element(patharray2,plulv_4_1);  /* Affects patharray2 */
		}
		:: else
		fi
	}
	:: else
	fi;
	if 
	:: child_dest!=NoofNodes -> {
		is_directory(child_dest,isdirectory_flag); 
		if
		:: isdirectory_flag -> {
			error=1;
			dput(parent_src);
			dput(child_src);
			dput(parent_dest);
			dput(child_dest)
		}
		:: else
		fi
	}
	:: else
	fi;
	if 
	:: error==0 && child_dest!=NoofNodes -> {
		is_directory(child_dest,isdirectory_flag); /* This check looks redundant */
		if
		:: !isdirectory_flag -> {
			is_directory(child_src,isdirectory_flag);
			if
			:: isdirectory_flag -> {
				error=1;
				dput(parent_src);
				dput(child_src);
				dput(parent_dest);
				dput(child_dest)
			}
			:: else
			fi
		}
		:: else
		fi
	}
	:: else
	fi;
	if 
	:: error==0 -> {
		is_directory(child_src,isdirectory_flag);
		if 
		:: isdirectory_flag && dpool.dentries[child_src].d_count > 2 -> {
			error=1;
			dput(parent_src);
			dput(child_src);
			dput(parent_dest);
			if 
			:: child_dest!=NoofNodes ->
				dput(child_dest) /* not guaranteed to exist */
			:: else
			fi
		}
		:: else
		fi
	}
	:: else
	fi;
	if 
	:: error ==0 -> {
		is_prefix(patharray2,patharray1,isdirectory_flag); /* Borrow isdirectory_flag */
		if
		:: isdirectory_flag -> {
			error=1;
			dput(parent_src);
			dput(child_src);
			dput(parent_dest);
			if 
			:: child_dest!=NoofNodes ->
				dput(child_dest) /* not guaranteed to exist */
			:: else
			fi
		}
		:: else
		fi
	}
	:: else
	fi;
 	if 
	:: error==0 -> {
		printf("Entered rename code\n");
		/* down(ipool.inodes[dpool.dentries[parent_src].d_inode].i_mutex);
		printf("Got src mutex\n"); - deadlock bug fix */ 
		printf("Getting %u's mutex, currently %u\n",dpool.dentries[parent_dest].d_inode,
			ipool.inodes[dpool.dentries[parent_dest].d_inode].i_mutex.islocked);
		down(ipool.inodes[dpool.dentries[parent_dest].d_inode].i_mutex);
		printf("Got both mutexes - getting dcache lock...\n");
		spinlock_lock(dcache_lock);
		printf("Got locks\n");
		if 
		:: child_dest!=NoofNodes -> { /* If destination file exists then remove it */
			printf("Removing existing file\n");
			printf("Current d_count = %u\n", dpool.dentries[child_dest].d_count);
			do
			:: dpool.dentries[child_dest].d_count!=0 -> {
				spinlock_lock(dpool.dentries[child_dest].d_lock);
				if
				:: dpool.dentries[child_dest].d_count==2 ->
					dpool.dentries[child_dest].d_count=0
				:: else
				fi;
				spinlock_unlock(dpool.dentries[child_dest].d_lock);
			}
			:: dpool.dentries[child_dest].d_count==0 -> break
			od;
			assert(dpool.dentries[child_dest].d_count==0); 
			/* Nothing should have been able to interfere */
			spinlock_lock(ipool.inodes[dpool.dentries[child_dest].d_inode].i_lock);
			dealloc_inode(ipool,dpool.dentries[child_dest].d_inode);
			spinlock_lock(dpool.dentries[child_dest].d_lock);
			dealloc_dentry(dpool,child_dest);
			update_parent(dpool.dentries[child_dest].d_parent,up_lv1,up_lv2,
				plulv_1_1,plulv_4_1,plulv_4_2); /* borrow plu lvs */
			child_dest=NoofNodes
		}
		:: else
		fi;
		/* Rename/Move */
		printf("Moving File\n"); 
		dpool.dentries[child_src].d_parent=parent_dest;
		last_component(patharray2,plulv_4_1) ; /* borrow plu lv */
		dpool.dentries[child_src].d_iname=plulv_4_1;
		update_parent(parent_src,up_lv1,up_lv2,
				plulv_1_1,plulv_4_1,plulv_4_2); /* borrow plu lvs */
		update_parent(parent_dest,up_lv1,up_lv2,
				plulv_1_1,plulv_4_1,plulv_4_2); /* borrow plu lvs */
		dput (parent_dest);
		/* path_release(child_src); - bug replaced with next two lines */
		dput(parent_src);
		dput(child_src);
		spinlock_unlock(dcache_lock);
		/* up(ipool.inodes[dpool.dentries[parent_src].d_inode].i_mutex); deadlock bugfix */
		up(ipool.inodes[dpool.dentries[parent_dest].d_inode].i_mutex)
	}
	:: else
	fi
}

inline sys_rename(patharray1,patharray2,cwd,error,parent_src,child_src,parent_dest,child_dest,
	isdirectory_flag,plulv_4_1,plulv_4_2,plulv_4_3,plulv_1_1,up_lv1,up_lv2,mfdlv_4_1) /* Affects patharray2 */
{
	error=0;
	path_lookup(patharray1,cwd,parent_src,child_src,plulv_4_1,plulv_4_2,plulv_4_3,plulv_1_1,mfdlv_4_1);		
	if
	:: parent_src == NoofNodes -> { /* Either parent and child null, or child=root for path_lookup(root)
					guards use of dput; not needed in pseudocode */
		error=1;
		if
		:: child_src!=NoofNodes -> {
			assert(child_src==0); /* Can only happen for root */
			dput(child_src)
		}
		:: else
		fi
	}
	:: else 
		if
		:: child_src == NoofNodes -> {
			dput(parent_src);
			error=1
		}
		:: else {
			path_lookup(patharray2,cwd,parent_dest,child_dest,plulv_4_1,plulv_4_2,plulv_4_3,
				plulv_1_1,mfdlv_4_1);
			if
			::  parent_dest == NoofNodes -> { /* destination's parent doesn't even exist or destination root */
				if 
				:: child_dest!=NoofNodes -> { /* dest root */
					assert(child_dest==0); /* should be root */
				}
				:: else {
					dput(parent_src);
					dput(child_src);
					error=1
				}
				fi
			}
			:: else
			fi;
			if 
			:: error==0 -> {
				if
				:: child_dest == child_src -> { /* can't be root - if src was root would have returned */
					dput(parent_src);
					dput(child_src);
					dput(parent_dest);
					if
					:: child_dest!=NoofNodes -> dput(child_dest)
					:: else
					fi;
					error=1
				}
				:: else sys_rename2(patharray1,patharray2,cwd,error,
					parent_src,child_src,parent_dest,child_dest,
					isdirectory_flag,plulv_4_1,plulv_4_2,plulv_4_3,plulv_1_1,
					up_lv1,up_lv2,mfdlv_4_1)
				fi
			}
			:: else
			fi
		}
		fi
	fi;
}


/* Test/verification harness */

/* Pretend CD */

inline cd(array,arg) /* scratch var cd_count */
{
	d_step { 
		if
		:: arg==0 -> { /* cd root */
			array[0]=0;
			array[1]=NoofNodes
		}
		:: arg==NoofNodes -> { /* cd .. */
/*			assert(array[0]==0 && array[1]!=NoofNodes);   Not root */
			if /* replaces assertion for verification purposes */
			:: array[0]!=0 || array[1]==NoofNodes
			:: else {
				cd_count=0;
				do
				:: array[cd_count]!=NoofNodes -> cd_count++
				:: array[cd_count]==NoofNodes -> break
				od;
/*				assert(cd_count!=0); */
				if /* replaces assertion for verification purposes */
				:: cd_count==0
				:: else
					array[cd_count-1]=NoofNodes
				fi
			}
			fi
		}
		:: else { /* cd id */
			cd_count=0;
			do
			:: array[cd_count]!=NoofNodes -> cd_count++
			:: array[cd_count]==NoofNodes -> break
			od;
/*			assert(cd_count<NoofNodes); This was wrong anyway! Needed +1 */
			if /* replaces assertion for verification purposes */
			:: cd_count+1>=NoofNodes
			:: else
				concat_element(array,arg)
			fi
		}
		fi
	}
};


/* Choose an id between 1 and NoofNodes-1 - assumes max noofnodes is 8 */
inline choose_id (returnval)
{
	d_step{
#if !defined(myverif)
		STDIN?c;
#endif
		if
		::
 #if !defined(myverif)
		c==49 &&
#endif
			NoofNames-1>=1 -> returnval=1
		:: 
#if !defined(myverif)
		c==50 &&
#endif
			NoofNames-1>=2 -> returnval=2
		:: 
#if !defined(myverif)
		c==51 &&
#endif
			NoofNames-1>=3 -> returnval=3
		:: 
#if !defined(myverif)
		c==52 &&
#endif
			NoofNames-1>=4 -> returnval=4
		:: 
#if !defined(myverif)
		c==53 &&
#endif
			NoofNames-1>=5 -> returnval=5
		::
#if !defined(myverif)
		c==54 &&
#endif	
			NoofNames-1>=6 -> returnval=6
		::
#if !defined(myverif)
		c==55 &&
#endif 
			NoofNames-1>=7 -> returnval=7
		fi
#if !defined(myverif)
		;
		printf("c=%c, returnval=%u\n",c,returnval);
		STDIN?c /* Get rid of carriage return */
#endif 
	}
};

inline copy_path(frompath,topath)
{
	d_step{
		cp_count=0;
		do
		:: frompath[cp_count]!=NoofNodes -> {
			topath[cp_count]=frompath[cp_count];
			cp_count++
		}
		:: frompath[cp_count]==NoofNodes -> {
			topath[cp_count]=NoofNodes;
			break
		}
		od
	}
};

/* Monitor functions */

inline print_relations(bitarray,localvar)
{
	localvar=0;
	do
	:: localvar<NoofNodes -> {
		if 
		:: bitarray[localvar]==1 -> printf("\n \t\t %u ",localvar)
		:: bitarray[localvar]==0 -> printf("\n \t\t - ")
		fi;
		localvar++;
	}
	:: localvar==NoofNodes -> break
	od
};

inline printdentries(dep,localvar,localvar2) { /* Needs 4 bit localvar */
d_step{
	localvar=0;
	printf("Dentry pool: \n\n");
	do
	:: localvar<=NoofNodes-1 -> {
		if 
		:: dep.available[localvar] ==1 -> {
			printf("\t Dentry %u in use\n",localvar);
			printf("\t d_name = %u, d_inode = %u, d_parent = %u \n",dep.dentries[localvar].d_iname,dep.dentries[localvar].d_inode,dep.dentries[localvar].d_parent);
			printf("\n");
			printf("d_count = %u\n\n", dep.dentries[localvar].d_count);
#if defined(myverif)
			assert(dep.dentries[localvar].d_count==1);
#endif 
			printf("\t Siblings: ");
			print_relations(dep.dentries[localvar].d_child,localvar2);
			printf("\n \t Sub Directories: ");
			print_relations(dep.dentries[localvar].d_subdirs,localvar2);
			printf("\n\n");
		}
		:: else printf("\t Dentry %u not in use\n",localvar)
		fi;
		localvar++
		}
	:: localvar==NoofNodes -> break
	od
} /*dstep */
};

inline printinodes(inp,localvar) { /* Needs 4 bit localvar */
d_step{
	localvar=0;
	printf("Inode pool: \n\n");
	do
	:: localvar<=NoofNodes-1 -> {
		if 
		:: inp.available[localvar] ==1 -> {
			printf("\t Inode %u in use\n",localvar);
			printf("\t i_dentry = %u\n",inp.inodes[localvar].i_dentry);
			printf("\t i_mutex.is_locked=%u\n\n",inp.inodes[localvar].i_mutex.islocked);
		}
		:: else printf("\t Inode %u not in use\n",localvar)
		fi;
		localvar++
		}
	:: localvar==NoofNodes -> break
	od
} /*dstep*/
};


inline print_path(path)
{
	d_step{
		ppa_count=0;
		do
		:: path[ppa_count]!=NoofNodes->{
			printf("%u",path[ppa_count]);
			ppa_count++
		}
		:: path[ppa_count]==NoofNodes->{
			printf("\n");
			break
		}
		od
	} 
}

/* No longer used */
inline checkrefcounts(dep,inp,noofdentries,noofinodes,localvar,acc) { /* 4 bit localvar,acc */
d_step{ 
	localvar=0;
	acc=0;
	do
	:: localvar<=NoofNodes-1 -> { 
		if
		:: dep.available[localvar]==1 -> acc++
		:: else 
		fi;
		localvar++;
		}
	:: localvar==NoofNodes -> break;
	od;
	printf("\n\nDentry Ref Count = %u; Actual: %u\n",noofdentries,acc);
	assert(acc==noofdentries);

	localvar=0;
	acc=0;
	do
	:: localvar<=NoofNodes-1 -> { 
		if
		:: inp.available[localvar]==1 -> acc++
		:: else 
		fi;
		localvar++;
		}
	:: localvar==NoofNodes -> break;
	od;
	printf("Inode Ref Count = %u; Actual: %u\n",noofinodes,acc);
	assert(acc==noofinodes)
} /* dstep*/
};


superblock super;
dentrypool dpool;
inodepool ipool;
lock dcache_lock;
lock inode_lock;

/* scratch variables passed up to alloc/dealloc funs */
hidden 	unsigned fourbitlv : 4, fourbitlv2: 4;

/* scratch variables referred to in prepend, concat and isprefix functions */
hidden 	byte pp_temparray [PathLength];
hidden 	unsigned pp_count : 4, pp_offset : 4;
hidden	byte pp_flag;
hidden	unsigned ce_count : 4;
hidden	unsigned ip_count : 4;

/* scratch variable for is_directory function */
hidden	unsigned id_count : 4;

/* scratch vaiable for last_component function */
hidden	unsigned lc_count : 4;

/* scratch variable for cd */
hidden	unsigned cd_count : 4;

/* scratch variable for print path */
hidden	unsigned ppa_count : 4;

/* scratch variable for copy path */
hidden	unsigned cp_count : 4;

#if !defined(myverif)
byte c;
#endif

active proctype test () {

	unsigned node : 3;
	bit onebitlv;
	bit flag,errorflag;

	byte srcpath [PathLength];
	byte dstpath [PathLength];
	byte tmppath [PathLength];
	byte cwd[PathLength];
	unsigned fourbitlv3 : 4, fourbitlv4: 4, fourbitlv5:4, fourbitlv6:4;
	unsigned fourbitlv7:4,fourbitlv8 : 4, fourbitlv9:4, fourbitlv10:4;
	unsigned threebitlv : 3;
	bit bitlv,bitlv2;
	bit bitarraylv_1 [NoofNodes];
	bit bitarraylv_2 [NoofNodes];

	/* Initialise Superblock */
	init_superblock(dpool,ipool,super,node,fourbitlv,onebitlv);

	cd(dstpath,0); /* dstpath=root */
	cd(srcpath,0); /* srcpath=root */
	cd(cwd,0);/* Set cwd to root - cwd never used by harness, all calls by abs path, this is just for call i/f */

	do 
	:: {
		printf("Choosing Id (1-NoofNodes-1)\n");
		choose_id(node); /* Set srcpath */
		printf("Choosing src cd (0:root,1:down,2:up,3:skip)\n");
		printf("Current src path=");
		print_path(srcpath);
#if !defined(myverif)
		STDIN?c;
#endif
		if
#if !defined(myverif)
		:: c==48 -> cd(srcpath,0) /* root */
#endif
		:: 
#if !defined(myverif)
		c==49 ->
#endif
			cd(srcpath,node) /* down to id */
		:: 
#if !defined(myverif)
		c==50 ->
#endif
			cd(srcpath,NoofNodes) /* .. */
		::
#if !defined(myverif)
		c==51 ->
#endif 
			skip
		fi;
#if !defined(myverif)
		STDIN?c; /* carriage return */
#endif

		printf("Choosing Id (1-NoofNodes-1)\n");
		choose_id(node); /* Set dstpath */
		printf("Choosing dst cd (0:root,1:down,2:up,3:skip)\n");
		printf("Current dst path=");
		print_path(dstpath);
#if !defined(myverif)
		STDIN?c;
#endif
		if
#if !defined(myverif)
		:: c==48 -> cd(dstpath,0)
#endif
		:: 
#if !defined(myverif)
		c==49 ->
#endif
			cd(dstpath,node)
		:: 
#if !defined(myverif)
		c==50 ->
#endif
			cd(dstpath,NoofNodes)
		:: 
#if !defined(myverif)
		c==51 ->
#endif 
			skip
		fi;
#if !defined(myverif)
		STDIN?c; /* carriage return */
#endif 

		printf("Choosing model functions (0:mkdir,1:creat,2:rename,3:unlink,4:rmdir,5:skip)\n");
#if !defined(myverif)
		STDIN?c;
#endif
		if  /* Possibly call one of the Model functions */
		:: 
#if !defined(myverif)
		c==48 ->
#endif 
		{
			sys_mkdir(srcpath,cwd,errorflag,fourbitlv3,fourbitlv4,bitlv,threebitlv,
				fourbitlv5,fourbitlv6,fourbitlv7,bitlv2,bitarraylv_1,bitarraylv_2,fourbitlv8);
			printf("Called Mkdir. Error=%u. Path=",errorflag);
			print_path(srcpath) 
		}
		:: 
#if !defined(myverif)
		c==49 ->
#endif 
		{	
			sys_creat(srcpath,cwd,errorflag,fourbitlv3,fourbitlv4,bitlv,threebitlv,
				fourbitlv5,fourbitlv6,fourbitlv7,bitlv2,bitarraylv_1,bitarraylv_2,fourbitlv8);
			printf("Called Creat. Error=%u. Path=",errorflag);
			print_path(srcpath)
		}
		:: 
#if !defined(myverif)
		c==50 ->
#endif 
		{	
			copy_path(dstpath,tmppath);
			sys_rename(srcpath,tmppath,cwd,errorflag,fourbitlv3,fourbitlv4,fourbitlv9,fourbitlv10,
				bitlv,fourbitlv5,fourbitlv6,fourbitlv7,bitlv2,bitarraylv_1,bitarraylv_2,fourbitlv8);
				/* may alter paths!!!!!!!!!!!! */
			printf("Called Rename. Error=%u. Src Path=",errorflag);
			print_path(srcpath);
			printf("Dst Path=");
			print_path(dstpath)
		}
		:: 
#if !defined(myverif)
		c==51 ->
#endif 
		{
			sys_unlink(srcpath,cwd,errorflag,fourbitlv3,fourbitlv4,bitlv,fourbitlv5,fourbitlv6,fourbitlv7,
				bitlv2,bitarraylv_1,bitarraylv_2,fourbitlv8);
			printf("Called Unlink. Error=%u. Path=",errorflag);
			print_path(srcpath)
		}
		:: 
#if !defined(myverif)
		c==52 ->
#endif 
		{
			sys_rmdir(srcpath,cwd,errorflag,fourbitlv3,fourbitlv4,bitlv,fourbitlv5,fourbitlv6,fourbitlv7,
				bitlv2,bitarraylv_1,bitarraylv_2,fourbitlv8);
			printf("Called Rmdir. Error=%u. Path=",errorflag);
			print_path(srcpath)
		}
		:: 
#if !defined(myverif)
		c==53 ->
#endif 
		{
			skip;
			printf("Called no function\n")
		}
		fi;
		printf("\n");
#if !defined(myverif)
		STDIN?c; /* carriage return */
#endif 

progress_testharn:
		printf("Report? (0:yes,1:no)\n");
#if !defined(myverif)
		STDIN?c;
#endif
		if /* Possibly report state of file system */
		:: 
#if !defined(myverif)
		c==48 ->
#endif 
		{
			printdentries(dpool,fourbitlv,fourbitlv2);
			printf("\n\n");
			printinodes(ipool,fourbitlv); 
		}
		:: 
#if !defined(myverif)
		c==49 ->
#endif 
			skip
		fi
#if !defined(myverif)
		;
		STDIN?c /* carriage return */
#endif 
	}
	od;
end:
	skip
}