Organizing

diff --git a/Repair/RepairCompiler/MCC/specs/oldfilesystem/test.constraints b/Repair/RepairCompiler/MCC/specs/oldfilesystem/test.constraints
new file mode 100755 (executable)
index 0000000..a6073fd
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/specs/oldfilesystem/test.constraints
@@ -0,0 +1,3 @@
+
+[forall u in UsedInode], u.inodestatus=literal(Used);
+[],sizeof(RootDirectoryInode)=1;
\ No newline at end of file

diff --git a/Repair/RepairCompiler/MCC/specs/oldfilesystem/test.model b/Repair/RepairCompiler/MCC/specs/oldfilesystem/test.model
new file mode 100755 (executable)
index 0000000..2c4e062
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/specs/oldfilesystem/test.model
@@ -0,0 +1 @@
+[], true => literal(0) in SuperBlock;

diff --git a/Repair/RepairCompiler/MCC/specs/oldfilesystem/test.space b/Repair/RepairCompiler/MCC/specs/oldfilesystem/test.space
new file mode 100755 (executable)
index 0000000..bd84734
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/specs/oldfilesystem/test.space
@@ -0,0 +1,73 @@
+// sEXT2 - Simple File System Example
+// Space Definition Language File
+
+set Block(int) : partition 
+    UsedBlock | 
+    FreeBlock;
+
+set FreeBlock(int);
+
+set Inode(int) : partition 
+    UsedInode | 
+    FreeInode;
+
+set FreeInode(int);
+
+set UsedInode(int) : partition 
+    FileInode | 
+    DirectoryInode ;
+
+set FileInode(int);
+
+set DirectoryInode(int) : RootDirectoryInode;
+
+set RootDirectoryInode(int);
+
+set UsedBlock(int) : partition 
+    SuperBlock | 
+    GroupBlock | 
+    FileDirectoryBlock | 
+    InodeTableBlock | 
+    InodeBitmapBlock | 
+    BlockBitmapBlock;
+
+set FileDirectoryBlock(int) : 
+    DirectoryBlock | 
+    FileBlock;
+
+set SuperBlock(int);
+
+set GroupBlock(int);
+
+set FileBlock(int);
+
+set DirectoryBlock(int);
+
+set InodeTableBlock(int);
+
+set InodeBitmapBlock(int);
+
+set BlockBitmapBlock(int);
+
+set DirectoryEntry(DirectoryEntry);
+
+// relations xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
+
+inodeof: DirectoryEntry -> UsedInode (many->1);
+
+contents: UsedInode -> FileDirectoryBlock (1->many);
+
+inodestatus: Inode -> token (many->1);
+
+blockstatus: Block -> token (many->1);
+
+referencecount: Inode -> int (many->1);
+
+filesize: Inode -> int (many->1);
+
+
+
+
+
+
+

diff --git a/Repair/RepairCompiler/MCC/specs/oldfilesystem/test.struct b/Repair/RepairCompiler/MCC/specs/oldfilesystem/test.struct
new file mode 100755 (executable)
index 0000000..c956e8b
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/specs/oldfilesystem/test.struct
@@ -0,0 +1,3 @@
+structure Block {
+     reserved byte[d.s.blocksize];
+}
\ No newline at end of file

