Commit fa6e3993 authored by Jonathan Shahen's avatar Jonathan Shahen

Formatting Changes to new formatter

parent 91969897
......@@ -14,11 +14,7 @@ import mohawk.helper.SMVSpecHelper;
import mohawk.singleton.MohawkSettings;
import mohawk.testing.TestingSuite;
/**
*
* @author Jonathan Shahen
*
*/
/** @author Jonathan Shahen */
public class MohawkInstance {
private final String VERSION = "v2.3.1";
......@@ -74,21 +70,21 @@ public class MohawkInstance {
String runVal = cmd.getOptionValue(OptionString.RUN.toString());
switch (runVal) {
case "all":
logger.info("[ALL ACTION] Will convert and then execute the testcase provided");
settings.tests.runTests();
break;
case "smv":
logger.info("[SMV ACTION] Will only convert the testcase provided");
settings.tests.onlyConvertSpecToSmvFormat();
break;
case "dia":
logger.info("[DIA ACTION] Will only calculate the estimated diameter of the testcase provided");
settings.tests.calculateDiameter();
break;
default:
logger.severe("The Run Option '" + runVal + "' has not been implemented. "
+ "Please see use 'mohawk -help' to see which Run Options have been implemented");
case "all" :
logger.info("[ALL ACTION] Will convert and then execute the testcase provided");
settings.tests.runTests();
break;
case "smv" :
logger.info("[SMV ACTION] Will only convert the testcase provided");
settings.tests.onlyConvertSpecToSmvFormat();
break;
case "dia" :
logger.info("[DIA ACTION] Will only calculate the estimated diameter of the testcase provided");
settings.tests.calculateDiameter();
break;
default :
logger.severe("The Run Option '" + runVal + "' has not been implemented. "
+ "Please see use 'mohawk -help' to see which Run Options have been implemented");
}
settings.tests.done();
......@@ -140,41 +136,32 @@ public class MohawkInstance {
"Checks that NuSMV is on the system and displays which version is installed");
// Add Logging Level Options
options.addOption(OptionBuilder
.withArgName("quiet|warning|info|fine|debug")
.withDescription("default is info level")
.hasArg()
.create(OptionString.LOGLEVEL.toString()));
options.addOption(OptionBuilder
.withArgName("logfile|'n'|'u'")
.withDescription(
"The filepath where the log file should be created; "
+ "No file will be created when equal to 'n'; "
+ "A unique filename will be created when equal to 'u'; "
+ "default it creates a log called '" + settings.Logger_filepath + "'")
.hasArg()
.create(OptionString.LOGFILE.toString()));
options.addOption(OptionBuilder
.withArgName("folderpath")
.withDescription(
"The folderpath where the log file should be created; "
+ "default it creates in the current directory")
.hasArg()
.create(OptionString.LOGFOLDER.toString()));
options.addOption(OptionBuilder.withArgName("quiet|warning|info|fine|debug")
.withDescription("default is info level").hasArg().create(OptionString.LOGLEVEL.toString()));
options.addOption(OptionBuilder.withArgName("logfile|'n'|'u'")
.withDescription("The filepath where the log file should be created; "
+ "No file will be created when equal to 'n'; "
+ "A unique filename will be created when equal to 'u'; " + "default it creates a log called '"
+ settings.Logger_filepath + "'")
.hasArg().create(OptionString.LOGFILE.toString()));
options.addOption(OptionBuilder.withArgName("folderpath")
.withDescription("The folderpath where the log file should be created; "
+ "default it creates in the current directory")
.hasArg().create(OptionString.LOGFOLDER.toString()));
options.addOption(OptionString.NOHEADER.toString(), false,
"Does not write the CSV file header to the output log");
options.addOption(OptionBuilder.withArgName("csvfile")
.withDescription("The file where the result should be stored").hasArg()
.create(OptionString.RESULTSFILE.toString()));
options.addOption(
OptionBuilder.withArgName("csvfile").withDescription("The file where the result should be stored")
.hasArg().create(OptionString.RESULTSFILE.toString()));
// custom Console Logging Options
options.addOption(OptionBuilder.withArgName("num")
.withDescription("The maximum width of the console (default 120)").hasArg()
.create(OptionString.MAXW.toString()));
options.addOption(
OptionBuilder.withArgName("num").withDescription("The maximum width of the console (default 120)")
.hasArg().create(OptionString.MAXW.toString()));
options.addOption(OptionBuilder.withArgName("string")
.withDescription("The new line string when wrapping a long line (default '\\n ')").hasArg()
.create(OptionString.LINESTR.toString()));
......@@ -188,17 +175,13 @@ public class MohawkInstance {
.withDescription("Path to the NuSMV program file (defaults to 'NuSMV')").hasArg()
.create(OptionString.NUSMVPATH.toString()));
options.addOption(OptionBuilder
.withArgName("smvfile|'n'")
.withDescription(
"The file/folder path where the SMV file(s) should be created; "
+ "Only temporary files will be used when equal to 'n'; "
+ "by default it creates a SMV called '" + settings.smvFilepath + "'")
.hasArg()
.create(OptionString.SMVFILE.toString()));
options.addOption(OptionBuilder
.withArgName("extension")
options.addOption(OptionBuilder.withArgName("smvfile|'n'")
.withDescription("The file/folder path where the SMV file(s) should be created; "
+ "Only temporary files will be used when equal to 'n'; "
+ "by default it creates a SMV called '" + settings.smvFilepath + "'")
.hasArg().create(OptionString.SMVFILE.toString()));
options.addOption(OptionBuilder.withArgName("extension")
.withDescription(
"File extention used when searching for SPEC files when the 'bulk' option is used. Default:'"
+ settings.specFileExt + "'")
......@@ -214,30 +197,21 @@ public class MohawkInstance {
options.addOption(OptionString.SKIPREFINE.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()));
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()));
options.addOption(OptionBuilder
.withArgName("seconds")
.withDescription(
"The timeout time in seconds for Mohawk's refinement loop. Default: "
+ settings.TIMEOUT_SECONDS)
options.addOption(OptionBuilder.withArgName("seconds").withDescription(
"The timeout time in seconds for Mohawk's refinement loop. Default: " + settings.TIMEOUT_SECONDS)
.hasArg().create(OptionString.TIMEOUT.toString()));
// Add Actionable Options
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()));
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()));
}
public void printHelp(CommandLine cmd, Options options) throws Exception {
......@@ -271,8 +245,8 @@ public class MohawkInstance {
logger.fine("[OPTION] Using temporary SMV Files - will be deleted after each use");
settings.smvDeleteFile = true;
} else {
logger.fine("[OPTION] Using a specific SMV File: "
+ cmd.getOptionValue(OptionString.SMVFILE.toString()));
logger.fine(
"[OPTION] Using a specific SMV File: " + cmd.getOptionValue(OptionString.SMVFILE.toString()));
settings.smvFilepath = cmd.getOptionValue(OptionString.SMVFILE.toString());
}
} else {
......@@ -315,17 +289,17 @@ public class MohawkInstance {
// Set the Mode of Operation for Converting SPEC to SMV
if (cmd.hasOption(OptionString.MODE.toString())) {
switch (cmd.getOptionValue(OptionString.MODE.toString())) {
case "bmc":
settings.mode = 1;
break;
case "smc":
settings.mode = 2;
break;
case "both":
settings.mode = 3;
break;
default:
logger.severe("[ERROR] Unknown mode: '" + cmd.getOptionValue(OptionString.MODE.toString()) + "'");
case "bmc" :
settings.mode = 1;
break;
case "smc" :
settings.mode = 2;
break;
case "both" :
settings.mode = 3;
break;
default :
logger.severe("[ERROR] Unknown mode: '" + cmd.getOptionValue(OptionString.MODE.toString()) + "'");
}
}
......@@ -445,8 +419,7 @@ public class MohawkInstance {
if (!settings.Logger_filepath.isEmpty()) {
File f = new File(settings.Logger_folderpath + File.separator);
f.mkdirs();
fileHandler = new FileHandler(
settings.Logger_folderpath + File.separator + settings.Logger_filepath, true);
fileHandler = new FileHandler(settings.Logger_folderpath + File.separator + settings.Logger_filepath, true);
fileHandler.setLevel(getLoggerLevel());
fileHandler.setFormatter(new MohawkCSVFileFormatter());
logger.addHandler(fileHandler);
......@@ -467,14 +440,14 @@ public class MohawkInstance {
if (cmd.hasOption(OptionString.NUSMVPATH.toString())) {
logger.info("Running with the 'nusmv' Custom Configuration. " + "Changing the path from '"
+ settings.getNuSMV_filepath()
+ "' to '" + cmd.getOptionValue(OptionString.NUSMVPATH.toString()) + "'");
+ settings.getNuSMV_filepath() + "' to '" + cmd.getOptionValue(OptionString.NUSMVPATH.toString())
+ "'");
settings.setNuSMV_filepath(cmd.getOptionValue(OptionString.NUSMVPATH.toString()));
}
if (cmd.hasOption(OptionString.CHECKNUSMV.toString())) {
try {
logger.fine("[OPTION] Checking the NuSMV version number");
String[] commands = { settings.getNuSMV_filepath(), "-help" };
String[] commands = {settings.getNuSMV_filepath(), "-help"};
ProcessBuilder pb = new ProcessBuilder(commands);
pb.redirectErrorStream(true);// REQUIRED: NuSVM uses STDERR
// will throw error if it cannot find NuSMV
......
package mohawk;
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"),
SKIPREFINE("skiprefine");
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"), SKIPREFINE("skiprefine");
private String _str;
......@@ -35,11 +18,9 @@ public enum OptionString {
return _str;
}
/**
* Returns the commandline equivalent with the hyphen and a space following: AUTHORS -> "-authors "
/** Returns the commandline equivalent with the hyphen and a space following: AUTHORS -> "-authors "
*
* @return
*/
* @return */
public String c() {
return "-" + _str + " ";
}
......
......@@ -8,10 +8,7 @@ import java.util.HashSet;
import java.util.Map;
import java.util.Set;
/**
* @author kjayaram
*
*/
/** @author kjayaram */
public class RoleDepTree {
public RoleDepTree() {
......@@ -26,8 +23,7 @@ public class RoleDepTree {
Set<String> setRoles = mPriorityQueue.get(level);
if (setRoles == null)
setRoles = new HashSet<String>();
if (setRoles == null) setRoles = new HashSet<String>();
setRoles.add(strRole);
mPriorityQueue.put(level, setRoles);
......
......@@ -11,10 +11,7 @@ import java.util.logging.Logger;
import mohawk.rbac.RBACInstance;
import mohawk.rbac.RBACSpecReader;
/**
* @author kjayaram
*
*/
/** @author kjayaram */
public class CalculateDiameter {
public final static Logger logger = Logger.getLogger("mohawk");
......
......@@ -11,10 +11,7 @@ import java.util.logging.Logger;
import mohawk.global.pieces.mohawk.CAEntry;
import mohawk.rbac.RBACInstance;
/**
* @author kjayaram
*
*/
/** @author kjayaram */
public class CalculateRMax {
public final static Logger logger = Logger.getLogger("mohawk");
......@@ -104,8 +101,7 @@ public class CalculateRMax {
}
if (tmpCAE2.getPreConditions().keySet().contains(roleindex)) {
if (tmpCAE2.getPreConditions().getConditional(roleindex) == 1)
return true;
if (tmpCAE2.getPreConditions().getConditional(roleindex) == 1) return true;
}
return false;
......
......@@ -9,10 +9,7 @@ import java.util.logging.Logger;
import mohawk.global.pieces.mohawk.*;
import mohawk.rbac.RBACInstance;
/**
* @author kjayaram
*
*/
/** @author kjayaram */
public class CalculateRplus {
public final static Logger logger = Logger.getLogger("mohawk");
......@@ -63,10 +60,8 @@ public class CalculateRplus {
PreCondition precond = cae.getPreConditions();
for (int roleindex : precond.keySet()) {
if (precond.getConditional(roleindex) == 1)
tmpR_plus.add(roleindex);
else
tmpR_minus.add(roleindex);
if (precond.getConditional(roleindex) == 1) tmpR_plus.add(roleindex);
else tmpR_minus.add(roleindex);
}
}
}
......
......@@ -14,10 +14,7 @@ import mohawk.global.pieces.mohawk.CAEntry;
import mohawk.global.pieces.mohawk.PreCondition;
import mohawk.rbac.RBACInstance;
/**
* @author kjayaram
*
*/
/** @author kjayaram */
public class CalculateRplusOnly {
public final static Logger logger = Logger.getLogger("mohawk");
......@@ -49,8 +46,7 @@ public class CalculateRplusOnly {
String nxtRole = qRoleQueue.remove();
Vector<CAEntry> vCAE = rbac_instance.getCA().get(nxtRole);
if (vCAE == null)
continue;
if (vCAE == null) continue;
for (int i = 0; i < vCAE.size(); i++) {
......@@ -107,15 +103,13 @@ public class CalculateRplusOnly {
for (String strTgtRole : rbac_instance.getCA().keySet()) {
Vector<CAEntry> vCAE = rbac_instance.getCA().get(strTgtRole);
if (vCAE == null)
continue;
if (vCAE == null) continue;
for (int i = 0; i < vCAE.size(); i++) {
PreCondition precond = vCAE.get(i).getPreConditions();
if (precond.keySet().contains(iRoleIndex)) {
if (precond.getConditional(iRoleIndex) == 2)
sNegRoles.add(strRole);
if (precond.getConditional(iRoleIndex) == 2) sNegRoles.add(strRole);
}
}
}
......
......@@ -35,10 +35,7 @@ import mohawk.global.pieces.mohawk.CAEntry;
import mohawk.global.pieces.mohawk.PreCondition;
import mohawk.rbac.RBACInstance;
/**
* @author kjayaram
*
*/
/** @author kjayaram */
public class EstimateDia {
public final static Logger logger = Logger.getLogger("mohawk");
......@@ -65,10 +62,8 @@ public class EstimateDia {
PreCondition precond = cae.getPreConditions();
for (int roleindex : precond.keySet()) {
if (precond.getConditional(roleindex) == 1)
tmpR_plus.add(roleindex);
else
tmpR_minus.add(roleindex);
if (precond.getConditional(roleindex) == 1) tmpR_plus.add(roleindex);
else tmpR_minus.add(roleindex);
}
}
}
......@@ -97,10 +92,8 @@ public class EstimateDia {
PreCondition precond = cae.getPreConditions();
for (int roleindex : precond.keySet()) {
if (precond.getConditional(roleindex) == 1)
tmpR_plus.add(roleindex);
else
tmpR_minus.add(roleindex);
if (precond.getConditional(roleindex) == 1) tmpR_plus.add(roleindex);
else tmpR_minus.add(roleindex);
}
}
}
......@@ -192,8 +185,7 @@ public class EstimateDia {
Vector<CAEntry> vMatchingCA = rbac_instance.getCA().get(strRole);
if (vMatchingCA == null)
return;
if (vMatchingCA == null) return;
for (int i = 0; i < vMatchingCA.size(); i++) {
CAEntry cae = vMatchingCA.get(i);
......@@ -203,10 +195,8 @@ public class EstimateDia {
for (int roleindex : pcPreCond.keySet()) {
String strDepRole = rbac_instance.getRoles().get(roleindex);
if (pcPreCond.getConditional(roleindex) == 1)
vPosDeps.add(strDepRole);
else
vNegDeps.add(strDepRole);
if (pcPreCond.getConditional(roleindex) == 1) vPosDeps.add(strDepRole);
else vNegDeps.add(strDepRole);
}
}
}
......
......@@ -33,12 +33,9 @@ import java.io.IOException;
import mohawk.rbac.RBACPAT;
/**
* @author Karthick Jayaraman
*
* STAND ALONE
/** @author Karthick Jayaraman
*
*/
* STAND ALONE */
public class CnvRBACPAT {
public static void main(String args[]) throws IOException, Exception {
......
......@@ -24,34 +24,24 @@ import mohawk.rbac.RBACInstance;
public class WriteNuSMV {
/**
* Filename on disk that will contain the NuSMV spec
*/
/** Filename on disk that will contain the NuSMV spec */
private String filename;
/**
* Flag indicates whether the SMV specification has been initialized in the string.
*/
/** Flag indicates whether the SMV specification has been initialized in the string. */
private Boolean done;
/**
* SMV spec code
*/
/** SMV spec code */
private String smvcode;
/**
* Flag that indicates if you want to old format, pre 2.5.0
*/
/** Flag that indicates if you want to old format, pre 2.5.0 */
public Boolean olderVersion = false;
// RBAC Instance
private RBACInstance rbac;
/**
* This setting changes how the user transitions are computed
/** This setting changes how the user transitions are computed
* The result should be functionally the same, but organized differently
* WARNING: version 2 DOES NOT WORK and is incomplete, it must be finished up later
*/
* WARNING: version 2 DOES NOT WORK and is incomplete, it must be finished up later */
public Integer userTransistionVersion = 1;
private ST strTCodeTemplateV1;
......@@ -60,9 +50,7 @@ public class WriteNuSMV {
private String strTransTemplateV1;
// private String strTransTemplateV2;
/**
* Controls the output for this class
*/
/** Controls the output for this class */
public Level logLevel = Level.WARNING;
public boolean includeRuleComment = true;
......@@ -116,10 +104,8 @@ public class WriteNuSMV {
Map<String, Vector<CAEntry>> mCA = rbac.getCA();
if (mCA != null)
return mCA.get(strRole);
else
return null;
if (mCA != null) return mCA.get(strRole);
else return null;
// return rbac.getCA().get(strRole);
// return vFilCA;
......@@ -147,10 +133,8 @@ public class WriteNuSMV {
String strtemplate = null;
String line;
while ((line = br.readLine()) != null) {
if (strtemplate == null)
strtemplate = line;
else
strtemplate = strtemplate + "\n" + line;
if (strtemplate == null) strtemplate = line;
else strtemplate = strtemplate + "\n" + line;
}
// System.out.println(strtemplate);
......@@ -189,12 +173,12 @@ public class WriteNuSMV {
System.out.println("[START] Setting up CA-CR rules (Using version " + userTransistionVersion + ") ...");
/* TIMING */timing.startTimer(timingPrefix + " (Setting up CA-CR rules v" + userTransistionVersion + ")");
switch (userTransistionVersion) {
case 1:
setupUserTransitionsv1(strTCodeTemplateV1);
break;
case 2:
setupUserTransitionsv2(strTCodeTemplateV2);
break;
case 1 :
setupUserTransitionsv1(strTCodeTemplateV1);
break;
case 2 :
setupUserTransitionsv2(strTCodeTemplateV2);
break;
}
/* TIMING */timing.stopTimer(timingPrefix + " (Setting up CA-CR rules v" + userTransistionVersion + ")");
......@@ -394,12 +378,8 @@ public class WriteNuSMV {
strPreCond = getTrue();
}
String strTemp = "user = $user$ & " +
"admin = $admin$ & " +
"$admin$[$adminRoleIndex$] = $True$ & " +
strPreCond + " & " +
"role = " + iDestRoleIndex + " & " +
"act = ADD: " + getTrue() + ";";
String strTemp = "user = $user$ & " + "admin = $admin$ & " + "$admin$[$adminRoleIndex$] = $True$ & "
+ strPreCond + " & " + "role = " + iDestRoleIndex + " & " + "act = ADD: " + getTrue() + ";";
for (String vAdminUser : vAdminUsers) {
for (String vUser : vUsers) {
......@@ -459,12 +439,9 @@ public class WriteNuSMV {
strTTrans.add("user", shortenUser(vUser));
strTTrans.add("admin", shortenUser(vAdminUser));
if (adminRoleIndex == -1)
strTTrans.add("precondition", getTrue());
else if (adminRoleIndex == -2)
strTTrans.add("precondition", getFalse());
else
strTTrans.add("precondition", vAdminUser + "[" + adminRoleIndex + "]=" + getTrue());
if (adminRoleIndex == -1) strTTrans.add("precondition", getTrue());
else if (adminRoleIndex == -2) strTTrans.add("precondition", getFalse());
else strTTrans.add("precondition", vAdminUser + "[" + adminRoleIndex + "]=" + getTrue());
if (strTransition == null) {
strTransition = strTTrans.render();
......@@ -622,10 +599,8 @@ public class WriteNuSMV {
strTTrans.add("precondition", strPreCond);
if (strTransition == null)
strTransition = strTTrans.render();
else
strTransition = strTransition + "\n" + strTTrans.render();
if (strTransition == null) strTransition = strTTrans.render();
else strTransition = strTransition + "\n" + strTTrans.render();
}
if (includeRuleComment) {
......@@ -672,17 +647,12 @@ public class WriteNuSMV {