From: bdemsky <bdemsky>
Date: Mon, 10 May 2004 21:55:09 +0000 (+0000)
Subject: Improved search....Updated filesystem model.  Added -aggressivesearch option.
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=repair.git;a=commitdiff_plain;h=736802f62200c790c5df3e57bbeaba25ea54c3d4

Improved search....Updated filesystem model.  Added -aggressivesearch option.
---

diff --git a/Repair/RepairCompiler/MCC/CLI.java b/Repair/RepairCompiler/MCC/CLI.java
index f03831e..a8b2bce 100755
--- a/Repair/RepairCompiler/MCC/CLI.java
+++ b/Repair/RepairCompiler/MCC/CLI.java
@@ -11,7 +11,7 @@ import java.util.StringTokenizer;
  * files.
  *
  * @author  le01, 6.035 Staff (<tt>6.035-staff@mit.edu</tt>)
- * @version <tt>$Id: CLI.java,v 1.3 2004/04/21 21:15:48 bdemsky Exp $</tt>
+ * @version <tt>$Id: CLI.java,v 1.4 2004/05/10 21:54:40 bdemsky Exp $</tt>
  */
 public class CLI {
     /**
@@ -104,6 +104,8 @@ public class CLI {
                 debug = true;
 	    } else if (args[i].equals("-checkonly")) {
                 Compiler.REPAIR=false;
+	    } else if (args[i].equals("-aggressivesearch")) {
+                Compiler.AGGRESSIVESEARCH=true;
             } else if (args[i].equals("-verbose") || args[i].equals("-v")) {
                 context = 0;
                 verbose++;
diff --git a/Repair/RepairCompiler/MCC/Compiler.java b/Repair/RepairCompiler/MCC/Compiler.java
index c0dca65..df09791 100755
--- a/Repair/RepairCompiler/MCC/Compiler.java
+++ b/Repair/RepairCompiler/MCC/Compiler.java
@@ -19,7 +19,8 @@ import MCC.IR.*;
 public class Compiler {
     /* Set this flag to false to turn repairs off */
     public static boolean REPAIR=true;
-    
+    public static boolean AGGRESSIVESEARCH=false;
+
     public static void main(String[] args) {
         State state = null;
         boolean success = true;
diff --git a/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java b/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java
index 192e212..0e718c2 100755
--- a/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java
+++ b/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java
@@ -161,8 +161,8 @@ public class ConstraintDependence {
 
 		    Set s=providesfunction(f);
 		    if (s.size()==0) {
-			System.out.println("Error: No constraint ensures that [forall v in "+f.getSet()+"], size(v."+(f.isInverse()?"~":"")+f.getRelation()+")=1");
-			System.exit(-1);
+			System.out.println("Warning: No constraint ensures that [forall v in "+f.getSet()+"], size(v."+(f.isInverse()?"~":"")+f.getRelation()+")=1");
+			continue;
 		    }
 		    Constraint c=(Constraint)s.iterator().next(); //Take the first one
 		    requiresConstraint(conjnode,c);
@@ -180,7 +180,7 @@ public class ConstraintDependence {
 		Expr e=f.isInverse()?ri.getRightExpr():ri.getLeftExpr();
 		SetDescriptor sd=e.getSet();
 		if (sd==null)
-		    sd=f.isInverse()?ri.getRelation().getRange():ri.getRelation().getDomain();
+		    return false;
 		if (!(sd.isSubset(f.getSet())||f.getSet().isSubset(sd)))
 		    continue; /* This rule doesn't effect the function */
 		if (foundrule) /* two different rules are a problem */
@@ -261,11 +261,17 @@ public class ConstraintDependence {
 	private RelationDescriptor rd;
 	private SetDescriptor sd;
 	private boolean inverse;
+	private Expr expr;
 
-	public Function(RelationDescriptor r, SetDescriptor sd, boolean inverse) {
+	public Function(RelationDescriptor r, SetDescriptor sd, boolean inverse,Expr e) {
 	    this.inverse=inverse;
 	    this.sd=sd;
 	    this.rd=r;
+	    this.expr=e;
+	}
+
+	public Expr getExpr() {
+	    return expr;
 	}
 
 	public SetDescriptor getSet() {
diff --git a/Repair/RepairCompiler/MCC/IR/Expr.java b/Repair/RepairCompiler/MCC/IR/Expr.java
index 655004b..766ae20 100755
--- a/Repair/RepairCompiler/MCC/IR/Expr.java
+++ b/Repair/RepairCompiler/MCC/IR/Expr.java
@@ -85,4 +85,12 @@ public abstract class Expr {
     public boolean isSafe() {
 	return true;
     }
+
+    public Expr getLower() {
+	return null;
+    }
+
+    public Expr getUpper() {
+	return null;
+    }
 }
diff --git a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
index 1e5a0ce..3e44b83 100755
--- a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
+++ b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
@@ -2,6 +2,7 @@ package MCC.IR;
 import java.util.*;
 import java.io.*;
 import MCC.State;
+import MCC.Compiler;
 
 public class GraphAnalysis {
     Termination termination;
@@ -15,6 +16,37 @@ public class GraphAnalysis {
 	termination=t;
     }
 
+    private boolean safetransclosure(GraphNode gn, Set removed, Set cantremove, Set couldremove) {
+	Stack workset=new Stack();
+	HashSet closureset=new HashSet();
+	workset.push(gn);
+	while(!workset.empty()) {
+	    GraphNode gn2=(GraphNode)workset.pop();
+	    if (!closureset.contains(gn2)) {
+		closureset.add(gn2);
+		boolean goodoption=false;
+		for(Iterator edgeit=gn2.edges();edgeit.hasNext();) {
+		    GraphNode gn3=((GraphNode.Edge)edgeit.next()).getTarget();
+		    if (removed.contains(gn3))
+			continue;
+		    if (termination.abstractrepair.contains(gn3)||
+			termination.conjunctions.contains(gn3)||
+			termination.updatenodes.contains(gn3))
+			return false;
+		    if (!removed.contains(gn3)&&
+			((!couldremove.contains(gn3))||cantremove.contains(gn3)))
+			goodoption=true;
+		    workset.push(gn3);
+		}
+		if (!goodoption) {
+		    if (termination.scopenodes.contains(gn2))
+			return false;
+		}		    
+	    }
+	}
+	return true;
+    }
+
     public Set doAnalysis() {
 	HashSet cantremove=new HashSet();
 	HashSet mustremove=new HashSet();
@@ -35,6 +67,25 @@ public class GraphAnalysis {
 	    couldremove.addAll(termination.consequencenodes);
 	    couldremove.retainAll(nodes);
 
+
+	    /* Check for consequence nodes which are fine */
+
+	    for(Iterator it=termination.consequencenodes.iterator();it.hasNext();) {
+		GraphNode gn=(GraphNode) it.next();
+		if (safetransclosure(gn, mustremove,cantremove, couldremove)) {
+			    couldremove.remove(gn);
+		}
+	    }
+
+	    /* Check for update nodes which are fine */
+
+	    for(Iterator it=termination.updatenodes.iterator();it.hasNext();) {
+		GraphNode gn=(GraphNode) it.next();
+		if (safetransclosure(gn, mustremove,cantremove, cantremove)) {
+			couldremove.remove(gn);
+		}
+	    }
+
 	    /* Look for constraints which can only be satisfied one way */
 	    
 	    Vector constraints=termination.state.vConstraints;
@@ -110,6 +161,28 @@ public class GraphAnalysis {
 		}
 	    }
 	    
+	    if (Compiler.AGGRESSIVESEARCH) {
+		/* Aggressively remove compensation nodes */
+		for(Iterator scopeit=termination.scopenodes.iterator();scopeit.hasNext();) {
+		    GraphNode gn=(GraphNode)scopeit.next();
+		    HashSet tmpset=new HashSet();
+		    boolean doremove=false;
+		    for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
+			GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
+			GraphNode gn2=e.getTarget();
+			if (termination.consequencenodes.contains(gn2)) {
+			    if (((!couldremove.contains(gn2))||cantremove.contains(gn2))&&
+				!mustremove.contains(gn2)) {
+				doremove=true;
+			    } else
+				break;
+			} else tmpset.add(gn2);
+		    }
+		    if (doremove)
+			mustremove.addAll(tmpset);
+		}
+	    }
+
 	    Set cycles2=GraphNode.findcycles(cantremove);
 	    for(Iterator it=cycles2.iterator();it.hasNext();) {
 		GraphNode gn=(GraphNode)it.next();
@@ -299,7 +372,7 @@ public class GraphAnalysis {
 		continue; //recalculate
 
 	    try {
-		GraphNode.DOTVisitor.visit(new FileOutputStream("graphsearch.dot"),nodes);
+		GraphNode.DOTVisitor.visit(new FileOutputStream("graphsearch.dot"),nodes,couldremove);
 	    } catch (Exception e) {
 		e.printStackTrace();
 		System.exit(-1);
@@ -435,7 +508,7 @@ public class GraphAnalysis {
 	}
 	if (incremented==false) /* Increase length */ {
 	    combination.add(new Integer(0));
-	    System.out.println("Expanding to :"+combination.size());
+	    System.out.println("Expanding to: "+combination.size());
 	}
     }
 
diff --git a/Repair/RepairCompiler/MCC/IR/GraphNode.java b/Repair/RepairCompiler/MCC/IR/GraphNode.java
index 13500ea..d8d2649 100755
--- a/Repair/RepairCompiler/MCC/IR/GraphNode.java
+++ b/Repair/RepairCompiler/MCC/IR/GraphNode.java
@@ -204,12 +204,17 @@ public class GraphNode {
         }
 
         Collection nodes;
+	Collection special;
         
         public static void visit(java.io.OutputStream output, Collection nodes) {
+	    visit(output,nodes,null);
+	}
+
+        public static void visit(java.io.OutputStream output, Collection nodes, Collection special) {
             DOTVisitor visitor = new DOTVisitor(output);
+	    visitor.special=special;
             visitor.nodes = nodes;
             visitor.make();
-
         }
         
         private void make() {
@@ -237,6 +242,8 @@ public class GraphNode {
 		String option="";
 		if (cycleset.contains(gn))
 		    option=",style=bold";
+		if (special!=null&&special.contains(gn))
+		    option+=",shape=box";
                 output.println("\t" + gn.getLabel() + " [label=\"" + label + "\"" + gn.dotnodeparams + option+"];");
 
                 while (edges.hasNext()) {
diff --git a/Repair/RepairCompiler/MCC/IR/ImageSetExpr.java b/Repair/RepairCompiler/MCC/IR/ImageSetExpr.java
index 2a61df6..99c4d89 100755
--- a/Repair/RepairCompiler/MCC/IR/ImageSetExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/ImageSetExpr.java
@@ -7,6 +7,14 @@ public class ImageSetExpr extends SetExpr {
     VarDescriptor vd;
     RelationDescriptor rd;
     boolean inverse;
+    ImageSetExpr ise;
+    boolean isimageset=false;
+
+    public ImageSetExpr(boolean inverse, VarDescriptor vd, RelationDescriptor rd) {
+        this.vd = vd;
+        this.rd = rd;
+        this.inverse = inverse;
+    }
 
     public ImageSetExpr(VarDescriptor vd, RelationDescriptor rd) {
         this.vd = vd;
@@ -14,6 +22,20 @@ public class ImageSetExpr extends SetExpr {
         this.inverse = false;
     }
 
+    public ImageSetExpr(boolean inverse, ImageSetExpr ise, RelationDescriptor rd) {
+        this.ise = ise;
+	this.isimageset=true;
+        this.rd = rd;
+        this.inverse = inverse;
+    }
+
+    public ImageSetExpr(ImageSetExpr ise, RelationDescriptor rd) {
+	this.ise = ise;
+	this.isimageset=true;
+        this.rd = rd;
+        this.inverse = false;
+    }
+
     public Set freeVars() {
 	HashSet hs=new HashSet();
 	hs.add(vd);
@@ -21,33 +43,38 @@ public class ImageSetExpr extends SetExpr {
     }
 
     public String name() {
-	String name=vd.toString()+".";
+	String name="";
+	if (isimageset)
+	    name+=ise.name();
+	else
+	    name+=vd.toString()+".";
 	if (inverse)
 	    name+="~";
 	name+=rd.toString();
 	return name;
     }
 
-    public ImageSetExpr(boolean inverse, VarDescriptor vd, RelationDescriptor rd) {
-        this.vd = vd;
-        this.rd = rd;
-        this.inverse = inverse;
-    }
-
     public boolean equals(Map remap, Expr e) {
 	if (e==null||!(e instanceof ImageSetExpr))
 	    return false;
-	ImageSetExpr ise=(ImageSetExpr)e;
-	if (ise.inverse!=inverse)
+	ImageSetExpr ise2=(ImageSetExpr)e;
+	if (ise2.isimageset!=isimageset)
 	    return false;
-	if (ise.rd!=rd)
+	if (ise2.inverse!=inverse)
 	    return false;
-	VarDescriptor nvde=vd;
-	if (remap.containsKey(nvde))
-	    nvde=(VarDescriptor)remap.get(nvde);
-	if (nvde!=ise.vd)
+	if (ise2.rd!=rd)
 	    return false;
-	return true;
+
+	if (isimageset) {
+	    return ise.equals(remap,ise2.ise);
+	} else {
+	    VarDescriptor nvde=vd;
+	    if (remap.containsKey(nvde))
+		nvde=(VarDescriptor)remap.get(nvde);
+	    if (nvde!=ise2.vd)
+		return false;
+	    return true;
+	}
     }
 
     public boolean inverted() {
@@ -58,6 +85,10 @@ public class ImageSetExpr extends SetExpr {
         return vd;
     }
 
+    public ImageSetExpr getImageSetExpr() {
+	return ise;
+    }
+
     public RelationDescriptor getRelation() {
         return rd;
     }
@@ -67,6 +98,8 @@ public class ImageSetExpr extends SetExpr {
     }
 
     public boolean usesDescriptor(Descriptor d) {
+	if (isimageset)
+	    return d==rd||ise.usesDescriptor(d);
 	return (d==rd)||(d==vd);
     }
 
@@ -91,7 +124,7 @@ public class ImageSetExpr extends SetExpr {
     public void generate_inclusion(CodeWriter writer, VarDescriptor dest, VarDescriptor element) {
         String hash = inverse ? "_hashinv->contains(" : "_hash->contains(" ;
         writer.outputline("int " + dest.getSafeSymbol() + " = " + rd.getSafeSymbol() + hash + vd.getSafeSymbol() + ", " + element.getSafeSymbol() + ");");
-    }    
+    }
 
     public void generate_size(CodeWriter writer, VarDescriptor dest) {
         assert dest != null;
diff --git a/Repair/RepairCompiler/MCC/IR/OpExpr.java b/Repair/RepairCompiler/MCC/IR/OpExpr.java
index 89bc976..957a35b 100755
--- a/Repair/RepairCompiler/MCC/IR/OpExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/OpExpr.java
@@ -8,6 +8,34 @@ public class OpExpr extends Expr {
     Expr right;
     Opcode opcode;
 
+    public Expr getUpper() {
+	Expr lupper=left.getUpper();
+	if (lupper==null)
+	    return null;
+	if (right!=null) {
+	    Expr rupper=right.getUpper();
+	    if (rupper==null)
+		return null;
+	    OpExpr oe=new OpExpr(this.opcode,lupper,rupper);
+	    oe.td = ReservedTypeDescriptor.INT;
+	    return oe;
+	} else return lupper;
+    }
+
+    public Expr getLower() {
+	Expr llower=left.getLower();
+	if (llower==null)
+	    return null;
+	if (right!=null) {
+	    Expr rlower=right.getLower();
+	    if (rlower==null)
+		return null;
+	    OpExpr oe=new OpExpr(this.opcode,llower,rlower);
+	    oe.td = ReservedTypeDescriptor.INT;
+	    return oe;
+	} else return llower;
+    }
+
     public boolean isSafe() {
 	if (right==null)
 	    return left.isSafe();
diff --git a/Repair/RepairCompiler/MCC/IR/RelationExpr.java b/Repair/RepairCompiler/MCC/IR/RelationExpr.java
index def9576..ca55892 100755
--- a/Repair/RepairCompiler/MCC/IR/RelationExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/RelationExpr.java
@@ -13,7 +13,7 @@ public class RelationExpr extends Expr {
 	Set exprfunctions=expr.getfunctions();
 	if (exprfunctions!=null)
 	    functions.addAll(exprfunctions);
-	functions.add(new ConstraintDependence.Function(relation,expr.getSet(),inverse));
+	functions.add(new ConstraintDependence.Function(relation,expr.getSet(),inverse,this));
 	
 	return functions;
     }
diff --git a/Repair/RepairCompiler/MCC/IR/SemanticChecker.java b/Repair/RepairCompiler/MCC/IR/SemanticChecker.java
index 61dc275..c3d2c5d 100755
--- a/Repair/RepairCompiler/MCC/IR/SemanticChecker.java
+++ b/Repair/RepairCompiler/MCC/IR/SemanticChecker.java
@@ -529,7 +529,7 @@ public class SemanticChecker {
             
             /* grab var */
             VarDescriptor vd = reserveName(pn.getChild("var"));
-
+	    
             if (vd == null) {
                 return null;
             }
@@ -542,10 +542,11 @@ public class SemanticChecker {
             Expr lower = parse_expr(pn.getChild("lower").getChild("expr"));
             Expr upper = parse_expr(pn.getChild("upper").getChild("expr"));
 
+
             if ((lower == null) || (upper == null)) {
                 return null;
             }
-
+	    vd.setBounds(lower,upper);
             fq.setBounds(lower, upper);
 
             return fq;
diff --git a/Repair/RepairCompiler/MCC/IR/VarDescriptor.java b/Repair/RepairCompiler/MCC/IR/VarDescriptor.java
index ef31f2b..c930360 100755
--- a/Repair/RepairCompiler/MCC/IR/VarDescriptor.java
+++ b/Repair/RepairCompiler/MCC/IR/VarDescriptor.java
@@ -9,6 +9,22 @@ public class VarDescriptor extends Descriptor {
 
     SetDescriptor sd=null;
 
+    Expr lower=null;
+    Expr upper=null;
+
+    public void setBounds(Expr l,Expr u) {
+	lower=l;
+	upper=u;
+    }
+
+    public Expr getLower() {
+	return lower;
+    }
+
+    public Expr getUpper() {
+	return upper;
+    }
+
     public SetDescriptor getSet() {
 	return sd;
     }
diff --git a/Repair/RepairCompiler/MCC/IR/VarExpr.java b/Repair/RepairCompiler/MCC/IR/VarExpr.java
index ddc0e8e..2e59733 100755
--- a/Repair/RepairCompiler/MCC/IR/VarExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/VarExpr.java
@@ -17,6 +17,14 @@ public class VarExpr extends Expr {
 	return hs;
     }
 
+    public Expr getLower() {
+	return vd.getLower();
+    }
+
+    public Expr getUpper() {
+	return vd.getUpper();
+    }
+
     public SetDescriptor getSet() {
 	return vd.getSet();
     }
diff --git a/Repair/RepairCompiler/MCC/specs/filesystem/test3.constraints b/Repair/RepairCompiler/MCC/specs/filesystem/test3.constraints
index 42b53d9..0b4dc23 100755
--- a/Repair/RepairCompiler/MCC/specs/filesystem/test3.constraints
+++ b/Repair/RepairCompiler/MCC/specs/filesystem/test3.constraints
@@ -23,7 +23,7 @@
 // C4
 // for all free blocks, verify that the blockstatus (built from the
 // block bitmap is marked 'free'
-[forall f in FreeBlock], f.blockstatus=false;
+//[forall f in FreeBlock], f.blockstatus=false;
 
 // C5
 // for all used inodes, verify that the reference count is equal to
@@ -34,12 +34,12 @@
 // 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);
+//[forall i in UsedInode], i.filesize <= sizeof(i.contents)*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);
+//[forall b in FileDirectoryBlock],sizeof(b.~contents)=1;
 
 // C8
 // verify that there is one superblock
@@ -51,11 +51,11 @@
 
 // C10
 // verify that there is one inodetableblock
-/*[],sizeof(InodeTableBlock)=1;*/
+[],sizeof(InodeTableBlock)=1;
 
 // C11
 // verify that there is one inodebitmapblock 
-/*[],sizeof(InodeBitmapBlock)=1;*/
+[],sizeof(InodeBitmapBlock)=1;
 
 // C12
 // verify that there is one blockbitmapblock
@@ -63,4 +63,4 @@
 
 // C13
 // verify that there is one rootdirectoryinode
-/*[],sizeof(RootDirectoryInode)=1;*/
+//[],sizeof(RootDirectoryInode)=1;
diff --git a/Repair/RepairCompiler/MCC/specs/filesystem/test3.model b/Repair/RepairCompiler/MCC/specs/filesystem/test3.model
index 3a86486..30e64e4 100755
--- a/Repair/RepairCompiler/MCC/specs/filesystem/test3.model
+++ b/Repair/RepairCompiler/MCC/specs/filesystem/test3.model
@@ -1,40 +1,37 @@
 // sEXT2 - Simple FileSystem Example -  MODEL DEFINITION FILE
 // rule 1 - adds the block number of the superblock to the superblock set
-/*[], true => d.s in SuperBlock;*/
+[], true => d.s in SuperBlock;
 
 // rule 2 - adds the block number of the groupblock to the groupblock set
-/*[], true => d.g in GroupBlock;*/
+[], true => d.g in GroupBlock;
 
-/*[], true => cast(InodeTable,d.b[d.g.InodeTableBlock]) in InodeTableBlock;*/
+[], true => cast(InodeTable,d.b[d.g.InodeTableBlock]) in InodeTableBlock;
 
 // rule 4 - adds the inodebitmapblock block number to the inodebitmapblock set
-/*[], true => cast(InodeBitmap,d.b[d.g.InodeBitmapBlock]) in InodeBitmapBlock;*/
+[], true => cast(InodeBitmap,d.b[d.g.InodeBitmapBlock]) in InodeBitmapBlock;
 
 // rule 5 - adds the blockbitmapblock number to the blockbitmapblock set
 [], true => cast(BlockBitmap,d.b[d.g.BlockBitmapBlock]) in BlockBitmapBlock;
 
 // rule 6 - adds the rootdirectoryinode number to the set
-/*[forall itb in InodeTableBlock], true => itb.itable[d.s.RootDirectoryInode] in RootDirectoryInode;*/
+[forall itb in InodeTableBlock], true => itb.itable[d.s.RootDirectoryInode] in RootDirectoryInode;
 
-/*[forall itb in InodeTableBlock, for j=0 to d.s.NumberofInodes-1], !(itb.itable[j] in? UsedInode) => itb.itable[j] in FreeInode;*/
+//r7
+[forall itb in InodeTableBlock, for j=0 to d.s.NumberofInodes-1], !(itb.itable[j] in? UsedInode) => itb.itable[j] in FreeInode;
 
+//r8
 [for j=0 to d.s.NumberofBlocks-1], !(d.b[j] in? UsedBlock) => d.b[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, for j=0 to ((d.s.blocksize/128)-1), for k=0 to 11],  true => cast(DirectoryBlock,d.b[di.Blockptr[k]]).de[j] in DirectoryEntry;*/
+[forall di in DirectoryInode, for j=0 to ((d.s.blocksize/128)-1), for k=0 to 11],  true => cast(DirectoryBlock,d.b[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;
-
+[forall i in UsedInode, for j=0 to 11], !(i.Blockptr[j]=0) => <i,d.b[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
@@ -45,36 +42,31 @@
 // 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
+
+[forall i in UsedInode, for j=0 to 11], !(i.Blockptr[j]=0) => d.b[i.Blockptr[j]] in FileBlock;
 
 // rule 13
 // same as rule 12/19, but instead with used inodes.
 
-/*[for j=0 to d.s.NumberofInodes-1, forall itb in InodeTableBlock, forall ibb in InodeBitmapBlock], true => <itb.itable[j], ibb.inodebitmap[j]> in inodestatus;*/
+[for j=0 to d.s.NumberofInodes-1, forall itb in InodeTableBlock, forall ibb in InodeBitmapBlock], true => <itb.itable[j], 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;
+[forall de in DirectoryEntry,forall itb in InodeTableBlock], !(de.inodenumber = 0) => itb.itable[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;
+[forall de in DirectoryEntry,forall itb in InodeTableBlock], !(de.inodenumber = 0 ) => <de, itb.itable[de.inodenumber]> in inodeof;
 
 // rule 16
 // populating the referencecount relation with the referencecount 
 // values for every usedinode
-/*[forall j in UsedInode], true => <j,j.referencecount> in referencecount;*/
+[forall j in UsedInode], true => <j,j.referencecount> in referencecount;
 
 // rule 17 - populate the filesize relation with the sizes inodes' files
-/*[forall j in UsedInode], true => <j,j.filesize> in filesize;*/
+[forall j in UsedInode], true => <j,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