Commit 381632a8 authored by Jonathan Shahen's avatar Jonathan Shahen
Browse files

combined options and started on loading in the spec files and defining where to put the SMV file(s)

MOHAWK-7 #time 2h
parent 5f8e3136
...@@ -2,12 +2,12 @@ package mohawk; ...@@ -2,12 +2,12 @@ package mohawk;
import java.io.BufferedReader; import java.io.BufferedReader;
import java.io.File; import java.io.File;
import java.io.FileOutputStream;
import java.io.IOException; import java.io.IOException;
import java.io.InputStreamReader; import java.io.InputStreamReader;
import java.text.SimpleDateFormat; import java.util.Vector;
import java.util.logging.ConsoleHandler; import java.util.logging.ConsoleHandler;
import java.util.logging.FileHandler; import java.util.logging.FileHandler;
import java.util.logging.Handler;
import java.util.logging.Level; import java.util.logging.Level;
import java.util.logging.Logger; import java.util.logging.Logger;
...@@ -21,6 +21,7 @@ import org.apache.commons.cli.HelpFormatter; ...@@ -21,6 +21,7 @@ import org.apache.commons.cli.HelpFormatter;
import org.apache.commons.cli.OptionBuilder; import org.apache.commons.cli.OptionBuilder;
import org.apache.commons.cli.Options; import org.apache.commons.cli.Options;
import org.apache.commons.cli.ParseException; import org.apache.commons.cli.ParseException;
import org.apache.commons.lang3.StringUtils;
/** /**
* *
...@@ -29,11 +30,13 @@ import org.apache.commons.cli.ParseException; ...@@ -29,11 +30,13 @@ import org.apache.commons.cli.ParseException;
*/ */
public class MohawkMain { public class MohawkMain {
public final static Logger logger = Logger.getLogger("mohawk");
public static String NuSMV_filepath = "NuSMV2"; public static String NuSMV_filepath = "NuSMV2";
public static SimpleDateFormat SDF = new SimpleDateFormat( public static Vector<String> SpecFiles = new Vector<String>();
"yyyy-MM-dd_HH-mm-ss-SSS");
public static String SMV_filepath = "latestRBAC2SMV.smv"; public static String SMV_filepath = "latestRBAC2SMV.smv";
public static Boolean SMV_deleteFile = false;
// Logger Fields
public final static Logger logger = Logger.getLogger("mohawk");
public static String Logger_filepath = "mohawk.log"; public static String Logger_filepath = "mohawk.log";
private static ConsoleHandler consoleHandler = new ConsoleHandler(); private static ConsoleHandler consoleHandler = new ConsoleHandler();
private static Level LoggerLevel; private static Level LoggerLevel;
...@@ -61,18 +64,23 @@ public class MohawkMain { ...@@ -61,18 +64,23 @@ public class MohawkMain {
"checks that NuSMV is installed on the system"); "checks that NuSMV is installed on the system");
// Add Logging Level Options // Add Logging Level Options
options.addOption( options.addOption(OptionBuilder
"quiet", .withArgName("quiet|debug|verbose")
false, .withDescription(
"Be extra quiet (takes precedence over verbose and debug), only stops output to the console"); "Be extra quiet only errors are shown; "
options.addOption("verbose", false, "Be extra verbose"); + "Show debugging information; "
options.addOption("debug", false, + "extra information is given for Verbose; "
"Print debugging information (takes precedence over verbose)"); + "default is warning level")
.create("loglevel"));
options.addOption(OptionBuilder options.addOption(OptionBuilder
.withArgName("logfile|'n'|'u'") .withArgName("logfile|'n'|'u'")
.withDescription( .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'") "The filepath where the log file should be created; "
.hasArg().create("output")); + "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 '"
+ Logger_filepath + "'").hasArg()
.create("output"));
options.addOption("a", false, "does not write the CSV file header"); options.addOption("a", false, "does not write the CSV file header");
options.addOption(OptionBuilder.withArgName("csvfile") options.addOption(OptionBuilder.withArgName("csvfile")
...@@ -103,20 +111,18 @@ public class MohawkMain { ...@@ -103,20 +111,18 @@ public class MohawkMain {
.hasArg().create("nusmv")); .hasArg().create("nusmv"));
options.addOption(OptionBuilder options.addOption(OptionBuilder
.withArgName("newfile") .withArgName("smvfile|'u'|'n'")
.withDescription( .withDescription(
"Path to the SMV file we will create/write over") "The filepath where the SMV file should be created; "
.hasArg().create("smvfile")); + "Only temporary files will be used when equal to 'n'; "
+ "A unique filename will be created when equal to 'u'; "
+ "default it creates a SMV called '"
+ SMV_filepath + "'").hasArg()
.create("smvfile"));
// Add Functional Options // Add Functional Options
options.addOption("rbacbulk", false, options.addOption("rbacbulk", false,
"Use the folder that rbacspec points to and run against all *.spec"); "Use the folder that rbacspec points to and run against all *.spec");
options.addOption(
"smvunique",
false,
"Export the SMV file to a unique name (the current datetime down to the millisecond)");
options.addOption("smvdelete", false,
"Delete the SMV file when the operation is complete");
options.addOption(OptionBuilder options.addOption(OptionBuilder
.withArgName("bmc|smc") .withArgName("bmc|smc")
.withDescription( .withDescription(
...@@ -135,22 +141,28 @@ public class MohawkMain { ...@@ -135,22 +141,28 @@ public class MohawkMain {
CommandLine cmd = parser.parse(options, args); CommandLine cmd = parser.parse(options, args);
// Logging Level // Logging Level
removeHandlers(logger.getHandlers()); logger.setUseParentHandlers(false);
consoleHandler.setFormatter(new MohawkConsoleFormatter()); consoleHandler.setFormatter(new MohawkConsoleFormatter());
if (cmd.hasOption("quiet")) { setLoggerLevel(Level.WARNING); // Default Level
setLoggerLevel(Level.SEVERE); if (cmd.hasOption("loglevel")) {
} else if (cmd.hasOption("debug")) { String loglevel = cmd.getOptionValue("loglevel");
setLoggerLevel(Level.FINEST); if (loglevel.equalsIgnoreCase("quiet")) {
} else if (cmd.hasOption("verbose")) { setLoggerLevel(Level.SEVERE);
setLoggerLevel(Level.INFO); } else if (loglevel.equalsIgnoreCase("debug")) {
} else { setLoggerLevel(Level.FINEST);
setLoggerLevel(Level.WARNING); } else if (loglevel.equalsIgnoreCase("verbose")) {
setLoggerLevel(Level.INFO);
}
} }
logger.setLevel(LoggerLevel); logger.setLevel(LoggerLevel);
consoleHandler.setLevel(LoggerLevel); consoleHandler.setLevel(LoggerLevel);
logger.addHandler(consoleHandler); logger.addHandler(consoleHandler);
// Add CSV File Headers
if (cmd.hasOption("a")) {
WriteCSVFileHeader = false;
}
// Set File Logger // Set File Logger
if (cmd.hasOption("output")) { if (cmd.hasOption("output")) {
// Check if no log file was requested // Check if no log file was requested
...@@ -161,18 +173,28 @@ public class MohawkMain { ...@@ -161,18 +173,28 @@ public class MohawkMain {
// Create a unique log file // Create a unique log file
Logger_filepath = "mohawk-log.%u.%g.txt"; Logger_filepath = "mohawk-log.%u.%g.txt";
} else { } else {
// Create a log file with a specific name try {
File logfile = new File(cmd.getOptionValue("output")); // Create a log file with a specific name
File logfile = new File(cmd.getOptionValue("output"));
if (!logfile.exists()) { if (!logfile.exists()) {
try {
logfile.createNewFile(); logfile.createNewFile();
} catch (IOException e) {
logger.severe(e.getMessage());
return;
} }
Logger_filepath = logfile.getAbsolutePath();
if (WriteCSVFileHeader) {
FileOutputStream writer = new FileOutputStream(
logfile, true); // Always append!
writer.write(MohawkCSVFileFormatter.csvHeaders()
.getBytes());
writer.flush();
writer.close();
}
} catch (IOException e) {
logger.severe(e.getMessage());
return;
} }
Logger_filepath = logfile.getAbsolutePath();
} }
} }
// Add Logger File Handler // Add Logger File Handler
...@@ -182,15 +204,24 @@ public class MohawkMain { ...@@ -182,15 +204,24 @@ public class MohawkMain {
fileHandler.setFormatter(new MohawkCSVFileFormatter()); fileHandler.setFormatter(new MohawkCSVFileFormatter());
logger.addHandler(fileHandler); logger.addHandler(fileHandler);
} }
// Add CSV File Headers
if (cmd.hasOption("a")) {
WriteCSVFileHeader = false;
}
// Return immediately // Return immediately --------------------------------------------
if (cmd.hasOption("help") == true || args.length < 1) { if (cmd.hasOption("help") == true || args.length < 1) {
HelpFormatter f = new HelpFormatter(); HelpFormatter f = new HelpFormatter();
if (cmd.hasOption("maxw")) {
try {
Integer maxw = Integer.decode(cmd
.getOptionValue("maxw"));
f.printHelp(maxw, "mohawk",
StringUtils.repeat("-", maxw), options,
StringUtils.repeat("-", maxw), true);
return;
} catch (Exception e) {
}
}
f.printHelp("mohawk", options, true); f.printHelp("mohawk", options, true);
return; return;
} }
...@@ -207,11 +238,11 @@ public class MohawkMain { ...@@ -207,11 +238,11 @@ public class MohawkMain {
NuSMV_filepath = cmd.getOptionValue("nusmv"); NuSMV_filepath = cmd.getOptionValue("nusmv");
} }
if (cmd.hasOption("checknusmv")) { if (cmd.hasOption("checknusmv")) {
logger.fine("[OPTION] Checking the NuSMV version number");
String[] commands = { NuSMV_filepath, "-help" };
ProcessBuilder pb = new ProcessBuilder(commands);
pb.redirectErrorStream(true); // REQUIRED: NuSVM uses STDERR
try { try {
logger.fine("[OPTION] Checking the NuSMV version number");
String[] commands = { NuSMV_filepath, "-help" };
ProcessBuilder pb = new ProcessBuilder(commands);
pb.redirectErrorStream(true); // REQUIRED: NuSVM uses STDERR
// will throw error if it cannot find NuSMV // will throw error if it cannot find NuSMV
Process proc = pb.start(); Process proc = pb.start();
...@@ -238,6 +269,7 @@ public class MohawkMain { ...@@ -238,6 +269,7 @@ public class MohawkMain {
return; return;
} }
} }
// END Return immediately -----------------------------------------
// Set the Console's Max Width // Set the Console's Max Width
if (cmd.hasOption("maxw")) { if (cmd.hasOption("maxw")) {
...@@ -257,23 +289,75 @@ public class MohawkMain { ...@@ -257,23 +289,75 @@ public class MohawkMain {
.getOptionValue("linestr"); .getOptionValue("linestr");
} }
// Load in SPEC Files
// SMV File
if (cmd.hasOption("smvfile")) {
// Check if no log file was requested
if (cmd.getOptionValue("output").equals("n")) {
// Create no log file
Logger_filepath = "";
} else if (cmd.getOptionValue("output").equals("u")) {
// Create a unique log file
Logger_filepath = "mohawk-log.%u.%g.txt";
} else {
// Create a log file with a specific name
File logfile = new File(cmd.getOptionValue("output"));
if (!logfile.exists()) {
try {
logfile.createNewFile();
} catch (IOException e) {
if (logger.getLevel() == Level.FINEST) {
e.printStackTrace();
}
logger.severe(e.getMessage());
return;
}
}
Logger_filepath = logfile.getAbsolutePath();
}
}
if (cmd.hasOption("rbacspec")) {
if (cmd.hasOption("rbacbulk")) {
// Load all files ending in .spec
logger.fine("[OPTION] Importing all SPEC files using the Bulk Import");
} else {
// use only the one file (check that it exists)
logger.fine("[OPTION] Importing SPEC file using the Single File Import");
}
}
// Execute the test cases // Execute the test cases
if (cmd.hasOption("run")) { if (cmd.hasOption("run")) {
logger.fine("TODO: Write the 'run' parameter"); logger.severe("TODO: Write the 'run' parameter");
String runVal = cmd.getOptionValue("run");
switch (runVal) {
case "all":
break;
case "smv":
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");
}
} }
} catch (ParseException e) { } catch (ParseException e) {
if (logger.getLevel() == Level.FINEST) {
e.printStackTrace();
}
logger.severe(e.getMessage()); logger.severe(e.getMessage());
} catch (Exception e) { } catch (Exception e) {
if (logger.getLevel() == Level.FINEST) {
e.printStackTrace();
}
logger.severe(e.getMessage()); logger.severe(e.getMessage());
return;
} }
} }
private static void removeHandlers(Handler[] handlers) {
logger.setUseParentHandlers(false);
/*
* for (int i = 0; i < handlers.length; i++) {
* logger.removeHandler(handlers[i]); }
*/
}
} }
...@@ -27,7 +27,7 @@ public class MohawkCSVFileFormatter extends Formatter { ...@@ -27,7 +27,7 @@ public class MohawkCSVFileFormatter extends Formatter {
return builder.toString(); return builder.toString();
} }
public String csvHeaders() { public static String csvHeaders() {
StringBuilder builder = new StringBuilder(100); StringBuilder builder = new StringBuilder(100);
builder.append("Datetime").append(","); builder.append("Datetime").append(",");
builder.append("Classname").append(","); builder.append("Classname").append(",");
......
Supports Markdown
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