Gold Copy of the code, all original testcase are tested and confirmed to...

Gold Copy of the code, all original testcase are tested and confirmed to reflect the times in the Karthick Paper

README.md

@@ -6,7 +6,7 @@
  *	
  * BEGIN DATE: October, 2009
  *
- * LICENSE: Please view LICENSE file in the home dir of this Programtt
+ * LICENSE: Please view LICENSE file in the home dir of this Program
  ********************************************************************/
 
 

ROLEMAPPING

-0 role149
-1 role128
-2 role77
-3 role86
-4 role198
-5 role155
-6 role123
-7 role115
-8 role200

src/mohawk/MohawkCUI.java

@@ -54,11 +54,15 @@ public class MohawkCUI {
 
     public static void printCommonCommands() {
         System.out.println("\n\n--- Common Commands ---");
-        System.out.println("-noheader -mode bmc -run all -rbacspec data/regressiontests/positive1.spec !exit");
-        System.out.println("-noheader -mode bmc -run all -rbacspec data/regressiontests/positive2.spec !exit");
-        System.out.println("-noheader -mode bmc -run all -rbacspec data/regressiontests/positive3.spec !exit");
-        System.out.println(" !exit");
-        System.out.println(" !exit");
+        System.out.println("-noheader -mode bmc -run all -input data/regressiontests/positive1.spec !exit");
+        System.out.println("-noheader -mode bmc -run all -input data/regressiontests/positive2.spec !exit");
+        System.out.println("-noheader -mode bmc -run all -input data/regressiontests/positive3.spec !exit");
+        System.out.println("-run smv -input data/testcases/positive/test7.spec -smvfile positive7.smv !exit");
+        System.out.println("-mode bmc -run all -input data/testcases/positive/test6.spec !exit");
+        System.out.println("-mode bmc -run all -input data/testcases/positive/slice6.spec !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("");
     }
 }

src/mohawk/MohawkInstance.java

@@ -77,13 +77,21 @@ public class MohawkInstance {
             setupResultOptions(cmd, options);
 
             // Execute the test cases
-            if (cmd.hasOption("run")) {
+            if (cmd.hasOption(OptionString.RUN.toString())) {
                 logger.info("[ACTION] Run paramter detected");
                 results = new MohawkResults();
                 timing = new MohawkTiming();
                 tests = new TestingSuite(SMV_helper, results, timing);
 
-                String runVal = cmd.getOptionValue("run");
+                if (cmd.hasOption(OptionString.NOSLICING.toString())) {
+                    tests.sliceRBAC = false;
+                }
+
+                if (cmd.hasOption(OptionString.SLICEQUERY.toString())) {
+                    tests.sliceRBACQuery = true;
+                }
+
+                String runVal = cmd.getOptionValue(OptionString.RUN.toString());
                 switch (runVal) {
                 case "all":
                     logger.info("[ACTION] Will convert and then execute the testcase provided");
@@ -117,6 +125,8 @@ public class MohawkInstance {
             return -1;
         }
 
+        logger.info("[EOF] Mohawk is done running");
+
         return 0;
     }
 
@@ -135,9 +145,9 @@ public class MohawkInstance {
     @SuppressWarnings("static-access")
     public void setupOptions(Options options) {
         // Add Information Options
-        options.addOption("help", false, "Print this message");
-        options.addOption("version", false, "Prints the version (" + VERSION + ") information");
-        options.addOption("checknusmv", false,
+        options.addOption(OptionString.HELP.toString(), false, "Print this message");
+        options.addOption(OptionString.VERSION.toString(), false, "Prints the version (" + VERSION + ") information");
+        options.addOption(OptionString.CHECKNUSMV.toString(), false,
                 "Checks that NuSMV is on the system and displays which version is installed");
 
         // Add Logging Level Options
@@ -146,7 +156,7 @@ public class MohawkInstance {
                 .withDescription(
                         "Be extra quiet only errors are shown; " + "Show debugging information; "
                                 + "extra information is given for Verbose; " + "default is warning level").hasArg()
-                .create("loglevel"));
+                .create(OptionString.LOGLEVEL.toString()));
 
         options.addOption(OptionBuilder
                 .withArgName("logfile|'n'|'u'")
@@ -155,33 +165,38 @@ public class MohawkInstance {
                                 + "No file will be created when equal to 'n'; "
                                 + "A unique filename will be created when equal to 'u'; "
                                 + "default it creates a log called '" + Logger_filepath + "'").hasArg()
-                .create("logfile"));
+                .create(OptionString.LOGFILE.toString()));
 
         options.addOption(OptionBuilder
                 .withArgName("folderpath")
                 .withDescription(
                         "The folderpath where the log file should be created; "
-                                + "default it creates in the current directory").hasArg().create("logfolder"));
+                                + "default it creates in the current directory").hasArg()
+                .create(OptionString.LOGFOLDER.toString()));
 
-        options.addOption("noheader", false, "Does not write the CSV file header to the output log");
+        options.addOption(OptionString.NOHEADER.toString(), false,
+                "Does not write the CSV file header to the output log");
 
         options.addOption(OptionBuilder.withArgName("csvfile")
-                .withDescription("The file where the result should be stored").hasArg().create("results"));
+                .withDescription("The file where the result should be stored").hasArg()
+                .create(OptionString.RESULTSFILE.toString()));
 
         // custom Console Logging Options
         options.addOption(OptionBuilder.withArgName("num")
-                .withDescription("The maximum width of the console (default 120)").hasArg().create("maxw"));
+                .withDescription("The maximum width of the console (default 120)").hasArg()
+                .create(OptionString.MAXW.toString()));
         options.addOption(OptionBuilder.withArgName("string")
                 .withDescription("The new line string when wrapping a long line (default '\\n    ')").hasArg()
-                .create("linestr"));
+                .create(OptionString.LINESTR.toString()));
 
         // Add File IO Options
         options.addOption(OptionBuilder.withArgName("file|folder")
                 .withDescription("Path to the RBAC Spec file or Folder if the 'bulk' option is set").hasArg()
-                .create("rbacspec"));
+                .create(OptionString.SPECFILE.toString()));
 
         options.addOption(OptionBuilder.withArgName("filepath")
-                .withDescription("Path to the NuSMV program file (defaults to 'NuSMV')").hasArg().create("nusmv"));
+                .withDescription("Path to the NuSMV program file (defaults to 'NuSMV')").hasArg()
+                .create(OptionString.NUSMVPATH.toString()));
 
         options.addOption(OptionBuilder
                 .withArgName("smvfile|'n'")
@@ -189,41 +204,46 @@ public class MohawkInstance {
                         "The file/folder path where the SMV file(s) should be created; "
                                 + "Only temporary files will be used when equal to 'n'; "
                                 + "by default it creates a SMV called '" + SMV_helper.smvFilepath + "'").hasArg()
-                .create("smvfile"));
+                .create(OptionString.SMVFILE.toString()));
 
         options.addOption(OptionBuilder
                 .withArgName("extension")
                 .withDescription(
                         "File extention used when searching for SPEC files when the 'bulk' option is used. Default:'"
-                                + SMV_helper.specFileExt + "'").hasArg().create("specext"));
+                                + SMV_helper.specFileExt + "'").hasArg().create(OptionString.SPECEXT.toString()));
 
         // Add Functional Options
