Role and Time-Interval mapping

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

@@ -9,7 +9,6 @@ import org.stringtemplate.v4.ST;
 
 import mohawk.converter.to.ConvertTo;
 import mohawk.global.helper.RoleHelper;
-import mohawk.global.helper.TimeIntervalHelper;
 import mohawk.global.pieces.*;
 import mohawk.global.timing.MohawkTiming;
 
@@ -29,21 +28,14 @@ public class ConvertToNuSMV extends ConvertTo {
     @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();
+            m.roleHelper.allowZeroRole = false;// roles start from 1 NOT 0!
+            m.roleHelper.setupSortedRoles();
             // Reduce TimeIntervals to Timeslots
-            timeIntervalHelper.allowZeroTimeslot = false;// time-slots start from t1 NOT t0!
+            m.timeIntervalHelper.allowZeroTimeslot = false;// time-slots start from t1 NOT t0!
             // Reduction (2)
-            timeIntervalHelper.reduceToTimeslots();
+            m.timeIntervalHelper.reduceToTimeslots();
             /* Timing */timing.stopTimer(tPrefix + "_" + "sortRolesReduceTimeslots");
 
             Set<Role> adminRoles = RoleHelper.getAdministratorRoles(m.getAllRules(), false);
@@ -54,33 +46,37 @@ public class ConvertToNuSMV extends ConvertTo {
             Integer cdRuleCount = m.canDisable.numberOfRules();
 
             /* Generate a list of users (roles + 1) to loop through */
-            ArrayList<Integer> users = new ArrayList<>(roleHelper.numberOfRoles() + 1);
-            for (int i = 1; i <= roleHelper.numberOfRoles() + 1; i++) {
+            ArrayList<Integer> users = new ArrayList<>(m.roleHelper.numberOfRoles() + 1);
+            for (int i = 1; i <= m.roleHelper.numberOfRoles() + 1; i++) {
                 users.add(i);
             }
 
             Set<RoleTimeSlot> roleTimeslots = new HashSet<>();
 
             for (Rule r : m.canAssign.getRules()) {
-                roleTimeslots.addAll(RoleTimeSlot.grabAll(r, timeIntervalHelper, roleHelper));
+                roleTimeslots.addAll(RoleTimeSlot.grabAll(r, m.timeIntervalHelper, m.roleHelper));
             }
 
-            /* Timing */timing.startTimer(tPrefix + "_" + "mappingString");
-            String mappingStr = ruleMapping(m);
-            /* Timing */timing.stopTimer(tPrefix + "_" + "mappingString");
+            /* Timing */timing.startTimer(tPrefix + "_" + "ruleMappingString");
+            String ruleMappingStr = ruleMapping(m);
+            /* Timing */timing.stopTimer(tPrefix + "_" + "ruleMappingString");
+
+            /* Timing */timing.startTimer(tPrefix + "_" + "roleMappingString");
+            String roleMappingStr = roleTimeslotMapping(m);
+            /* Timing */timing.stopTimer(tPrefix + "_" + "roleMappingString");
 
             // 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("numUsers", roleHelper.numberOfRoles() + 1);
-            st.add("numRoles", roleHelper.numberOfRoles());
+            st.add("numUsers", m.roleHelper.numberOfRoles() + 1);
+            st.add("numRoles", m.roleHelper.numberOfRoles());
             st.add("numAdminRoles", adminRoles.size());
-            st.add("numTimeSlots", timeIntervalHelper.sizeReduced());
+            st.add("numTimeSlots", m.timeIntervalHelper.sizeReduced());
 
-            st.add("queryStr", workableQuery.getString());
-            st.add("goalRoles", RoleTimeSlot.grabAll(workableQuery._roles, workableQuery._timeslot, timeIntervalHelper,
-                    roleHelper));
+            st.add("queryStr", m.query.getString());
+            st.add("goalRoles", RoleTimeSlot.grabAll(m.query._roles, m.query._timeslot, m.timeIntervalHelper,
+                    m.roleHelper));
 
             st.add("caruleslist", stringList("CA", caRuleCount));
             st.add("crruleslist", stringList("CR", crRuleCount));
@@ -103,13 +99,21 @@ public class ConvertToNuSMV extends ConvertTo {
                 }
                 Files.write(convertedFile.toPath(), convertedStr.getBytes());
 
-                // Mapping file
+                // Rule Mapping file
                 convertedFile = new File(file.getAbsolutePath() + getFileExtenstion() + ".rulemapping");
 
                 if (!convertedFile.exists()) {
                     convertedFile.createNewFile();
                 }
-                Files.write(convertedFile.toPath(), mappingStr.getBytes());
+                Files.write(convertedFile.toPath(), ruleMappingStr.getBytes());
+
+                // Role Mapping file
+                convertedFile = new File(file.getAbsolutePath() + getFileExtenstion() + ".roletimemapping");
+
+                if (!convertedFile.exists()) {
+                    convertedFile.createNewFile();
+                }
+                Files.write(convertedFile.toPath(), roleMappingStr.getBytes());
                 /* Timing */timing.stopTimer(tPrefix + "_" + "Files.write");
             }
             lastError = null;
@@ -177,6 +181,26 @@ public class ConvertToNuSMV extends ConvertTo {
         return sb.toString();
     }
 
+    private String roleTimeslotMapping(MohawkT m) {
+        StringBuilder sb = new StringBuilder(50 * m.numberOfRules());
+        sb.append("Role Mapping\n");
+        sb.append("-----------------------------------------------------------------\n");
+
+        for (String r : m.roleHelper._hashedRoles.keySet()) {
+            sb.append(r).append(" = r").append(m.roleHelper._hashedRoles.get(r)).append("\n");
+        }
+        sb.append("-----------------------------------------------------------------\n\n\n");
+
+        sb.append("Time Interval Mapping\n");
+        sb.append("-----------------------------------------------------------------\n");
+
+        for (TimeInterval ti : m.timeIntervalHelper._reducedTimeIntervals.keySet()) {
+            sb.append(ti).append(" = t").append(m.timeIntervalHelper._reducedTimeIntervals.get(ti)).append("\n");
+        }
+
+        return sb.toString();
+    }
+
     private String stringList(String prefix, Integer count) {
         return stringList(prefix, count, ",");
     }