// 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(Used);

// C2
// for all free inodes, verify that the inodestatus (built from the 
// inodebitmap is marked 'free'
[forall f in FreeInode], f.inodestatus=literal(Free);

// C3
// for all used blocks, verify that the blockstatus (built from the
// blockbitmap is marked 'used'
[forall u in UsedBlock], u.blockstatus=literal(Used);

// C4
// for all free blocks, verify that the blockstatus (built from the
// block bitmap is marked 'free'
[forall f in FreeBlock], f.blockstatus=literal(Free);

// 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);