Commit b4474568 authored by Jonathan Shahen's avatar Jonathan Shahen

Successfully verified the Mohawk Reduction!

parent 8b72e149
......@@ -3,3 +3,7 @@ data/testcases/mohawk.jar
*.csv
mohawk.log*
src/mohawk/rbac/generated/
data/reductions/
rbacinstancefile1
rbacinstancefile2
ROLEMAPPING
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
-- This NuSMV specification was automatically generated by the
-- RBAC2SMV tool.
MODULE main
VAR
-- This section will contain state variables. For each user, we will have
-- an array.
user0 : array 0..3 of boolean;
user1 : array 0..3 of boolean;
user2 : array 0..3 of boolean;
user3 : array 0..3 of boolean;
user4 : array 0..3 of boolean;
-- This section will contain enumerations for users and actions
act : {ADD, REMOVE};
user : {user0,user1,user2,user3,user4};
admin : {user4};
role : 0 .. 3;
ASSIGN
-- Assigning UA
init(user0[0]) := 0;
init(user0[1]) := 0;
init(user0[2]) := 0;
init(user0[3]) := 0;
init(user1[0]) := 0;
init(user1[1]) := 0;
init(user1[2]) := 0;
init(user1[3]) := 0;
init(user2[0]) := 0;
init(user2[1]) := 0;
init(user2[2]) := 0;
init(user2[3]) := 0;
init(user3[0]) := 0;
init(user3[1]) := 0;
init(user3[2]) := 0;
init(user3[3]) := 0;
init(user4[0]) := 0;
init(user4[1]) := 0;
init(user4[2]) := 0;
init(user4[3]) := 1;
-- This section will contain state transition rules
next(user0[0]) :=
case
user = user0 & admin = user4 & user4[3] = 1 & user0[1]=1 & user0[2]=1 & role = 0 & act = ADD: 1;
user = user0 & admin = user4 & user4[3] = 1 & user0[1]=0 & role = 0 & act = ADD: 1;
user = user0 & admin = user4 & user4[3] = 1 & user0[1]=0 & user0[2]=1 & role = 0 & act = ADD: 1;
1 : user0[0];
esac;
next(user0[1]) :=
case
user = user0 & admin = user4 & user4[3] = 1 & user0[0]=1 & user0[2]=1 & role = 1 & act = ADD: 1;
user = user0 & admin = user4 & user4[3] = 1 & user0[0]=0 & user0[2]=1 & role = 1 & act = ADD: 1;
user = user0 & admin = user4 & user4[3] = 1 & user0[0]=0 & role = 1 & act = ADD: 1;
1 : user0[1];
esac;
next(user0[2]) :=
case
user = user0 & admin = user4 & user4[3] = 1 & user0[0]=1 & user0[1]=1 & role = 2 & act = ADD: 1;
user = user0 & admin = user4 & user4[3] = 1 & user0[0]=1 & user0[1]=0 & role = 2 & act = ADD: 1;
user = user0 & admin = user4 & 0 & role = 2 & act = REMOVE: 0;
1 : user0[2];
esac;
next(user0[3]) := user0[3];
-- Another user
next(user1[0]) :=
case
user = user1 & admin = user4 & user4[3] = 1 & user1[1]=1 & user1[2]=1 & role = 0 & act = ADD: 1;
user = user1 & admin = user4 & user4[3] = 1 & user1[1]=0 & role = 0 & act = ADD: 1;
user = user1 & admin = user4 & user4[3] = 1 & user1[1]=0 & user1[2]=1 & role = 0 & act = ADD: 1;
1 : user1[0];
esac;
next(user1[1]) :=
case
user = user1 & admin = user4 & user4[3] = 1 & user1[0]=1 & user1[2]=1 & role = 1 & act = ADD: 1;
user = user1 & admin = user4 & user4[3] = 1 & user1[0]=0 & user1[2]=1 & role = 1 & act = ADD: 1;
user = user1 & admin = user4 & user4[3] = 1 & user1[0]=0 & role = 1 & act = ADD: 1;
1 : user1[1];
esac;
next(user1[2]) :=
case
user = user1 & admin = user4 & user4[3] = 1 & user1[0]=1 & user1[1]=1 & role = 2 & act = ADD: 1;
user = user1 & admin = user4 & user4[3] = 1 & user1[0]=1 & user1[1]=0 & role = 2 & act = ADD: 1;
user = user1 & admin = user4 & 0 & role = 2 & act = REMOVE: 0;
1 : user1[2];
esac;
next(user1[3]) := user1[3];
-- Another user
next(user2[0]) :=
case
user = user2 & admin = user4 & user4[3] = 1 & user2[1]=1 & user2[2]=1 & role = 0 & act = ADD: 1;
user = user2 & admin = user4 & user4[3] = 1 & user2[1]=0 & role = 0 & act = ADD: 1;
user = user2 & admin = user4 & user4[3] = 1 & user2[1]=0 & user2[2]=1 & role = 0 & act = ADD: 1;
1 : user2[0];
esac;
next(user2[1]) :=
case
user = user2 & admin = user4 & user4[3] = 1 & user2[0]=1 & user2[2]=1 & role = 1 & act = ADD: 1;
user = user2 & admin = user4 & user4[3] = 1 & user2[0]=0 & user2[2]=1 & role = 1 & act = ADD: 1;
user = user2 & admin = user4 & user4[3] = 1 & user2[0]=0 & role = 1 & act = ADD: 1;
1 : user2[1];
esac;
next(user2[2]) :=
case
user = user2 & admin = user4 & user4[3] = 1 & user2[0]=1 & user2[1]=1 & role = 2 & act = ADD: 1;
user = user2 & admin = user4 & user4[3] = 1 & user2[0]=1 & user2[1]=0 & role = 2 & act = ADD: 1;
user = user2 & admin = user4 & 0 & role = 2 & act = REMOVE: 0;
1 : user2[2];
esac;
next(user2[3]) := user2[3];
-- Another user
next(user3[0]) :=
case
user = user3 & admin = user4 & user4[3] = 1 & user3[1]=1 & user3[2]=1 & role = 0 & act = ADD: 1;
user = user3 & admin = user4 & user4[3] = 1 & user3[1]=0 & role = 0 & act = ADD: 1;
user = user3 & admin = user4 & user4[3] = 1 & user3[1]=0 & user3[2]=1 & role = 0 & act = ADD: 1;
1 : user3[0];
esac;
next(user3[1]) :=
case
user = user3 & admin = user4 & user4[3] = 1 & user3[0]=1 & user3[2]=1 & role = 1 & act = ADD: 1;
user = user3 & admin = user4 & user4[3] = 1 & user3[0]=0 & user3[2]=1 & role = 1 & act = ADD: 1;
user = user3 & admin = user4 & user4[3] = 1 & user3[0]=0 & role = 1 & act = ADD: 1;
1 : user3[1];
esac;
next(user3[2]) :=
case
user = user3 & admin = user4 & user4[3] = 1 & user3[0]=1 & user3[1]=1 & role = 2 & act = ADD: 1;
user = user3 & admin = user4 & user4[3] = 1 & user3[0]=1 & user3[1]=0 & role = 2 & act = ADD: 1;
user = user3 & admin = user4 & 0 & role = 2 & act = REMOVE: 0;
1 : user3[2];
esac;
next(user3[3]) := user3[3];
-- Another user
next(user4[0]) :=
case
user = user4 & admin = user4 & user4[3] = 1 & user4[1]=1 & user4[2]=1 & role = 0 & act = ADD: 1;
user = user4 & admin = user4 & user4[3] = 1 & user4[1]=0 & role = 0 & act = ADD: 1;
user = user4 & admin = user4 & user4[3] = 1 & user4[1]=0 & user4[2]=1 & role = 0 & act = ADD: 1;
1 : user4[0];
esac;
next(user4[1]) :=
case
user = user4 & admin = user4 & user4[3] = 1 & user4[0]=1 & user4[2]=1 & role = 1 & act = ADD: 1;
user = user4 & admin = user4 & user4[3] = 1 & user4[0]=0 & user4[2]=1 & role = 1 & act = ADD: 1;
user = user4 & admin = user4 & user4[3] = 1 & user4[0]=0 & role = 1 & act = ADD: 1;
1 : user4[1];
esac;
next(user4[2]) :=
case
user = user4 & admin = user4 & user4[3] = 1 & user4[0]=1 & user4[1]=1 & role = 2 & act = ADD: 1;
user = user4 & admin = user4 & user4[3] = 1 & user4[0]=1 & user4[1]=0 & role = 2 & act = ADD: 1;
user = user4 & admin = user4 & 0 & role = 2 & act = REMOVE: 0;
1 : user4[2];
esac;
next(user4[3]) := user4[3];
-- LTLSPEC
LTLSPEC G (user1[1]=0)
\ No newline at end of file
......@@ -63,6 +63,7 @@ public class MohawkCUI {
System.out.println("-mode bmc -run all -bulk -input data/testcases/positive !exit");
System.out.println("-mode bmc -run all -bulk -input data/testcases/mixednocr !exit");
System.out.println("-mode bmc -run all -bulk -input data/testcases/mixed !exit");
System.out.println("-mode bmc -run all -bulk -input data/reductions !exit");
System.out.println("");
}
}
......@@ -35,12 +35,12 @@ import org.apache.commons.lang3.StringUtils;
*/
public class MohawkInstance {
private final String VERSION = "v2.0.1";
private final String VERSION = "v2.1.0";
private static final String AUTHORS = "Jonathan Shahen <jmshahen@uwaterloo.ca>; Karthick Jayaraman";
// Logger Fields
public static final Logger logger = Logger.getLogger("mohawk");
private String Logger_filepath = "mohawk.log";
private String Logger_filepath = "mohawk.csv";
private String Logger_folderpath = "logs";
private ConsoleHandler consoleHandler = new ConsoleHandler();
private Level LoggerLevel;
......
......@@ -15,7 +15,7 @@ public class SMVSpecHelper {
public String smvFilepath = "latestRBAC2SMV.smv";
public Boolean smvDeleteFile = false;
public String specFile = "";
public String specFileExt = ".spec";
public String specFileExt = ".mohawk";
public ArrayList<File> specFiles = new ArrayList<File>();
public boolean bulk = false;
public int mode = 3; // 1 for bmc, 2 for smc, 3 for both
......@@ -97,7 +97,7 @@ public class SMVSpecHelper {
logger.info("Done converting Spec file to their SMV format.");
}
public File getSmvFile(File specFile2) {
public File getSmvFile(File specFile) {
File nusmvFile = null;
if (smvDeleteFile) {
try {
......@@ -110,8 +110,7 @@ public class SMVSpecHelper {
}
if (bulk) {
nusmvFile = new File(new File(smvFilepath).getAbsolutePath() + File.pathSeparator + specFile2.getName()
+ ".smv");
nusmvFile = new File(specFile.getAbsolutePath() + ".smv");
} else {
nusmvFile = new File(smvFilepath);
}
......
......@@ -75,7 +75,7 @@ public class CalculateDiameter {
Set<String> R_minus = crplus.getRMinus();
Set<String> RevRoles = crplus.CalIrrevocableRoles();
Set<String> R_plusonly = crplusonly.getRplusOnly();
Set<String> RMaxRoles = rmax.CalRMax();
//Set<String> RMaxRoles = rmax.CalRMax();
Set<String> RUnionRoles = new HashSet<String>();
RUnionRoles.addAll(R_plus);
RUnionRoles.addAll(R_minus);
......
......@@ -106,7 +106,11 @@ public class WriteNuSMV {
}
public String shortenUser(String user) {
return user.replace("user", "u");
if (user.startsWith("user")) {
return user.replace("user", "u");
} else {
return user + "_" + user.length();
}
}
public void setupUA(StringTemplate inSmvSpec) {
......
......@@ -99,13 +99,14 @@ public class TestingSuite {
/* TIMING */timing.startTimer("runTests.mainLoop");
ExecutorService executor = Executors.newSingleThreadExecutor();
for (Integer i = 0; i < smvHelper.specFiles.size(); i++) {
/* TIMING */timing.startTimer("runTests.mainLoop (" + i + ")");
Integer numSpecFiles = smvHelper.specFiles.size();
for (Integer i = 0; i < numSpecFiles; i++) {
/* TIMING */timing.startTimer("runTests.mainLoop (" + i + "/" + numSpecFiles + ")");
for (Integer j = 0; j < modes.size(); j++) {
String specFile = smvHelper.specFiles.get(i).getAbsolutePath();
String timerName = "runTests.mainLoop (" + i + ") - " + smvHelper.specFiles.get(i).getName() + " ("
+ modes.get(j) + ")";
String timerName = "runTests.mainLoop (" + i + "/" + numSpecFiles + ") - "
+ smvHelper.specFiles.get(i).getName() + " (" + modes.get(j) + ")";
/* TIMING */timing.startTimer(timerName);
logger.info("Working on " + timerName);
......@@ -152,7 +153,8 @@ public class TestingSuite {
// Setup Timeout Timer
Future<ExecutionResult> future = executor.submit(new TestRunner(absrefine));
try {
logger.info("[RUNNING] Running Mohawk on testcase " + i + " (mode=" + modes.get(j) + "):");
logger.info("[RUNNING] Running Mohawk on testcase " + i + "/" + numSpecFiles + " (mode="
+ modes.get(j) + "):");
if (smvHelper.TIMEOUT_SECONDS == 0) {
lastResult = future.get();
......
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