Commit de89aff7 authored by Jonathan Shahen's avatar Jonathan Shahen

fix for weird error for timing

parent b4474568
Pipeline #7930 skipped
......@@ -65,5 +65,7 @@ public class MohawkCUI {
System.out.println("-mode bmc -run all -bulk -input data/testcases/mixed !exit");
System.out.println("-mode bmc -run all -bulk -input data/reductions !exit");
System.out.println("");
System.out.println("-mode bmc -run all -bulk -input data/tests !exit");
System.out.println("-mode bmc -run smv -bulk -input data/tests !exit");
}
}
......@@ -36,7 +36,7 @@ import org.apache.commons.lang3.StringUtils;
public class MohawkInstance {
private final String VERSION = "v2.1.0";
private static final String AUTHORS = "Jonathan Shahen <jmshahen@uwaterloo.ca>; Karthick Jayaraman";
private static final String AUTHORS = "Jonathan Shahen <jmshahen [AT] uwaterloo [DOT] ca>; Karthick Jayaraman";
// Logger Fields
public static final Logger logger = Logger.getLogger("mohawk");
......
......@@ -2,6 +2,8 @@ package mohawk.helper;
import java.io.File;
import java.io.IOException;
import java.io.PrintWriter;
import java.io.StringWriter;
import java.util.ArrayList;
import java.util.logging.Logger;
......@@ -9,6 +11,8 @@ import mohawk.output.WriteNuSMV;
import mohawk.rbac.RBACInstance;
import mohawk.rbac.RBACSpecReader;
import mohawk.refine.RolesAbsRefine;
import mohawk.slicer.RoleSlicer;
import mohawk.slicer.SliceQueryRole;
public class SMVSpecHelper {
public final static Logger logger = Logger.getLogger("mohawk");
......@@ -20,6 +24,8 @@ public class SMVSpecHelper {
public boolean bulk = false;
public int mode = 3; // 1 for bmc, 2 for smc, 3 for both
public Long TIMEOUT_SECONDS = (long) 0; // Default infinite
public boolean sliceRBAC = true;
public boolean sliceRBACQuery = false;
public void loadSpecFiles() throws IOException {
if (this.bulk == true) {
......@@ -84,6 +90,30 @@ public class SMVSpecHelper {
RBACInstance rbac = reader.getRBAC();
RolesAbsRefine absrefine = new RolesAbsRefine(rbac);
try {
if (sliceRBAC) {
logger.info("[Slicing] Slicing the Spec File");
RoleSlicer roleslicer = new RoleSlicer(rbac);
rbac = roleslicer.getSlicedPolicy();
logger.info("[DETAILS] After Slicing -> Number of Roles: " + rbac.getNumRoles()
+ "; Number of Rules: " + (rbac.getCA().size() + rbac.getCR().size()));
}
if (sliceRBACQuery) {
logger.info("[Slicing] Slicing the Spec's Query");
SliceQueryRole scRole = new SliceQueryRole(rbac);
rbac = scRole.getSlicedPolicy();
}
} catch (Exception e) {
StringWriter errors = new StringWriter();
e.printStackTrace(new PrintWriter(errors));
logger.severe(errors.toString());
logger.severe(e.getMessage());
}
RBACInstance rbac_refined = absrefine.refineOnly();
WriteNuSMV nusmv = new WriteNuSMV(nusmvFile.getAbsolutePath(), "smvtemplate");
......
......@@ -195,7 +195,7 @@ public class TestingSuite {
logger.info("Previous Elapsed Time: " + timing.getLastElapsedTimeSec() + " seconds");
}
/* TIMING */timing.stopTimer("runTests.mainLoop (" + i + ")");
/* TIMING */timing.stopTimer("runTests.mainLoop (" + i + "/" + numSpecFiles + ")");
}
executor.shutdown();
/* TIMING */timing.stopTimer("runTests.mainLoop");
......
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