diff --git a/Repair/RepairCompiler/MCC/specs/oldfilesystem/test2.constraints b/Repair/RepairCompiler/MCC/specs/oldfilesystem/test2.constraints
new file mode 100755 (executable)
index 0000000..bbc92e4
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/specs/oldfilesystem/test2.constraints
@@ -0,0 +1,66 @@
+// sEXT2 - Simple File System Example
+// Constraint Definition Language File
+
+// Constraints 1-4 verify that the bitmaps and references to block's match up
+// Constraints 5-6 verify that references counts and filesizes match up
+// Constraints 7-13 are singleton tests
+
+// C1
+// for all used inodes, verify that the inodestatus (built from the
+// inodebitmap is marked 'used'
+//[forall u in UsedInode], u.inodestatus=literal(true);
+
+// C2
+// for all free inodes, verify that the inodestatus (built from the 
+// inodebitmap is marked 'free'
+//[forall f in FreeInode], f.inodestatus=literal(false);
+
+// C3
+// for all used blocks, verify that the blockstatus (built from the
+// blockbitmap is marked 'used'
+//[forall u in UsedBlock], u.blockstatus=literal(true);
+
+// C4
+// for all free blocks, verify that the blockstatus (built from the
+// block bitmap is marked 'free'
+//[forall f in FreeBlock], f.blockstatus=literal(false);
+
+// C5
+// for all used inodes, verify that the reference count is equal to
+// the number of directory entries (files/links) that refer to that
+// inode
+//[forall i in UsedInode], i.referencecount=sizeof(i.~inodeof);
+
+// C6
+// for all used inodes, verify that the filesize is consistent with
+// the number of blocks used (those in i.contents)
+//[forall i in UsedInode], i.filesize <= sizeof(i.contents)*literal(8192);
+
+// C7
+// ??? for all files and directory blocks check that
+// only one inode references this block
+//[forall b in FileDirectoryBlock],sizeof(b.~contents)=literal(1);
+
+// C8
+// verify that there is one superblock
+//[],sizeof(SuperBlock)=literal(1);
+
+// C9
+// verify that there is one groupblock
+//[],sizeof(GroupBlock)=literal(1);
+
+// C10
+// verify that there is one inodetableblock
+//[],sizeof(InodeTableBlock)=literal(1);
+
+// C11
+// verify that there is one inodebitmapblock 
+[],sizeof(InodeBitmapBlock)=literal(1);
+
+// C12
+// verify that there is one blockbitmapblock
+//[],sizeof(BlockBitmapBlock)=literal(1);
+
+// C13
+// verify that there is one rootdirectoryinode
+//[],sizeof(RootDirectoryInode)=literal(1);

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;
+

diff --git a/Repair/RepairCompiler/MCC/specs/oldfilesystem/test2.space b/Repair/RepairCompiler/MCC/specs/oldfilesystem/test2.space
new file mode 100755 (executable)
index 0000000..8b303c6
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/specs/oldfilesystem/test2.space
@@ -0,0 +1,66 @@
+// sEXT2 - Simple File System Example
+// Space Definition Language File
+
+set Block(int) :
+    UsedBlock | 
+    FreeBlock;
+
+set FreeBlock(int);
+
+set Inode(int) :
+    UsedInode | 
+    FreeInode;
+
+set FreeInode(int);
+
+set UsedInode(int) : partition 
+    FileInode | 
+    DirectoryInode ;
+
+set FileInode(int);
+
+set DirectoryInode(int) : RootDirectoryInode;
+
+set RootDirectoryInode(int);
+
+set UsedBlock(int) :
+    SuperBlock | 
+    GroupBlock | 
+    FileDirectoryBlock | 
+    InodeTableBlock | 
+    InodeBitmapBlock | 
+    BlockBitmapBlock;
+
+set FileDirectoryBlock(int) : 
+    DirectoryBlock | 
+    FileBlock;
+
+set SuperBlock(int);
+
+set GroupBlock(int);
+
+set FileBlock(int);
+
+set DirectoryBlock(int);
+
+set InodeTableBlock(int);
+
+set InodeBitmapBlock(int);
+
+set BlockBitmapBlock(int);
+
+set DirectoryEntry(DirectoryEntry);
+
+// relations xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
+
+inodeof: DirectoryEntry -> UsedInode (many->1);
+
+contents: UsedInode -> FileDirectoryBlock (1->many);
+
+inodestatus: Inode -> int (many->1);
+
+blockstatus: Block -> int (many->1);
+
+referencecount: Inode -> int (many->1);
+
+filesize: Inode -> int (many->1);

diff --git a/Repair/RepairCompiler/MCC/specs/oldfilesystem/test2.struct b/Repair/RepairCompiler/MCC/specs/oldfilesystem/test2.struct
new file mode 100755 (executable)
index 0000000..bf765ef
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/specs/oldfilesystem/test2.struct
@@ -0,0 +1,67 @@
+// sEXT2 - Simple File System Example
+// Type Definition Language File
+
+// structures are assumed to be aligned to double-word
+// boundaries. fields are tightly packed, so reserved bits 
+// can be used to add neccesary padding
+
+Disk *d; 
+
+structure Block {
+     reserved byte[d.s.blocksize];
+}
+
+structure Disk {
+     Block  b[d.s.NumberofBlocks];
+     label b[literal(0)]: Superblock s;
+     label b[literal(1)]: Groupblock g;
+}
+
+structure Superblock subtype of Block {
+     int FreeBlockCount;
+     int FreeInodeCount;
+     int NumberofBlocks;
+     int NumberofInodes;
+     int RootDirectoryInode;
+     int blocksize;
+}
+
+structure Groupblock subtype of Block {
+     int BlockBitmapBlock;
+     int InodeBitmapBlock;
+     int InodeTableBlock; 
+     int GroupFreeBlockCount;
+     int GroupFreeInodeCount;
+}
+
+structure InodeTable subtype of Block {
+     Inode itable[d.s.NumberofInodes];
+}
+
+structure InodeBitmap subtype of Block {
+     bit inodebitmap[d.s.NumberofInodes];
+}
+
+structure BlockBitmap subtype of Block {
+     bit blockbitmap[d.s.NumberofBlocks];
+}
+
+structure Inode {
+     int filesize;
+     int Blockptr[literal(12)];
+     int referencecount;
+}
+
+structure DirectoryBlock subtype of Block {
+     DirectoryEntry de[d.s.blocksize/literal(128)];
+}
+
+structure DirectoryEntry {
+     byte name[literal(124)];
+     int inodenumber;
+}
+
+
+
+
+