-        options.addOption("bulk", false, "Use the folder that rbacspec points to and run against all *.spec");
+        options.addOption(OptionString.BULK.toString(), false,
+                "Use the folder that rbacspec points to and run against all *.spec");
+        options.addOption(OptionString.NOSLICING.toString(), false,
+                "Turns off the slicing of the RBAC Inpuit Spec file (Slices by default)");
+        options.addOption(OptionString.SLICEQUERY.toString(), false,
+                "Turns on the slicing of the RBAC Inpuit Spec Query (Does not slice by default)");
 
         options.addOption(OptionBuilder
                 .withArgName("bmc|smc|both")
                 .withDescription(
                         "Uses the Bound Estimation Checker when equal to 'bmc'; Uses Symbolic Model Checking when equal to 'smc'")
-                .hasArg().create("mode"));
+                .hasArg().create(OptionString.MODE.toString()));
 
         options.addOption(OptionBuilder
                 .withArgName("seconds")
                 .withDescription(
                         "The timeout time in seconds for Mohawk's refinement loop. Default: "
-                                + SMV_helper.TIMEOUT_SECONDS).hasArg().create("timeout"));
+                                + SMV_helper.TIMEOUT_SECONDS).hasArg().create(OptionString.TIMEOUT.toString()));
 
         // Add Actionable Options
         options.addOption(OptionBuilder
                 .withArgName("all|smv")
                 .withDescription(
                         "Runs the whole model checker when equal to 'all'; Runs only the SMV conversion when equal to 'smv'")
-                .hasArg().create("run"));
+                .hasArg().create(OptionString.RUN.toString()));
     }
 
     public void printHelp(CommandLine cmd, Options options) throws Exception {
-        if (cmd.hasOption("maxw")) {
+        if (cmd.hasOption(OptionString.MAXW.toString())) {
             try {
-                Integer maxw = Integer.decode(cmd.getOptionValue("maxw"));
+                Integer maxw = Integer.decode(cmd.getOptionValue(OptionString.MAXW.toString()));
                 printHelp(options, maxw);
             } catch (Exception e) {
                 printHelp(options, 80);
@@ -246,35 +266,37 @@ public class MohawkInstance {
     private void setupSmvSpecOptions(CommandLine cmd, Options options) {
         // Load in SPEC Files
         // SMV File
-        if (cmd.hasOption("smvfile")) {
-            if (cmd.getOptionValue("smvfile").equals("n")) {
+        if (cmd.hasOption(OptionString.SMVFILE.toString())) {
+            if (cmd.getOptionValue(OptionString.SMVFILE.toString()).equals("n")) {
                 logger.fine("[OPTION] Using temporary SMV Files - will be deleted after each use");
                 SMV_helper.smvDeleteFile = true;
             } else {
-                logger.fine("[OPTION] Using a specific SMV File: " + cmd.getOptionValue("smvfile"));
-                SMV_helper.smvFilepath = cmd.getOptionValue("smvfile");
+                logger.fine("[OPTION] Using a specific SMV File: "
+                        + cmd.getOptionValue(OptionString.SMVFILE.toString()));
+                SMV_helper.smvFilepath = cmd.getOptionValue(OptionString.SMVFILE.toString());
             }
         } else {
             logger.fine("[OPTION] No SMV Filename included, saving file under: " + SMV_helper.smvFilepath);
         }
 
         // Grab the SPEC file
-        if (cmd.hasOption("rbacspec")) {
-            logger.fine("[OPTION] Using a specific SPEC File: " + cmd.getOptionValue("rbacspec"));
-            SMV_helper.specFile = cmd.getOptionValue("rbacspec");
+        if (cmd.hasOption(OptionString.SPECFILE.toString())) {
+            logger.fine("[OPTION] Using a specific SPEC File: " + cmd.getOptionValue(OptionString.SPECFILE.toString()));
+            SMV_helper.specFile = cmd.getOptionValue(OptionString.SPECFILE.toString());
         } else {
             logger.fine("[OPTION] No Spec File included");
         }
 
-        if (cmd.hasOption("specext")) {
-            logger.fine("[OPTION] Using a specific SPEC File Extension: " + cmd.getOptionValue("specext"));
-            SMV_helper.specFileExt = cmd.getOptionValue("specext");
+        if (cmd.hasOption(OptionString.SPECEXT.toString())) {
+            logger.fine("[OPTION] Using a specific SPEC File Extension: "
+                    + cmd.getOptionValue(OptionString.SPECEXT.toString()));
+            SMV_helper.specFileExt = cmd.getOptionValue(OptionString.SPECEXT.toString());
         } else {
             logger.fine("[OPTION] Using the default SPEC File Extension: " + SMV_helper.specFileExt);
         }
 
         // Load more than one file from the SPEC File?
-        if (cmd.hasOption("bulk")) {
+        if (cmd.hasOption(OptionString.BULK.toString())) {
             logger.fine("[OPTION] Bulk SPEC File inclusion: Enabled");
             SMV_helper.bulk = true;
         } else {
@@ -282,8 +304,8 @@ public class MohawkInstance {
         }
 
         // Set the Mode of Operation for Converting SPEC to SMV
-        if (cmd.hasOption("mode")) {
-            switch (cmd.getOptionValue("mode")) {
+        if (cmd.hasOption(OptionString.MODE.toString())) {
+            switch (cmd.getOptionValue(OptionString.MODE.toString())) {
             case "bmc":
                 SMV_helper.mode = 1;
                 break;
@@ -294,14 +316,14 @@ public class MohawkInstance {
                 SMV_helper.mode = 3;
                 break;
             default:
-                logger.severe("[ERROR] Unknown mode: '" + cmd.getOptionValue("mode") + "'");
+                logger.severe("[ERROR] Unknown mode: '" + cmd.getOptionValue(OptionString.MODE.toString()) + "'");
             }
         }
 
         // 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"));
+        if (cmd.hasOption(OptionString.TIMEOUT.toString())) {
+            logger.fine("[OPTION] Timeout: " + cmd.getOptionValue(OptionString.TIMEOUT.toString()) + " seconds");
+            SMV_helper.TIMEOUT_SECONDS = new Long(cmd.getOptionValue(OptionString.TIMEOUT.toString()));
         } else {
             logger.fine("[OPTION] Bulk SPEC File inclusion: Disabled");
         }
@@ -309,11 +331,11 @@ public class MohawkInstance {
 
     private void setupUserPreferenceOptions(CommandLine cmd, Options options) {
         // Set the Console's Max Width
-        if (cmd.hasOption("maxw")) {
+        if (cmd.hasOption(OptionString.MAXW.toString())) {
             logger.fine("[OPTION] Setting the console's maximum width");
             String maxw = "";
             try {
-                maxw = cmd.getOptionValue("maxw");
+                maxw = cmd.getOptionValue(OptionString.MAXW.toString());
                 ((MohawkConsoleFormatter) consoleHandler.getFormatter()).maxWidth = Integer.decode(maxw);
             } catch (NumberFormatException e) {
                 logger.severe("[ERROR] Could not decode 'maxw': " + maxw + ";\n" + e.getMessage());
@@ -323,9 +345,10 @@ public class MohawkInstance {
         }
 
         // Set the Console's Wrap String
-        if (cmd.hasOption("linestr")) {
+        if (cmd.hasOption(OptionString.LINESTR.toString())) {
             logger.fine("[OPTION] Setting the console's new line string");
-            ((MohawkConsoleFormatter) consoleHandler.getFormatter()).newLineStr = cmd.getOptionValue("linestr");
+            ((MohawkConsoleFormatter) consoleHandler.getFormatter()).newLineStr = cmd
+                    .getOptionValue(OptionString.LINESTR.toString());
         } else {
             logger.fine("[OPTION] Default Line String Used");
         }
@@ -337,8 +360,8 @@ public class MohawkInstance {
         logger.setUseParentHandlers(false);
         consoleHandler.setFormatter(new MohawkConsoleFormatter());
         setLoggerLevel(Level.INFO); // Default Level
-        if (cmd.hasOption("loglevel")) {
-            String loglevel = cmd.getOptionValue("loglevel");
+        if (cmd.hasOption(OptionString.LOGLEVEL.toString())) {
+            String loglevel = cmd.getOptionValue(OptionString.LOGLEVEL.toString());
             if (loglevel.equalsIgnoreCase("quiet")) {
                 setLoggerLevel(Level.WARNING);
             } else if (loglevel.equalsIgnoreCase("debug")) {
@@ -353,38 +376,39 @@ public class MohawkInstance {
         logger.addHandler(consoleHandler);
 
         // Add CSV File Headers
-        if (cmd.hasOption("noheader")) {
+        if (cmd.hasOption(OptionString.NOHEADER.toString())) {
             WriteCSVFileHeader = false;
         }
 
         // Set Logger Folder
-        if (cmd.hasOption("logfolder")) {
-            File logfile = new File(cmd.getOptionValue("logfolder"));
+        if (cmd.hasOption(OptionString.LOGFOLDER.toString())) {
+            File logfile = new File(cmd.getOptionValue(OptionString.LOGFOLDER.toString()));
 
             if (!logfile.exists()) {
                 logfile.mkdir();
             }
 
             if (logfile.isDirectory()) {
-                Logger_folderpath = cmd.getOptionValue("logfolder");
+                Logger_folderpath = cmd.getOptionValue(OptionString.LOGFOLDER.toString());
             } else {
                 logger.severe("logfolder did not contain a folder that exists or that could be created!");
             }
         }
 
         // Set File Logger
-        if (cmd.hasOption("logfile")) {
+        if (cmd.hasOption(OptionString.LOGFILE.toString())) {
             // Check if no log file was requested
-            if (cmd.getOptionValue("logfile").equals("n")) {
+            if (cmd.getOptionValue(OptionString.LOGFILE.toString()).equals("n")) {
                 // Create no log file
                 Logger_filepath = "";
-            } else if (cmd.getOptionValue("logfile").equals("u")) {
+            } else if (cmd.getOptionValue(OptionString.LOGFILE.toString()).equals("u")) {
                 // Create a unique log file
                 Logger_filepath = "mohawk-log.%u.%g.txt";
             } else {
                 try {
                     // Create a log file with a specific name
-                    File logfile = new File(Logger_folderpath + File.separator + cmd.getOptionValue("logfile"));
+                    File logfile = new File(Logger_folderpath + File.separator
+                            + cmd.getOptionValue(OptionString.LOGFILE.toString()));
 
                     if (!logfile.exists()) {
                         logfile.createNewFile();
@@ -416,12 +440,12 @@ public class MohawkInstance {
     }
 
     private Boolean setupReturnImmediatelyOptions(CommandLine cmd, Options options) throws Exception {
-        if (cmd.hasOption("help") == true || cmd.getOptions().length < 1) {
+        if (cmd.hasOption(OptionString.HELP.toString()) == true || cmd.getOptions().length < 1) {
             printHelp(cmd, options);
             return true;
         }
 
-        if (cmd.hasOption("version")) {
+        if (cmd.hasOption(OptionString.VERSION.toString())) {
             // keep it as simple as possible for the version
             System.out.println(VERSION);
             return true;
@@ -429,10 +453,10 @@ public class MohawkInstance {
 
         if (cmd.hasOption("numsmv")) {
             logger.info("Running with the 'nusmv' Custom Configuration. " + "Changing the path from '" + NuSMV_filepath
-                    + "' to '" + cmd.getOptionValue("nusmv") + "'");
-            NuSMV_filepath = cmd.getOptionValue("nusmv");
+                    + "' to '" + cmd.getOptionValue(OptionString.NUSMVPATH.toString()) + "'");
+            NuSMV_filepath = cmd.getOptionValue(OptionString.NUSMVPATH.toString());
         }
-        if (cmd.hasOption("checknusmv")) {
+        if (cmd.hasOption(OptionString.CHECKNUSMV.toString())) {
             try {
                 logger.fine("[OPTION] Checking the NuSMV version number");
                 String[] commands = { NuSMV_filepath, "-help" };
@@ -465,9 +489,9 @@ public class MohawkInstance {
     }
 
     private void setupResultOptions(CommandLine cmd, Options options) {
-        if (cmd.hasOption("results")) {
+        if (cmd.hasOption(OptionString.RESULTSFILE.toString())) {
             logger.fine("[OPTION] Changing the results file");
-            resultsFile = cmd.getOptionValue("results");
+            resultsFile = cmd.getOptionValue(OptionString.RESULTSFILE.toString());
         }
         logger.info("Results File: " + resultsFile);
     }

src/mohawk/OptionString.java

+package mohawk;
+
+public enum OptionString {
+    HELP("help"), AUTHORS("authors"), VERSION("version"), CHECKNUSMV("checknusmv"), LOGLEVEL("loglevel"), LOGFILE(
+            "logfile"), LOGFOLDER("logfolder"), NOHEADER("noheader"), RESULTSFILE("output"), MAXW("maxw"), LINESTR(
+            "linstr"), SPECFILE("input"), SMVFILE("smvfile"), SPECEXT("specext"), BULK("bulk"), NOSLICING("noslicing"), SLICEQUERY(
+            "slicequery"), MODE("mode"), TIMEOUT("timeout"), RUN("run"), NUSMVPATH("nusmv");
+
+    private String _str;
+
+    private OptionString(String s) {
+        _str = s;
+    }
+
+    @Override
+    public String toString() {
+        return _str;
+    }
+
+    /**
+     * Returns the commandline equivalent with the hyphen and a space following: AUTHORS -> "-authors "
+     * 
+     * @return
+     */
+    public String c() {
+        return "-" + _str + " ";
+    }
+}

src/mohawk/helper/SMVSpecHelper.java

@@ -45,6 +45,12 @@ public class SMVSpecHelper {
                     + "a specific file, or change the option to point to a folder");
         }
 
+        for (File f : folder.listFiles()) {
+            if (f.getName().endsWith(specFileExt)) {
+                logger.fine("Adding file to specFiles: " + f.getAbsolutePath());
+                specFiles.add(f);
+            }
+        }
     }
 
     public void addSpecFile(String path) throws IOException {

src/mohawk/output/WriteNuSMV.java

@@ -44,6 +44,11 @@ public class WriteNuSMV {
      */
     private String smvcode;
 
+    /**
+     * Flag that indicates if you want to old format, pre 2.5.0
+     */
+    public Boolean olderVersion = false;
+
     // RBAC Instance
     private RBACInstance rbac;
 
@@ -80,12 +85,20 @@ public class WriteNuSMV {
         for (int i = 0; i < vUsers.size(); i++) {
             String user = vUsers.get(i);
             inSmvSpec.setAttribute("userarrays", user + " : array 0.." + (noRoles - 1) + " of boolean");
-            inSmvSpec.setAttribute("users", shortenUser(user));
+            if (olderVersion) {
+                inSmvSpec.setAttribute("users", user);
+            } else {
+                inSmvSpec.setAttribute("users", shortenUser(user));
+            }
         }
 
         for (int i = 0; i < vAdmin.size(); i++) {
             String user = vAdmin.get(i);
-            inSmvSpec.setAttribute("admin", shortenUser(user));
+            if (olderVersion) {
+                inSmvSpec.setAttribute("admin", user);
+            } else {
+                inSmvSpec.setAttribute("admin", shortenUser(user));
+            }
         }
 
         inSmvSpec.setAttribute("role", "0 .. " + (noRoles - 1));
@@ -112,12 +125,14 @@ public class WriteNuSMV {
                 String value;
 
                 if (vUserUA != null) {
-                    if (vUserUA.contains(j))
-                        value = "TRUE";
-                    else
-                        value = "FALSE";
-                } else
-                    value = "FALSE";
+                    if (vUserUA.contains(j)) {
+                        value = getTrue();
+                    } else {
+                        value = getFalse();
+                    }
+                } else {
+                    value = getFalse();
+                }
 
                 String uaassign = "init(" + user + "[" + j + "]" + ") := " + value;
                 inSmvSpec.setAttribute("ua", uaassign);
@@ -171,13 +186,19 @@ public class WriteNuSMV {
             e1.printStackTrace();
         }
 
+        String strTemp = "user = $user$ & admin = $admin$ & $admincond$ & $precondition$ & role = " + iDestRoleIndex
+                + " & act = ADD: " + getTrue() + ";";
+
         for (int i = 0; i < vAdminUsers.size(); i++) {
-            StringTemplate strTTrans = new StringTemplate(
-                    "user = $user$ & admin = $admin$ & $admincond$ & $precondition$ & role = " + iDestRoleIndex
-                            + " & act = ADD: TRUE;");
+            StringTemplate strTTrans = new StringTemplate(strTemp);
 
-            strTTrans.setAttribute("user", shortenUser(inUser));
-            strTTrans.setAttribute("admin", shortenUser(vAdminUsers.get(i)));
+            if (olderVersion) {
+                strTTrans.setAttribute("user", inUser);
+                strTTrans.setAttribute("admin", vAdminUsers.get(i));
+            } else {
+                strTTrans.setAttribute("user", shortenUser(inUser));
+                strTTrans.setAttribute("admin", shortenUser(vAdminUsers.get(i)));
+            }
             PreCondition pcPreCond = inCAEntry.getPreConditions();
             String strPreCond = null;
             int adminRoleIndex = 0;
@@ -188,7 +209,8 @@ public class WriteNuSMV {
                 e.printStackTrace();
             }
 
-            String strAdminCondRole = vAdminUsers.get(i) + "[" + adminRoleIndex + "] = TRUE";
+            String strAdminCondRole = vAdminUsers.get(i) + "[" + adminRoleIndex + "] = " + getTrue();
+
             strTTrans.setAttribute("admincond", strAdminCondRole);
 
             if (pcPreCond.size() != 0) {
@@ -197,18 +219,21 @@ public class WriteNuSMV {
 
                     String strCond = null;
 
-                    if (value == 1)
-                        strCond = inUser + "[" + iroleindex + "]=TRUE";
-                    else
-                        strCond = inUser + "[" + iroleindex + "]=FALSE";
+                    if (value == 1) {
+                        strCond = inUser + "[" + iroleindex + "]=" + getTrue();
+                    } else {
+                        strCond = inUser + "[" + iroleindex + "]=" + getFalse();
+                    }
 
-                    if (strPreCond == null)
+                    if (strPreCond == null) {
                         strPreCond = strCond;
-                    else
+                    } else {
                         strPreCond = strPreCond + " & " + strCond;
+                    }
                 }
-            } else
-                strPreCond = "TRUE";
+            } else {
+                strPreCond = getTrue();
+            }
 
             strTTrans.setAttribute("precondition", strPreCond);
 
@@ -242,18 +267,28 @@ public class WriteNuSMV {
             e.printStackTrace();
         }
 
+        String strTemp;
+
+        strTemp = "user = $user$ & admin = $admin$ & $precondition$ & role = " + iDestRoleIndex + " & act = REMOVE: "
+                + getFalse() + ";";
+
         for (int i = 0; i < vAdminUsers.size(); i++) {
-            StringTemplate strTTrans = new StringTemplate("user = $user$ & admin = $admin$ & $precondition$ & role = "
-                    + iDestRoleIndex + " & act = REMOVE: FALSE;");
-            strTTrans.setAttribute("user", shortenUser(inUser));
-            strTTrans.setAttribute("admin", shortenUser(vAdminUsers.get(i)));
+            StringTemplate strTTrans = new StringTemplate(strTemp);
+
+            if (olderVersion) {
+                strTTrans.setAttribute("user", inUser);
+                strTTrans.setAttribute("admin", vAdminUsers.get(i));
+            } else {
+                strTTrans.setAttribute("user", shortenUser(inUser));
+                strTTrans.setAttribute("admin", shortenUser(vAdminUsers.get(i)));
+            }
 
             if (adminRoleIndex == -1)
-                strTTrans.setAttribute("precondition", "TRUE");
+                strTTrans.setAttribute("precondition", getTrue());
             else if (adminRoleIndex == -2)
-                strTTrans.setAttribute("precondition", "FALSE");
+                strTTrans.setAttribute("precondition", getFalse());
             else
-                strTTrans.setAttribute("precondition", vAdminUsers.get(i) + "[" + adminRoleIndex + "]=TRUE");
+                strTTrans.setAttribute("precondition", vAdminUsers.get(i) + "[" + adminRoleIndex + "]=" + getTrue());
 
             if (strTransition == null)
                 strTransition = strTTrans.toString();
@@ -264,6 +299,14 @@ public class WriteNuSMV {
         return strTransition;
     }
 
+    private String getFalse() {
+        return ((olderVersion) ? "0" : "FALSE");
+    }
+
+    private String getTrue() {
+        return ((olderVersion) ? "1" : "TRUE");
+    }
+
     public String setupEachUser(String inUser) {
 
         Vector<String> vRoles = rbac.getRoles();
@@ -307,6 +350,7 @@ public class WriteNuSMV {