Changes with respect to timing and testing; changes should have been commited...

Changes with respect to timing and testing; changes should have been commited a while ago, but was not due to forgetfulness
parent de89aff7
......@@ -97,7 +97,7 @@
<target name="regression" depends="dist" description="Performs a regression test">
<!-- @author Jonathan Shahen -->
<junit haltonfailure="true" printsummary="true">
<test name="mohawk.testing.RegressionTests" />
<test name="mohawk.testing.MohawkRegressionTests" />
<formatter type="plain" usefile="false" />
<classpath refid="test.classpath" />
</junit>
......
......@@ -67,5 +67,9 @@ public class MohawkCUI {
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");
System.out.println("");
System.out.println("-mode bmc -run all -bulk -input data/testcases/positive !exit");
System.out.println("-mode bmc -run all -bulk -input data/testcases/mixednocr !exit");
System.out.println("-mode bmc -run all -bulk -input data/testcases/mixed !exit");
}
}
......@@ -47,6 +47,7 @@ public class MohawkInstance {
private FileHandler fileHandler;
private Boolean WriteCSVFileHeader = true;
private String resultsFile = "latestMohawkResults.csv";
private String timingFile = "logs/MohawkTiming.csv";
// Reference
private String NuSMV_filepath = "NuSMV";
......@@ -108,6 +109,7 @@ public class MohawkInstance {
tests.done();
logger.info("[TIMING] " + tests.timing);
tests.timing.writeOut(new File(timingFile), false);
}
} catch (ParseException e) {
StringWriter errors = new StringWriter();
......@@ -432,7 +434,7 @@ public class MohawkInstance {
if (!Logger_filepath.isEmpty()) {
File f = new File(Logger_folderpath + File.separator);
f.mkdirs();
fileHandler = new FileHandler(Logger_folderpath + File.separator + Logger_filepath);
fileHandler = new FileHandler(Logger_folderpath + File.separator + Logger_filepath, true);
fileHandler.setLevel(getLoggerLevel());
fileHandler.setFormatter(new MohawkCSVFileFormatter());
logger.addHandler(fileHandler);
......
......@@ -5,6 +5,8 @@ import java.io.IOException;
import java.io.PrintWriter;
import java.io.StringWriter;
import java.util.ArrayList;
import java.util.Collections;
import java.util.Comparator;
import java.util.logging.Logger;
import mohawk.output.WriteNuSMV;
......@@ -57,6 +59,13 @@ public class SMVSpecHelper {
specFiles.add(f);
}
}
// Need to sort for linux
Collections.sort(specFiles, new Comparator<File>(){
public int compare(File p1, File p2) {
return p1.getName().compareToIgnoreCase(p2.getName());
}
});
}
public void addSpecFile(String path) throws IOException {
......
......@@ -62,6 +62,7 @@ public class NuSMV {
}
// Run the NuSMV engine using the specified command and input
// Returns TRUE is the QUERY is reachable, FALSE if it is unreachable
private static Boolean RunNuSMV(List<String> commands, String smvmodel) throws IOException, InterruptedException {
// Run the NuSMV engine
ProcessBuilder builder = new ProcessBuilder(commands);
......@@ -86,6 +87,7 @@ public class NuSMV {
System.out.println(_lastOutput.toString());
execProcess.waitFor();
if (_lastOutput.toString().indexOf("= FALSE is false") != -1) { return true; }
if (_lastOutput.toString().indexOf("false") != -1) { return true; }
return false;
......
......@@ -16,14 +16,11 @@ admin : {$admin; separator=","$};
role : $role$;
ASSIGN
-- Assigning UA
$ua; separator=";\n"$;
-- This section will contain state transition rules
$transitions; separator= "\n-- Another user \n" $
-- LTLSPEC
-- LTLSPEC: "G p" means that a certain condition p holds in all future time instants
LTLSPEC G ($user$[$roleindex$]=$falseWord$)
\ No newline at end of file
......@@ -58,6 +58,10 @@ public class RBACInstance {
return vRoles.size();
}
public int getNumRules() {
return mCR.size() + mCA.size();
}
public int getUserIndex(String inStrUser) throws Exception {
return getMapKey(mUserIndex, inStrUser);
}
......
......@@ -314,19 +314,23 @@ public class RolesAbsRefine {
} catch (IOException e1) {
e1.printStackTrace();
}
// NuSMV bmc mode
CalculateDiameter diameter = new CalculateDiameter();
int bound = diameter.GetDiameter(nextinstance);
System.out.println(String.format("Estimate Diameter - No of Roles %d Diameter %d",
nextinstance.getNumRoles(), bound));
System.out.printf("\n\n-----\n Starting Refinement Step %d, with %d Roles and %d Rules\n",
fileno, nextinstance.getNumRoles(), nextinstance.getNumRules());
// NuSMV bmc
Boolean result;
if (mode == NuSMVMode.BMC)
if (mode == NuSMVMode.BMC) {
CalculateDiameter diameter = new CalculateDiameter();
int bound = diameter.GetDiameter(nextinstance);
System.out.println(String.format("Estimate Diameter - No of Roles %d Diameter %d",
nextinstance.getNumRoles(), bound));
result = NuSMV.BMC(bound, nusmv.getNuSMVCode());
else
}
else {
result = NuSMV.SMC(nusmv.getNuSMVCode());
}
if (result) {
System.out.println("Found counter example in step " + (fileno));
......@@ -343,7 +347,7 @@ public class RolesAbsRefine {
return ExecutionResult.ERROR_OCCURRED;
}
System.out.println("No counter example found in " + (fileno - 1) + " refinement steps");
System.out.println("\n\n----\n No counter example found in " + (fileno - 1) + " refinement steps");
return ExecutionResult.GOAL_UNREACHABLE;
}
......
......@@ -18,7 +18,7 @@ public class MohawkRegressionTests {
@Test
public void runPositive1() {
String param = "-rbacspec data/regressiontests/positive1.spec -run all -mode bmc";
String param = "-input data/regressiontests/positive1.spec -run all -mode bmc";
ExecutionResult expectedResult = ExecutionResult.GOAL_REACHABLE;
MohawkInstance mohawk = new MohawkInstance();
......@@ -29,7 +29,7 @@ public class MohawkRegressionTests {
@Test
public void runPositive2() {
String param = "-rbacspec data/regressiontests/positive2.spec -run all -mode bmc";
String param = "-input data/regressiontests/positive2.spec -run all -mode bmc";
ExecutionResult expectedResult = ExecutionResult.GOAL_REACHABLE;
MohawkInstance mohawk = new MohawkInstance();
......@@ -40,7 +40,7 @@ public class MohawkRegressionTests {
@Test
public void runPositive3() {
String param = "-rbacspec data/regressiontests/positive3.spec -run all -mode bmc";
String param = "-input data/regressiontests/positive3.spec -run all -mode bmc";
ExecutionResult expectedResult = ExecutionResult.GOAL_REACHABLE;
MohawkInstance mohawk = new MohawkInstance();
......@@ -51,7 +51,7 @@ public class MohawkRegressionTests {
@Test
public void runPositive4() {
String param = "-rbacspec data/regressiontests/positive4.spec -run all -mode bmc";
String param = "-input data/regressiontests/positive4.spec -run all -mode bmc";
ExecutionResult expectedResult = ExecutionResult.GOAL_REACHABLE;
MohawkInstance mohawk = new MohawkInstance();
......
package mohawk.testing;
import java.io.File;
import java.io.FileWriter;
import java.io.IOException;
import java.io.PrintWriter;
import java.io.StringWriter;
......@@ -96,18 +97,17 @@ public class TestingSuite {
/* TIMING */timing.startTimer("smvHelper.loadSpecFiles");
smvHelper.loadSpecFiles();
/* TIMING */timing.stopTimer("smvHelper.loadSpecFiles");
/* TIMING */timing.startTimer("runTests.mainLoop");
ExecutorService executor = Executors.newSingleThreadExecutor();
Integer numSpecFiles = smvHelper.specFiles.size();
for (Integer i = 0; i < numSpecFiles; i++) {
/* TIMING */timing.startTimer("runTests.mainLoop (" + i + "/" + numSpecFiles + ")");
for (Integer j = 0; j < modes.size(); j++) {
String specFile = smvHelper.specFiles.get(i).getAbsolutePath();
String timerName = "runTests.mainLoop (" + i + "/" + numSpecFiles + ") - "
+ smvHelper.specFiles.get(i).getName() + " (" + modes.get(j) + ")";
String specFile = smvHelper.specFiles.get(i).getAbsolutePath();
String timerName = "runTests.mainLoop (" + i + "/" + numSpecFiles + ") - "
+ smvHelper.specFiles.get(i).getName() + " (" + modes.get(j) + ")";
/* TIMING */timing.startTimer(timerName);
logger.info("Working on " + timerName);
......@@ -200,6 +200,8 @@ public class TestingSuite {
executor.shutdown();
/* TIMING */timing.stopTimer("runTests.mainLoop");
logger.exiting(getClass().getName(), "runTests()");
}
......
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