diff --git a/Repair/RepairCompiler/MCC/test.constraints b/Repair/RepairCompiler/MCC/test.constraints
deleted file mode 100755 (executable)
index a6073fd..0000000
--- a/Repair/RepairCompiler/MCC/test.constraints
+++ /dev/null
@@ -1,3 +0,0 @@
-
-[forall u in UsedInode], u.inodestatus=literal(Used);
-[],sizeof(RootDirectoryInode)=1;
\ No newline at end of file

diff --git a/Repair/RepairCompiler/MCC/test.model b/Repair/RepairCompiler/MCC/test.model
deleted file mode 100755 (executable)
index 2c4e062..0000000
--- a/Repair/RepairCompiler/MCC/test.model
+++ /dev/null
@@ -1 +0,0 @@
-[], true => literal(0) in SuperBlock;

diff --git a/Repair/RepairCompiler/MCC/test.space b/Repair/RepairCompiler/MCC/test.space
deleted file mode 100755 (executable)
index bd84734..0000000
--- a/Repair/RepairCompiler/MCC/test.space
+++ /dev/null
@@ -1,73 +0,0 @@
-// sEXT2 - Simple File System Example
-// Space Definition Language File
-
-set Block(int) : partition 
-    UsedBlock | 
-    FreeBlock;
-
-set FreeBlock(int);
-
-set Inode(int) : partition 
-    UsedInode | 
-    FreeInode;
-
-set FreeInode(int);
-
-set UsedInode(int) : partition 
-    FileInode | 
-    DirectoryInode ;
-
-set FileInode(int);
-
-set DirectoryInode(int) : RootDirectoryInode;
-
-set RootDirectoryInode(int);
-
-set UsedBlock(int) : partition 
-    SuperBlock | 
-    GroupBlock | 
-    FileDirectoryBlock | 
-    InodeTableBlock | 
-    InodeBitmapBlock | 
-    BlockBitmapBlock;
-
-set FileDirectoryBlock(int) : 
-    DirectoryBlock | 
-    FileBlock;
-
-set SuperBlock(int);
-
-set GroupBlock(int);
-
-set FileBlock(int);
-
-set DirectoryBlock(int);
-
-set InodeTableBlock(int);
-
-set InodeBitmapBlock(int);
-
-set BlockBitmapBlock(int);
-
-set DirectoryEntry(DirectoryEntry);
-
-// relations xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
-
-inodeof: DirectoryEntry -> UsedInode (many->1);
-
-contents: UsedInode -> FileDirectoryBlock (1->many);
-
-inodestatus: Inode -> token (many->1);
-
-blockstatus: Block -> token (many->1);
-
-referencecount: Inode -> int (many->1);
-
-filesize: Inode -> int (many->1);
-
-
-
-
-
-
-

diff --git a/Repair/RepairCompiler/MCC/test.struct b/Repair/RepairCompiler/MCC/test.struct
deleted file mode 100755 (executable)
index c956e8b..0000000
--- a/Repair/RepairCompiler/MCC/test.struct
+++ /dev/null
@@ -1,3 +0,0 @@
-structure Block {
-     reserved byte[d.s.blocksize];
-}
\ No newline at end of file

