intermediate commit

src/mohawk/converter/OptionString.java

 package mohawk.converter;
 
 public enum OptionString {
+	/** Outputs the authors who have contributed code to this project. Does not allow any other actions to occur. */
     AUTHORS("authors"),
     BULK("bulk"),
+    /** Outputs whether NuSMV could be found. Does not allow any other actions to occur. */
     CHECKNUSMV("checknusmv"),
+    /** Outputs the help menu. Does not allow any other actions to occur. */
     HELP("help"),
     LINESTR("linstr"),
     LOGLEVEL("loglevel"),
@@ -20,9 +23,13 @@ public enum OptionString {
     TO_ASAPTIME_NSA("to_asaptime_nsa"),
     TO_ASAPTIME_SA("to_asaptime_sa"),
     TO_MOHAWK("to_mohawk"),
+    /** Takes in a potentially messy Mohawk+T policy and outputs a well nice formatted Mohawk+T policy. */
     TO_MOHAWK_T("to_mohawk_t"),
+    /** Converts a Mohawk+T policy to a NuSMV/NuXMV model. */
+    TO_NUSMV("to_nusmv"),
     TO_TROLE("to_trole"),
     TO_TRULE("to_trule"),
+    /** Outputs the current version of this code repository. Does not allow any other actions to occur.*/
     VERSION("version");
 
     private String _str;

src/mohawk/converter/to/nusmv/ConvertToNuSMV.java

 package mohawk.converter.to.nusmv;
 
 import java.io.File;
-import java.io.PrintWriter;
-import java.io.StringWriter;
-import java.nio.file.Files;
 import java.util.logging.Logger;
 
-import org.stringtemplate.v4.ST;
-
 import mohawk.converter.to.ConvertTo;
 import mohawk.global.pieces.MohawkT;
 import mohawk.global.timing.MohawkTiming;
 
 public class ConvertToNuSMV extends ConvertTo {
-	public static final Logger logger = Logger.getLogger("mohawk");
+    public static final Logger logger = Logger.getLogger("mohawk");
+    /** Change this number to change from Reduction 2 to Reduction 3. */
+    public static final Integer reduction = 3;
+    public boolean shortRolenames = false;
 
-	public ConvertToNuSMV(MohawkTiming timing) {
-		super(timing);
-		tPrefix = "ConvertToNuSMV";
-	}
+    public ConvertToNuSMV(MohawkTiming timing) {
+        super(timing);
+        tPrefix = "ConvertToNuSMV";
+    }
 
-	@Override
+    @Override
     public String convert(MohawkT m, File file, Boolean writeToFile) {
-        try {
-        	// Generate the Converted String
-            /* Timing */timing.startTimer(tPrefix + "_" + "template");
-            String template = ConvertTo.readFile(this.getClass().getResource("ASAPTimeNSATemplate.st"));
-            ST st = new ST(template);
-            /*
-            st.add("numRoles", roleHelper.numberOfRoles()); 
-            st.add("numTimeslots", timeIntervalHelper.sizeReduced());
-            st.add("goalRole", query.goalRole);
-            st.add("goalTimeslot", query.goalTimeslot);
-            st.add("rules_nsa", rules);
-             */
-            convertedStr = st.render();
-            /* Timing */timing.stopTimer(tPrefix + "_" + "template");
-
-            // Write the converted string out to "file + getFileExtenstion()"
-            if (writeToFile) {
-                /* Timing */timing.startTimer(tPrefix + "_" + "Files.write");
-                File convertedFile = new File(file.getAbsolutePath() + getFileExtenstion());
-
-                if (!convertedFile.exists()) {
-                    convertedFile.createNewFile();
-                }
-                Files.write(convertedFile.toPath(), convertedStr.getBytes());
-                /* Timing */timing.stopTimer(tPrefix + "_" + "Files.write");
-            }
-            lastError = null;
-        } catch (Exception e) {
-            StringWriter errors = new StringWriter();
-            e.printStackTrace(new PrintWriter(errors));
-            logger.fine(errors.toString());
-
-            logger.warning("[ERROR] Unable to convert to Ranise: " + e.getMessage());
-            lastError = "Error ConvertToRanise.convert.Exception #1";
-        }
+        logger.warning("[ERROR] Pick a specific Reduction to NuSMV");
+        lastError = "Pick a specific Reduction to NuSMV";
 
         return convertedStr;
-	}
+    }
 }

src/mohawk/converter/to/nusmv/ConvertToNuSMVReduction2.java

+package mohawk.converter.to.nusmv;
+
+import java.io.*;
+import java.nio.file.Files;
+import java.util.logging.Logger;
+
+import org.stringtemplate.v4.ST;
+
+import mohawk.converter.to.ConvertTo;
+import mohawk.global.helper.RoleHelper;
+import mohawk.global.helper.TimeIntervalHelper;
+import mohawk.global.pieces.MohawkT;
+import mohawk.global.pieces.Query;
+import mohawk.global.timing.MohawkTiming;
+
+public class ConvertToNuSMVReduction2 extends ConvertToNuSMV {
+    public static final Logger logger = Logger.getLogger("mohawk");
+
+    public ConvertToNuSMVReduction2(MohawkTiming timing) {
+        super(timing);
+        tPrefix = "ConvertToNuSMV";
+    }
+
+    @Override
+    public String convert(MohawkT m, File file, Boolean writeToFile) {
+        try {
+            // Deep Copy Helpers
+            /* Timing */timing.startTimer(tPrefix + "_" + "deepcopy");
+            RoleHelper roleHelper = new RoleHelper(m.roleHelper);
+            TimeIntervalHelper timeIntervalHelper = new TimeIntervalHelper(m.timeIntervalHelper);
+            Query workableQuery = new Query(m.query);
+            /* Timing */timing.stopTimer(tPrefix + "_" + "deepcopy");
+
+            /* Timing */timing.startTimer(tPrefix + "_" + "sortRolesReduceTimeslots");
+            // Reduce Roles to Integers
+            roleHelper.allowZeroRole = false;// roles start from 1 NOT 0!
+            roleHelper.setupSortedRoles();
+            // Reduce TimeIntervals to Timeslots
+            timeIntervalHelper.allowZeroTimeslot = false;// time-slots start from t1 NOT t0!
+            // Reduction (2)
+            timeIntervalHelper.reduceToTimeslots();
+            /* Timing */timing.stopTimer(tPrefix + "_" + "sortRolesReduceTimeslots");
+
+            // Generate the Converted String
+            /* Timing */timing.startTimer(tPrefix + "_" + "template");
+            String template = ConvertTo.readFile(this.getClass().getResource("nusmvTemplate.st"));
+            ST st = new ST(template);
+            /*
+            st.add("numRoles", roleHelper.numberOfRoles()); 
+            st.add("numTimeslots", timeIntervalHelper.sizeReduced());
+            st.add("goalRole", query.goalRole);
+            st.add("goalTimeslot", query.goalTimeslot);
+            st.add("rules_nsa", rules);
+             */
+            convertedStr = st.render();
+            /* Timing */timing.stopTimer(tPrefix + "_" + "template");
+
+            // Write the converted string out to "file + getFileExtenstion()"
+            if (writeToFile) {
+                /* Timing */timing.startTimer(tPrefix + "_" + "Files.write");
+                File convertedFile = new File(file.getAbsolutePath() + getFileExtenstion());
+
+                if (!convertedFile.exists()) {
+                    convertedFile.createNewFile();
+                }
+                Files.write(convertedFile.toPath(), convertedStr.getBytes());
+                /* Timing */timing.stopTimer(tPrefix + "_" + "Files.write");
+            }
+            lastError = null;
+        } catch (Exception e) {
+            StringWriter errors = new StringWriter();
+            e.printStackTrace(new PrintWriter(errors));
+            logger.fine(errors.toString());
+
+            logger.warning("[ERROR] Unable to convert to Ranise: " + e.getMessage());
+            lastError = "Error ConvertToRanise.convert.Exception #1";
+        }
+
+        return convertedStr;
+    }
+}

src/mohawk/converter/to/nusmv/ConvertToNuSMVReduction3.java

+package mohawk.converter.to.nusmv;
+
+import java.io.File;
+import java.io.PrintWriter;
+import java.io.StringWriter;
+import java.nio.file.Files;
+import java.util.logging.Logger;
+
+import org.stringtemplate.v4.ST;
+
+import mohawk.converter.to.ConvertTo;
+import mohawk.global.pieces.MohawkT;
+import mohawk.global.timing.MohawkTiming;
+
+public class ConvertToNuSMVReduction3 extends ConvertToNuSMV {
+	public static final Logger logger = Logger.getLogger("mohawk");
+
+	public ConvertToNuSMVReduction3(MohawkTiming timing) {
+		super(timing);
+		tPrefix = "ConvertToNuSMV";
+	}
+
+	@Override
+    public String convert(MohawkT m, File file, Boolean writeToFile) {
+        try {
+        	// Generate the Converted String
+            /* Timing */timing.startTimer(tPrefix + "_" + "template");
+            String template = ConvertTo.readFile(this.getClass().getResource("ASAPTimeNSATemplate.st"));
+            ST st = new ST(template);
+            /*
+            st.add("numRoles", roleHelper.numberOfRoles()); 
+            st.add("numTimeslots", timeIntervalHelper.sizeReduced());
+            st.add("goalRole", query.goalRole);
+            st.add("goalTimeslot", query.goalTimeslot);
+            st.add("rules_nsa", rules);
+             */
+            convertedStr = st.render();
+            /* Timing */timing.stopTimer(tPrefix + "_" + "template");
+
+            // Write the converted string out to "file + getFileExtenstion()"
+            if (writeToFile) {
+                /* Timing */timing.startTimer(tPrefix + "_" + "Files.write");
+                File convertedFile = new File(file.getAbsolutePath() + getFileExtenstion());
+
+                if (!convertedFile.exists()) {
+                    convertedFile.createNewFile();
+                }
+                Files.write(convertedFile.toPath(), convertedStr.getBytes());
+                /* Timing */timing.stopTimer(tPrefix + "_" + "Files.write");
+            }
+            lastError = null;
+        } catch (Exception e) {
+            StringWriter errors = new StringWriter();
+            e.printStackTrace(new PrintWriter(errors));
+            logger.fine(errors.toString());
+
+            logger.warning("[ERROR] Unable to convert to Ranise: " + e.getMessage());
+            lastError = "Error ConvertToRanise.convert.Exception #1";
+        }
+
+        return convertedStr;
+	}
+}

src/mohawk/converter/to/nusmv/nusmvTemplate.st

-<! Roles role0 role1 role2 role3; !>
-Roles <roles:{r|<r.Name>}; separator=" "> <adminrole>;
+MODULE main
 
-<! Users user0 user1 user2 user3 user4; !>
-Users <users; separator=" ">;
+DEFINE
+numroles := 4;
+numadminroles := 3;  -- Might be used later as a optimization
+numusers := numroles + 1;
+numtimeslots := 4;
 
-<! UA <user4,Admin>; !>
-UA \<<adminuser>,<adminrole>>;
+VAR
+RoleEnabled : array 1..numroles of 
+              array 1..numtimeslots of boolean;
 
-<! CR <Admin,role0> <Admin,role2>; !>
-CR <canrevoke:{cr|\<<adminrole>,<cr.role>>}; separator="\n\t">;
+rule : {CA01, CA02, CA03, ..., CR01, CR02, ..., CE01, ..., CD01, ...};
+user : 1 .. numusers;
+admin: 1 .. numusers;
 
-<! CA <role3,role2,role0> <role3,role2&role1,role0> <role3,role2&role0,role1> <role3,TRUE,role1> <role3,role0,role1>; !>
-CA <canassign:{ca|\<<adminrole>,<if(ca.precondition)><ca.precondition; separator="&"><else>TRUE<endif>,<ca.role>>}; separator="\n\t">;
+-- Users Variable
+U01R01T01 : boolean;
+-- Continue Above...
 
-<! ADMIN user4; !>
-ADMIN <adminuser>;
+-- RoleEnabled
+RE01T01 : boolean
+-- Continue Above...
 
-<! SPEC user0 role1; !>
-SPEC <specuser> <specrole>;
+ASSIGN
+-- Disabling User Role Assignments
+init(U01R01T01) := FALSE;
+-- Continue Above...
+
+-- Disabling Roles
+init(RE01T01) := FALSE;
+-- Continue Above...
\ No newline at end of file