Repair/RepairInterpreter/testabstract

   1 [], true => literal(0) in SuperBlock
   2 [], true => literal(1) in GroupBlock
   3 [], d.g.InodeTableBlock < d.s.NumberofBlocks => d.g.InodeTableBlock in InodeTableBlock
   4 [], d.g.InodeBitmapBlock < d.s.NumberofBlocks => d.g.InodeBitmapBlock in InodeBitmapBlock
   5 [], d.g.BlockBitmapBlock < d.s.NumberofBlocks => d.g.BlockBitmapBlock in BlockBitmapBlock
   6 [], d.s.RootDirectoryInode < d.s.NumberofInodes => d.s.RootDirectoryInode in RootDirectoryInode
   7 delay [for j=literal(0) to d.s.NumberofInodes-literal(1)], !(j in UsedInode) => j in FreeInode
   8 delay [for j=literal(0) to d.s.NumberofBlocks-literal(1)], !(j in UsedBlock) => j in FreeBlock
   9 [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
  10 [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
  11 [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 FileDirectoryBlock
  12 [for j=literal(0) to d.s.NumberofInodes-literal(1), forall ibb in InodeBitmapBlock], cast(InodeBitmap,d.b[ibb]).inodebitmap[j]=literal(false) => <j,literal(Free)> in inodestatus
  13 [for j=literal(0) to d.s.NumberofInodes-literal(1), forall ibb in InodeBitmapBlock], cast(InodeBitmap,d.b[ibb]).inodebitmap[j]=literal(true) => <j,literal(Used)> in inodestatus
  14 [forall de in DirectoryEntry], de.inodenumber<d.s.NumberofInodes and !de.inodenumber = literal(0) => de.inodenumber in FileInode
  15 [forall de in DirectoryEntry], de.inodenumber<d.s.NumberofInodes => <de, de.inodenumber> in inodeof
  16 [forall j in UsedInode, forall itb in InodeTableBlock], true => <j,cast(InodeTable,d.b[itb]).itable[j].referencecount> in referencecount
  17 [forall j in UsedInode, forall itb in InodeTableBlock], true => <j,cast(InodeTable,d.b[itb]).itable[j].filesize> in filesize
  18 [for j=literal(0) to d.s.NumberofBlocks-literal(1), forall bbb in BlockBitmapBlock], cast(BlockBitmap,d.b[bbb]).blockbitmap[j]=literal(false) => <j,literal(Free)> in blockstatus
  19 [for j=literal(0) to d.s.NumberofBlocks-literal(1), forall bbb in BlockBitmapBlock], cast(BlockBitmap,d.b[bbb]).blockbitmap[j]=literal(true) => <j,literal(Used)> in blockstatus