diff --git a/Repair/RepairCompiler/MCC/test2.constraints b/Repair/RepairCompiler/MCC/test2.constraints
deleted file mode 100755 (executable)
index bbc92e4..0000000
--- a/Repair/RepairCompiler/MCC/test2.constraints
+++ /dev/null
@@ -1,66 +0,0 @@
-// sEXT2 - Simple File System Example
-// Constraint Definition Language File
-
-// Constraints 1-4 verify that the bitmaps and references to block's match up
-// Constraints 5-6 verify that references counts and filesizes match up
-// Constraints 7-13 are singleton tests
-
-// C1
-// for all used inodes, verify that the inodestatus (built from the
-// inodebitmap is marked 'used'
-//[forall u in UsedInode], u.inodestatus=literal(true);
-
-// C2
-// for all free inodes, verify that the inodestatus (built from the 
-// inodebitmap is marked 'free'
-//[forall f in FreeInode], f.inodestatus=literal(false);
-
-// C3
-// for all used blocks, verify that the blockstatus (built from the
-// blockbitmap is marked 'used'
-//[forall u in UsedBlock], u.blockstatus=literal(true);
-
-// C4
-// for all free blocks, verify that the blockstatus (built from the
-// block bitmap is marked 'free'
-//[forall f in FreeBlock], f.blockstatus=literal(false);
-
-// C5
-// for all used inodes, verify that the reference count is equal to
-// the number of directory entries (files/links) that refer to that
-// inode
-//[forall i in UsedInode], i.referencecount=sizeof(i.~inodeof);
-
-// C6
-// for all used inodes, verify that the filesize is consistent with
-// the number of blocks used (those in i.contents)
-//[forall i in UsedInode], i.filesize <= sizeof(i.contents)*literal(8192);
-
-// C7
-// ??? for all files and directory blocks check that
-// only one inode references this block
-//[forall b in FileDirectoryBlock],sizeof(b.~contents)=literal(1);
-
-// C8
-// verify that there is one superblock
-//[],sizeof(SuperBlock)=literal(1);
-
-// C9
-// verify that there is one groupblock
-//[],sizeof(GroupBlock)=literal(1);
-
-// C10
-// verify that there is one inodetableblock
-//[],sizeof(InodeTableBlock)=literal(1);
-
-// C11
-// verify that there is one inodebitmapblock 
-[],sizeof(InodeBitmapBlock)=literal(1);
-
-// C12
-// verify that there is one blockbitmapblock
-//[],sizeof(BlockBitmapBlock)=literal(1);
-
-// C13
-// verify that there is one rootdirectoryinode
-//[],sizeof(RootDirectoryInode)=literal(1);

diff --git a/Repair/RepairCompiler/MCC/test2.model b/Repair/RepairCompiler/MCC/test2.model
deleted file mode 100755 (executable)
index 78f8a9d..0000000
--- a/Repair/RepairCompiler/MCC/test2.model
+++ /dev/null
@@ -1,96 +0,0 @@
-// 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;
-

diff --git a/Repair/RepairCompiler/MCC/test2.model.dep b/Repair/RepairCompiler/MCC/test2.model.dep
deleted file mode 100755 (executable)
index 13befd7..0000000
--- a/Repair/RepairCompiler/MCC/test2.model.dep
+++ /dev/null
@@ -1,108 +0,0 @@
-// dependency information for 
-// testabstract from sEXT2
-
-1-6: none
-
-7: delayed 14
-8: delayed 1 2 3 4 5 11
-
- 9: 3     6
-10: 3     6   14
-11: 3     6   14
-12:   4
-13:   4
-14:         9
-15:         9
-16: 3     6   14
-17: 3     6   14
-18:     5
-19:     5
-
- 9: 3 6
-10: 3 6 14
-11: 3 6 14
-12: 4
-13: 4
-14: 9
-15: 9
-16: 3 6 14
-17: 3 6 14
-18: 5
-19: 5
- 
-
-algorithm:
-
-a. if quantifiers are empty than rule has no dependencies
-b. if not ( x in Set ) or relation than dependent on everything that
-   touches the Set or Relation (also known as delayed).
-c. otherwise, if set or relation mentioned in quantifier, edge between
-   that rule and any rule who modifies that set or relation (in the 
-   inclusion constraint portion of any rule)
-
-
-// dependency information betweeen constraints and rules
-
- 1:           6           12 13 14
- 2:             7         12 13
- 3: 1 2 3 4 5          11                   18 19
- 4:               8                         18 19
- 5:           6                 14 15 16
- 6:           6     10          14       17
- 7:                 10 11
- 8: 1
- 9:   2
-10:     3
-11:       4
-12:         5
-13:           6
-
- 1:  6 12 13 14
- 2:  7 12 13
- 3:  1  2  3  4  5 11 18 19
- 4:  8 18 19
- 5:  6 14 15 16
- 6:  6 10 14 17
- 7: 10 11
- 8:  1
- 9:  2
-10:  3 
-11:  4
-12:  5
-13:  6 
-
-
-algorithm:
-
-a. if quantifier mentions a set, include all rules that touch that set
-   or its subsets/partitions
-b. if the body mentions a set or relation, add that an edge to any rule
-   that touches those sets or relations
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-

