Commit 1b4e5320 authored by Jonathan Shahen's avatar Jonathan Shahen

Adds stats to the SMV files, useful to know how many roles have no transitions...

Adds stats to the SMV files, useful to know how many roles have no transitions besides staying at FALSE; This will be used to show the possibilities of a future optimization
parent 61e4dd14
......@@ -114,6 +114,12 @@ public class SMVSpecHelper {
nusmv.fillAttributes(rbac_refined);
}
System.out.println("Number of role without rules: " + nusmv.roleWithoutRules);
System.out.println("Number of role with rules: " + nusmv.roleWithRules);
System.out.println("Ratio without / with: " + (new Float(nusmv.roleWithoutRules) / nusmv.roleWithRules) +
"; without / total: "
+ (new Float(nusmv.roleWithoutRules) / (nusmv.roleWithRules + nusmv.roleWithoutRules)));
nusmv.writeFile();
} catch (IOException e1) {
logger.severe("[ERROR] Unable to write to the SMV file: " + nusmvFile.getAbsolutePath());
......
......@@ -56,6 +56,8 @@ public class WriteNuSMV {
public Level logLevel = Level.WARNING;
public boolean includeRuleComment = true;
public Integer roleWithRules;
public Integer roleWithoutRules;
/*
* The constructor should initialize the target file and the filename for the template.
......@@ -63,6 +65,8 @@ public class WriteNuSMV {
public WriteNuSMV(String fname, String tname) {
filename = fname;
done = false;
roleWithRules = 0;
roleWithoutRules = 0;
try {
// String template = ConvertTo.readFile(this.getClass().getResource("smvtemplate.st"));
......@@ -144,9 +148,9 @@ public class WriteNuSMV {
* into the template based on the RBAC state.
*/
public void fillAttributes(RBACInstance inRbac) throws IOException {
rbac = inRbac;
// StringTemplate StrTSmvspec = new StringTemplate(strtemplate);
// StringTemplate strTrans = new StringTemplate(transtemplate);
System.out.println("Setting up user arrays");
......@@ -155,16 +159,16 @@ public class WriteNuSMV {
this.setupUA(strTCodeTemplate);
System.out.println("Setting up CA-CR rules");
this.setupUserTransitions(strTCodeTemplate);
// Setup LTLSPEC
System.out.println("Setting up SPEC");
String strUser = rbac.getSpec().get(0);
String strRole = rbac.getSpec().get(1);
setupSpec(strTCodeTemplate, strUser, strRole);
// this.setupTransactions(this.strCodeTemplate, this.strCodeTemplate);
smvcode = strTCodeTemplate.render();
done = true;
}
......@@ -239,23 +243,23 @@ public class WriteNuSMV {
public void setupUserTransitions(ST strTCodeTemplate) {
Vector<String> vUsers = rbac.getUsers();
for (int i = 0; i < vUsers.size(); i++) {
if (logLevel.intValue() <= Level.FINE.intValue()) {
System.out.println("Writing for user " + vUsers.get(i));
}
String strUser = vUsers.get(i);
String strTransitions = this.setupEachUser(strUser);
strTCodeTemplate.add("transitions", strTransitions);
}
}
public String setupEachUser(String inUser) {
Vector<String> vRoles = rbac.getRoles();
String strUserSection = null;
for (int i = 0; i < vRoles.size(); i++) {
String strRole = vRoles.get(i);
Vector<CAEntry> vCA = getMatchingCA(strRole);
......@@ -263,7 +267,7 @@ public class WriteNuSMV {
StringBuilder transitions = null;
String strTmpUser = null;
ST strTTrans = new ST(strTransTemplate, '$', '$');
if (vCA != null) {
for (int j = 0; j < vCA.size(); j++) {
String strTmpTrans = addCAEntry(inUser, vCA.get(j));
......@@ -277,7 +281,7 @@ public class WriteNuSMV {
}
}
}
if (vCR != null) {
for (int j = 0; j < vCR.size(); j++) {
String strTmpTrans = addCREntry(inUser, vCR.get(j));
......@@ -291,23 +295,27 @@ public class WriteNuSMV {
}
}
}
if (transitions != null) {
strTTrans.add("rolename", strRole);
strTTrans.add("transition", transitions);
strTTrans.add("trueWord", getTrue());
strTTrans.add("roleindex1", inUser + "[" + i + "]");
strTTrans.add("roleindex2", inUser + "[" + i + "]");
strTmpUser = strTTrans.render();
roleWithRules++;
} else {
strTmpUser = "next(" + inUser + "[" + i + "]) := " + inUser + "[" + i + "];";
strTmpUser = "-- " + strRole + "\nnext(" + inUser + "[" + i + "]) := " + inUser + "[" + i + "];";
roleWithoutRules++;
}
if (strUserSection == null)
if (strUserSection == null) {
strUserSection = strTmpUser;
else
} else {
strUserSection = strUserSection + "\n\n" + strTmpUser;
}
}
return strUserSection;
}
......@@ -455,6 +463,10 @@ public class WriteNuSMV {
strTCodeTemplate.add("user", inStrUser);
strTCodeTemplate.add("roleindex", roleindex);
strTCodeTemplate.add("falseWord", getFalse());
strTCodeTemplate.add("roleWithoutRules", roleWithoutRules);
strTCodeTemplate.add("roleWithRules", roleWithRules);
strTCodeTemplate.add("roleWithoutWithRatio", new Float(roleWithoutRules) / roleWithRules);
strTCodeTemplate.add("roleWithoutTotalRatio", new Float(roleWithoutRules) / (roleWithoutRules + roleWithRules));
}
......
-- This NuSMV specification was automatically generated by the
-- RBAC2SMV tool.
-- This NuSMV specification was automatically generated by Mohawk 2.0
-- Stats
-- Number of role without rules: $roleWithoutRules$
-- Number of role with rules: $roleWithRules$
-- Ratio without / with: $roleWithoutWithRatio$
-- Ratio without / total: $roleWithoutTotalRatio$
MODULE main
VAR
......
-- $rolename$
next($roleindex1$) :=
case
$transition; separator=";\n" $
......
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