User Role Timeslot next case statements done; testing required

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

@@ -63,6 +63,9 @@ public class ConvertToNuSMV extends ConvertTo {
             /* Generate a list of NuSMVRule_Role */
             ArrayList<NuSMVRule_Role> enabledRoleRules = getEnabledRoleRules(m, enabledRoleTimeslots);
 
+            /* Generate a list of NuSMVRule_Role */
+            ArrayList<NuSMVRule_Role> roleTimeslotRules = getRoleTimeslotRules(m, roleTimeslots);
+
             // ---------------------------------------------------------------------
             /* Timing */timing.startTimer(tPrefix + "_" + "ruleMappingString");
             String ruleMappingStr = ruleMapping(m);
@@ -95,6 +98,7 @@ public class ConvertToNuSMV extends ConvertTo {
             st.add("enabledRoles", enabledRoleTimeslots);
 
             st.add("enabledRoleRules", enabledRoleRules);
+            st.add("roleTimeslotRules", roleTimeslotRules);
 
             convertedStr = st.render();
             /* Timing */timing.stopTimer(tPrefix + "_" + "template");
@@ -139,6 +143,40 @@ public class ConvertToNuSMV extends ConvertTo {
         return convertedStr;
     }
 
+    private ArrayList<NuSMVRule_Role> getRoleTimeslotRules(MohawkT m, Set<RoleTimeSlot> roleTimeslots) {
+        /** Role Index --> NuSMVRule_Role{} */
+        HashMap<Integer, NuSMVRule_Role> roleMap = new HashMap<>(m.numberOfRoles());
+
+        for (RoleTimeSlot rts : roleTimeslots) {
+            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);
+        }
+
+        ArrayList<Rule> allRules = m.canAssign.getRules();
+        allRules.addAll(m.canRevoke.getRules());
+
+        for (Rule r : allRules) {
+            Integer role = m.roleHelper.indexOf(r._role);
+
+            NuSMVRule_Role tmp = roleMap.get(role);
+            if (tmp != null) {
+                tmp.addRule(m, r);
+            } else {
+                logger.fine("getEnabledRoleRules: Skipping role: " + r._role);
+            }
+        }
+
+        return new ArrayList<NuSMVRule_Role>(roleMap.values());
+    }
+
     private ArrayList<NuSMVRule_Role> getEnabledRoleRules(MohawkT m, Set<RoleTimeSlot> enabledRoles) {
         /** Role Index --> NuSMVRule_Role{} */
         HashMap<Integer, NuSMVRule_Role> roleMap = new HashMap<>(m.numberOfRoles());

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

@@ -32,7 +32,24 @@ RE : array 1..numroles of
 
 ASSIGN
 
--- enabledRules -> [{role1:[{t1:[case1, case2]}, ..., t8:[]]}, ..., {role10:[]}]
+<users:{u|<roleTimeslotRules:{r|
+<if(r.timeslots)>
+----------------------------------------------------------------------------
+----------------------------------------------------------------------------
+-- User <u>, Role <r.role> Assign/Revoke 
+<r.timeslots:{ts|
+<if(ts.cases)>
+next(U[<u>][<r.role>][<ts.timeslot>]) := case
+<ts.cases:{c|<\t>user=<u> & <c.condition> : <if(c.trueResult)>TRUE<else>FALSE<endif>}; separator="\n">
+<\t>TRUE : U[<u>][<r.role>][<ts.timeslot>];
+esac;
+<else>next(U[<u>][<r.role>][<ts.timeslot>]) := U[<u>][<r.role>][<ts.timeslot>];
+<endif>
+}; separator="\n">
+<else>-- Skipping <r.role>
+<endif>
+}; separator="\n">}; separator="\n">
+
 <enabledRoleRules:{r|
 <if(r.timeslots)>
 -------------------------------------------------------------------------------
@@ -51,13 +68,17 @@ esac;
 <endif>
 }; separator="\n">
 
-<! TODO: Figure out admin conditions
+
+<!
+-------------------------------------------------------- 
+-- TODO: Figure out admin conditions
 VAR
 -- <numUsers> Users Variable
 <users:{u|<roleTimeslots:{rt|U<u><rt.string> : boolean;}; separator="  ">}; separator="\n">
 
 -- <numRolesEnabled> RoleEnabled
 <enabledRoles:{rt|RE<rt.string> : boolean;}; separator="  ">
+------------------------------------------------------------
 !>
 
 ASSIGN