diff --git a/Mohawk+T notepad++ language b/Mohawk+T notepad++ language new file mode 100644 index 0000000000000000000000000000000000000000..8b55097b5e15789decfdc1ce99b4299875751468 --- /dev/null +++ b/Mohawk+T notepad++ language @@ -0,0 +1,64 @@ + + + + + + + + 00// 01 02 03/* 04*/ + t + + + + + + + ~ & < > , { } + NOT TRUE + { + + } + + + + + + + CanAssign CanRevoke CanDisable CanEnable Query Expected + UNKNOWN GOAL_REACHABLE REACHABLE + GOAL_UNREACHABLE UNREACHABLE + + + + + + 00 01 02 03 04 05 06 07 08 09 10 11 12 13 14 15 16 17 18 19 20 21 22 23 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/src/mohawk/converter/ConverterCUI.java b/src/mohawk/converter/ConverterCUI.java index cec93735ecb2f7a170908ce1b3f455f50b399239..71100678e4ad0e1281d2db0b563fbbe7ab6c61c9 100644 --- a/src/mohawk/converter/ConverterCUI.java +++ b/src/mohawk/converter/ConverterCUI.java @@ -54,7 +54,7 @@ public class ConverterCUI { break; } - if (cmd.equals("!prev")) { + if (cmd.equals("!p")) { argv.clear(); argv.addAll(Arrays.asList(previousCmd.split(" "))); break; @@ -67,7 +67,7 @@ public class ConverterCUI { System.out.println("Commands: " + argv); try { - if (!cmd.equals("!prev")) { + if (!cmd.equals("!p")) { FileWriter fw; fw = new FileWriter(previousCommandFilename, false); fw.write(fullCommand.toString()); @@ -147,13 +147,15 @@ public class ConverterCUI { + OptionString.LOGLEVEL.c("quiet") + "!exit"); System.out.println(OptionString.TO_MOHAWK.c() + OptionString.SPECFILE.c("data/bug/11-CA-no-role3.mohawk.T") + OptionString.LOGLEVEL.c("quiet") + "!exit"); + System.out.println(""); + System.out.println(OptionString.TO_NUSMV.c() + OptionString.SPECFILE.c("data/nusmv/test01.mohawkt") + "!exit"); System.out.println(""); try { BufferedReader bfr = new BufferedReader(new FileReader(previousCommandFilename)); previousCmd = bfr.readLine(); bfr.close(); - System.out.println("Previous Command ('!prev' to use the previous command): " + previousCmd); + System.out.println("Previous Command ('!p' to use the previous command): " + previousCmd); } catch (IOException e) { System.out.println("[ERROR] Unable to load previous command!"); } diff --git a/src/mohawk/converter/ConverterInstance.java b/src/mohawk/converter/ConverterInstance.java index a49ffbc395e5fb184c03d2f718c36f8d4fe03df7..dcb004c0f12efc3e3e6e1eb4194ec2377f6f3476 100644 --- a/src/mohawk/converter/ConverterInstance.java +++ b/src/mohawk/converter/ConverterInstance.java @@ -1,24 +1,10 @@ package mohawk.converter; -import java.io.File; -import java.io.FileOutputStream; -import java.io.FileWriter; -import java.io.IOException; -import java.io.PrintWriter; -import java.io.StringWriter; +import java.io.*; import java.util.ArrayList; -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; - -import org.apache.commons.cli.BasicParser; -import org.apache.commons.cli.CommandLine; -import org.apache.commons.cli.CommandLineParser; -import org.apache.commons.cli.HelpFormatter; -import org.apache.commons.cli.OptionBuilder; -import org.apache.commons.cli.Options; +import java.util.logging.*; + +import org.apache.commons.cli.*; import org.apache.commons.lang3.StringUtils; import mohawk.converter.helper.SpecHelper; @@ -28,8 +14,6 @@ import mohawk.converter.to.asaptime.ConvertToASAPTimeNSA; import mohawk.converter.to.asaptime.ConvertToASAPTimeSA; import mohawk.converter.to.mohawk.ConvertToMohawk; import mohawk.converter.to.nusmv.ConvertToNuSMV; -import mohawk.converter.to.nusmv.ConvertToNuSMVReduction2; -import mohawk.converter.to.nusmv.ConvertToNuSMVReduction3; import mohawk.converter.to.tred.ConvertToTRole; import mohawk.global.FileExtensions; import mohawk.global.helper.RoleHelper; @@ -39,639 +23,581 @@ import mohawk.global.pieces.Rule; import mohawk.global.timing.MohawkTiming; public class ConverterInstance { - private static final String VERSION = "v1.3.1"; - private static final String AUTHORS = "Jonathan Shahen "; - // Logger Fields - public static final Logger logger = Logger.getLogger("mohawk"); - private String Logger_filepath = "mohawk-converter.log.csv"; - private String Logger_folderpath = "logs"; - private ConsoleHandler consoleHandler = new ConsoleHandler(); - private Level LoggerLevel; - private FileHandler fileHandler; - private Boolean WriteCSVFileHeader = true; - private String resultsFile = "latest_Mohawk-T_Converter_Results.csv"; - - // Helpers - public SpecHelper specHelper = new SpecHelper(); - public MohawkTiming timing = new MohawkTiming(); - public FileExtensions fileExt = new FileExtensions(); - - private CommandLine init(String[] args) throws Exception { - Options options = new Options(); - setupOptions(options); - - CommandLineParser cmdParser = new BasicParser(); - CommandLine cmd = cmdParser.parse(options, args); - - setupLoggerOptions(cmd, options); - - if (setupReturnImmediatelyOptions(cmd, options)) { - return null; - } - - /* Timing */timing.startTimer("totalTime"); - - setupUserPreferenceOptions(cmd, options); - setupSpecOptions(cmd, options); - setupResultOptions(cmd, options); - - return cmd; - } - - public int run(String[] args) { - try { - CommandLine cmd = init(args); - - if (cmd == null) { - return 0; - } - - /* Timing */timing.startTimer("loadFile"); - specHelper.loadSpecFiles(); - /* Timing */timing.stopTimer("loadFile"); - - logger.info("Spec File(s) to Convert: " + specHelper.specFiles); - for (Integer i = 1; i <= specHelper.specFiles.size(); i++) { - File specFile = specHelper.specFiles.get(i - 1); - - /* Timing */timing.startTimer("parseFile (" + i + ")"); - logger.info("Processing File (" + i + "/" - + specHelper.specFiles.size() + "): " - + specFile.getAbsolutePath()); - - MohawkTARBACParser parser = specHelper - .parseMohawkTFile(specFile); - /* Timing */timing.stopTimer("parseFile (" + i + ")"); - - MohawkT m = parser.mohawkT; - - if (specHelper.error.errorFound) { - logger.warning( - "[PARSING ERROR] Skipping this file due to a parsing error"); - continue; - } else { - logger.info( - "No errors found while parsing file, continuing on to converting"); - } - - // ONLY reductions instead of full reductions up here - if (cmd.hasOption(OptionString.ONLYREDUCTION.toString())) { - String onlyOpt = cmd.getOptionValue( - OptionString.ONLYREDUCTION.toString()); - - ArrayList workableRules = null; - RoleHelper roleHelper = new RoleHelper(m.roleHelper); - MohawkT m2 = new MohawkT(); - if (onlyOpt.equals("enable1")) { - workableRules = roleHelper - .removeEnableDisableRules(m.getAllRules()); - - m2.generatorName = "Remove CanEnable v1"; - } else if (onlyOpt.equals("enable2")) { - workableRules = roleHelper - .removeEnableDisableRulesv2(m.getAllRules()); - - m2.generatorName = "Remove CanEnable v2"; - } - - if (workableRules != null) { - m2.query = m.query; - m2.roleHelper = m.roleHelper; - m2.timeIntervalHelper = m.timeIntervalHelper; - m2.expectedResult = m.expectedResult; - - m2.addRules(workableRules); - - FileWriter fw = new FileWriter( - specFile.getAbsolutePath() + "_ONLY_" - + onlyOpt); - fw.write(m2.getString(null, true, true)); - fw.close(); - } - } else { - if (cmd.hasOption(OptionString.TO_ASAPTIME_NSA.toString()) - || cmd.hasOption(OptionString.TO_ALL.toString())) { - logger.info( - "[CONVERTING] Converting to ASAPTime NSA... " - + specFile.getName()); - /* Timing */timing - .startTimer("convertToASAPTimeNSA (" + i + ")"); - - ConvertToASAPTimeNSA toASAPTimeNSA = new ConvertToASAPTimeNSA( - timing); - toASAPTimeNSA.convert(m, specFile, true); - - if (toASAPTimeNSA.lastError == null) { - logger.info( - "[SUCCESS] Successfully converted to ASAPTimeNSA's Input Format"); - } else { - logger.warning( - "[FAILURE] Failed to convert to ASAPTimeNSA's Input Format; Error code " - + toASAPTimeNSA.lastError); - } - - /* Timing */timing - .stopTimer("convertToASAPTimeNSA (" + i + ")"); - logger.info( - "[CONVERTING] ...Done Converting to ASAPTime NSA"); - } - - if (cmd.hasOption(OptionString.TO_ASAPTIME_SA.toString()) - || cmd.hasOption(OptionString.TO_ALL.toString())) { - logger.info("[CONVERTING] Converting to ASAPTime SA... " - + specFile.getName()); - /* Timing */timing - .startTimer("convertToASAPTimeSA (" + i + ")"); - - ConvertToASAPTimeSA toASAPTimeSA = new ConvertToASAPTimeSA( - timing); - toASAPTimeSA.convert(m, specFile, true); - - if (toASAPTimeSA.lastError == null) { - logger.info( - "[SUCCESS] Successfully converted to ASAPTimeSA's Input Format"); - } else { - logger.warning( - "[FAILURE] Failed to convert to ASAPTimeSA's Input Format; Error code " - + toASAPTimeSA.lastError); - } - - /* Timing */timing - .stopTimer("convertToASAPTimeSA (" + i + ")"); - logger.info( - "[CONVERTING] ...Done Converting to ASAPTime SA"); - } - - if (cmd.hasOption(OptionString.TO_TROLE.toString()) - || cmd.hasOption(OptionString.TO_ALL.toString())) { - logger.info("[CONVERTING] Converting to TRole... " - + specFile.getName()); - /* Timing */timing - .startTimer("convertToTRole (" + i + ")"); - - ConvertToTRole toTRole = new ConvertToTRole(timing); - toTRole.convert(m, specFile, true); - - if (toTRole.lastError == null) { - logger.info( - "[SUCCESS] Successfully converted to TRole Input Format"); - } else { - logger.warning( - "[FAILURE] Failed to convert to TRole Input Format; Error code " - + toTRole.lastError); - } - - /* Timing */timing - .stopTimer("convertToTRole (" + i + ")"); - logger.info("[CONVERTING] ...Done Converting to TRole"); - } - - if (cmd.hasOption(OptionString.TO_MOHAWK.toString()) - || cmd.hasOption(OptionString.TO_ALL.toString())) { - logger.info("[CONVERTING] Converting to Mohawk... " - + specFile.getName()); - /* Timing */timing - .startTimer("convertToMohawk (" + i + ")"); - - ConvertToMohawk toMohawk = new ConvertToMohawk(timing); - - if (cmd.hasOption( - OptionString.SHORT_ROLENAMES.toString())) { - logger.fine("[OPTION] Short Rolenames: Enabled"); - toMohawk.shortRolenames = true; - } else { - logger.fine("[OPTION] Short Rolenames: Disabled"); - } - - toMohawk.convert(m, specFile, true); - - if (toMohawk.lastError == null) { - logger.info( - "[SUCCESS] Successfully converted to Mohawk's Input Format"); - } else { - logger.warning( - "[FAILURE] Failed to convert to Mohawk's Input Format; Error code " - + toMohawk.lastError); - } - - /* Timing */timing - .stopTimer("convertToMohawk (" + i + ")"); - logger.info( - "[CONVERTING] ...Done Converting to Mohawk"); - } - - if (cmd.hasOption(OptionString.TO_MOHAWK_T.toString())) { - logger.info("[CONVERTING] Converting to Mohawk-T... " - + specFile.getName()); - /* Timing */timing - .startTimer("convertToMohawkT (" + i + ")"); - - FileWriter fw = new FileWriter( - specFile.getAbsolutePath() + "_2"); - fw.write(m.getString("\n\n", true, true)); - fw.close(); - - /* Timing */timing - .stopTimer("convertToMohawkT (" + i + ")"); - logger.info( - "[CONVERTING] ...Done Converting to Mohawk-T"); - } - - if (cmd.hasOption(OptionString.TO_NUSMV.toString()) - || cmd.hasOption(OptionString.TO_ALL.toString())) { - logger.info("[CONVERTING] Converting to NuSMV... " - + specFile.getName()); - /* Timing */timing - .startTimer("convertToNuSMV (" + i + ")"); - - ConvertToNuSMV toNuSMV = null; - - if (ConvertToNuSMV.reduction == 2) { - logger.info( - "[OPTION] Using ConvertToNuSMVReduction2"); - toNuSMV = new ConvertToNuSMVReduction2(timing); - } else if (ConvertToNuSMV.reduction == 3) { - logger.info( - "[OPTION] Using ConvertToNuSMVReduction3"); - toNuSMV = new ConvertToNuSMVReduction3(timing); - } else { - /* Timing */timing - .cancelTimer("convertToNuSMV (" + i + ")"); - throw new Exception( - "[CONVERTING] Unknown Reduction number: " - + ConvertToNuSMV.reduction); - } - - if (cmd.hasOption( - OptionString.SHORT_ROLENAMES.toString())) { - logger.info("[OPTION] Short Rolenames: Enabled"); - toNuSMV.shortRolenames = true; - } else { - logger.info("[OPTION] Short Rolenames: Disabled"); - } - - toNuSMV.convert(m, specFile, true); - - if (toNuSMV.lastError == null) { - logger.info( - "[SUCCESS] Successfully converted to Mohawk's Input Format"); - } else { - logger.warning( - "[FAILURE] Failed to convert to Mohawk's Input Format; Error code " - + toNuSMV.lastError); - } - - /* Timing */timing - .stopTimer("convertToNuSMV (" + i + ")"); - logger.info( - "[CONVERTING] ...Done Converting to Mohawk"); - } - } - } - /* Timing */timing.stopTimer("totalTime"); - - logger.info(timing.toString()); - - } catch (Exception e) { - StringWriter errors = new StringWriter(); - e.printStackTrace(new PrintWriter(errors)); - logger.severe(errors.toString()); - logger.severe(e.getMessage()); - } - - logger.info("[EOF] Converter Instance done running"); - - for (Handler h : logger.getHandlers()) { - h.close();// must call h.close or a .LCK file will remain. - } - return 0; - } - - public void printHelp(CommandLine cmd, Options options) throws Exception { - if (cmd.hasOption("maxw")) { - try { - Integer maxw = Integer.decode(cmd.getOptionValue("maxw")); - printHelp(options, maxw); - } catch (Exception e) { - printHelp(options, 80); - - e.printStackTrace(); - throw new Exception( - "An error occured when trying to print out the help options!"); - } - } else { - printHelp(options, 80); - } - } - - public void printHelp(Options options, int maxw) { - HelpFormatter f = new HelpFormatter(); - f.printHelp(maxw, "mohawk-converter", - StringUtils.repeat("-", maxw) + "\nAuthors: " + AUTHORS + "\n" - + StringUtils.repeat("-", 20), - options, StringUtils.repeat("-", maxw), true); - } - - @SuppressWarnings("static-access") - public void setupOptions(Options options) { - // Add Information Options - options.addOption(OptionString.HELP.toString(), false, - "Print this message"); - options.addOption(OptionString.AUTHORS.toString(), false, - "Prints the authors"); - options.addOption(OptionString.VERSION.toString(), false, - "Prints the version (" + VERSION + ") information"); - options.addOption(OptionString.CHECKNUSMV.toString(), false, - "Checks that NuSMV is on the system and displays which version is installed"); - - // Add Logging Level Options - options.addOption(OptionBuilder.withArgName("quiet|debug|verbose") - .withDescription( - "quiet - Be extra quiet only errors are shown;\n" - + "verbose - extra information is given for Verbose;\n" - + "debug - Show debugging information;\n" - + "Default is between debug and verbose level") - .hasArg().create(OptionString.LOGLEVEL.toString())); - options.addOption(OptionBuilder.withArgName("logfile|'n'|'u'") - .withDescription( - "The filepath where the log file should be created;\n" - + "No file will be created when equal to 'n';\n" - + "A unique filename will be created when equal to 'u';\n" - + "default it creates a log called '" - + Logger_filepath + "'") - .hasArg().create(OptionString.LOGFILE.toString())); - options.addOption(OptionBuilder.withArgName("folder path") - .withDescription( - "The path to the location that the logs should be placed, " - + "default it puts the logs in the folder '" - + Logger_folderpath + "'") - .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())); - - // 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("string") - .withDescription( - "The new line string when wrapping a long line (default '\\n ')") - .hasArg().create(OptionString.LINESTR.toString())); - - // Add File IO Options - options.addOption(OptionBuilder.withArgName("file|folder") - .withDescription( - "Path to the Mohawk-T Spec File, or Folder if the 'bulk' option is set") - .hasArg().create(OptionString.SPECFILE.toString())); - - options.addOption(OptionBuilder.withArgName("extension") - .withDescription( - "File extention used when searching for SPEC files when the 'bulk' option is used. " - + "Default:'" + specHelper.fileExt + "'") - .hasArg().create(OptionString.SPECEXT.toString())); - - // Add Functional Options - options.addOption(OptionString.BULK.toString(), false, - "Use the folder that rbacspec points to and run against all *.spec"); - - options.addOption(OptionString.SHORT_ROLENAMES.toString(), false, - "Converted file will have short names (only works for to_mohawk)"); - - options.addOption(OptionString.TO_ASAPTIME_NSA.toString(), false, - "Convert input SPEC file to ASAPTime NSA format"); - options.addOption(OptionString.TO_ASAPTIME_SA.toString(), false, - "Convert input SPEC file to ASAPTime SA format"); - options.addOption(OptionString.TO_TROLE.toString(), false, - "Convert input SPEC file to TRole format"); - options.addOption(OptionString.TO_TRULE.toString(), false, - "Convert input SPEC file to TRule format"); - options.addOption(OptionString.TO_MOHAWK.toString(), false, - "Convert input SPEC file to Mohawk's ARBAC format"); - options.addOption(OptionString.TO_MOHAWK_T.toString(), false, - "Convert input SPEC file to Mohawk-T's ATRBAC format"); - options.addOption(OptionString.TO_ALL.toString(), false, - "Convert input SPEC file to All formats except Mohawk-T (Mohawk, ASAPTime NSA, ASAPTime SA, TRole, TRule)"); - - // ONLY Commands (limits the reduction steps - options.addOption(OptionBuilder.withArgName("reduction") - .withDescription( - "Only reduce using one reduction (overwrites the 'TO_' commands:\n" - + " enable1 - Remove CanEnable/CanDisable Reduction V1,\n" - + " enable2 - Remove CanEnable/CanDisable Reduction V2,\n" - + " (others to be added)") - .hasArg().create(OptionString.ONLYREDUCTION.toString())); - } - - public Level getLoggerLevel() { - return LoggerLevel; - } - - public void setLoggerLevel(Level loggerLevel) { - LoggerLevel = loggerLevel; - } - - private void setupLoggerOptions(CommandLine cmd, Options options) - throws SecurityException, IOException { - // Logging Level - logger.setUseParentHandlers(false); - consoleHandler.setFormatter(new MohawkConsoleFormatter()); - setLoggerLevel(Level.FINE);// Default Level - if (cmd.hasOption(OptionString.LOGLEVEL.toString())) { - String loglevel = cmd - .getOptionValue(OptionString.LOGLEVEL.toString()); - if (loglevel.equalsIgnoreCase("quiet")) { - setLoggerLevel(Level.WARNING); - } else if (loglevel.equalsIgnoreCase("debug")) { - setLoggerLevel(Level.FINEST); - } else if (loglevel.equalsIgnoreCase("verbose")) { - setLoggerLevel(Level.INFO); - } - } - - logger.setLevel(LoggerLevel); - consoleHandler.setLevel(LoggerLevel); - logger.addHandler(consoleHandler); - - // Add CSV File Headers - if (cmd.hasOption(OptionString.NOHEADER.toString())) { - WriteCSVFileHeader = false; - } - - // Set Logger Folder - if (cmd.hasOption(OptionString.LOGFOLDER.toString())) { - Logger_folderpath = cmd - .getOptionValue(OptionString.LOGFOLDER.toString()); - } - - // Set File Logger - if (cmd.hasOption(OptionString.LOGFILE.toString())) { - // Check if no log file was requested - if (cmd.getOptionValue(OptionString.LOGFILE.toString()) - .equals("n")) { - // Create no log file - Logger_filepath = ""; - } else if (cmd.getOptionValue(OptionString.LOGFILE.toString()) - .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(Logger_folderpath + File.separator - + cmd.getOptionValue( - OptionString.LOGFILE.toString())); - - 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(e.getMessage()); - return; - } - } - } - // Add Logger File Handler - if (!Logger_filepath.isEmpty()) { - File logfile = new File(Logger_folderpath); - logfile.mkdirs(); - - if (!logfile.isDirectory()) { - logger.severe( - "logfolder did not contain a folder that exists or that could be created!"); - } - fileHandler = new FileHandler( - Logger_folderpath + File.separator + Logger_filepath); - fileHandler.setLevel(getLoggerLevel()); - fileHandler.setFormatter(new MohawkCSVFileFormatter()); - logger.addHandler(fileHandler); - } - } - - private Boolean setupReturnImmediatelyOptions(CommandLine cmd, - Options options) throws Exception { - if (cmd.hasOption(OptionString.HELP.toString()) == true - || cmd.getOptions().length == 0) { - printHelp(cmd, options); - return true; - } - - if (cmd.hasOption(OptionString.VERSION.toString())) { - // keep it as simple as possible for the version - System.out.println(VERSION); - return true; - } - - if (cmd.hasOption(OptionString.AUTHORS.toString())) { - // keep it as simple as possible for the version - System.out.println(AUTHORS); - return true; - } - - return false; - } - - private void setupSpecOptions(CommandLine cmd, Options options) { - // Grab the SPEC file - if (cmd.hasOption(OptionString.SPECFILE.toString())) { - logger.fine("[OPTION] Using a specific SPEC File: " - + cmd.getOptionValue(OptionString.SPECFILE.toString())); - specHelper.specFile = cmd - .getOptionValue(OptionString.SPECFILE.toString()); - } else { - logger.fine("[OPTION] No Spec File included"); - } - - if (cmd.hasOption(OptionString.SPECEXT.toString())) { - logger.fine("[OPTION] Using a specific SPEC File Extension: " - + cmd.getOptionValue(OptionString.SPECEXT.toString())); - specHelper.fileExt = cmd - .getOptionValue(OptionString.SPECEXT.toString()); - } else { - logger.fine("[OPTION] Using the default SPEC File Extension: " - + specHelper.fileExt); - } - - // Load more than one file from the SPEC File? - if (cmd.hasOption(OptionString.BULK.toString())) { - logger.fine("[OPTION] Bulk SPEC File inclusion: Enabled"); - specHelper.bulk = true; - } else { - logger.fine("[OPTION] Bulk SPEC File inclusion: Disabled"); - } - } - - private void setupUserPreferenceOptions(CommandLine cmd, Options options) { - // Set the Console's Max Width - if (cmd.hasOption(OptionString.MAXW.toString())) { - logger.fine("[OPTION] Setting the console's maximum width"); - String maxw = ""; - try { - maxw = cmd.getOptionValue(OptionString.MAXW.toString()); - ((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"); - } - - // Set the Console's Wrap String - if (cmd.hasOption(OptionString.LINESTR.toString())) { - logger.fine("[OPTION] Setting the console's new line string"); - ((MohawkConsoleFormatter) consoleHandler - .getFormatter()).newLineStr = cmd - .getOptionValue(OptionString.LINESTR.toString()); - } else { - logger.fine("[OPTION] Default Line String Used"); - } - - } - - private void setupResultOptions(CommandLine cmd, Options options) { - if (cmd.hasOption(OptionString.RESULTSFILE.toString())) { - logger.fine("[OPTION] Changing the results file"); - resultsFile = cmd.getOptionValue("results"); - } - logger.info("Results File: " + resultsFile); - - if (!cmd.hasOption(OptionString.TO_ALL.toString())) { - if (!cmd.hasOption(OptionString.TO_ASAPTIME_NSA.toString())) { - logger.info("[SKIP] Skipping converting to ASAPTime NSA"); - } - if (!cmd.hasOption(OptionString.TO_ASAPTIME_SA.toString())) { - logger.info("[SKIP] Skipping converting to ASAPTime SA"); - } - if (!cmd.hasOption(OptionString.TO_TROLE.toString())) { - logger.info("[SKIP] Skipping converting to TRole"); - } - if (!cmd.hasOption(OptionString.TO_TRULE.toString())) { - logger.info("[SKIP] Skipping converting to TRule"); - } - if (!cmd.hasOption(OptionString.TO_MOHAWK.toString())) { - logger.info("[SKIP] Skipping converting to Mohawk"); - } - } - } + private static final String VERSION = "v1.3.1"; + private static final String AUTHORS = "Jonathan Shahen "; + /*Logger Fields*/ + public static final Logger logger = Logger.getLogger("mohawk"); + private String Logger_filepath = "mohawk-converter.log.csv"; + private String Logger_folderpath = "logs"; + private ConsoleHandler consoleHandler = new ConsoleHandler(); + private Level LoggerLevel; + private FileHandler fileHandler; + private Boolean WriteCSVFileHeader = true; + private String resultsFile = "latest_Mohawk-T_Converter_Results.csv"; + + /* Helpers*/ + public SpecHelper specHelper = new SpecHelper(); + public MohawkTiming timing = new MohawkTiming(); + public FileExtensions fileExt = new FileExtensions(); + + private CommandLine init(String[] args) throws Exception { + Options options = new Options(); + setupOptions(options); + + CommandLineParser cmdParser = new BasicParser(); + CommandLine cmd = cmdParser.parse(options, args); + + setupLoggerOptions(cmd, options); + + if (setupReturnImmediatelyOptions(cmd, options)) { return null; } + + /* Timing */timing.startTimer("totalTime"); + + setupUserPreferenceOptions(cmd, options); + setupSpecOptions(cmd, options); + setupResultOptions(cmd, options); + + return cmd; + } + + public int run(String[] args) { + try { + CommandLine cmd = init(args); + + if (cmd == null) { return 0; } + + /* Timing */timing.startTimer("loadFile"); + specHelper.loadSpecFiles(); + /* Timing */timing.stopTimer("loadFile"); + + logger.info("Spec File(s) to Convert: " + specHelper.specFiles); + for (Integer i = 1; i <= specHelper.specFiles.size(); i++) { + File specFile = specHelper.specFiles.get(i - 1); + + /* Timing */timing.startTimer("parseFile (" + i + ")"); + logger.info("Processing File (" + i + "/" + specHelper.specFiles.size() + "): " + + specFile.getAbsolutePath()); + + MohawkTARBACParser parser = specHelper.parseMohawkTFile(specFile); + /* Timing */timing.stopTimer("parseFile (" + i + ")"); + + MohawkT m = parser.mohawkT; + + if (specHelper.error.errorFound) { + logger.warning("[PARSING ERROR] Skipping this file due to a parsing error"); + continue; + } else { + logger.info("No errors found while parsing file, continuing on to converting"); + } + + /*ONLY reductions instead of full reductions up here*/ + if (cmd.hasOption(OptionString.ONLYREDUCTION.toString())) { + String onlyOpt = cmd.getOptionValue(OptionString.ONLYREDUCTION.toString()); + + ArrayList workableRules = null; + RoleHelper roleHelper = new RoleHelper(m.roleHelper); + MohawkT m2 = new MohawkT(); + if (onlyOpt.equals("enable1")) { + workableRules = roleHelper.removeEnableDisableRules(m.getAllRules()); + + m2.generatorName = "Remove CanEnable v1"; + } else if (onlyOpt.equals("enable2")) { + workableRules = roleHelper.removeEnableDisableRulesv2(m.getAllRules()); + + m2.generatorName = "Remove CanEnable v2"; + } + + if (workableRules != null) { + m2.query = m.query; + m2.roleHelper = m.roleHelper; + m2.timeIntervalHelper = m.timeIntervalHelper; + m2.expectedResult = m.expectedResult; + + m2.addRules(workableRules); + + FileWriter fw = new FileWriter(specFile.getAbsolutePath() + "_ONLY_" + onlyOpt); + fw.write(m2.getString(null, true, true)); + fw.close(); + } + } else { + if (cmd.hasOption(OptionString.TO_ASAPTIME_NSA.toString()) + || cmd.hasOption(OptionString.TO_ALL.toString())) { + logger.info("[CONVERTING] Converting to ASAPTime NSA... " + specFile.getName()); + /* Timing */timing.startTimer("convertToASAPTimeNSA (" + i + ")"); + + ConvertToASAPTimeNSA toASAPTimeNSA = new ConvertToASAPTimeNSA(timing); + toASAPTimeNSA.convert(m, specFile, true); + + if (toASAPTimeNSA.lastError == null) { + logger.info("[SUCCESS] Successfully converted to ASAPTimeNSA's Input Format"); + } else { + logger.warning("[FAILURE] Failed to convert to ASAPTimeNSA's Input Format; Error code " + + toASAPTimeNSA.lastError); + } + + /* Timing */timing.stopTimer("convertToASAPTimeNSA (" + i + ")"); + logger.info("[CONVERTING] ...Done Converting to ASAPTime NSA"); + } + + if (cmd.hasOption(OptionString.TO_ASAPTIME_SA.toString()) + || cmd.hasOption(OptionString.TO_ALL.toString())) { + logger.info("[CONVERTING] Converting to ASAPTime SA... " + specFile.getName()); + /* Timing */timing.startTimer("convertToASAPTimeSA (" + i + ")"); + + ConvertToASAPTimeSA toASAPTimeSA = new ConvertToASAPTimeSA(timing); + toASAPTimeSA.convert(m, specFile, true); + + if (toASAPTimeSA.lastError == null) { + logger.info("[SUCCESS] Successfully converted to ASAPTimeSA's Input Format"); + } else { + logger.warning("[FAILURE] Failed to convert to ASAPTimeSA's Input Format; Error code " + + toASAPTimeSA.lastError); + } + + /* Timing */timing.stopTimer("convertToASAPTimeSA (" + i + ")"); + logger.info("[CONVERTING] ...Done Converting to ASAPTime SA"); + } + + if (cmd.hasOption(OptionString.TO_TROLE.toString()) + || cmd.hasOption(OptionString.TO_ALL.toString())) { + logger.info("[CONVERTING] Converting to TRole... " + + specFile.getName()); + /* Timing */timing + .startTimer("convertToTRole (" + i + ")"); + + ConvertToTRole toTRole = new ConvertToTRole(timing); + toTRole.convert(m, specFile, true); + + if (toTRole.lastError == null) { + logger.info( + "[SUCCESS] Successfully converted to TRole Input Format"); + } else { + logger.warning( + "[FAILURE] Failed to convert to TRole Input Format; Error code " + + toTRole.lastError); + } + + /* Timing */timing + .stopTimer("convertToTRole (" + i + ")"); + logger.info("[CONVERTING] ...Done Converting to TRole"); + } + + if (cmd.hasOption(OptionString.TO_MOHAWK.toString()) + || cmd.hasOption(OptionString.TO_ALL.toString())) { + logger.info("[CONVERTING] Converting to Mohawk... " + + specFile.getName()); + /* Timing */timing + .startTimer("convertToMohawk (" + i + ")"); + + ConvertToMohawk toMohawk = new ConvertToMohawk(timing); + + if (cmd.hasOption( + OptionString.SHORT_ROLENAMES.toString())) { + logger.fine("[OPTION] Short Rolenames: Enabled"); + toMohawk.shortRolenames = true; + } else { + logger.fine("[OPTION] Short Rolenames: Disabled"); + } + + toMohawk.convert(m, specFile, true); + + if (toMohawk.lastError == null) { + logger.info( + "[SUCCESS] Successfully converted to Mohawk's Input Format"); + } else { + logger.warning( + "[FAILURE] Failed to convert to Mohawk's Input Format; Error code " + + toMohawk.lastError); + } + + /* Timing */timing + .stopTimer("convertToMohawk (" + i + ")"); + logger.info( + "[CONVERTING] ...Done Converting to Mohawk"); + } + + if (cmd.hasOption(OptionString.TO_MOHAWK_T.toString())) { + logger.info("[CONVERTING] Converting to Mohawk-T... " + + specFile.getName()); + /* Timing */timing + .startTimer("convertToMohawkT (" + i + ")"); + + FileWriter fw = new FileWriter( + specFile.getAbsolutePath() + "_2"); + fw.write(m.getString("\n\n", true, true)); + fw.close(); + + /* Timing */timing + .stopTimer("convertToMohawkT (" + i + ")"); + logger.info( + "[CONVERTING] ...Done Converting to Mohawk-T"); + } + + if (cmd.hasOption(OptionString.TO_NUSMV.toString()) + || cmd.hasOption(OptionString.TO_ALL.toString())) { + logger.info("[CONVERTING] Converting to NuSMV... " + + specFile.getName()); + /* Timing */timing + .startTimer("convertToNuSMV (" + i + ")"); + + ConvertToNuSMV toNuSMV = new ConvertToNuSMV(timing); + + toNuSMV.convert(m, specFile, true); + + if (toNuSMV.lastError == null) { + logger.info("[SUCCESS] Successfully converted to Mohawk's Input Format"); + } else { + logger.warning("[FAILURE] Failed to convert to Mohawk's Input Format; Error code " + + toNuSMV.lastError); + } + + /* Timing */timing.stopTimer("convertToNuSMV (" + i + ")"); + logger.info("[CONVERTING] ...Done Converting to Mohawk"); + } + } + } + /* Timing */timing.stopTimer("totalTime"); + + logger.info(timing.toString()); + + } catch (Exception e) { + StringWriter errors = new StringWriter(); + e.printStackTrace(new PrintWriter(errors)); + logger.severe(errors.toString()); + logger.severe(e.getMessage()); + } + + logger.info("[EOF] Converter Instance done running"); + + for (Handler h : logger.getHandlers()) { + h.close();/* must call h.close or a .LCK file will remain.*/ + } + return 0; + } + + public void printHelp(CommandLine cmd, Options options) throws Exception { + if (cmd.hasOption("maxw")) { + try { + Integer maxw = Integer.decode(cmd.getOptionValue("maxw")); + printHelp(options, maxw); + } catch (Exception e) { + printHelp(options, 80); + + e.printStackTrace(); + throw new Exception( + "An error occured when trying to print out the help options!"); + } + } else { + printHelp(options, 80); + } + } + + public void printHelp(Options options, int maxw) { + HelpFormatter f = new HelpFormatter(); + f.printHelp(maxw, "mohawk-converter", + StringUtils.repeat("-", maxw) + "\nAuthors: " + AUTHORS + "\n" + + StringUtils.repeat("-", 20), + options, StringUtils.repeat("-", maxw), true); + } + + @SuppressWarnings("static-access") + public void setupOptions(Options options) { + /* Add Information Options*/ + options.addOption(OptionString.HELP.toString(), false, "Print this message"); + options.addOption(OptionString.AUTHORS.toString(), false, "Prints the authors"); + options.addOption(OptionString.VERSION.toString(), false, "Prints the version (" + VERSION + ") information"); + options.addOption(OptionString.CHECKNUSMV.toString(), false, + "Checks that NuSMV is on the system and displays which version is installed"); + + /* Add Logging Level Options*/ + options.addOption(OptionBuilder.withArgName("quiet|debug|verbose") + .withDescription( + "quiet - Be extra quiet only errors are shown;\n" + + "verbose - extra information is given for Verbose;\n" + + "debug - Show debugging information;\n" + + "Default is between debug and verbose level") + .hasArg().create(OptionString.LOGLEVEL.toString())); + options.addOption(OptionBuilder.withArgName("logfile|'n'|'u'") + .withDescription( + "The filepath where the log file should be created;\n" + + "No file will be created when equal to 'n';\n" + + "A unique filename will be created when equal to 'u';\n" + + "default it creates a log called '" + + Logger_filepath + "'") + .hasArg().create(OptionString.LOGFILE.toString())); + options.addOption(OptionBuilder.withArgName("folder path") + .withDescription( + "The path to the location that the logs should be placed, " + + "default it puts the logs in the folder '" + + Logger_folderpath + "'") + .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())); + + /* 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("string") + .withDescription( + "The new line string when wrapping a long line (default '\\n ')") + .hasArg().create(OptionString.LINESTR.toString())); + + /* Add File IO Options*/ + options.addOption(OptionBuilder.withArgName("file|folder") + .withDescription( + "Path to the Mohawk-T Spec File, or Folder if the 'bulk' option is set") + .hasArg().create(OptionString.SPECFILE.toString())); + + options.addOption(OptionBuilder.withArgName("extension") + .withDescription( + "File extention used when searching for SPEC files when the 'bulk' option is used. " + + "Default:'" + specHelper.fileExt + "'") + .hasArg().create(OptionString.SPECEXT.toString())); + + /* Add Functional Options*/ + options.addOption(OptionString.BULK.toString(), false, + "Use the folder that rbacspec points to and run against all *.spec"); + + options.addOption(OptionString.SHORT_ROLENAMES.toString(), false, + "Converted file will have short names (only works for to_mohawk)"); + + options.addOption(OptionString.TO_ASAPTIME_NSA.toString(), false, + "Convert input SPEC file to ASAPTime NSA format"); + options.addOption(OptionString.TO_ASAPTIME_SA.toString(), false, + "Convert input SPEC file to ASAPTime SA format"); + options.addOption(OptionString.TO_TROLE.toString(), false, + "Convert input SPEC file to TRole format"); + options.addOption(OptionString.TO_TRULE.toString(), false, + "Convert input SPEC file to TRule format"); + options.addOption(OptionString.TO_MOHAWK.toString(), false, + "Convert input SPEC file to Mohawk's ARBAC format"); + options.addOption(OptionString.TO_MOHAWK_T.toString(), false, + "Convert input SPEC file to Mohawk-T's ATRBAC format"); + options.addOption(OptionString.TO_NUSMV.toString(), false, + "Convert input SPEC file to NuSMV format"); + options.addOption(OptionString.TO_ALL.toString(), false, + "Convert input SPEC file to All formats except Mohawk-T (Mohawk, ASAPTime NSA, ASAPTime SA, TRole, TRule)"); + + /* ONLY Commands (limits the reduction steps*/ + options.addOption(OptionBuilder.withArgName("reduction") + .withDescription( + "Only reduce using one reduction (overwrites the 'TO_' commands:\n" + + " enable1 - Remove CanEnable/CanDisable Reduction V1,\n" + + " enable2 - Remove CanEnable/CanDisable Reduction V2,\n" + + " (others to be added)") + .hasArg().create(OptionString.ONLYREDUCTION.toString())); + } + + public Level getLoggerLevel() { + return LoggerLevel; + } + + public void setLoggerLevel(Level loggerLevel) { + LoggerLevel = loggerLevel; + } + + private void setupLoggerOptions(CommandLine cmd, Options options) + throws SecurityException, IOException { + /* Logging Level*/ + logger.setUseParentHandlers(false); + consoleHandler.setFormatter(new MohawkConsoleFormatter()); + setLoggerLevel(Level.FINE);/* Default Level*/ + if (cmd.hasOption(OptionString.LOGLEVEL.toString())) { + String loglevel = cmd + .getOptionValue(OptionString.LOGLEVEL.toString()); + if (loglevel.equalsIgnoreCase("quiet")) { + setLoggerLevel(Level.WARNING); + } else if (loglevel.equalsIgnoreCase("debug")) { + setLoggerLevel(Level.FINEST); + } else if (loglevel.equalsIgnoreCase("verbose")) { + setLoggerLevel(Level.INFO); + } + } + + logger.setLevel(LoggerLevel); + consoleHandler.setLevel(LoggerLevel); + logger.addHandler(consoleHandler); + + /* Add CSV File Headers*/ + if (cmd.hasOption(OptionString.NOHEADER.toString())) { + WriteCSVFileHeader = false; + } + + /* Set Logger Folder*/ + if (cmd.hasOption(OptionString.LOGFOLDER.toString())) { + Logger_folderpath = cmd + .getOptionValue(OptionString.LOGFOLDER.toString()); + } + + /* Set File Logger*/ + if (cmd.hasOption(OptionString.LOGFILE.toString())) { + /* Check if no log file was requested*/ + if (cmd.getOptionValue(OptionString.LOGFILE.toString()) + .equals("n")) { + /* Create no log file*/ + Logger_filepath = ""; + } else if (cmd.getOptionValue(OptionString.LOGFILE.toString()) + .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(Logger_folderpath + File.separator + + cmd.getOptionValue( + OptionString.LOGFILE.toString())); + + 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(e.getMessage()); + return; + } + } + } + /* Add Logger File Handler*/ + if (!Logger_filepath.isEmpty()) { + File logfile = new File(Logger_folderpath); + logfile.mkdirs(); + + if (!logfile.isDirectory()) { + logger.severe( + "logfolder did not contain a folder that exists or that could be created!"); + } + fileHandler = new FileHandler( + Logger_folderpath + File.separator + Logger_filepath); + fileHandler.setLevel(getLoggerLevel()); + fileHandler.setFormatter(new MohawkCSVFileFormatter()); + logger.addHandler(fileHandler); + } + } + + private Boolean setupReturnImmediatelyOptions(CommandLine cmd, + Options options) throws Exception { + if (cmd.hasOption(OptionString.HELP.toString()) == true + || cmd.getOptions().length == 0) { + printHelp(cmd, options); + return true; + } + + if (cmd.hasOption(OptionString.VERSION.toString())) { + /* keep it as simple as possible for the version*/ + System.out.println(VERSION); + return true; + } + + if (cmd.hasOption(OptionString.AUTHORS.toString())) { + /* keep it as simple as possible for the version*/ + System.out.println(AUTHORS); + return true; + } + + return false; + } + + private void setupSpecOptions(CommandLine cmd, Options options) { + /* Grab the SPEC file*/ + if (cmd.hasOption(OptionString.SPECFILE.toString())) { + logger.fine("[OPTION] Using a specific SPEC File: " + + cmd.getOptionValue(OptionString.SPECFILE.toString())); + specHelper.specFile = cmd + .getOptionValue(OptionString.SPECFILE.toString()); + } else { + logger.fine("[OPTION] No Spec File included"); + } + + if (cmd.hasOption(OptionString.SPECEXT.toString())) { + logger.fine("[OPTION] Using a specific SPEC File Extension: " + + cmd.getOptionValue(OptionString.SPECEXT.toString())); + specHelper.fileExt = cmd + .getOptionValue(OptionString.SPECEXT.toString()); + } else { + logger.fine("[OPTION] Using the default SPEC File Extension: " + + specHelper.fileExt); + } + + /* Load more than one file from the SPEC File?*/ + if (cmd.hasOption(OptionString.BULK.toString())) { + logger.fine("[OPTION] Bulk SPEC File inclusion: Enabled"); + specHelper.bulk = true; + } else { + logger.fine("[OPTION] Bulk SPEC File inclusion: Disabled"); + } + } + + private void setupUserPreferenceOptions(CommandLine cmd, Options options) { + /* Set the Console's Max Width*/ + if (cmd.hasOption(OptionString.MAXW.toString())) { + logger.fine("[OPTION] Setting the console's maximum width"); + String maxw = ""; + try { + maxw = cmd.getOptionValue(OptionString.MAXW.toString()); + ((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"); + } + + /* Set the Console's Wrap String*/ + if (cmd.hasOption(OptionString.LINESTR.toString())) { + logger.fine("[OPTION] Setting the console's new line string"); + ((MohawkConsoleFormatter) consoleHandler + .getFormatter()).newLineStr = cmd + .getOptionValue(OptionString.LINESTR.toString()); + } else { + logger.fine("[OPTION] Default Line String Used"); + } + + } + + private void setupResultOptions(CommandLine cmd, Options options) { + if (cmd.hasOption(OptionString.RESULTSFILE.toString())) { + logger.fine("[OPTION] Changing the results file"); + resultsFile = cmd.getOptionValue("results"); + } + logger.info("Results File: " + resultsFile); + + if (!cmd.hasOption(OptionString.TO_ALL.toString())) { + if (!cmd.hasOption(OptionString.TO_ASAPTIME_NSA.toString())) { + logger.info("[SKIP] Skipping converting to ASAPTime NSA"); + } + if (!cmd.hasOption(OptionString.TO_ASAPTIME_SA.toString())) { + logger.info("[SKIP] Skipping converting to ASAPTime SA"); + } + if (!cmd.hasOption(OptionString.TO_TROLE.toString())) { + logger.info("[SKIP] Skipping converting to TRole"); + } + if (!cmd.hasOption(OptionString.TO_TRULE.toString())) { + logger.info("[SKIP] Skipping converting to TRule"); + } + if (!cmd.hasOption(OptionString.TO_MOHAWK.toString())) { + logger.info("[SKIP] Skipping converting to Mohawk"); + } + } + } } diff --git a/src/mohawk/converter/to/nusmv/ConvertToNuSMV.java b/src/mohawk/converter/to/nusmv/ConvertToNuSMV.java index fc71144e24ba3f8de521b7f82d39b2b9b0215499..fe4ce30954d8371173dba6275d1b34285bb7920d 100644 --- a/src/mohawk/converter/to/nusmv/ConvertToNuSMV.java +++ b/src/mohawk/converter/to/nusmv/ConvertToNuSMV.java @@ -1,28 +1,130 @@ package mohawk.converter.to.nusmv; -import java.io.File; +import java.io.*; +import java.nio.file.Files; +import java.util.*; import java.util.logging.Logger; +import org.stringtemplate.v4.ST; + import mohawk.converter.to.ConvertTo; -import mohawk.global.pieces.MohawkT; +import mohawk.global.helper.RoleHelper; +import mohawk.global.helper.TimeIntervalHelper; +import mohawk.global.pieces.*; import mohawk.global.timing.MohawkTiming; public class ConvertToNuSMV extends ConvertTo { public static final Logger logger = Logger.getLogger("mohawk"); - /** Change this number to change from Reduction 2 to Reduction 3. */ - public static final Integer reduction = 3; - public boolean shortRolenames = false; public ConvertToNuSMV(MohawkTiming timing) { super(timing); tPrefix = "ConvertToNuSMV"; } + @Override + public String getFileExtenstion() { + return ".smv"; + } + @Override public String convert(MohawkT m, File file, Boolean writeToFile) { - logger.warning("[ERROR] Pick a specific Reduction to NuSMV"); - lastError = "Pick a specific Reduction to NuSMV"; + try { + // Deep Copy Helpers + /* Timing */timing.startTimer(tPrefix + "_" + "deepcopy"); + RoleHelper roleHelper = new RoleHelper(m.roleHelper); + TimeIntervalHelper timeIntervalHelper = new TimeIntervalHelper(m.timeIntervalHelper); + Query workableQuery = new Query(m.query); + /* Timing */timing.stopTimer(tPrefix + "_" + "deepcopy"); + + /* Timing */timing.startTimer(tPrefix + "_" + "sortRolesReduceTimeslots"); + // Reduce Roles to Integers + roleHelper.allowZeroRole = false;// roles start from 1 NOT 0! + roleHelper.setupSortedRoles(); + // Reduce TimeIntervals to Timeslots + timeIntervalHelper.allowZeroTimeslot = false;// time-slots start from t1 NOT t0! + // Reduction (2) + timeIntervalHelper.reduceToTimeslots(); + /* Timing */timing.stopTimer(tPrefix + "_" + "sortRolesReduceTimeslots"); + + Set adminRoles = RoleHelper.getAdministratorRoles(m.getAllRules(), false); + + Integer caRuleCount = m.canAssign.numberOfRules(); + Integer crRuleCount = m.canRevoke.numberOfRules(); + Integer ceRuleCount = m.canEnable.numberOfRules(); + Integer cdRuleCount = m.canDisable.numberOfRules(); + + /* Generate a list of users (roles + 1) to loop through */ + ArrayList users = new ArrayList<>(roleHelper.numberOfRoles() + 1); + for (int i = 1; i <= roleHelper.numberOfRoles() + 1; i++) { + users.add(i); + } + + Set roleTimeslots = new HashSet<>(); + + for (Rule r : m.canAssign.getRules()) { + roleTimeslots.addAll(RoleTimeSlot.grabAll(r)); + } + + // Generate the Converted String + /* Timing */timing.startTimer(tPrefix + "_" + "template"); + String template = ConvertTo.readFile(this.getClass().getResource("nusmvTemplate.st")); + ST st = new ST(template); + st.add("numRoles", roleHelper.numberOfRoles()); + st.add("numAdminRoles", adminRoles.size()); + st.add("numTimeSlots", timeIntervalHelper.sizeReduced()); + + st.add("queryStr", workableQuery.getString()); + st.add("goalRoles", workableQuery._roles); + st.add("goalTimeSlot", workableQuery._timeslot._start); + + st.add("caruleslist", stringList("CA", caRuleCount)); + st.add("crruleslist", stringList("CR", crRuleCount)); + st.add("ceruleslist", stringList("CE", ceRuleCount)); + st.add("cdruleslist", stringList("CD", cdRuleCount)); + + st.add("users", users); + st.add("roleTimeslots", roleTimeslots); + + convertedStr = st.render(); + /* Timing */timing.stopTimer(tPrefix + "_" + "template"); + + // Write the converted string out to "file + getFileExtenstion()" + if (writeToFile) { + /* Timing */timing.startTimer(tPrefix + "_" + "Files.write"); + File convertedFile = new File(file.getAbsolutePath() + getFileExtenstion()); + + if (!convertedFile.exists()) { + convertedFile.createNewFile(); + } + Files.write(convertedFile.toPath(), convertedStr.getBytes()); + /* Timing */timing.stopTimer(tPrefix + "_" + "Files.write"); + } + lastError = null; + } catch (Exception e) { + StringWriter errors = new StringWriter(); + e.printStackTrace(new PrintWriter(errors)); + logger.fine(errors.toString()); + + logger.warning("[ERROR] Unable to convert to Ranise: " + e.getMessage()); + lastError = "Error ConvertToRanise.convert.Exception #1"; + } return convertedStr; } + + private String stringList(String prefix, Integer count) { + return stringList(prefix, count, ","); + } + + private String stringList(String prefix, Integer count, String suffix) { + StringBuilder sb = new StringBuilder((prefix.length() + count.toString().length()) * count); + + for (int i = 1; i <= count - 1; i++) { + sb.append(prefix).append(i).append(suffix); + } + /*Add the last one*/ + sb.append(prefix).append(count); + + return sb.toString(); + } } diff --git a/src/mohawk/converter/to/nusmv/ConvertToNuSMVReduction2.java b/src/mohawk/converter/to/nusmv/ConvertToNuSMVReduction2.java deleted file mode 100644 index 04d9da717a4723c5900666ad6f3632302cf258d6..0000000000000000000000000000000000000000 --- a/src/mohawk/converter/to/nusmv/ConvertToNuSMVReduction2.java +++ /dev/null @@ -1,81 +0,0 @@ -package mohawk.converter.to.nusmv; - -import java.io.*; -import java.nio.file.Files; -import java.util.logging.Logger; - -import org.stringtemplate.v4.ST; - -import mohawk.converter.to.ConvertTo; -import mohawk.global.helper.RoleHelper; -import mohawk.global.helper.TimeIntervalHelper; -import mohawk.global.pieces.MohawkT; -import mohawk.global.pieces.Query; -import mohawk.global.timing.MohawkTiming; - -public class ConvertToNuSMVReduction2 extends ConvertToNuSMV { - public static final Logger logger = Logger.getLogger("mohawk"); - - public ConvertToNuSMVReduction2(MohawkTiming timing) { - super(timing); - tPrefix = "ConvertToNuSMV"; - } - - @Override - public String convert(MohawkT m, File file, Boolean writeToFile) { - try { - // Deep Copy Helpers - /* Timing */timing.startTimer(tPrefix + "_" + "deepcopy"); - RoleHelper roleHelper = new RoleHelper(m.roleHelper); - TimeIntervalHelper timeIntervalHelper = new TimeIntervalHelper(m.timeIntervalHelper); - Query workableQuery = new Query(m.query); - /* Timing */timing.stopTimer(tPrefix + "_" + "deepcopy"); - - /* Timing */timing.startTimer(tPrefix + "_" + "sortRolesReduceTimeslots"); - // Reduce Roles to Integers - roleHelper.allowZeroRole = false;// roles start from 1 NOT 0! - roleHelper.setupSortedRoles(); - // Reduce TimeIntervals to Timeslots - timeIntervalHelper.allowZeroTimeslot = false;// time-slots start from t1 NOT t0! - // Reduction (2) - timeIntervalHelper.reduceToTimeslots(); - /* Timing */timing.stopTimer(tPrefix + "_" + "sortRolesReduceTimeslots"); - - // Generate the Converted String - /* Timing */timing.startTimer(tPrefix + "_" + "template"); - String template = ConvertTo.readFile(this.getClass().getResource("nusmvTemplate.st")); - ST st = new ST(template); - /* - st.add("numRoles", roleHelper.numberOfRoles()); - st.add("numTimeslots", timeIntervalHelper.sizeReduced()); - st.add("goalRole", query.goalRole); - st.add("goalTimeslot", query.goalTimeslot); - st.add("rules_nsa", rules); - */ - convertedStr = st.render(); - /* Timing */timing.stopTimer(tPrefix + "_" + "template"); - - // Write the converted string out to "file + getFileExtenstion()" - if (writeToFile) { - /* Timing */timing.startTimer(tPrefix + "_" + "Files.write"); - File convertedFile = new File(file.getAbsolutePath() + getFileExtenstion()); - - if (!convertedFile.exists()) { - convertedFile.createNewFile(); - } - Files.write(convertedFile.toPath(), convertedStr.getBytes()); - /* Timing */timing.stopTimer(tPrefix + "_" + "Files.write"); - } - lastError = null; - } catch (Exception e) { - StringWriter errors = new StringWriter(); - e.printStackTrace(new PrintWriter(errors)); - logger.fine(errors.toString()); - - logger.warning("[ERROR] Unable to convert to Ranise: " + e.getMessage()); - lastError = "Error ConvertToRanise.convert.Exception #1"; - } - - return convertedStr; - } -} diff --git a/src/mohawk/converter/to/nusmv/ConvertToNuSMVReduction3.java b/src/mohawk/converter/to/nusmv/ConvertToNuSMVReduction3.java deleted file mode 100644 index f1c575785cfde65d4c6e93c763ea02876341f043..0000000000000000000000000000000000000000 --- a/src/mohawk/converter/to/nusmv/ConvertToNuSMVReduction3.java +++ /dev/null @@ -1,63 +0,0 @@ -package mohawk.converter.to.nusmv; - -import java.io.File; -import java.io.PrintWriter; -import java.io.StringWriter; -import java.nio.file.Files; -import java.util.logging.Logger; - -import org.stringtemplate.v4.ST; - -import mohawk.converter.to.ConvertTo; -import mohawk.global.pieces.MohawkT; -import mohawk.global.timing.MohawkTiming; - -public class ConvertToNuSMVReduction3 extends ConvertToNuSMV { - public static final Logger logger = Logger.getLogger("mohawk"); - - public ConvertToNuSMVReduction3(MohawkTiming timing) { - super(timing); - tPrefix = "ConvertToNuSMV"; - } - - @Override - public String convert(MohawkT m, File file, Boolean writeToFile) { - try { - // Generate the Converted String - /* Timing */timing.startTimer(tPrefix + "_" + "template"); - String template = ConvertTo.readFile(this.getClass().getResource("ASAPTimeNSATemplate.st")); - ST st = new ST(template); - /* - st.add("numRoles", roleHelper.numberOfRoles()); - st.add("numTimeslots", timeIntervalHelper.sizeReduced()); - st.add("goalRole", query.goalRole); - st.add("goalTimeslot", query.goalTimeslot); - st.add("rules_nsa", rules); - */ - convertedStr = st.render(); - /* Timing */timing.stopTimer(tPrefix + "_" + "template"); - - // Write the converted string out to "file + getFileExtenstion()" - if (writeToFile) { - /* Timing */timing.startTimer(tPrefix + "_" + "Files.write"); - File convertedFile = new File(file.getAbsolutePath() + getFileExtenstion()); - - if (!convertedFile.exists()) { - convertedFile.createNewFile(); - } - Files.write(convertedFile.toPath(), convertedStr.getBytes()); - /* Timing */timing.stopTimer(tPrefix + "_" + "Files.write"); - } - lastError = null; - } catch (Exception e) { - StringWriter errors = new StringWriter(); - e.printStackTrace(new PrintWriter(errors)); - logger.fine(errors.toString()); - - logger.warning("[ERROR] Unable to convert to Ranise: " + e.getMessage()); - lastError = "Error ConvertToRanise.convert.Exception #1"; - } - - return convertedStr; - } -} diff --git a/src/mohawk/converter/to/nusmv/nusmvTemplate.st b/src/mohawk/converter/to/nusmv/nusmvTemplate.st index 5ecbf9df466b66b95b7e59645db4effa7d10cd83..05fe77515314f6f7e80c817b034e894ef4169c8e 100644 --- a/src/mohawk/converter/to/nusmv/nusmvTemplate.st +++ b/src/mohawk/converter/to/nusmv/nusmvTemplate.st @@ -1,32 +1,43 @@ MODULE main DEFINE -numroles := 4; -numadminroles := 3; -- Might be used later as a optimization -numusers := numroles + 1; -numtimeslots := 4; +numroles := ; +numadminroles := ; -- Might be used later as a optimization +numusers := ; -- should be = numroles + 1 +numtimeslots := ; -VAR -RoleEnabled : array 1..numroles of - array 1..numtimeslots of boolean; +-- LTLSPEC: "G p" means that a certain condition p holds in all future time instants +-- +LTLSPEC G !(T = TRUE}; separator=" & ">) -rule : {CA01, CA02, CA03, ..., CR01, CR02, ..., CE01, ..., CD01, ...}; +VAR +rule : { + -- CanAssign + + -- CanRevoke + + -- CanEnable + + -- CanDisable + +}; user : 1 .. numusers; admin: 1 .. numusers; --- Users Variable -U01R01T01 : boolean; --- Continue Above... +ASSIGN + + + +VAR +-- Users Variable +RT : boolean;}; separator="\n">}; separator="\n"> --- RoleEnabled -RE01T01 : boolean --- Continue Above... +-- RoleEnabled + : boolean;}; separator="\n"> ASSIGN -- Disabling User Role Assignments -init(U01R01T01) := FALSE; --- Continue Above... +):=FALSE;}; separator="\n"> -- Disabling Roles -init(RE01T01) := FALSE; --- Continue Above... \ No newline at end of file +) := FALSE;}; separator="\n"> \ No newline at end of file