Skip to content

mohawk-2.0
mohawk-2.0
Commit 9ff9ec5c authored by Jonathan Shahen's avatar Jonathan Shahen
Browse files
Options

Moving function convertSpecToSMVFormat() out of SMVSpecHelper and into the... 

Moving function convertSpecToSMVFormat() out of SMVSpecHelper and into the TestingSuite and adding better error warning into CalculateDiameter
parent 53db13b0
Hide whitespace changes
Inline Side-by-side
Showing with 59 additions and 86 deletions
src/mohawk/helper/SMVSpecHelper.java
View file @ 9ff9ec5c
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) {
......
src/mohawk/math/CalculateDiameter.java
View file @ 9ff9ec5c
......@@ -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<String> R_plus = crplus.getRPlus();
Set<String> R_minus = crplus.getRMinus();
Set<String> 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<String> R_plus = crplus.getRPlus();
Set<String> R_minus = crplus.getRMinus();
Set<String> RevRoles = crplus.CalIrrevocableRoles();
Set<String> R_plusonly = crplusonly.getRplusOnly();
//Set<String> RMaxRoles = rmax.CalRMax();
// Set<String> RMaxRoles = rmax.CalRMax();
Set<String> RUnionRoles = new HashSet<String>();
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<String, Integer> CalDiameterFile(String filename) {
public static Map<String, Integer> CalDiameterFile(String filename) throws IOException {
File rbacfile = new File(filename);
return CalDiameterFile(rbacfile);
}
public static Map<String, Integer> CalDiameterFile(File rbacfile) {
public static Map<String, Integer> 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<String> R_plus = crplus.getRPlus();
Set<String> R_minus = crplus.getRMinus();
Set<String> RevRoles = crplus.CalIrrevocableRoles();
Set<String> R_plusonly = crplusonly.getRplusOnly();
//Set<String> RMaxRoles = rmax.CalRMax();
// Set<String> RMaxRoles = rmax.CalRMax();
Set<String> RUnionRoles = new HashSet<String>();
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();
......
src/mohawk/testing/TestingSuite.java
View file @ 9ff9ec5c
......@@ -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
......
Markdown is supported
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