Ability to write out each SMV file, currently deactivated (must manually...

Ability to write out each SMV file, currently deactivated (must manually change this - only do this if you want to manually run NuSMV), also now writes out (can disable) the rule that created each NuSMV NEXT case

.gitignore

@@ -13,3 +13,4 @@ rbacinstancefile*
 MohawkCUIPreviousCommand.txt
 data/testcases/mohawk.jar
 data/
+smvinstancefile*

src/mohawk/output/WriteNuSMV.java

@@ -55,6 +55,8 @@ public class WriteNuSMV {
      */
     public Level logLevel = Level.WARNING;
 
+    public boolean includeRuleComment = true;
+
     /*
      * The constructor should initialize the target file and the filename for the template.
      */
@@ -71,6 +73,70 @@ public class WriteNuSMV {
         }
     }
 
+    public String getTrue() {
+        return ((olderVersion) ? "1" : "TRUE");
+    }
+
+    public String getFalse() {
+        return ((olderVersion) ? "0" : "FALSE");
+    }
+
+    public Vector<CAEntry> getMatchingCA(String strRole) {
+
+        /*
+         * Vector<CAEntry> vFullCA = rbac.getCA(); Vector<CAEntry> vFilCA = new Vector<CAEntry>();
+         * 
+         * for(int i=0; i<vFullCA.size(); i++) { CAEntry tmpCA = vFullCA.get(i); if(tmpCA.strRole.equals(strRole))
+         * vFilCA.add(tmpCA); }
+         */
+
+        Map<String, Vector<CAEntry>> mCA = rbac.getCA();
+
+        if (mCA != null)
+            return rbac.getCA().get(strRole);
+        else
+            return null;
+
+        // return rbac.getCA().get(strRole);
+        // return vFilCA;
+
+    }
+
+    public Vector<CREntry> getMatchingCR(String strRole) {
+
+        /*
+         * Vector<CREntry> vFullCR = rbac.getCR(); Vector<CREntry> vFilCR = new Vector<CREntry>();
+         * 
+         * for(int i=0; i<vFullCR.size(); i++) { CREntry tmpCR = vFullCR.get(i); if(tmpCR.strRole.equals(strRole))
+         * vFilCR.add(tmpCR); }
+         * 
+         * return vFilCR;
+         */
+        return rbac.getCR().get(strRole);
+    }
+
+    /* Load template contents from textfile */
+    public String getTemplateStr(String filename) throws IOException {
+
+        InputStream is = getClass().getResourceAsStream(filename);
+        BufferedReader br = new BufferedReader(new InputStreamReader(is));
+        String strtemplate = null;
+        String line;
+        while ((line = br.readLine()) != null) {
+            if (strtemplate == null)
+                strtemplate = line;
+            else
+                strtemplate = strtemplate + "\n" + line;
+        }
+        // System.out.println(strtemplate);
+
+        return strtemplate;
+    }
+
+    public String getNuSMVCode() {
+        return this.smvcode;
+    }
+
     public void setupUsers(ST inSmvSpec) {
 
         int noRoles = rbac.getRoles().size();
@@ -140,40 +206,6 @@ public class WriteNuSMV {
         }
     }
 
-    Vector<CAEntry> getMatchingCA(String strRole) {
-
-        /*
-         * Vector<CAEntry> vFullCA = rbac.getCA(); Vector<CAEntry> vFilCA = new Vector<CAEntry>();
-         * 
-         * for(int i=0; i<vFullCA.size(); i++) { CAEntry tmpCA = vFullCA.get(i); if(tmpCA.strRole.equals(strRole))
-         * vFilCA.add(tmpCA); }
-         */
-
-        Map<String, Vector<CAEntry>> mCA = rbac.getCA();
-
-        if (mCA != null)
-            return rbac.getCA().get(strRole);
-        else
-            return null;
-
-        // return rbac.getCA().get(strRole);
-        // return vFilCA;
-
-    }
-
-    Vector<CREntry> getMatchingCR(String strRole) {
-
-        /*
-         * Vector<CREntry> vFullCR = rbac.getCR(); Vector<CREntry> vFilCR = new Vector<CREntry>();
-         * 
-         * for(int i=0; i<vFullCR.size(); i++) { CREntry tmpCR = vFullCR.get(i); if(tmpCR.strRole.equals(strRole))
-         * vFilCR.add(tmpCR); }
-         * 
-         * return vFilCR;
-         */
-        return rbac.getCR().get(strRole);
-    }
-
     public String addCAEntry(String inUser, CAEntry inCAEntry) {
 
         Vector<String> vAdminUsers = rbac.getAdmin();
@@ -242,6 +274,10 @@ public class WriteNuSMV {
                 strTransition = strTransition + "\n" + strTTrans.render();
         }
 
+        if (includeRuleComment) {
+            strTransition = "-- CA Rule: " + inCAEntry + "\n" + strTransition;
+        }
+
         return strTransition;
     }
 
@@ -253,15 +289,15 @@ public class WriteNuSMV {
         int iDestRoleIndex = 0;
 
         try {
-
             iDestRoleIndex = rbac.getRoleIndex(crentry.getStrRole());
 
-            if (crentry.getPreCond().equalsIgnoreCase("true"))
+            if (crentry.getPreCond().equalsIgnoreCase("true")) {
                 adminRoleIndex = -1;
-            else if (crentry.getPreCond().equalsIgnoreCase("false"))
+            } else if (crentry.getPreCond().equalsIgnoreCase("false")) {
                 adminRoleIndex = -2;
-            else
+            } else {
                 adminRoleIndex = rbac.getRoleIndex(crentry.getPreCond());
+            }
         } catch (Exception e) {
             e.printStackTrace();
         }
@@ -295,15 +331,11 @@ public class WriteNuSMV {
                 strTransition = strTransition + "\n" + strTTrans.render();
         }
 
-        return strTransition;
-    }
-
-    private String getFalse() {
-        return ((olderVersion) ? "0" : "FALSE");
-    }
+        if (includeRuleComment) {
+            strTransition = "-- CR Rule: " + crentry + "\n" + strTransition;
+        }
 
-    private String getTrue() {
-        return ((olderVersion) ? "1" : "TRUE");
+        return strTransition;
     }
 
     public String setupEachUser(String inUser) {
@@ -395,24 +427,6 @@ public class WriteNuSMV {
 
     }
 
-    /* Load template contents from textfile */
-    String getTemplateStr(String filename) throws IOException {
-
-        InputStream is = getClass().getResourceAsStream(filename);
-        BufferedReader br = new BufferedReader(new InputStreamReader(is));
-        String strtemplate = null;
-        String line;
-        while ((line = br.readLine()) != null) {
-            if (strtemplate == null)
-                strtemplate = line;
-            else
-                strtemplate = strtemplate + "\n" + line;
-        }
-        // System.out.println(strtemplate);
-
-        return strtemplate;
-    }
-
     /*
      * Fill attributes in the StringTemplate
      * 
@@ -444,10 +458,6 @@ public class WriteNuSMV {
         done = true;
     }
 
-    public String getNuSMVCode() {
-        return this.smvcode;
-    }
-
     public void writeFile() throws IOException {
         if (done) {
 

src/mohawk/refine/RolesAbsRefine.java

@@ -46,6 +46,8 @@ public class RolesAbsRefine {
     private int lastpriority;
     private NuSMVMode mode;// mode
 
+    public boolean skipSMVFile = true;
+
     public RolesAbsRefine(RBACInstance inRbac) {
 
         mode = NuSMVMode.BMC;// Default mode is BMC
@@ -87,8 +89,13 @@ public class RolesAbsRefine {
     }
 
     public Boolean getResult(RBACInstance curInstance, Integer fileno) throws IOException, InterruptedException {
-        WriteNuSMV nusmv = new WriteNuSMV("rbacinstancefile" + fileno, "smvtemplate");
+        WriteNuSMV nusmv = new WriteNuSMV("logs/smvinstancefile" + fileno + ".txt", "smvtemplate");
         nusmv.fillAttributes(curInstance);
+
+        if (!skipSMVFile) {
+            nusmv.writeFile();
+        }
+
         // NuSMV bmc
         Boolean result;
         if (mode == NuSMVMode.BMC) {
@@ -209,7 +216,7 @@ public class RolesAbsRefine {
             while (refine()) {
                 WriteRBACSpec writer = new WriteRBACSpec("rbac.st");
                 try {
-                    writer.Write2File(nextinstance, "rbacinstancefile" + fileno);
+                    writer.Write2File(nextinstance, "logs/rbacinstancefile" + fileno + ".txt");
                 } catch (IOException e1) {
                     e1.printStackTrace();
                 }