From 9ff9ec5cb042dd98519b26d53bb7d3ff390c8fa8 Mon Sep 17 00:00:00 2001 From: Jonathan Shahen Date: Sat, 16 Jan 2016 04:00:21 -0500 Subject: [PATCH] Moving function convertSpecToSMVFormat() out of SMVSpecHelper and into the TestingSuite and adding better error warning into CalculateDiameter --- src/mohawk/helper/SMVSpecHelper.java | 73 +------------------------- src/mohawk/math/CalculateDiameter.java | 24 ++++----- src/mohawk/testing/TestingSuite.java | 48 ++++++++++++++++- 3 files changed, 59 insertions(+), 86 deletions(-) diff --git a/src/mohawk/helper/SMVSpecHelper.java b/src/mohawk/helper/SMVSpecHelper.java index eaa203c..e6f36dd 100644 --- a/src/mohawk/helper/SMVSpecHelper.java +++ b/src/mohawk/helper/SMVSpecHelper.java @@ -1,16 +1,11 @@ package mohawk.helper; -import java.io.*; +import java.io.File; +import java.io.IOException; import java.util.*; import java.util.logging.Logger; -import mohawk.output.WriteNuSMV; -import mohawk.rbac.RBACInstance; -import mohawk.rbac.RBACSpecReader; -import mohawk.refine.RolesAbsRefine; import mohawk.singleton.MohawkSettings; -import mohawk.slicer.RoleSlicer; -import mohawk.slicer.SliceQueryRole; public class SMVSpecHelper { public final static Logger logger = Logger.getLogger("mohawk"); @@ -76,70 +71,6 @@ public class SMVSpecHelper { specFiles.add(file2); } - public void convertSpecToSMVFormat(File specFile, File nusmvFile) throws Exception { - logger.info("Converting the Spec file (" + specFile.getName() + ") to their SMV format..."); - - if (!specFile.exists()) { - logger.severe("[ERROR] Unable to find the SPEC file: " + specFile.getName()); - throw new FileNotFoundException("Unable to find the SPEC file: " + specFile.getName()); - } - - try { - WriteNuSMV nusmv = new WriteNuSMV(nusmvFile.getAbsolutePath(), "smvtemplate", settings.timing, - "convertSpecToSMVFormat(" + specFile.getName() + ")"); - RBACSpecReader reader = new RBACSpecReader(specFile.getAbsolutePath()); - RBACInstance rbac = reader.getRBAC(); - - if (settings.sliceRBAC) { - logger.info("[Slicing] Slicing the Spec File"); - - RoleSlicer roleslicer = new RoleSlicer(rbac, settings.timing, - "convertSpecToSMVFormat(" + specFile.getName() + ")"); - rbac = roleslicer.getSlicedPolicy(); - - logger.info("[DETAILS] After Slicing -> Number of Roles: " + rbac.getNumRoles() + - "; Number of Rules: " + (rbac.getCA().size() + rbac.getCR().size())); - } - - if (settings.sliceRBACQuery) { - logger.info("[Slicing] Slicing the Spec's Query"); - - SliceQueryRole scRole = new SliceQueryRole(rbac); - rbac = scRole.getSlicedPolicy(); - } - - if (settings.skipRefine) { - nusmv.fillAttributes(rbac); - } else { - RolesAbsRefine absrefine = new RolesAbsRefine(rbac, settings.timing, - "convertSpecToSMVFormat(" + specFile.getName() + ")"); - RBACInstance rbac_refined = absrefine.refineOnly(); - - nusmv.fillAttributes(rbac_refined); - } - System.out.println("Number of role without rules: " + nusmv.roleWithoutRules); - System.out.println("Number of role with rules: " + nusmv.roleWithRules); - System.out.println("Ratio without / with: " + (new Float(nusmv.roleWithoutRules) / nusmv.roleWithRules) + - "; without / total: " - + (new Float(nusmv.roleWithoutRules) / (nusmv.roleWithRules + nusmv.roleWithoutRules))); - - nusmv.writeFile(); - } catch (IOException e1) { - logger.severe("[ERROR] Unable to write to the SMV file: " + nusmvFile.getAbsolutePath()); - - throw e1; - } catch (Exception e) { - StringWriter errors = new StringWriter(); - e.printStackTrace(new PrintWriter(errors)); - logger.severe(errors.toString()); - logger.severe(e.getMessage()); - - throw e; - } - - logger.info("Done converting Spec file to their SMV format."); - } - public File getSmvFile(File specFile) { File nusmvFile = null; if (settings.smvDeleteFile) { diff --git a/src/mohawk/math/CalculateDiameter.java b/src/mohawk/math/CalculateDiameter.java index 0c1e060..719499d 100644 --- a/src/mohawk/math/CalculateDiameter.java +++ b/src/mohawk/math/CalculateDiameter.java @@ -4,10 +4,8 @@ package mohawk.math; import java.io.File; -import java.util.HashMap; -import java.util.HashSet; -import java.util.Map; -import java.util.Set; +import java.io.IOException; +import java.util.*; import java.util.logging.Logger; import mohawk.rbac.RBACInstance; @@ -22,7 +20,7 @@ public class CalculateDiameter { // public CalculateDiameter() {} - public static void main(String args[]) { + public static void main(String args[]) throws IOException { if (args.length < 1) { System.out.println("Usage: java -jar ./rbac2smv.jar CalculateDiameter rbacspec"); @@ -48,7 +46,7 @@ public class CalculateDiameter { CalculateRplus crplus = new CalculateRplus(rbac); CalculateRplusOnly crplusonly = new CalculateRplusOnly(rbac); - //CalculateRMax rmax = new CalculateRMax(rbac); + // CalculateRMax rmax = new CalculateRMax(rbac); Set R_plus = crplus.getRPlus(); Set R_minus = crplus.getRMinus(); Set RevRoles = crplus.CalIrrevocableRoles(); @@ -73,12 +71,12 @@ public class CalculateDiameter { int no_roles = rbac.getNumRoles(); CalculateRplus crplus = new CalculateRplus(rbac); CalculateRplusOnly crplusonly = new CalculateRplusOnly(rbac); - //CalculateRMax rmax = new CalculateRMax(rbac); + // CalculateRMax rmax = new CalculateRMax(rbac); Set R_plus = crplus.getRPlus(); Set R_minus = crplus.getRMinus(); Set RevRoles = crplus.CalIrrevocableRoles(); Set R_plusonly = crplusonly.getRplusOnly(); - //Set RMaxRoles = rmax.CalRMax(); + // Set RMaxRoles = rmax.CalRMax(); Set RUnionRoles = new HashSet(); RUnionRoles.addAll(R_plus); RUnionRoles.addAll(R_minus); @@ -95,13 +93,13 @@ public class CalculateDiameter { return ((int) Math.pow(2, (no_roles - tightenings)) - 1 + tightenings); } - public static Map CalDiameterFile(String filename) { + public static Map CalDiameterFile(String filename) throws IOException { File rbacfile = new File(filename); return CalDiameterFile(rbacfile); } - public static Map CalDiameterFile(File rbacfile) { + public static Map CalDiameterFile(File rbacfile) throws IOException { if (!rbacfile.exists()) { System.out.println("The RBAC specification file " + rbacfile + " does not exists."); return null; @@ -121,12 +119,12 @@ public class CalculateDiameter { CalculateRplus crplus = new CalculateRplus(rbac); CalculateRplusOnly crplusonly = new CalculateRplusOnly(rbac); - //CalculateRMax rmax = new CalculateRMax(rbac); + // CalculateRMax rmax = new CalculateRMax(rbac); Set R_plus = crplus.getRPlus(); Set R_minus = crplus.getRMinus(); Set RevRoles = crplus.CalIrrevocableRoles(); Set R_plusonly = crplusonly.getRplusOnly(); - //Set RMaxRoles = rmax.CalRMax(); + // Set RMaxRoles = rmax.CalRMax(); Set RUnionRoles = new HashSet(); RUnionRoles.addAll(R_plus); RUnionRoles.addAll(R_minus); @@ -137,7 +135,7 @@ public class CalculateDiameter { System.out.println("Tightening 2 - R+ : " + R_plus.size()); System.out.println("Tightening 3 - R_p : " + R_plusonly.size()); System.out.println("Tightening 4 - R_irrev : " + RevRoles.size()); - //System.out.println("Tightening 5 - R_max : " + RMaxRoles.size()); + // System.out.println("Tightening 5 - R_max : " + RMaxRoles.size()); System.out.println("Union of Tightenings : " + RUnionRoles.size()); int tightenings = RUnionRoles.size(); diff --git a/src/mohawk/testing/TestingSuite.java b/src/mohawk/testing/TestingSuite.java index 6586d10..ff5f279 100644 --- a/src/mohawk/testing/TestingSuite.java +++ b/src/mohawk/testing/TestingSuite.java @@ -79,7 +79,12 @@ public class TestingSuite { } /* TIMING */settings.timing.startTimer("smvHelper.loadSpecFiles"); - settings.smvHelper.loadSpecFiles(); + try { + settings.smvHelper.loadSpecFiles(); + } catch (IOException e1) { + // TODO Auto-generated catch block + e1.printStackTrace(); + } /* TIMING */settings.timing.stopTimer("smvHelper.loadSpecFiles"); /* TIMING */settings.timing.startTimer("runTests.mainLoop"); @@ -298,9 +303,48 @@ public class TestingSuite { try { File specFile = settings.smvHelper.specFiles.get(i); File nusmvFile = settings.smvHelper.getSmvFile(specFile); + String timerName = "onlyConvertSpecToSmvFormat.mainLoop (" + (i + 1) + "/" + + settings.smvHelper.specFiles.size() + ") - " + specFile.getName(); + logger.info("[FILE IO] Using SMV File: " + nusmvFile.getCanonicalPath()); - settings.smvHelper.convertSpecToSMVFormat(specFile, nusmvFile); + if (!specFile.exists()) { + logger.severe("[ERROR] Unable to find the SPEC file: " + specFile.getName()); + throw new FileNotFoundException("Unable to find the SPEC file: " + specFile.getName()); + } + + WriteNuSMV nusmv = new WriteNuSMV(nusmvFile.getAbsolutePath(), settings.timing, + "convertSpecToSMVFormat(" + specFile.getName() + ")"); + RBACSpecReader reader = new RBACSpecReader(specFile.getAbsolutePath()); + RBACInstance rbac = reader.getRBAC(); + + rbac = optimizeRBAC(rbac, timerName); + + logger.info("[DETAILS] (after optimizing 2)Number of Roles: " + rbac.getNumRoles() + + "; Number of Rules: " + rbac.getNumRules()); + + if (rbac.getNumRoles() == 0) { + logger.info("[HEURISTIC #3a] There are no roles after optimization, thus the state isd UNREACHABLE " + + "and will not convert to SMV and run"); + continue; + } + + if (rbac.getNumRules() == 0) { + logger.info("[HEURISTIC #3b] There are no rules after optimization, thus the state isd UNREACHABLE " + + "and will not convert to SMV and run"); + continue; + } + + nusmv.fillAttributes(rbac); + + System.out.println("Number of role without rules: " + nusmv.roleWithoutRules); + System.out.println("Number of role with rules: " + nusmv.roleWithRules); + System.out.println("Ratio without / with: " + + (new Float(nusmv.roleWithoutRules) / nusmv.roleWithRules) + + "; without / total: " + + (new Float(nusmv.roleWithoutRules) / (nusmv.roleWithRules + nusmv.roleWithoutRules))); + + nusmv.writeFile(); // This option is available for testing purposes as there isn't a // practical reason to convert and immediately delete -- 2.26.2