Commit 5db68eeb authored by Jonathan Shahen's avatar Jonathan Shahen

Closes the log handles and adds the option to not refine the SMV

parent 54c404da
......@@ -9,6 +9,7 @@ import java.io.PrintWriter;
import java.io.StringWriter;
import java.util.logging.ConsoleHandler;
import java.util.logging.FileHandler;
import java.util.logging.Handler;
import java.util.logging.Level;
import java.util.logging.Logger;
......@@ -85,25 +86,31 @@ public class MohawkInstance {
tests = new TestingSuite(SMV_helper, results, timing);
if (cmd.hasOption(OptionString.NOSLICING.toString())) {
logger.fine("[OPTION] RBAC Slicing is OFF");
tests.sliceRBAC = false;
} else {
logger.fine("[OPTION] RBAC Slicing is ON");
}
if (cmd.hasOption(OptionString.SLICEQUERY.toString())) {
logger.fine("[OPTION] RBAC Query Slicing is ON");
tests.sliceRBACQuery = true;
} else {
logger.fine("[OPTION] RBAC Query Slicing is OFF");
}
String runVal = cmd.getOptionValue(OptionString.RUN.toString());
switch (runVal) {
case "all":
logger.info("[ACTION] Will convert and then execute the testcase provided");
logger.info("[ALL ACTION] Will convert and then execute the testcase provided");
tests.runTests();
break;
case "smv":
logger.info("[ACTION] Will only convert the testcase provided");
logger.info("[SMV ACTION] Will only convert the testcase provided");
tests.onlyConvertSpecToSmvFormat();
break;
case "dia":
logger.info("[ACTION] Will only calculate the estimated diameter of the testcase provided");
logger.info("[DIA ACTION] Will only calculate the estimated diameter of the testcase provided");
tests.calculateDiameter();
break;
default:
......@@ -132,6 +139,9 @@ public class MohawkInstance {
}
logger.info("[EOF] Mohawk is done running");
for (Handler h : logger.getHandlers()) {
h.close(); //must call h.close or a .LCK file will remain.
}
return 0;
}
......@@ -222,15 +232,18 @@ public class MohawkInstance {
options.addOption(OptionString.BULK.toString(), false,
"Use the folder that rbacspec points to and run against all *.spec");
options.addOption(OptionString.NOSLICING.toString(), false,
"Turns off the slicing of the RBAC Inpuit Spec file (Slices by default)");
"Turns off the slicing of the RBAC Input Spec file (Slices by default)");
options.addOption(OptionString.SLICEQUERY.toString(), false,
"Turns on the slicing of the RBAC Inpuit Spec Query (Does not slice by default)");
"Turns on the slicing of the RBAC Input Spec Query (Does not slice by default)");
options.addOption(OptionString.NOREFINE.toString(), false,
"Turns off the refining step of the RBAC Input Spec (Refines by default)");
options.addOption(OptionBuilder
.withArgName("bmc|smc|both")
.withDescription(
"Uses the Bound Estimation Checker when equal to 'bmc'; Uses Symbolic Model Checking when equal to 'smc'")
.hasArg().create(OptionString.MODE.toString()));
"Uses the Bound Estimation Checker when equal to 'bmc'; "
+ "Uses Symbolic Model Checking when equal to 'smc'").hasArg()
.create(OptionString.MODE.toString()));
options.addOption(OptionBuilder
.withArgName("seconds")
......@@ -242,8 +255,10 @@ public class MohawkInstance {
options.addOption(OptionBuilder
.withArgName("all|smv|dia")
.withDescription(
"Runs the whole model checker when equal to 'all'; Runs only the SMV conversion when equal to 'smv'; Calculates the diameter when equal to 'dia'")
.hasArg().create(OptionString.RUN.toString()));
"Runs the whole model checker when equal to 'all'; "
+ "Runs only the SMV conversion when equal to 'smv'; "
+ "Calculates the diameter when equal to 'dia'").hasArg()
.create(OptionString.RUN.toString()));
}
public void printHelp(CommandLine cmd, Options options) throws Exception {
......@@ -285,6 +300,14 @@ public class MohawkInstance {
logger.fine("[OPTION] No SMV Filename included, saving file under: " + SMV_helper.smvFilepath);
}
// Turn off refining of the RBAC File
if (cmd.hasOption(OptionString.NOREFINE.toString())) {
logger.fine("[OPTION] RBAC Role Refining is OFF");
SMV_helper.refineRoles = false;
} else {
logger.fine("[OPTION] RBAC Role Refining is ON");
}
// Grab the SPEC file
if (cmd.hasOption(OptionString.SPECFILE.toString())) {
logger.fine("[OPTION] Using a specific SPEC File: " + cmd.getOptionValue(OptionString.SPECFILE.toString()));
......@@ -365,7 +388,7 @@ public class MohawkInstance {
// Logging Level
logger.setUseParentHandlers(false);
consoleHandler.setFormatter(new MohawkConsoleFormatter());
setLoggerLevel(Level.INFO); // Default Level
setLoggerLevel(Level.FINEST); // Default Level
if (cmd.hasOption(OptionString.LOGLEVEL.toString())) {
String loglevel = cmd.getOptionValue(OptionString.LOGLEVEL.toString());
if (loglevel.equalsIgnoreCase("quiet")) {
......
......@@ -4,7 +4,7 @@ public enum OptionString {
HELP("help"), AUTHORS("authors"), VERSION("version"), CHECKNUSMV("checknusmv"), LOGLEVEL("loglevel"), LOGFILE(
"logfile"), LOGFOLDER("logfolder"), NOHEADER("noheader"), RESULTSFILE("output"), MAXW("maxw"), LINESTR(
"linstr"), SPECFILE("input"), SMVFILE("smvfile"), SPECEXT("specext"), BULK("bulk"), NOSLICING("noslicing"), SLICEQUERY(
"slicequery"), MODE("mode"), TIMEOUT("timeout"), RUN("run"), NUSMVPATH("nusmv");
"slicequery"), MODE("mode"), TIMEOUT("timeout"), RUN("run"), NUSMVPATH("nusmv"), NOREFINE("norefine");
private String _str;
......
......@@ -19,15 +19,16 @@ import mohawk.slicer.SliceQueryRole;
public class SMVSpecHelper {
public final static Logger logger = Logger.getLogger("mohawk");
public String smvFilepath = "latestRBAC2SMV.smv";
public Boolean smvDeleteFile = false;
public String specFile = "";
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
public Long TIMEOUT_SECONDS = (long) 0; // Default infinite
public boolean bulk = false;
public Boolean smvDeleteFile = false;
public boolean sliceRBAC = true;
public boolean sliceRBACQuery = false;
public boolean refineRoles = true;
public void loadSpecFiles() throws IOException {
if (this.bulk == true) {
......@@ -59,11 +60,11 @@ public class SMVSpecHelper {
specFiles.add(f);
}
}
// Need to sort for linux
Collections.sort(specFiles, new Comparator<File>(){
Collections.sort(specFiles, new Comparator<File>() {
public int compare(File p1, File p2) {
return p1.getName().compareToIgnoreCase(p2.getName());
return p1.getName().compareToIgnoreCase(p2.getName());
}
});
}
......@@ -95,42 +96,43 @@ public class SMVSpecHelper {
}
try {
WriteNuSMV nusmv = new WriteNuSMV(nusmvFile.getAbsolutePath(), "smvtemplate");
RBACSpecReader reader = new RBACSpecReader(specFile.getAbsolutePath());
RBACInstance rbac = reader.getRBAC();
RolesAbsRefine absrefine = new RolesAbsRefine(rbac);
try {
if (sliceRBAC) {
logger.info("[Slicing] Slicing the Spec File");
RoleSlicer roleslicer = new RoleSlicer(rbac);
rbac = roleslicer.getSlicedPolicy();
logger.info("[DETAILS] After Slicing -> Number of Roles: " + rbac.getNumRoles()
+ "; Number of Rules: " + (rbac.getCA().size() + rbac.getCR().size()));
}
if (sliceRBACQuery) {
logger.info("[Slicing] Slicing the Spec's Query");
SliceQueryRole scRole = new SliceQueryRole(rbac);
rbac = scRole.getSlicedPolicy();
}
} catch (Exception e) {
StringWriter errors = new StringWriter();
e.printStackTrace(new PrintWriter(errors));
logger.severe(errors.toString());
logger.severe(e.getMessage());
if (sliceRBAC) {
logger.info("[Slicing] Slicing the Spec File");
RoleSlicer roleslicer = new RoleSlicer(rbac);
rbac = roleslicer.getSlicedPolicy();
logger.info("[DETAILS] After Slicing -> Number of Roles: " + rbac.getNumRoles() + "; Number of Rules: "
+ (rbac.getCA().size() + rbac.getCR().size()));
}
RBACInstance rbac_refined = absrefine.refineOnly();
if (sliceRBACQuery) {
logger.info("[Slicing] Slicing the Spec's Query");
WriteNuSMV nusmv = new WriteNuSMV(nusmvFile.getAbsolutePath(), "smvtemplate");
SliceQueryRole scRole = new SliceQueryRole(rbac);
rbac = scRole.getSlicedPolicy();
}
if (refineRoles) {
RolesAbsRefine absrefine = new RolesAbsRefine(rbac);
RBACInstance rbac_refined = absrefine.refineOnly();
nusmv.fillAttributes(rbac_refined);
nusmv.fillAttributes(rbac_refined);
} else {
nusmv.fillAttributes(rbac);
}
nusmv.writeFile();
} catch (IOException e1) {
logger.severe("[ERROR] Unable to write to the SMV file: " + nusmvFile.getAbsolutePath());
} catch (Exception e) {
StringWriter errors = new StringWriter();
e.printStackTrace(new PrintWriter(errors));
logger.severe(errors.toString());
logger.severe(e.getMessage());
}
logger.info("Done converting Spec file to their SMV format.");
......
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