Commit 5107a615 authored by Jonathan Shahen's avatar Jonathan Shahen
Browse files

Finished Mohawk-22 and moved files to Globals repo

parent 26e5c71f
......@@ -29,5 +29,6 @@
</attributes>
</classpathentry>
<classpathentry kind="con" path="org.eclipse.jdt.junit.JUNIT_CONTAINER/4"/>
<classpathentry combineaccessrules="false" kind="src" path="/Mohawk-T Globals"/>
<classpathentry kind="output" path="bin"/>
</classpath>
0 role149
1 role128
2 role77
3 role86
4 role198
5 role155
6 role123
7 role115
8 role200
......@@ -4,6 +4,9 @@
<project name="mohawk" default="dist" basedir=".">
<description>Mohawk Tool Implementation.</description>
<!-- Properties for the JAR file -->
<property name="user.name" location="Jonathan Shahen" />
<!-- set global properties for this build -->
<property name="src" location="src" />
<property name="lib" location="lib" />
......@@ -16,6 +19,18 @@
<property name="template" location="${mohawksrc}/output" />
<property name="rbac" location="${mohawksrc}/rbac/generated" />
<property name="antlr" location="${lib}/antlr-3.2.jar" />
<property name="junit" location="${lib}/junit-4.12.jar" />
<!-- Customize this line to point to the 'Mohawk-T Globals' Project's source folder -->
<property name="src.globals" location="../Mohawk-T Globals/src" />
<path id="test.classpath">
<pathelement location="${build}" />
<pathelement location="${junit}" />
<fileset dir="${lib}">
<include name="**/*.jar" />
</fileset>
</path>
<target name="init">
<!-- create the bin directory -->
......@@ -38,6 +53,8 @@
<target name="compile" depends="parser" description="compile the source ">
<!-- compile the java code from ${src} into ${build} -->
<javac srcdir="${src}" destdir="${build}" debug="on" deprecation="true">
<src path="${src}" />
<src path="${src.globals}" />
<classpath>
<fileset dir="${lib}">
<include name="**/*.jar" />
......@@ -79,10 +96,18 @@
<target name="regression" depends="dist" description="Performs a regression test">
<!-- @author Jonathan Shahen -->
<junit haltonfailure="true" printsummary="true">
<test name="mohawk.testing.RegressionTests" />
<formatter type="plain" usefile="false" />
<classpath refid="test.classpath" />
</junit>
<!-- OLD Windows ONLY running JUnit through the commandline
<exec executable="cmd" dir="${dist}" failonerror="true">
<arg value="/c" />
<arg value="java -jar mohawk.jar -mode bmc -run all -rbacspec ../../data/regressiontests/positive1.spec" />
</exec>
-->
</target>
<target name="clean" description="clean up">
......
This diff is collapsed.
......@@ -10,10 +10,10 @@ import java.util.logging.FileHandler;
import java.util.logging.Level;
import java.util.logging.Logger;
import mohawk.global.MohawkCSVFileFormatter;
import mohawk.global.MohawkConsoleFormatter;
import mohawk.global.MohawkTiming;
import mohawk.helper.SMVSpecHelper;
import mohawk.logging.MohawkCSVFileFormatter;
import mohawk.logging.MohawkConsoleFormatter;
import mohawk.logging.MohawkTiming;
import mohawk.testing.TestingResults;
import mohawk.testing.TestingSuite;
......
package mohawk.helper;
public enum MohawkResult {
GOAL_REACHABLE, GOAL_UNREACHABLE, ERROR_OCCURRED, TIMEOUT, OUT_OF_MEMORY
}
package mohawk.logging;
import java.text.DateFormat;
import java.text.SimpleDateFormat;
import java.util.Date;
import java.util.logging.Formatter;
import java.util.logging.Handler;
import java.util.logging.LogRecord;
import java.util.logging.Logger;
import org.apache.commons.lang3.StringEscapeUtils;
public class MohawkCSVFileFormatter extends Formatter {
public final static Logger logger = Logger.getLogger("mohawk");
private static final DateFormat df = new SimpleDateFormat("yyyy/MM/dd hh:mm:ss.SSSZ");
public String format(LogRecord record) {
StringBuilder builder = new StringBuilder(1000);
builder.append(df.format(new Date(record.getMillis()))).append(",");
builder.append(record.getSourceClassName()).append(",");
builder.append(record.getSourceMethodName()).append(",");
builder.append(record.getLevel()).append(",");
builder.append(StringEscapeUtils.escapeCsv(formatMessage(record)));
builder.append("\n");
return builder.toString();
}
public static String csvHeaders() {
StringBuilder builder = new StringBuilder(100);
builder.append("Datetime").append(",");
builder.append("Classname").append(",");
builder.append("Method").append(",");
builder.append("Level").append(",");
builder.append("Message");
builder.append("\n");
return builder.toString();
}
public String getHead(Handler h) {
return super.getHead(h);
}
public String getTail(Handler h) {
return super.getTail(h);
}
}
package mohawk.logging;
import java.text.DateFormat;
import java.text.SimpleDateFormat;
import java.util.Date;
import java.util.logging.Formatter;
import java.util.logging.Handler;
import java.util.logging.Level;
import java.util.logging.LogRecord;
import java.util.logging.Logger;
import org.apache.commons.lang3.text.WordUtils;
public class MohawkConsoleFormatter extends Formatter {
public final static Logger logger = Logger.getLogger("mohawk");
private static final DateFormat df = new SimpleDateFormat("yyyy/MM/dd hh:mm:ss.SSSZ");
public Integer padLeft = Level.WARNING.toString().length() + 1;
public Integer maxWidth = 0;
public String newLineStr = "\n ";
public String format(LogRecord record) {
StringBuilder builder = new StringBuilder(1000);
// Date Time
builder.append(df.format(new Date(record.getMillis()))).append(" - ");
// Class Name
builder.append("[").append(record.getSourceClassName()).append(".");
// Method Name
builder.append(record.getSourceMethodName()).append(" #");
// Thread ID
builder.append(record.getThreadID()).append("]:\n");
// Logging Level
String signifcantLevel = "";
char padChar = ' ';
if (record.getLevel() == Level.WARNING || record.getLevel() == Level.SEVERE) {
signifcantLevel = "";
padChar = '*';
}
builder.append("[");
builder.append(String.format("%1$" + signifcantLevel + padLeft + "s", record.getLevel()).replace(' ', padChar));
builder.append("] ");
// Message
builder.append(formatMessage(record));
builder.append("\n"); // End of Message
if (maxWidth == 0) {
return builder.toString();
} else {
return WordUtils.wrap(builder.toString(), maxWidth, newLineStr, true);
}
}
/**
* Get the current line number.
*
* @return int - Current line number.
*/
public static int getLineNumber() {
return Thread.currentThread().getStackTrace()[2].getLineNumber();
}
public String getHead(Handler h) {
return super.getHead(h);
}
public String getTail(Handler h) {
return super.getTail(h);
}
}
package mohawk.logging;
import java.util.Hashtable;
import java.util.Map;
public class MohawkTiming {
private Map<String, Long> timings = new Hashtable<String, Long>();
public Map<String, Long> getTimings() {
return timings;
}
public void startTimer(String key) {
timings.put(key, System.currentTimeMillis());
}
public void stopTimer(String key) {
timings.put(key, System.currentTimeMillis() - (Long) timings.get(key));
}
/**
* Used to indicate that the operation failed after a certain amount of time by calculating the time difference and
* then multiplying by -1. If the elapsed time is zero then the time will be changed to -1.
*
* @param key
*/
public void cancelTimer(String key) {
Long time = (System.currentTimeMillis() - (Long) timings.get(key)) * -1;
if (time == 0) {
time = (long) -1;
}
timings.put(key, time);
}
@Override
public String toString() {
StringBuilder t = new StringBuilder();
int i = 0;
for (Map.Entry<String, Long> entry : timings.entrySet()) {
t.append(entry.getKey() + ": ");
t.append(entry.getValue());
t.append("ms");
i++;
if (i != timings.size()) {
t.append(" - ");
}
}
return t.toString();
}
}
......@@ -14,7 +14,7 @@ import java.util.Vector;
import mohawk.collections.NuSMVMode;
import mohawk.collections.RoleDepTree;
import mohawk.helper.MohawkResult;
import mohawk.global.TestResult;
import mohawk.math.CalculateDiameter;
import mohawk.nusmv.NuSMV;
import mohawk.output.WriteNuSMV;
......@@ -302,7 +302,7 @@ public class RolesAbsRefine {
return result;
}
public MohawkResult absrefineloop() {
public TestResult absrefineloop() {
int fileno = 1;
try {
......@@ -334,7 +334,7 @@ public class RolesAbsRefine {
if (result) {
System.out.println("Found counter example in step " + (fileno));
WriteMapping(nextinstance, "ROLEMAPPING");
return MohawkResult.GOAL_REACHABLE;
return TestResult.GOAL_REACHABLE;
} else {
System.out.println("No counter example found in refinement step " + fileno);
}
......@@ -344,11 +344,11 @@ public class RolesAbsRefine {
} catch (Exception e) {
// TODO Auto-generated catch block
e.printStackTrace();
return MohawkResult.ERROR_OCCURRED;
return TestResult.ERROR_OCCURRED;
}
System.out.println("No counter example found in " + (fileno - 1) + " refinement steps");
return MohawkResult.GOAL_UNREACHABLE;
return TestResult.GOAL_UNREACHABLE;
}
/**
......
......@@ -2,7 +2,7 @@ package mohawk.testing;
import static org.junit.Assert.assertEquals;
import mohawk.MohawkInstance;
import mohawk.helper.MohawkResult;
import mohawk.global.TestResult;
import org.junit.Test;
......@@ -18,8 +18,8 @@ public class RegressionTests {
@Test
public void runPositive1() {
String param = "-rbacspec ./data/regressiontests/positive1.spec -run all -mode bmc";
MohawkResult expectedResult = MohawkResult.GOAL_REACHABLE;
String param = "-rbacspec data/regressiontests/positive1.spec -run all -mode bmc";
TestResult expectedResult = TestResult.GOAL_REACHABLE;
MohawkInstance mohawk = new MohawkInstance();
mohawk.run(params(param));
......@@ -29,8 +29,8 @@ public class RegressionTests {
@Test
public void runPositive2() {
String param = "-rbacspec ./data/regressiontests/positive2.spec -run all -mode bmc";
MohawkResult expectedResult = MohawkResult.GOAL_REACHABLE;
String param = "-rbacspec data/regressiontests/positive2.spec -run all -mode bmc";
TestResult expectedResult = TestResult.GOAL_REACHABLE;
MohawkInstance mohawk = new MohawkInstance();
mohawk.run(params(param));
......@@ -40,8 +40,8 @@ public class RegressionTests {
@Test
public void runPositive3() {
String param = "-rbacspec ./data/regressiontests/positive3.spec -run all -mode bmc";
MohawkResult expectedResult = MohawkResult.GOAL_REACHABLE;
String param = "-rbacspec data/regressiontests/positive3.spec -run all -mode bmc";
TestResult expectedResult = TestResult.GOAL_REACHABLE;
MohawkInstance mohawk = new MohawkInstance();
mohawk.run(params(param));
......@@ -51,8 +51,8 @@ public class RegressionTests {
@Test
public void runPositive4() {
String param = "-rbacspec ./data/regressiontests/positive4.spec -run all -mode bmc";
MohawkResult expectedResult = MohawkResult.GOAL_REACHABLE;
String param = "-rbacspec data/regressiontests/positive4.spec -run all -mode bmc";
TestResult expectedResult = TestResult.GOAL_REACHABLE;
MohawkInstance mohawk = new MohawkInstance();
mohawk.run(params(param));
......
......@@ -2,10 +2,10 @@ package mohawk.testing;
import java.util.concurrent.Callable;
import mohawk.helper.MohawkResult;
import mohawk.global.TestResult;
import mohawk.refine.RolesAbsRefine;
public class RunTest implements Callable<MohawkResult> {
public class RunTest implements Callable<TestResult> {
RolesAbsRefine absrefine;
public RunTest(RolesAbsRefine absrefine) {
......@@ -13,8 +13,8 @@ public class RunTest implements Callable<MohawkResult> {
}
@Override
public MohawkResult call() throws Exception {
MohawkResult result = absrefine.absrefineloop();
public TestResult call() throws Exception {
TestResult result = absrefine.absrefineloop();
return result;
}
......
package mohawk.testing;
/**
*
* @author Jonathan Shahen
*
*/
public class TestResults {
public TestResults(String resultsFile) {
}
}
......@@ -6,6 +6,8 @@ import java.io.IOException;
import java.util.ArrayList;
import java.util.logging.Logger;
import mohawk.global.TestResult;
/**
*
* @author Jonathan Shahen
......@@ -15,7 +17,7 @@ import java.util.logging.Logger;
public class TestingResults {
public final static Logger logger = Logger.getLogger("mohawk");
public FileOutputStream writer = null;
public ArrayList<TestResults> history = new ArrayList<TestResults>();
public ArrayList<TestResult> history = new ArrayList<TestResult>();
public TestingResults(String resultsFile) {
try {
......@@ -41,11 +43,11 @@ public class TestingResults {
}
}
public void addTestResult(TestResults result) {
public void addTestResult(TestResult result) {
this.addTestResults(result, true, true);
}
public void addTestResults(TestResults result, boolean writeToConsole, boolean writeToFile) {
public void addTestResults(TestResult result, boolean writeToConsole, boolean writeToFile) {
history.add(result);
if (writeToConsole == true) {
writeToConsole(result);
......@@ -55,12 +57,12 @@ public class TestingResults {
}
}
public void writeToConsole(TestResults results) {
public void writeToConsole(TestResult results) {
// TODO Auto-generated method stub
}
public void writeToFile(TestResults results) {
public void writeToFile(TestResult results) {
// TODO Auto-generated method stub
}
......
......@@ -13,9 +13,9 @@ import java.util.logging.Level;
import java.util.logging.Logger;
import mohawk.collections.NuSMVMode;
import mohawk.helper.MohawkResult;
import mohawk.global.MohawkTiming;
import mohawk.global.TestResult;
import mohawk.helper.SMVSpecHelper;
import mohawk.logging.MohawkTiming;
import mohawk.rbac.RBACInstance;
import mohawk.rbac.RBACSpecReader;
import mohawk.refine.RolesAbsRefine;
......@@ -26,7 +26,10 @@ public class TestingSuite {
public TestingResults results;
public MohawkTiming timing;
public SMVSpecHelper smvHelper;
public MohawkResult lastResult;
public TestResult lastResult;
public String timingResultsFile = "logs/mohawkTimingResults.csv";
public String testingResultsFile = "logs/mohawkTestingResults.csv";
public TestingSuite(SMVSpecHelper smvHelper, TestingResults results, MohawkTiming timing) {
this.smvHelper = smvHelper;
......@@ -35,8 +38,19 @@ public class TestingSuite {
this.timing.startTimer("totalTime");
}
public void done() {
public Boolean done() {
this.timing.stopTimer("totalTime");
File results = new File(timingResultsFile);
try {
this.timing.writeOut(results);
} catch (IOException e) {
logger.warning("[TIMING] Unable to save the Timing Results to the file: " + results.getAbsolutePath());
return false;
}
logger.info("[TIMING] Saved Timing Results to the file: " + results.getAbsolutePath());
return true;
}
/**
......@@ -86,7 +100,7 @@ public class TestingSuite {
absrefine.setMode(modes.get(j));
// Setup Timeout Timer
Future<MohawkResult> future = executor.submit(new RunTest(absrefine));
Future<TestResult> future = executor.submit(new RunTest(absrefine));
try {
logger.info("[RUNNING] Running Mohawk on testcase " + i + " (mode=" + modes.get(j) + "):");
......@@ -99,13 +113,13 @@ public class TestingSuite {
} catch (TimeoutException e) {
logger.warning("[TIMEOUT] Mohawk has timed out for SPEC file: " + specFile);
lastResult = MohawkResult.TIMEOUT;
lastResult = TestResult.TIMEOUT;
/* TIMING */timing.cancelTimer(timerName);
} catch (OutOfMemoryError e) {
logger.warning("[OUT OF MEMORY] Mohawk has ran out of memory out for SPEC file: " + specFile);
lastResult = MohawkResult.OUT_OF_MEMORY;
lastResult = TestResult.OUT_OF_MEMORY;
/* TIMING */timing.cancelTimer(timerName);
} catch (InterruptedException e) {
......
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