--- /dev/null
+
+[forall u in UsedInode], u.inodestatus=literal(Used);
+[],sizeof(RootDirectoryInode)=1;
\ No newline at end of file
--- /dev/null
+[], true => literal(0) in SuperBlock;
--- /dev/null
+// 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);
+
+
+
+
+
+
+
--- /dev/null
+structure Block {
+ reserved byte[d.s.blocksize];
+}
\ No newline at end of file
--- /dev/null
+// 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);
--- /dev/null
+// 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;
+
--- /dev/null
+// 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);
--- /dev/null
+// 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;
+}
+
+
+
+
+
+++ /dev/null
-
-[forall u in UsedInode], u.inodestatus=literal(Used);
-[],sizeof(RootDirectoryInode)=1;
\ No newline at end of file
+++ /dev/null
-[], true => literal(0) in SuperBlock;
+++ /dev/null
-// 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);
-
-
-
-
-
-
-
+++ /dev/null
-structure Block {
- reserved byte[d.s.blocksize];
-}
\ No newline at end of file
+++ /dev/null
-// 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);
+++ /dev/null
-// 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;
-
+++ /dev/null
-// 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
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+++ /dev/null
-// 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);
+++ /dev/null
-// 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;
-}
-
-
-
-
-
projects / repair.git / commitdiff