// sEXT2 - Simple FileSystem Example -  MODEL DEFINITION FILE

// rule 1 - adds the block number of the superblock to the superblock set
[], literal(true) => literal(0) in SuperBlock;

// rule 2 - adds the block number of the groupblock to the groupblock set
[], literal(true) => literal(1) in GroupBlock;

// rule 3 - adds the inodetableblock block number to the inodetableblock set
[], d.g.InodeTableBlock < d.s.NumberofBlocks => 
d.g.InodeTableBlock in InodeTableBlock; 

// rule 4 - adds the inodebitmapblock block number to the inodebitmapblock set
[], d.g.InodeBitmapBlock < d.s.NumberofBlocks => 
d.g.InodeBitmapBlock in InodeBitmapBlock; 

// rule 5 - adds the blockbitmapblock number to the blockbitmapblock set
[], d.g.BlockBitmapBlock < d.s.NumberofBlocks => 
d.g.BlockBitmapBlock in BlockBitmapBlock; 

// rule 6 - adds the rootdirectoryinode number to the set
[], d.s.RootDirectoryInode < d.s.NumberofInodes =>
d.s.RootDirectoryInode in RootDirectoryInode; 

// rule 7 
delay [for j=literal(0) to d.s.NumberofInodes-literal(1)], 
!(j in? UsedInode) => j in FreeInode; 

// rule 8
delay [for j=literal(0) to d.s.NumberofBlocks-literal(1)], 
!(j in? UsedBlock) => j in FreeBlock; 

// rule 9
// for all directoryinodes, loop through there blockptr's and then add
// all their directoryentries to DirectoryEntry set
[forall di in DirectoryInode, 
 forall itb in InodeTableBlock, 
 for j=literal(0) to (d.s.blocksize/literal(128))-literal(1), 
 for k=literal(0) to literal(11)], 
 cast(InodeTable,d.b[itb]).itable[di].Blockptr[k] < d.s.NumberofBlocks =>
 cast(DirectoryBlock,d.b[cast(InodeTable,d.b[itb]).itable[di].Blockptr[k]]).de[j]
 in DirectoryEntry;

// rule 10
// all non-zero blocks in an used inodes blockptr list should be 
// added to the contents relation 
[forall i in UsedInode, 
 forall itb in InodeTableBlock, 
 for j=literal(0) to literal(11)],
     !(cast(InodeTable,d.b[itb]).itable[i].Blockptr[j]=literal(0)) =>
     <i,cast(InodeTable,d.b[itb]).itable[i].Blockptr[j]> in contents; 


// rule 11 seems to be imperfect because it is adding directories and files
// to the filedirectoryblock but these automatically get funneled into
// fileblock (and hence the change below). Perhaps these should discriminate
// because otherwise, there is no direct use of DirectoryBlock (subset
// of FileDirectoryBlock) anywhere in the model definition at all.

// rule 11 
// for each inode in use, add non-zero, valid blocks mentioned in the 
// inode's blockptr list in the inodetableblock to fileblock
[forall i in UsedInode, forall itb in InodeTableBlock, for j=literal(0) to literal(11)],
cast(InodeTable,d.b[itb]).itable[i].Blockptr[j]<d.s.NumberofBlocks and
!(cast(InodeTable,d.b[itb]).itable[i].Blockptr[j]=literal(0)) =>
cast(InodeTable,d.b[itb]).itable[i].Blockptr[j] in FileBlock; // was FileDirectoryBlock

// rule 12
// if the bit in the inodebitmap is 0 then that inode is marked as
// free in the inodestatus relation
[for j=literal(0) to d.s.NumberofInodes-literal(1), forall ibb in InodeBitmapBlock],
cast(InodeBitmap,d.b[ibb]).inodebitmap[j]=literal(false) =>
<j,literal(Free)> in inodestatus; 

// rule 13
// same as rule 12/19, but instead with used inodes. 
[for j=literal(0) to d.s.NumberofInodes-literal(1), forall ibb in InodeBitmapBlock],
cast(InodeBitmap,d.b[ibb]).inodebitmap[j]=literal(true) =>
<j,literal(Used)> in inodestatus; 

// rule 14
// adds all non-zero inodenumbers of directory entries to the set
// FileInode
[forall de in DirectoryEntry], de.inodenumber<d.s.NumberofInodes and
!(de.inodenumber = literal(0)) => de.inodenumber in FileInode; 

// rule 15
// builds up relation 'inodeof' such that <x,y> means x is a
// directory entry with inode numbered y
[forall de in DirectoryEntry], de.inodenumber<d.s.NumberofInodes => 
<de, de.inodenumber> in inodeof; 

// rule 16
// populating the referencecount relation with the referencecount 
// values for every usedinode
[forall j in UsedInode, forall itb in InodeTableBlock], literal(true) =>
<j,cast(InodeTable,d.b[itb]).itable[j].referencecount> in referencecount; 

// rule 17 - populate the filesize relation with the sizes inodes' files
[forall j in UsedInode, forall itb in InodeTableBlock], literal(true) =>
<j,cast(InodeTable,d.b[itb]).itable[j].filesize> in filesize; 

// rule - similar to rule 19, if the bit in the block bitmap is 0 the that
// block is marked as free in the blockstatus relation
[for j=literal(0) to d.s.NumberofBlocks-literal(1), forall bbb in BlockBitmapBlock],
cast(BlockBitmap,d.b[bbb]).blockbitmap[j]=literal(false) =>
<j,literal(Free)> in blockstatus; 

// rule 19
// if the bit in the blockbitmap is 1 then that block is marked as 
// used in the blockstatus relation
[for j=literal(0) to d.s.NumberofBlocks-literal(1), forall bbb in BlockBitmapBlock],
cast(BlockBitmap,d.b[bbb]).blockbitmap[j]=literal(true) =>
<j,literal(Used)> in blockstatus;