diff --git a/Repair/RepairCompiler/MCC/test2.space b/Repair/RepairCompiler/MCC/test2.space
deleted file mode 100755 (executable)
index 8b303c6..0000000
--- a/Repair/RepairCompiler/MCC/test2.space
+++ /dev/null
@@ -1,66 +0,0 @@
-// sEXT2 - Simple File System Example
-// Space Definition Language File
-
-set Block(int) :
-    UsedBlock | 
-    FreeBlock;
-
-set FreeBlock(int);
-
-set Inode(int) :
-    UsedInode | 
-    FreeInode;
-
-set FreeInode(int);
-
-set UsedInode(int) : partition 
-    FileInode | 
-    DirectoryInode ;
-
-set FileInode(int);
-
-set DirectoryInode(int) : RootDirectoryInode;
-
-set RootDirectoryInode(int);
-
-set UsedBlock(int) :
-    SuperBlock | 
-    GroupBlock | 
-    FileDirectoryBlock | 
-    InodeTableBlock | 
-    InodeBitmapBlock | 
-    BlockBitmapBlock;
-
-set FileDirectoryBlock(int) : 
-    DirectoryBlock | 
-    FileBlock;
-
-set SuperBlock(int);
-
-set GroupBlock(int);
-
-set FileBlock(int);
-
-set DirectoryBlock(int);
-
-set InodeTableBlock(int);
-
-set InodeBitmapBlock(int);
-
-set BlockBitmapBlock(int);
-
-set DirectoryEntry(DirectoryEntry);
-
-// relations xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
-
-inodeof: DirectoryEntry -> UsedInode (many->1);
-
-contents: UsedInode -> FileDirectoryBlock (1->many);
-
-inodestatus: Inode -> int (many->1);
-
-blockstatus: Block -> int (many->1);
-
-referencecount: Inode -> int (many->1);
-
-filesize: Inode -> int (many->1);

diff --git a/Repair/RepairCompiler/MCC/test2.struct b/Repair/RepairCompiler/MCC/test2.struct
deleted file mode 100755 (executable)
index bf765ef..0000000
--- a/Repair/RepairCompiler/MCC/test2.struct
+++ /dev/null
@@ -1,67 +0,0 @@
-// sEXT2 - Simple File System Example
-// Type Definition Language File
-
-// structures are assumed to be aligned to double-word
-// boundaries. fields are tightly packed, so reserved bits 
-// can be used to add neccesary padding
-
-Disk *d; 
-
-structure Block {
-     reserved byte[d.s.blocksize];
-}
-
-structure Disk {
-     Block  b[d.s.NumberofBlocks];
-     label b[literal(0)]: Superblock s;
-     label b[literal(1)]: Groupblock g;
-}
-
-structure Superblock subtype of Block {
-     int FreeBlockCount;
-     int FreeInodeCount;
-     int NumberofBlocks;
-     int NumberofInodes;
-     int RootDirectoryInode;
-     int blocksize;
-}
-
-structure Groupblock subtype of Block {
-     int BlockBitmapBlock;
-     int InodeBitmapBlock;
-     int InodeTableBlock; 
-     int GroupFreeBlockCount;
-     int GroupFreeInodeCount;
-}
-
-structure InodeTable subtype of Block {
-     Inode itable[d.s.NumberofInodes];
-}
-
-structure InodeBitmap subtype of Block {
-     bit inodebitmap[d.s.NumberofInodes];
-}
-
-structure BlockBitmap subtype of Block {
-     bit blockbitmap[d.s.NumberofBlocks];
-}
-
-structure Inode {
-     int filesize;
-     int Blockptr[literal(12)];
-     int referencecount;
-}
-
-structure DirectoryBlock subtype of Block {
-     DirectoryEntry de[d.s.blocksize/literal(128)];
-}
-
-structure DirectoryEntry {
-     byte name[literal(124)];
-     int inodenumber;
-}
-
-
-
-
-