Skip to content

GitLab

Commit 65a0b9ac authored by Jonathan Shahen's avatar Jonathan Shahen
Browse files

reordering functions for easier reading

parent fe5c1cad
Show whitespace changes
Inline Side-by-side
Showing with 105 additions and 105 deletions
src/mohawk/output/WriteNuSMV.java
View file @ 65a0b9ac
...@@ -137,6 +137,37 @@ public class WriteNuSMV { ...@@ -137,6 +137,37 @@ public class WriteNuSMV {
return this.smvcode; return this.smvcode;
} }
/*
* Fill attributes in the StringTemplate
*
* Maybe This function should be passed an object that represents the RBAC state. The parameters should be plugged
* 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");
this.setupUsers(strTCodeTemplate);
System.out.println("Setting up UA");
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;
}
public void setupUsers(ST inSmvSpec) { public void setupUsers(ST inSmvSpec) {
int noRoles = rbac.getRoles().size(); int noRoles = rbac.getRoles().size();
...@@ -206,6 +237,80 @@ public class WriteNuSMV { ...@@ -206,6 +237,80 @@ 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);
Vector<CREntry> vCR = getMatchingCR(strRole);
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));
if (transitions == null) {
transitions = new StringBuilder();
transitions = transitions.append(strTmpTrans);
} else {
transitions.append("\n");
transitions.append(strTmpTrans);
// transitions = transitions + "\n" + strTmpTrans;
}
}
}
if (vCR != null) {
for (int j = 0; j < vCR.size(); j++) {
String strTmpTrans = addCREntry(inUser, vCR.get(j));
if (transitions == null) {
transitions = new StringBuilder();
transitions = transitions.append(strTmpTrans);
} else {
transitions.append("\n");
transitions.append(strTmpTrans);
// transitions = transitions + "\n" + strTmpTrans;
}
}
}
if (transitions != null) {
strTTrans.add("transition", transitions);
strTTrans.add("trueWord", getTrue());
strTTrans.add("roleindex1", inUser + "[" + i + "]");
strTTrans.add("roleindex2", inUser + "[" + i + "]");
strTmpUser = strTTrans.render();
} else {
strTmpUser = "next(" + inUser + "[" + i + "]) := " + inUser + "[" + i + "];";
}
if (strUserSection == null)
strUserSection = strTmpUser;
else
strUserSection = strUserSection + "\n\n" + strTmpUser;
}
return strUserSection;
}
public String addCAEntry(String inUser, CAEntry inCAEntry) { public String addCAEntry(String inUser, CAEntry inCAEntry) {
Vector<String> vAdminUsers = rbac.getAdmin(); Vector<String> vAdminUsers = rbac.getAdmin();
...@@ -338,80 +443,6 @@ public class WriteNuSMV { ...@@ -338,80 +443,6 @@ public class WriteNuSMV {
return strTransition; return strTransition;
} }
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);
Vector<CREntry> vCR = getMatchingCR(strRole);
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));
if (transitions == null) {
transitions = new StringBuilder();
transitions = transitions.append(strTmpTrans);
} else {
transitions.append("\n");
transitions.append(strTmpTrans);
// transitions = transitions + "\n" + strTmpTrans;
}
}
}
if (vCR != null) {
for (int j = 0; j < vCR.size(); j++) {
String strTmpTrans = addCREntry(inUser, vCR.get(j));
if (transitions == null) {
transitions = new StringBuilder();
transitions = transitions.append(strTmpTrans);
} else {
transitions.append("\n");
transitions.append(strTmpTrans);
// transitions = transitions + "\n" + strTmpTrans;
}
}
}
if (transitions != null) {
strTTrans.add("transition", transitions);
strTTrans.add("trueWord", getTrue());
strTTrans.add("roleindex1", inUser + "[" + i + "]");
strTTrans.add("roleindex2", inUser + "[" + i + "]");
strTmpUser = strTTrans.render();
} else {
strTmpUser = "next(" + inUser + "[" + i + "]) := " + inUser + "[" + i + "];";
}
if (strUserSection == null)
strUserSection = strTmpUser;
else
strUserSection = strUserSection + "\n\n" + strTmpUser;
}
return strUserSection;
}
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 void setupSpec(ST strTCodeTemplate, String inStrUser, String inStrRole) { public void setupSpec(ST strTCodeTemplate, String inStrUser, String inStrRole) {
int roleindex = 0; int roleindex = 0;
...@@ -427,37 +458,6 @@ public class WriteNuSMV { ...@@ -427,37 +458,6 @@ public class WriteNuSMV {
} }
/*
* Fill attributes in the StringTemplate
*
* Maybe This function should be passed an object that represents the RBAC state. The parameters should be plugged
* 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");
this.setupUsers(strTCodeTemplate);
System.out.println("Setting up UA");
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;
}
public boolean writeFile() throws IOException { public boolean writeFile() throws IOException {
if (done) { if (done) {
FileWriter file = new FileWriter(filename); FileWriter file = new FileWriter(filename);
......
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