Commit df58ae3f authored by Jonathan Shahen's avatar Jonathan Shahen

NuSMV Reduction RoleEnabled cases done

parent d4cad56f
......@@ -39,6 +39,8 @@ public class ConvertToNuSMV extends ConvertTo {
m.timeIntervalHelper.reduceToTimeslots();
/* Timing */timing.stopTimer(tPrefix + "_" + "sortRolesReduceTimeslots");
m.indexAllRules();
Set<Role> adminRoles = RoleHelper.getAdministratorRoles(m.getAllRules(), false);
Integer caRuleCount = m.canAssign.numberOfRules();
......@@ -138,6 +140,7 @@ public class ConvertToNuSMV extends ConvertTo {
}
private ArrayList<NuSMVRule_Role> getEnabledRoleRules(MohawkT m, Set<RoleTimeSlot> enabledRoles) {
/** Role Index --> NuSMVRule_Role{} */
HashMap<Integer, NuSMVRule_Role> roleMap = new HashMap<>(m.numberOfRoles());
for (RoleTimeSlot rts : enabledRoles) {
......@@ -153,6 +156,20 @@ public class ConvertToNuSMV extends ConvertTo {
tmp.addTimeslot(rts._time);
}
ArrayList<Rule> allRules = m.canEnable.getRules();
allRules.addAll(m.canDisable.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());
}
......@@ -244,6 +261,7 @@ public class ConvertToNuSMV extends ConvertTo {
StringBuilder sb = new StringBuilder(50 * m.numberOfRules());
sb.append("Role Mapping\n");
sb.append("-----------------------------------------------------------------\n");
sb.append("Input Role Name = NuSMV Role Name\n");
for (String r : m.roleHelper._hashedRoles.keySet()) {
sb.append(r).append(" = r").append(m.roleHelper._hashedRoles.get(r)).append("\n");
......@@ -252,6 +270,7 @@ public class ConvertToNuSMV extends ConvertTo {
sb.append("Time Interval Mapping\n");
sb.append("-----------------------------------------------------------------\n");
sb.append("Input Time Interval = NuSMV Time Slot\n");
for (TimeInterval ti : m.timeIntervalHelper._reducedTimeIntervals.keySet()) {
sb.append(ti).append(" = t").append(m.timeIntervalHelper._reducedTimeIntervals.get(ti)).append("\n");
......
......@@ -24,6 +24,12 @@ rule : {
user : 1 .. numusers;
admin: 1 .. numusers;
U : array 1..numusers of
array 1..numroles of
array 1..numtimeslots of boolean;
RE : array 1..numroles of
array 1..numtimeslots of boolean;
ASSIGN
-- enabledRules -> [{role1:[{t1:[case1, case2]}, ..., t8:[]]}, ..., {role10:[]}]
......@@ -34,28 +40,29 @@ ASSIGN
-- 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>;
next(RE[<r.role>][<ts.timeslot>]) := case
<ts.cases:{c|<\t><c.condition> : <if(c.trueResult)>TRUE<else>FALSE<endif>}; separator="\n">
<\t>TRUE : RE[<r.role>][<ts.timeslot>];
esac;
<else>next(RER<r.role>T<ts.timeslot>) := RER<r.role>T<ts.timeslot>;
<else>next(RE[<r.role>][<ts.timeslot>]) := RE[<r.role>][<ts.timeslot>];
<endif>
}; separator="\n">
<else>-- Skipping <r.role>
<endif>
}; separator="\n">
<! 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
-- Disabling User Role Assignments
<users:{u|<roleTimeslots:{rt|init(U<u><rt.string>) := FALSE;}; separator=" ">}; separator="\n">
<users:{u|<roleTimeslots:{rt|init(U[<u>]<rt.string>) := FALSE;}; separator=" ">}; separator="\n">
-- Disabling Roles
<enabledRoles:{rt|init(RE<rt.string>) := FALSE;}; separator=" ">
\ No newline at end of file
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment