Commit deab72b6 authored by Jonathan Shahen's avatar Jonathan Shahen
Browse files

working SPEC to NuSMV conversion

parent 1be9c401
-- 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
2014/12/11 04:55:32.093-0500,mohawk.MohawkMain,setupUserPreferenceOptions,FINE,[OPTION] Setting the console's maximum width
2014/12/11 04:55:32.109-0500,mohawk.MohawkMain,setupUserPreferenceOptions,FINE,[OPTION] Default Line String Used
2014/12/11 04:55:32.110-0500,mohawk.MohawkMain,setupSmvSpecOptions,FINE,[OPTION] No SMV File included
2014/12/11 04:55:32.110-0500,mohawk.MohawkMain,setupSmvSpecOptions,FINE,[OPTION] Using a specific SPEC File: ./data/testcases/mixed/test1.spec
2014/12/11 04:55:32.110-0500,mohawk.MohawkMain,setupSmvSpecOptions,FINE,[OPTION] Using the default SPEC File Extension: .spec
2014/12/11 04:55:32.110-0500,mohawk.MohawkMain,setupSmvSpecOptions,FINE,[OPTION] Bulk SPEC File inclusion: Disabled
2014/12/11 04:55:32.110-0500,mohawk.MohawkMain,setupResultOptions,INFO,Results File: latestMohawkResults.csv
2014/12/11 04:55:37.509-0500,mohawk.testing.TestingSuite,onlyConvertSpecToSmvFormat,FINE,specFile: ./data/testcases/mixed/test1.spec
......@@ -10,10 +10,11 @@ import java.util.logging.FileHandler;
import java.util.logging.Level;
import java.util.logging.Logger;
import mohawk.helper.SMVSpecHelper;
import mohawk.logging.MohawkCSVFileFormatter;
import mohawk.logging.MohawkConsoleFormatter;
import mohawk.logging.MohawkTiming;
import mohawk.testing.TestingResults;
import mohawk.testing.TestingResultsExport;
import mohawk.testing.TestingSuite;
import org.apache.commons.cli.BasicParser;
......@@ -34,10 +35,8 @@ import org.apache.commons.lang3.StringUtils;
public class MohawkMain {
private static final String VERSION = "v2.0.1";
public static String NuSMV_filepath = "NuSMV2";
public static TestingSuite tests = new TestingSuite();
private static String SpecFileExtension = ".spec";
public static String SMV_filepath = "latestRBAC2SMV.smv";
public static Boolean SMV_deleteFile = false;
public static TestingSuite tests;
public static SMVSpecHelper SMV_helper = new SMVSpecHelper();
// Logger Fields
public final static Logger logger = Logger.getLogger("mohawk");
public static String Logger_filepath = "mohawk.log";
......@@ -45,7 +44,9 @@ public class MohawkMain {
private static Level LoggerLevel;
private static FileHandler fileHandler;
private static Boolean WriteCSVFileHeader = true;
private static String ResultsFile = "latestMohawkResults.csv";
private static String resultsFile = "latestMohawkResults.csv";
private static TestingResults results;
private static MohawkTiming timing;
public static Level getLoggerLevel() {
return LoggerLevel;
......@@ -55,11 +56,62 @@ public class MohawkMain {
LoggerLevel = loggerLevel;
}
@SuppressWarnings("static-access")
public static void main(String[] args) {
// create Options object
Options options = new Options();
setupOptions(options, args);
CommandLineParser parser = new BasicParser();
try {
CommandLine cmd = parser.parse(options, args);
setupLoggerOptions(cmd, options, args);
setupReturnImmediatelyOptions(cmd, options, args);
setupUserPreferenceOptions(cmd, options, args);
setupSmvSpecOptions(cmd, options, args);
setupResultOptions(cmd, options, args);
// Execute the test cases
if (cmd.hasOption("run")) {
results = new TestingResults(resultsFile);
timing = new MohawkTiming();
tests = new TestingSuite(SMV_helper, results, timing);
String runVal = cmd.getOptionValue("run");
switch (runVal) {
case "all":
tests.runTests();
break;
case "smv":
tests.onlyConvertSpecToSmvFormat();
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) {
if (logger.getLevel() == Level.FINEST) {
e.printStackTrace();
}
logger.severe(e.getMessage());
} catch (Exception e) {
if (logger.getLevel() == Level.FINEST) {
e.printStackTrace();
}
logger.severe(e.getMessage());
}
}
@SuppressWarnings("static-access")
private static void setupOptions(Options options, String[] args) {
// Add Information Options
options.addOption("help", false, "Print this message");
options.addOption("version", false, "Prints the version (" + VERSION
......@@ -85,7 +137,7 @@ public class MohawkMain {
+ "default it creates a log called '"
+ Logger_filepath + "'").hasArg()
.create("output"));
options.addOption("a", false,
options.addOption("noheader", false,
"Does not write the CSV file header to the output log");
options.addOption(OptionBuilder.withArgName("csvfile")
......@@ -105,9 +157,11 @@ public class MohawkMain {
.hasArg().create("linestr"));
// Add File IO Options
options.addOption(OptionBuilder.withArgName("file")
.withDescription("Path to the RBAC Spec file").hasArg()
.create("rbacspec"));
options.addOption(OptionBuilder
.withArgName("file|folder")
.withDescription(
"Path to the RBAC Spec file or Folder if the 'bulk' option is set")
.hasArg().create("rbacspec"));
options.addOption(OptionBuilder
.withArgName("filepath")
......@@ -121,249 +175,263 @@ public class MohawkMain {
"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 '"
+ SMV_filepath + "'").hasArg()
+ SMV_helper.smvFilepath + "'").hasArg()
.create("smvfile"));
options.addOption(OptionBuilder
.withArgName("extension")
.withDescription(
"File extention used when searching for SPEC files when the 'bulk' option is used. Default:'"
+ SMV_helper.specFileExt + "'").hasArg()
.create("specext"));
// Add Functional Options
options.addOption("bulk", false,
"Use the folder that rbacspec points to and run against all *.spec");
options.addOption(OptionBuilder
.withArgName("bmc|smc")
.withArgName("bmc|smc|both")
.withDescription(
"Uses the Bound Estimation Checker when equal to 'bmc'; Uses Symbolic Model Checking when equal to 'smc'")
.hasArg().create("mode"));
// Add Actionable Options
options.addOption(OptionBuilder
.withArgName("all/smv")
.withArgName("all|smv")
.withDescription(
"Runs the whole model checker when equal to 'all'; Runs only the SMV conversion when equal to 'smv'")
.hasArg().create("run"));
}
CommandLineParser parser = new BasicParser();
try {
CommandLine cmd = parser.parse(options, args);
// Logging Level
logger.setUseParentHandlers(false);
consoleHandler.setFormatter(new MohawkConsoleFormatter());
setLoggerLevel(Level.WARNING); // Default Level
if (cmd.hasOption("loglevel")) {
String loglevel = cmd.getOptionValue("loglevel");
if (loglevel.equalsIgnoreCase("quiet")) {
setLoggerLevel(Level.SEVERE);
} else if (loglevel.equalsIgnoreCase("debug")) {
setLoggerLevel(Level.FINEST);
} else if (loglevel.equalsIgnoreCase("verbose")) {
setLoggerLevel(Level.INFO);
}
private static void setupSmvSpecOptions(CommandLine cmd, Options options,
String[] args) {
// Load in SPEC Files
// SMV File
if (cmd.hasOption("smvfile")) {
if (cmd.getOptionValue("smvfile").equals("n")) {
logger.fine("[OPTION] Using temporary SMV Files - will be deleted after each use");
SMV_helper.smvDeleteFile = true;
} else {
logger.fine("[OPTION] Using a specific SMV File: "
+ cmd.getOptionValue("smvfile"));
// SMV_helper.addSpecFile(cmd.getOptionValue("smvfile"));
}
} else {
logger.fine("[OPTION] No SMV File included");
}
logger.setLevel(LoggerLevel);
consoleHandler.setLevel(LoggerLevel);
logger.addHandler(consoleHandler);
// Grab the SPEC file
if (cmd.hasOption("rbacspec")) {
logger.fine("[OPTION] Using a specific SPEC File: "
+ cmd.getOptionValue("rbacspec"));
SMV_helper.specFile = cmd.getOptionValue("rbacspec");
} else {
logger.fine("[OPTION] No Spec File included");
}
// Add CSV File Headers
if (cmd.hasOption("a")) {
WriteCSVFileHeader = false;
}
// Set File Logger
if (cmd.hasOption("output")) {
// 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 {
try {
// Create a log file with a specific name
File logfile = new File(cmd.getOptionValue("output"));
if (cmd.hasOption("specext")) {
logger.fine("[OPTION] Using a specific SPEC File Extension: "
+ cmd.getOptionValue("specext"));
SMV_helper.specFileExt = cmd.getOptionValue("specext");
} else {
logger.fine("[OPTION] Using the default SPEC File Extension: "
+ SMV_helper.specFileExt);
}
if (!logfile.exists()) {
logfile.createNewFile();
}
Logger_filepath = logfile.getAbsolutePath();
if (WriteCSVFileHeader) {
FileOutputStream writer = new FileOutputStream(
logfile, true); // Always append!
writer.write(MohawkCSVFileFormatter.csvHeaders()
.getBytes());
writer.flush();
writer.close();
}
// Load more than one file from the SPEC File?
if (cmd.hasOption("bulk")) {
logger.fine("[OPTION] Bulk SPEC File inclusion: Enabled");
SMV_helper.bulk = true;
} else {
logger.fine("[OPTION] Bulk SPEC File inclusion: Disabled");
}
} catch (IOException e) {
logger.severe(e.getMessage());
return;
}
}
// Set the Mode of Operation for Converting SPEC to SMV
if (cmd.hasOption("mode")) {
switch (cmd.getOptionValue("mode")) {
case "bmc":
SMV_helper.mode = 1;
break;
case "smc":
SMV_helper.mode = 2;
break;
case "both":
SMV_helper.mode = 3;
break;
default:
logger.severe("[ERROR] Unknown mode: '"
+ cmd.getOptionValue("mode") + "'");
}
// Add Logger File Handler
if (!Logger_filepath.isEmpty()) {
fileHandler = new FileHandler(Logger_filepath);
fileHandler.setLevel(getLoggerLevel());
fileHandler.setFormatter(new MohawkCSVFileFormatter());
logger.addHandler(fileHandler);
}
}
private static void setupUserPreferenceOptions(CommandLine cmd,
Options options, String[] args) {
// Set the Console's Max Width
if (cmd.hasOption("maxw")) {
logger.fine("[OPTION] Setting the console's maximum width");
String maxw = "";
try {
maxw = cmd.getOptionValue("maxw");
((MohawkConsoleFormatter) consoleHandler.getFormatter()).maxWidth = Integer
.decode(maxw);
} catch (NumberFormatException e) {
logger.severe("[ERROR] Could not decode 'maxw': " + maxw
+ ";\n" + e.getMessage());
}
} else {
logger.fine("[OPTION] Default Console Maximum Width Used");
}
// Return immediately --------------------------------------------
if (cmd.hasOption("help") == true || args.length < 1) {
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) {
// Set the Console's Wrap String
if (cmd.hasOption("linestr")) {
logger.fine("[OPTION] Setting the console's new line string");
((MohawkConsoleFormatter) consoleHandler.getFormatter()).newLineStr = cmd
.getOptionValue("linestr");
} else {
logger.fine("[OPTION] Default Line String Used");
}
}
}
f.printHelp("mohawk", options, true);
}
return;
private static void setupLoggerOptions(CommandLine cmd, Options options,
String[] args) throws SecurityException, IOException {
// Logging Level
logger.setUseParentHandlers(false);
consoleHandler.setFormatter(new MohawkConsoleFormatter());
setLoggerLevel(Level.WARNING); // Default Level
if (cmd.hasOption("loglevel")) {
String loglevel = cmd.getOptionValue("loglevel");
if (loglevel.equalsIgnoreCase("quiet")) {
setLoggerLevel(Level.SEVERE);
} else if (loglevel.equalsIgnoreCase("debug")) {
setLoggerLevel(Level.FINEST);
} else if (loglevel.equalsIgnoreCase("verbose")) {
setLoggerLevel(Level.INFO);
}
}
if (cmd.hasOption("version")) {
// keep it as simple as possible for the version
System.out.println(VERSION);
return;
}
logger.setLevel(LoggerLevel);
consoleHandler.setLevel(LoggerLevel);
logger.addHandler(consoleHandler);
if (cmd.hasOption("numsmv")) {
logger.info("Running with the 'nusmv' Custom Configuration. "
+ "Changing the path from '" + NuSMV_filepath
+ "' to '" + cmd.getOptionValue("nusmv") + "'");
NuSMV_filepath = cmd.getOptionValue("nusmv");
}
if (cmd.hasOption("checknusmv")) {
// Add CSV File Headers
if (cmd.hasOption("noheader")) {
WriteCSVFileHeader = false;
}
// Set File Logger
if (cmd.hasOption("output")) {
// 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 {
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
Process proc = pb.start();
BufferedReader br = new BufferedReader(
new InputStreamReader(proc.getInputStream()));
String strLine = null;
if (br.ready()) {
while ((strLine = br.readLine()) != null) {
if (strLine.contains("This is NuSMV")) {
logger.info(strLine);
break;
}
}
} else {
logger.warning("No output was given by NuSMV, "
+ "maybe the commandline arguments have changed "
+ "or the file " + NuSMV_filepath
+ " points to the wrong file");
// Create a log file with a specific name
File logfile = new File(cmd.getOptionValue("output"));
if (!logfile.exists()) {
logfile.createNewFile();
}
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("No Version of NuSMV was found, "
+ "please check that NuSMV is on the PATH.");
logger.severe(e.getMessage());
return;
}
}
// END Return immediately -----------------------------------------
}
// Add Logger File Handler
if (!Logger_filepath.isEmpty()) {
fileHandler = new FileHandler(Logger_filepath);
fileHandler.setLevel(getLoggerLevel());
fileHandler.setFormatter(new MohawkCSVFileFormatter());