Commit 990ad7e2 authored by Jonathan Shahen's avatar Jonathan Shahen

Updated the NuSMV format for newer version of NuSMV

parent bd498ad7
...@@ -74,18 +74,22 @@ public class WriteNuSMV { ...@@ -74,18 +74,22 @@ public class WriteNuSMV {
String user = vUsers.get(i); String user = vUsers.get(i);
inSmvSpec.setAttribute("userarrays", user + " : array 0.." inSmvSpec.setAttribute("userarrays", user + " : array 0.."
+ (noRoles - 1) + " of boolean"); + (noRoles - 1) + " of boolean");
inSmvSpec.setAttribute("users", user); inSmvSpec.setAttribute("users", shortenUser(user));
} }
for (int i = 0; i < vAdmin.size(); i++) { for (int i = 0; i < vAdmin.size(); i++) {
String user = vAdmin.get(i); String user = vAdmin.get(i);
inSmvSpec.setAttribute("admin", user); inSmvSpec.setAttribute("admin", shortenUser(user));
} }
inSmvSpec.setAttribute("role", "0 .. " + (noRoles - 1)); inSmvSpec.setAttribute("role", "0 .. " + (noRoles - 1));
} }
public String shortenUser(String user) {
return user.replace("user", "u");
}
public void setupUA(StringTemplate inSmvSpec) { public void setupUA(StringTemplate inSmvSpec) {
Vector<String> vUsers = rbac.getUsers(); Vector<String> vUsers = rbac.getUsers();
...@@ -103,11 +107,11 @@ public class WriteNuSMV { ...@@ -103,11 +107,11 @@ public class WriteNuSMV {
if (vUserUA != null) { if (vUserUA != null) {
if (vUserUA.contains(j)) if (vUserUA.contains(j))
value = "1"; value = "TRUE";
else else
value = "0"; value = "FALSE";
} else } else
value = "0"; value = "FALSE";
String uaassign = "init(" + user + "[" + j + "]" + ") := " String uaassign = "init(" + user + "[" + j + "]" + ") := "
+ value; + value;
...@@ -168,10 +172,10 @@ public class WriteNuSMV { ...@@ -168,10 +172,10 @@ public class WriteNuSMV {
for (int i = 0; i < vAdminUsers.size(); i++) { for (int i = 0; i < vAdminUsers.size(); i++) {
StringTemplate strTTrans = new StringTemplate( StringTemplate strTTrans = new StringTemplate(
"user = $user$ & admin = $admin$ & $admincond$ & $precondition$ & role = " "user = $user$ & admin = $admin$ & $admincond$ & $precondition$ & role = "
+ iDestRoleIndex + " & act = ADD: 1;"); + iDestRoleIndex + " & act = ADD: TRUE;");
strTTrans.setAttribute("user", inUser); strTTrans.setAttribute("user", shortenUser(inUser));
strTTrans.setAttribute("admin", vAdminUsers.get(i)); strTTrans.setAttribute("admin", shortenUser(vAdminUsers.get(i)));
PreCondition pcPreCond = inCAEntry.getPreConditions(); PreCondition pcPreCond = inCAEntry.getPreConditions();
String strPreCond = null; String strPreCond = null;
int adminRoleIndex = 0; int adminRoleIndex = 0;
...@@ -184,7 +188,7 @@ public class WriteNuSMV { ...@@ -184,7 +188,7 @@ public class WriteNuSMV {
} }
String strAdminCondRole = vAdminUsers.get(i) + "[" + adminRoleIndex String strAdminCondRole = vAdminUsers.get(i) + "[" + adminRoleIndex
+ "] = 1"; + "] = TRUE";
strTTrans.setAttribute("admincond", strAdminCondRole); strTTrans.setAttribute("admincond", strAdminCondRole);
if (pcPreCond.size() != 0) { if (pcPreCond.size() != 0) {
...@@ -194,9 +198,9 @@ public class WriteNuSMV { ...@@ -194,9 +198,9 @@ public class WriteNuSMV {
String strCond = null; String strCond = null;
if (value == 1) if (value == 1)
strCond = inUser + "[" + iroleindex + "]=1"; strCond = inUser + "[" + iroleindex + "]=TRUE";
else else
strCond = inUser + "[" + iroleindex + "]=0"; strCond = inUser + "[" + iroleindex + "]=FALSE";
if (strPreCond == null) if (strPreCond == null)
strPreCond = strCond; strPreCond = strCond;
...@@ -204,7 +208,7 @@ public class WriteNuSMV { ...@@ -204,7 +208,7 @@ public class WriteNuSMV {
strPreCond = strPreCond + " & " + strCond; strPreCond = strPreCond + " & " + strCond;
} }
} else } else
strPreCond = "1"; strPreCond = "TRUE";
strTTrans.setAttribute("precondition", strPreCond); strTTrans.setAttribute("precondition", strPreCond);
...@@ -242,17 +246,17 @@ public class WriteNuSMV { ...@@ -242,17 +246,17 @@ public class WriteNuSMV {
for (int i = 0; i < vAdminUsers.size(); i++) { for (int i = 0; i < vAdminUsers.size(); i++) {
StringTemplate strTTrans = new StringTemplate( StringTemplate strTTrans = new StringTemplate(
"user = $user$ & admin = $admin$ & $precondition$ & role = " "user = $user$ & admin = $admin$ & $precondition$ & role = "
+ iDestRoleIndex + " & act = REMOVE: 0;"); + iDestRoleIndex + " & act = REMOVE: FALSE;");
strTTrans.setAttribute("user", inUser); strTTrans.setAttribute("user", shortenUser(inUser));
strTTrans.setAttribute("admin", vAdminUsers.get(i)); strTTrans.setAttribute("admin", shortenUser(vAdminUsers.get(i)));
if (adminRoleIndex == -1) if (adminRoleIndex == -1)
strTTrans.setAttribute("precondition", "1"); strTTrans.setAttribute("precondition", "TRUE");
else if (adminRoleIndex == -2) else if (adminRoleIndex == -2)
strTTrans.setAttribute("precondition", "0"); strTTrans.setAttribute("precondition", "FALSE");
else else
strTTrans.setAttribute("precondition", vAdminUsers.get(i) + "[" strTTrans.setAttribute("precondition", vAdminUsers.get(i) + "["
+ adminRoleIndex + "]=1"); + adminRoleIndex + "]=TRUE");
if (strTransition == null) if (strTransition == null)
strTransition = strTTrans.toString(); strTransition = strTTrans.toString();
......
...@@ -26,4 +26,4 @@ $transitions; separator= "\n-- Another user \n" $ ...@@ -26,4 +26,4 @@ $transitions; separator= "\n-- Another user \n" $
-- LTLSPEC -- LTLSPEC
LTLSPEC G ($user$[$roleindex$]=0) LTLSPEC G ($user$[$roleindex$]=FALSE)
\ No newline at end of file \ No newline at end of file
next($roleindex1$) := next($roleindex1$) :=
case case
$transition; separator=";\n" $ $transition; separator=";\n" $
1 : $roleindex2$; TRUE : $roleindex2$;
esac; esac;
\ 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