Merge branch 'master' of bitbucket.org:jshahen/mohawk-2.0 into hotfix1

Conflicts:
	src/mohawk/MohawkCUI.java
	src/mohawk/refine/RolesAbsRefine.java

build.xml

@@ -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>

src/mohawk/MohawkCUI.java

@@ -84,6 +84,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("-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");
         System.out.println("");
         try {
             BufferedReader bfr = new BufferedReader(new FileReader(previousCommandFilename));

src/mohawk/MohawkInstance.java

@@ -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";
@@ -112,6 +113,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();
@@ -436,7 +438,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);

src/mohawk/helper/SMVSpecHelper.java

@@ -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 {

src/mohawk/nusmv/NuSMV.java

@@ -65,6 +65,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);
@@ -89,6 +90,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;

src/mohawk/output/smvtemplate.st

@@ -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

src/mohawk/rbac/RBACInstance.java

@@ -60,6 +60,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);
     }

src/mohawk/refine/RolesAbsRefine.java

@@ -317,14 +317,17 @@ public class RolesAbsRefine {
                     e1.printStackTrace();
                 }
 
-                // NuSMV bmc mode
-                int bound = CalculateDiameter.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) {
+                    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 {
                     result = NuSMV.SMC(nusmv.getNuSMVCode());
@@ -345,7 +348,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;
     }
 

src/mohawk/testing/MohawkRegressionTests.java

@@ -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();

src/mohawk/testing/TestingSuite.java

 package mohawk.testing;
 
 import java.io.File;
+import java.io.FileWriter;
 import java.io.IOException;
 import java.io.PrintWriter;
 import java.io.StringWriter;
@@ -98,18 +99,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);
 
@@ -202,6 +202,8 @@ public class TestingSuite {
         executor.shutdown();
         /* TIMING */timing.stopTimer("runTests.mainLoop");
 
+        
+        
         logger.exiting(getClass().getName(), "runTests()");
     }