Commit 60fd5eb2 authored by Jonathan Shahen's avatar Jonathan Shahen
Browse files

Working on creating a timeout for the Refinement Loop in Mohawk

parent 990ad7e2
...@@ -188,12 +188,20 @@ public class MohawkMain { ...@@ -188,12 +188,20 @@ public class MohawkMain {
// Add Functional Options // Add Functional Options
options.addOption("bulk", false, options.addOption("bulk", false,
"Use the folder that rbacspec points to and run against all *.spec"); "Use the folder that rbacspec points to and run against all *.spec");
options.addOption(OptionBuilder options.addOption(OptionBuilder
.withArgName("bmc|smc|both") .withArgName("bmc|smc|both")
.withDescription( .withDescription(
"Uses the Bound Estimation Checker when equal to 'bmc'; Uses Symbolic Model Checking when equal to 'smc'") "Uses the Bound Estimation Checker when equal to 'bmc'; Uses Symbolic Model Checking when equal to 'smc'")
.hasArg().create("mode")); .hasArg().create("mode"));
options.addOption(OptionBuilder
.withArgName("seconds")
.withDescription(
"The timeout time in seconds for Mohawk's refinement loop. Default: "
+ SMV_helper.TIMEOUT_SECONDS).hasArg()
.create("timeout"));
// Add Actionable Options // Add Actionable Options
options.addOption(OptionBuilder options.addOption(OptionBuilder
.withArgName("all|smv") .withArgName("all|smv")
...@@ -263,6 +271,15 @@ public class MohawkMain { ...@@ -263,6 +271,15 @@ public class MohawkMain {
+ cmd.getOptionValue("mode") + "'"); + cmd.getOptionValue("mode") + "'");
} }
} }
// Load more than one file from the SPEC File?
if (cmd.hasOption("timeout")) {
logger.fine("[OPTION] Timeout: " + cmd.getOptionValue("timeout")
+ " seconds");
SMV_helper.TIMEOUT_SECONDS = new Long(cmd.getOptionValue("timeout"));
} else {
logger.fine("[OPTION] Bulk SPEC File inclusion: Disabled");
}
} }
private static void setupUserPreferenceOptions(CommandLine cmd, private static void setupUserPreferenceOptions(CommandLine cmd,
......
...@@ -19,6 +19,7 @@ public class SMVSpecHelper { ...@@ -19,6 +19,7 @@ public class SMVSpecHelper {
public ArrayList<File> specFiles = new ArrayList<File>(); public ArrayList<File> specFiles = new ArrayList<File>();
public boolean bulk = false; public boolean bulk = false;
public int mode = 3; // 1 for bmc, 2 for smc, 3 for both public int mode = 3; // 1 for bmc, 2 for smc, 3 for both
public Long TIMEOUT_SECONDS = (long) 120; // Default 2 minutes
public void loadSpecFiles() throws IOException { public void loadSpecFiles() throws IOException {
if (this.bulk == true) { if (this.bulk == true) {
......
...@@ -28,7 +28,7 @@ public class MohawkConsoleFormatter extends Formatter { ...@@ -28,7 +28,7 @@ public class MohawkConsoleFormatter extends Formatter {
// Method Name // Method Name
builder.append(record.getSourceMethodName()).append(" #"); builder.append(record.getSourceMethodName()).append(" #");
// Thread ID // Thread ID
builder.append(record.getThreadID()).append("] - "); builder.append(record.getThreadID()).append("]:\n");
// Logging Level // Logging Level
String signifcantLevel = ""; String signifcantLevel = "";
char padChar = ' '; char padChar = ' ';
......
package mohawk.testing;
import java.util.concurrent.Callable;
import mohawk.RolesAbsRefine;
public class RunTest implements Callable<String> {
RolesAbsRefine absrefine;
public RunTest(RolesAbsRefine absrefine) {
this.absrefine = absrefine;
}
@Override
public String call() throws Exception {
absrefine.absrefineloop();
return "done";
}
}
...@@ -3,6 +3,13 @@ package mohawk.testing; ...@@ -3,6 +3,13 @@ package mohawk.testing;
import java.io.File; import java.io.File;
import java.io.IOException; import java.io.IOException;
import java.util.ArrayList; import java.util.ArrayList;
import java.util.concurrent.ExecutionException;
import java.util.concurrent.ExecutorService;
import java.util.concurrent.Executors;
import java.util.concurrent.Future;
import java.util.concurrent.TimeUnit;
import java.util.concurrent.TimeoutException;
import java.util.logging.Level;
import java.util.logging.Logger; import java.util.logging.Logger;
import mohawk.RBACInstance; import mohawk.RBACInstance;
...@@ -52,16 +59,44 @@ public class TestingSuite { ...@@ -52,16 +59,44 @@ public class TestingSuite {
+ new Integer(smvHelper.mode)); + new Integer(smvHelper.mode));
} }
timing.startTimer("smvHelper.loadSpecFiles");
smvHelper.loadSpecFiles(); smvHelper.loadSpecFiles();
timing.stopTimer("smvHelper.loadSpecFiles");
ExecutorService executor = Executors.newSingleThreadExecutor();
for (int i = 0; i < smvHelper.specFiles.size(); i++) { for (int i = 0; i < smvHelper.specFiles.size(); i++) {
for (int j = 0; j < modes.size(); j++) { for (int j = 0; j < modes.size(); j++) {
String specFile = smvHelper.specFiles.get(i).getAbsolutePath(); String specFile = smvHelper.specFiles.get(i).getAbsolutePath();
timing.startTimer(specFile);
RBACSpecReader reader = new RBACSpecReader(specFile); RBACSpecReader reader = new RBACSpecReader(specFile);
RBACInstance rbac = reader.getRBAC(); RBACInstance rbac = reader.getRBAC();
RolesAbsRefine absrefine = new RolesAbsRefine(rbac); RolesAbsRefine absrefine = new RolesAbsRefine(rbac);
absrefine.setMode(modes.get(j)); absrefine.setMode(modes.get(j));
absrefine.absrefineloop();
// Setup Timeout Timer
Future<String> future = executor.submit(new RunTest(absrefine));
try {
future.get(smvHelper.TIMEOUT_SECONDS, TimeUnit.SECONDS);
logger.info("[COMPLETED] The following spec file is completed testing for mode "
+ modes.get(j) + ": " + specFile);
timing.stopTimer(specFile);
} catch (TimeoutException e) {
logger.warning("[TIMEOUT] Mohawk has timed out for SPEC file: "
+ specFile);
timing.cancelTimer(specFile);
} catch (InterruptedException e) {
if (logger.getLevel() == Level.FINEST) {
e.printStackTrace();
}
logger.severe(e.getMessage());
} catch (ExecutionException e) {
if (logger.getLevel() == Level.FINEST) {
e.printStackTrace();
}
logger.severe(e.getMessage());
}
} }
} }
} }
......
Supports Markdown
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