Organizing

[repair.git] / Repair / RepairCompiler / MCC / specs / oldfilesystem / test2.model

diff --git a/Repair/RepairCompiler/MCC/specs/oldfilesystem/test2.model b/Repair/RepairCompiler/MCC/specs/oldfilesystem/test2.model
new file mode 100755 (executable)
index 0000000..78f8a9d
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/specs/oldfilesystem/test2.model
@@ -0,0 +1,96 @@
+// 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
+[], literal(true) => 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 13
+// same as rule 12/19, but instead with used inodes.
+[forall j in Inode, forall ibb in InodeBitmapBlock], literal(true) => <j, cast(InodeBitmap,d.b[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, 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
+//[forall j in Block, forall bbb in BlockBitmapBlock], literal(true) => <j,cast(BlockBitmap,d.b[bbb]).blockbitmap[j]> in blockstatus;
+