Skeleton for the RoleEnabled Rules Reduction

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

@@ -10,6 +10,7 @@ import org.stringtemplate.v4.ST;
 import mohawk.converter.to.ConvertTo;
 import mohawk.global.helper.RoleHelper;
 import mohawk.global.pieces.*;
+import mohawk.global.pieces.reduced.nusmv.NuSMVRule_Role;
 import mohawk.global.timing.MohawkTiming;
 
 public class ConvertToNuSMV extends ConvertTo {
@@ -51,12 +52,16 @@ public class ConvertToNuSMV extends ConvertTo {
                 users.add(i);
             }
 
-            Set<RoleTimeSlot> roleTimeslots = new HashSet<>();
+            /* Generate a list of Role/Timeslots that need to be state variables */
+            Set<RoleTimeSlot> roleTimeslots = getUserRoleTimeslots(m);
 
-            for (Rule r : m.canAssign.getRules()) {
-                roleTimeslots.addAll(RoleTimeSlot.grabAll(r, m.timeIntervalHelper, m.roleHelper));
-            }
+            /* Generate a list of Role/Timeslots that need to be state variables */
+            Set<RoleTimeSlot> enabledRoleTimeslots = getEnabledRoles(m);
+
+            /* Generate a list of NuSMVRule_Role */
+            ArrayList<NuSMVRule_Role> enabledRoleRules = getEnabledRoleRules(m, enabledRoleTimeslots);
 
+            // ---------------------------------------------------------------------
             /* Timing */timing.startTimer(tPrefix + "_" + "ruleMappingString");
             String ruleMappingStr = ruleMapping(m);
             /* Timing */timing.stopTimer(tPrefix + "_" + "ruleMappingString");
@@ -85,6 +90,9 @@ public class ConvertToNuSMV extends ConvertTo {
 
             st.add("users", users);
             st.add("roleTimeslots", roleTimeslots);
+            st.add("enabledRoles", enabledRoleTimeslots);
+
+            st.add("enabledRoleRules", enabledRoleRules);
 
             convertedStr = st.render();
             /* Timing */timing.stopTimer(tPrefix + "_" + "template");
@@ -129,6 +137,57 @@ public class ConvertToNuSMV extends ConvertTo {
         return convertedStr;
     }
 
+    private ArrayList<NuSMVRule_Role> getEnabledRoleRules(MohawkT m, Set<RoleTimeSlot> enabledRoles) {
+        HashMap<Integer, NuSMVRule_Role> roleMap = new HashMap<>(m.numberOfRoles());
+
+        for (RoleTimeSlot rts : enabledRoles) {
+            if (!roleMap.containsKey(rts._role)) {
+                roleMap.put(rts._role, new NuSMVRule_Role(rts._role));
+            }
+            NuSMVRule_Role tmp = roleMap.get(rts._role);
+            if (tmp == null) {
+                // How did this happen!!
+                throw new ArrayIndexOutOfBoundsException("Something happened that I cannot really explain!?");
+            }
+
+            tmp.addTimeslot(rts._time);
+        }
+
+        return new ArrayList<NuSMVRule_Role>(roleMap.values());
+    }
+
+    private Set<RoleTimeSlot> getEnabledRoles(MohawkT m) {
+        Set<RoleTimeSlot> enabledRoles = new HashSet<>();
+        /* TODO: limit the number of required state variables
+        // List of Assignable Roles
+        for (Rule r : m.canAssign.getRules()) {
+            roleTimeslots.addAll(RoleTimeSlot.grabAll(r, m.timeIntervalHelper, m.roleHelper));
+        }*/
+
+        for (int r = 1; r <= m.roleHelper._hashedRoles.size(); r++) {
+            for (int t = 1; t <= m.timeIntervalHelper.getNumberOfTimeSlots(); t++) {
+                enabledRoles.add(new RoleTimeSlot(r, t));
+            }
+        }
+        return enabledRoles;
+    }
+
+    private Set<RoleTimeSlot> getUserRoleTimeslots(MohawkT m) {
+        Set<RoleTimeSlot> roleTimeslots = new HashSet<>();
+        /* TODO: limit the number of required state variables
+        // List of Assignable Roles
+        for (Rule r : m.canAssign.getRules()) {
+            roleTimeslots.addAll(RoleTimeSlot.grabAll(r, m.timeIntervalHelper, m.roleHelper));
+        }*/
+
+        for (int r = 1; r <= m.roleHelper._hashedRoles.size(); r++) {
+            for (int t = 1; t <= m.timeIntervalHelper.getNumberOfTimeSlots(); t++) {
+                roleTimeslots.add(new RoleTimeSlot(r, t));
+            }
+        }
+        return roleTimeslots;
+    }
+
     private String ruleMapping(MohawkT m) {
         StringBuilder sb = new StringBuilder(50 * m.numberOfRules());
         sb.append("/*\nRule Mapping\n\n");

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

@@ -26,18 +26,36 @@ admin: 1 .. numusers;
 
 ASSIGN
 
-
+-- enabledRules -> [{role1:[{t1:[case1, case2]}, ..., t8:[]]}, ..., {role10:[]}]
+<enabledRoleRules:{r|
+<if(r.timeslots)>
+-------------------------------------------------------------------------------
+-------------------------------------------------------------------------------
+-- Role <r.role> Enable/Disable
+<r.timeslots:{ts|
+<if(ts.cases)>
+next(RER<r.role>T<ts.timeslot>) := case
+<ts.cases:{c|
+<\t><c.condition> : <if(c.trueResult)>TRUE<else>FALSE<endif>}; separator="\n">
+<\t>TRUE : RER<r.role>T<ts.timeslot>;
+esac;
+<else>next(RER<r.role>T<ts.timeslot>) := RER<r.role>T<ts.timeslot>;
+<endif>
+}; separator="\n">
+<else>-- Skipping <r.role>
+<endif>
+}; separator="\n">
 
 VAR
 -- <numUsers> Users Variable
-<users:{u|<roleTimeslots:{rt|U<u><rt.string> : boolean;}; separator="\n">}; separator="\n">
+<users:{u|<roleTimeslots:{rt|U<u><rt.string> : boolean;}; separator="  ">}; separator="\n">
 
 -- <numRolesEnabled> RoleEnabled
-<enabledRoles:{r|<r> : boolean;}; separator="\n">
+<enabledRoles:{rt|RE<rt.string> : boolean;}; separator="  ">
 
 ASSIGN
 -- Disabling User Role Assignments
-<users:{u|init(<u>):=FALSE;}; separator="\n">
+<users:{u|<roleTimeslots:{rt|init(U<u><rt.string>) := FALSE;}; separator="  ">}; separator="\n">
 
 -- Disabling Roles
-<enabledRoles:{r|init(<r>) := FALSE;}; separator="\n">
\ No newline at end of file
+<enabledRoles:{rt|init(RE<rt.string>) := FALSE;}; separator="  ">
\ No newline at end of file