Commit 61e4dd14 authored by Jonathan Shahen's avatar Jonathan Shahen

Lots of iterative work to find the bug....currently it looks like it is the...

Lots of iterative work to find the bug....currently it looks like it is the NuSMV version 2.5.4 that is buggy, but these bug hunt changes do provide much needed cleanup to the code (see the singleton MohawkSettings)
parent d3d07284
This diff is collapsed.
......@@ -8,28 +8,21 @@ 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");
public String smvFilepath = "latestRBAC2SMV.smv";
public String specFile = "";
public String specFileExt = ".mohawk";
private MohawkSettings settings = MohawkSettings.getInstance();
public ArrayList<File> specFiles = new ArrayList<File>();
public int mode = 3;// 1 for bmc, 2 for smc, 3 for both
public Long TIMEOUT_SECONDS = (long) 0;// Default infinite
public boolean bulk = false;
public Boolean smvDeleteFile = false;
public boolean sliceRBAC = true;
public boolean sliceRBACQuery = false;
public boolean skipRefine = true;
public void loadSpecFiles() throws IOException {
if (this.bulk == true) {
this.loadSpecFilesFromFolder(this.specFile);
if (settings.bulk == true) {
this.loadSpecFilesFromFolder(settings.specFile);
} else {
this.addSpecFile(this.specFile);
this.addSpecFile(settings.specFile);
}
}
......@@ -50,7 +43,7 @@ public class SMVSpecHelper {
}
for (File f : folder.listFiles()) {
if (f.getName().endsWith(specFileExt)) {
if (f.getName().endsWith(settings.specFileExt)) {
logger.fine("Adding file to specFiles: " + f.getAbsolutePath());
specFiles.add(f);
}
......@@ -96,7 +89,7 @@ public class SMVSpecHelper {
RBACSpecReader reader = new RBACSpecReader(specFile.getAbsolutePath());
RBACInstance rbac = reader.getRBAC();
if (sliceRBAC) {
if (settings.sliceRBAC) {
logger.info("[Slicing] Slicing the Spec File");
RoleSlicer roleslicer = new RoleSlicer(rbac);
......@@ -106,14 +99,14 @@ public class SMVSpecHelper {
+ (rbac.getCA().size() + rbac.getCR().size()));
}
if (sliceRBACQuery) {
if (settings.sliceRBACQuery) {
logger.info("[Slicing] Slicing the Spec's Query");
SliceQueryRole scRole = new SliceQueryRole(rbac);
rbac = scRole.getSlicedPolicy();
}
if (skipRefine) {
if (settings.skipRefine) {
nusmv.fillAttributes(rbac);
} else {
RolesAbsRefine absrefine = new RolesAbsRefine(rbac);
......@@ -140,7 +133,7 @@ public class SMVSpecHelper {
public File getSmvFile(File specFile) {
File nusmvFile = null;
if (smvDeleteFile) {
if (settings.smvDeleteFile) {
try {
nusmvFile = File.createTempFile("smvTempFile", ".smv");
} catch (IOException e) {
......@@ -150,10 +143,10 @@ public class SMVSpecHelper {
return nusmvFile;
}
if (bulk) {
if (settings.bulk) {
nusmvFile = new File(specFile.getAbsolutePath() + ".smv");
} else {
nusmvFile = new File(smvFilepath);
nusmvFile = new File(settings.smvFilepath);
}
if (!nusmvFile.exists()) {
......
package mohawk.singleton;
import java.util.logging.Level;
import mohawk.global.nusmv.NuSMV;
import mohawk.global.results.MohawkResults;
import mohawk.global.results.TestingResult;
import mohawk.global.timing.MohawkTiming;
import mohawk.helper.SMVSpecHelper;
import mohawk.testing.TestingSuite;
public class MohawkSettings {
private static volatile MohawkSettings _instance = null;
public String Logger_filepath = "mohawk.csv";
public String Logger_folderpath = "logs";
public Level LoggerLevel;
public Boolean WriteCSVFileHeader = true;
public String timingResultsFile = "logs/mohawkTimingResults.csv";
public String testingResultsFile = "logs/mohawkTestingResults.csv";
public String smvFilepath = "latestRBAC2SMV.smv";
// Reference
protected String NuSMV_filepath = "NuSMV";
public String getNuSMV_filepath() {
return NuSMV_filepath;
}
public void setNuSMV_filepath(String nuSMV_filepath) {
NuSMV_filepath = nuSMV_filepath;
NuSMV.NuSMVProcessName = nuSMV_filepath;
}
// Helpers
public MohawkResults results;
public MohawkTiming timing;
public TestingSuite tests;
public SMVSpecHelper smvHelper;
public TestingResult lastResult;
// SMV
public Long TIMEOUT_SECONDS = (long) 0;// Default infinite
public boolean bulk = false;
public Boolean smvDeleteFile = false;
public String specFile = "";
public String specFileExt = ".mohawk";
public int mode = 3;// 1 for bmc, 2 for smc, 3 for both
/**
* Flag for Slicing the RBAC Specification file before entering the Refinement Loop
*/
public boolean sliceRBAC = true;
/**
* Flag for Slicing the RBAC Specification Query before entering the Refinement Loop
*/
public boolean sliceRBACQuery = false;
/**
* Flag for skipping the abstraction-refinement step
*/
public boolean skipRefine = false;
protected MohawkSettings() {
}
public static MohawkSettings getInstance() {
if (_instance == null) {
_instance = new MohawkSettings();
}
return _instance;
}
@Override
public String toString() {
StringBuilder s = new StringBuilder();
s.append("MohawkSettings{");
s.append("sliceRBAC: ").append(sliceRBAC).append("; ");
s.append("sliceRBACQuery: ").append(sliceRBACQuery).append("; ");
s.append("skipRefine: ").append(skipRefine).append("; ");
s.append("NuSMV_filepath: ").append(NuSMV_filepath);
s.append("}");
return s.toString();
}
}
......@@ -6,6 +6,7 @@ import org.junit.Test;
import mohawk.MohawkInstance;
import mohawk.global.results.ExecutionResult;
import mohawk.singleton.MohawkSettings;
/**
* Run these JUnit tests before adding any branch to master
......@@ -25,7 +26,7 @@ public class MohawkRegressionTests {
MohawkInstance mohawk = new MohawkInstance();
mohawk.run(params(param));
assertEquals("The result was not correct!", expectedResult, mohawk.getTestingSuite().lastResult);
assertEquals("The result was not correct!", expectedResult, MohawkSettings.getInstance().lastResult);
}
@Test
......@@ -36,7 +37,7 @@ public class MohawkRegressionTests {
MohawkInstance mohawk = new MohawkInstance();
mohawk.run(params(param));
assertEquals("The result was not correct!", expectedResult, mohawk.getTestingSuite().lastResult);
assertEquals("The result was not correct!", expectedResult, MohawkSettings.getInstance().lastResult);
}
@Test
......@@ -47,7 +48,7 @@ public class MohawkRegressionTests {
MohawkInstance mohawk = new MohawkInstance();
mohawk.run(params(param));
assertEquals("The result was not correct!", expectedResult, mohawk.getTestingSuite().lastResult);
assertEquals("The result was not correct!", expectedResult, MohawkSettings.getInstance().lastResult);
}
@Test
......@@ -58,7 +59,7 @@ public class MohawkRegressionTests {
MohawkInstance mohawk = new MohawkInstance();
mohawk.run(params(param));
assertEquals("The result was not correct!", expectedResult, mohawk.getTestingSuite().lastResult);
assertEquals("The result was not correct!", expectedResult, MohawkSettings.getInstance().lastResult);
}
private String[] params(String param) {
......
package mohawk.testing;
import java.io.IOException;
import java.util.concurrent.Callable;
import java.util.logging.Logger;
import mohawk.global.results.ExecutionResult;
import mohawk.global.results.TestingResult;
import mohawk.output.WriteRBACSpec;
import mohawk.refine.RolesAbsRefine;
import mohawk.singleton.MohawkSettings;
public class TestRunner implements Callable<ExecutionResult> {
public class TestRunner implements Callable<TestingResult> {
public final static Logger logger = Logger.getLogger("mohawk");
public RolesAbsRefine absrefine = null;
public Boolean skipRefine = false;
private MohawkSettings settings = MohawkSettings.getInstance();
public TestRunner(RolesAbsRefine absrefine, boolean skipRefine) {
public TestRunner(RolesAbsRefine absrefine) {
this.absrefine = absrefine;
this.skipRefine = skipRefine;
}
@Override
public ExecutionResult call() throws Exception {
public TestingResult call() throws Exception {
ExecutionResult result = null;
if (skipRefine) {
if (settings.skipRefine) {
try {
WriteRBACSpec writer = new WriteRBACSpec("rbac.st");
writer.Write2File(absrefine.getInputRBACInstance(), "logs/rbacinstancefile" + 1 + ".txt");
} catch (IOException e1) {
e1.printStackTrace();
}
logger.info("[TestRunner] Skipping the Abstraction-Refinement Step");
Boolean counterExampleFound = absrefine.getResult(absrefine.getInputRBACInstance(), 1);
......@@ -35,7 +45,7 @@ public class TestRunner implements Callable<ExecutionResult> {
logger.info("[TestRunner] Running the Abstraction-Refinement Step");
result = absrefine.absrefineloop();
}
return result;
return new TestingResult(result, (long) 0, "", "Return Result: " + absrefine.getReturnValue());
}
}
This diff is collapsed.
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