// sEXT2 - Simple FileSystem Example -  MODEL DEFINITION FILE
// rule 1 - adds the block number of the superblock to the superblock set
/*[], true => d.s in SuperBlock;*/

// rule 2 - adds the block number of the groupblock to the groupblock set
/*[], true => d.g in GroupBlock;*/

/*[], true => cast(InodeTable,d.b[d.g.InodeTableBlock]) in InodeTableBlock;*/

// rule 4 - adds the inodebitmapblock block number to the inodebitmapblock set
/*[], true => cast(InodeBitmap,d.b[d.g.InodeBitmapBlock]) in InodeBitmapBlock;*/

// rule 5 - adds the blockbitmapblock number to the blockbitmapblock set
[], true => cast(BlockBitmap,d.b[d.g.BlockBitmapBlock]) in BlockBitmapBlock;

// rule 6 - adds the rootdirectoryinode number to the set
/*[forall itb in InodeTableBlock], true => itb.itable[d.s.RootDirectoryInode] in RootDirectoryInode;*/

/*[forall itb in InodeTableBlock, for j=0 to d.s.NumberofInodes-1], !(itb.itable[j] in? UsedInode) => itb.itable[j] in FreeInode;*/

[for j=0 to d.s.NumberofBlocks-1], !(d.b[j] in? UsedBlock) => d.b[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, for j=0 to ((d.s.blocksize/128)-1), for k=0 to 11],  true => cast(DirectoryBlock,d.b[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 13
// same as rule 12/19, but instead with used inodes.

/*[for j=0 to d.s.NumberofInodes-1, forall itb in InodeTableBlock, forall ibb in InodeBitmapBlock], true => <itb.itable[j], ibb.inodebitmap[j]> 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], true => <j,j.referencecount> in referencecount;*/

// rule 17 - populate the filesize relation with the sizes inodes' files
/*[forall j in UsedInode], true => <j,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=0 to d.s.NumberofBlocks-1, forall bbb in BlockBitmapBlock], true => <d.b[j],bbb.blockbitmap[j]> in blockstatus;