From 9a951e34049fd301165cd724f2f706b4b480a68f Mon Sep 17 00:00:00 2001
From: Jonathan Shahen <jonathan.shahen@gmail.com>
Date: Wed, 19 Oct 2016 20:34:55 -0400
Subject: [PATCH] Intermediate commit: role mapping file produced to make it
 easier to understand the NuSMV file (role mapping to come)

---
 src/mohawk/converter/ConverterInstance.java   |  1 +
 .../converter/to/nusmv/ConvertToNuSMV.java    | 71 ++++++++++++++++++-
 .../converter/to/nusmv/nusmvTemplate.st       |  4 +-
 3 files changed, 71 insertions(+), 5 deletions(-)

diff --git a/src/mohawk/converter/ConverterInstance.java b/src/mohawk/converter/ConverterInstance.java
index 2784fdc..dbf0f84 100644
--- a/src/mohawk/converter/ConverterInstance.java
+++ b/src/mohawk/converter/ConverterInstance.java
@@ -82,6 +82,7 @@ public class ConverterInstance {
                 /* Timing */timing.stopTimer("parseFile (" + i + ")");
 
                 MohawkT m = parser.mohawkT;
+                m.generatorName = "Mohawk+T Converter " + VERSION;
 
                 if (specHelper.error.errorFound) {
                     logger.warning("[PARSING ERROR] Skipping this file due to a parsing error");
diff --git a/src/mohawk/converter/to/nusmv/ConvertToNuSMV.java b/src/mohawk/converter/to/nusmv/ConvertToNuSMV.java
index fe4ce30..43678ac 100644
--- a/src/mohawk/converter/to/nusmv/ConvertToNuSMV.java
+++ b/src/mohawk/converter/to/nusmv/ConvertToNuSMV.java
@@ -62,20 +62,25 @@ public class ConvertToNuSMV extends ConvertTo {
             Set<RoleTimeSlot> roleTimeslots = new HashSet<>();
 
             for (Rule r : m.canAssign.getRules()) {
-                roleTimeslots.addAll(RoleTimeSlot.grabAll(r));
+                roleTimeslots.addAll(RoleTimeSlot.grabAll(r, timeIntervalHelper, roleHelper));
             }
 
+            /* Timing */timing.startTimer(tPrefix + "_" + "mappingString");
+            String mappingStr = ruleMapping(m);
+            /* Timing */timing.stopTimer(tPrefix + "_" + "mappingString");
+
             // Generate the Converted String
             /* Timing */timing.startTimer(tPrefix + "_" + "template");
             String template = ConvertTo.readFile(this.getClass().getResource("nusmvTemplate.st"));
             ST st = new ST(template);
+            st.add("numUsers", roleHelper.numberOfRoles() + 1);
             st.add("numRoles", roleHelper.numberOfRoles());
             st.add("numAdminRoles", adminRoles.size());
             st.add("numTimeSlots", timeIntervalHelper.sizeReduced());
 
             st.add("queryStr", workableQuery.getString());
-            st.add("goalRoles", workableQuery._roles);
-            st.add("goalTimeSlot", workableQuery._timeslot._start);
+            st.add("goalRoles", RoleTimeSlot.grabAll(workableQuery._roles, workableQuery._timeslot, timeIntervalHelper,
+                    roleHelper));
 
             st.add("caruleslist", stringList("CA", caRuleCount));
             st.add("crruleslist", stringList("CR", crRuleCount));
@@ -97,6 +102,14 @@ public class ConvertToNuSMV extends ConvertTo {
                     convertedFile.createNewFile();
                 }
                 Files.write(convertedFile.toPath(), convertedStr.getBytes());
+
+                // Mapping file
+                convertedFile = new File(file.getAbsolutePath() + getFileExtenstion() + ".rulemapping");
+
+                if (!convertedFile.exists()) {
+                    convertedFile.createNewFile();
+                }
+                Files.write(convertedFile.toPath(), mappingStr.getBytes());
                 /* Timing */timing.stopTimer(tPrefix + "_" + "Files.write");
             }
             lastError = null;
@@ -112,6 +125,58 @@ public class ConvertToNuSMV extends ConvertTo {
         return convertedStr;
     }
 
+    private String ruleMapping(MohawkT m) {
+        StringBuilder sb = new StringBuilder(50 * m.numberOfRules());
+        sb.append("/*\nRule Mapping\n\n");
+
+        if (m.generatedComment == null) {
+            m.generateComment(false);
+        }
+
+        sb.append(m.generatedComment).append("\n\n");
+
+        sb.append("CanAssign Rules : ").append(m.canAssign.numberOfRules());
+        sb.append("\nCanRevoke Rules : ").append(m.canRevoke.numberOfRules());
+        sb.append("\nCanEnable Rules : ").append(m.canEnable.numberOfRules());
+        sb.append("\nCanDisable Rules: ").append(m.canDisable.numberOfRules());
+        sb.append("\n*/\n\n").append(Rule.getInfoCodeHeader());
+        int i;
+
+        sb.append("\n\nCanAssign Rules:\n");
+        i = 1;
+        for (Rule r : m.canAssign.getRules()) {
+            sb.append(r.getString(i, 0)).append("\n");
+            i++;
+        }
+        sb.append("-----------------------------------------------------------------\n");
+
+        sb.append("\n\nCanRevoke Rules:\n");
+        i = 1;
+        for (Rule r : m.canRevoke.getRules()) {
+            sb.append(r.getString(i, 0)).append("\n");
+            i++;
+        }
+        sb.append("-----------------------------------------------------------------\n");
+
+        sb.append("\n\nCanEnable Rules:\n");
+        i = 1;
+        for (Rule r : m.canEnable.getRules()) {
+            sb.append(r.getString(i, 0)).append("\n");
+            i++;
+        }
+        sb.append("-----------------------------------------------------------------\n");
+
+        sb.append("\n\nCanDisable Rules:\n");
+        i = 1;
+        for (Rule r : m.canDisable.getRules()) {
+            sb.append(r.getString(i, 0)).append("\n");
+            i++;
+        }
+        sb.append("-----------------------------------------------------------------\n");
+
+        return sb.toString();
+    }
+
     private String stringList(String prefix, Integer count) {
         return stringList(prefix, count, ",");
     }
diff --git a/src/mohawk/converter/to/nusmv/nusmvTemplate.st b/src/mohawk/converter/to/nusmv/nusmvTemplate.st
index 05fe775..45e8a5f 100644
--- a/src/mohawk/converter/to/nusmv/nusmvTemplate.st
+++ b/src/mohawk/converter/to/nusmv/nusmvTemplate.st
@@ -8,7 +8,7 @@ numtimeslots := <numTimeSlots>;
 
 -- LTLSPEC: "G p" means that a certain condition p holds in all future time instants
 -- <queryStr>
-LTLSPEC G !(<goalRoles:{r|U1R<r.getName>T<goalTimeSlot> = TRUE}; separator=" & ">)
+LTLSPEC G !(<goalRoles:{r|U1<r.string> = TRUE}; separator=" & ">)
 
 VAR
 rule : {
@@ -30,7 +30,7 @@ ASSIGN
 
 VAR
 -- <numUsers> Users Variable
-<users:{u|<roleTimeslots:{rt|U<u>R<rt.role>T<rt.time> : boolean;}; separator="\n">}; separator="\n">
+<users:{u|<roleTimeslots:{rt|U<u><rt.string> : boolean;}; separator="\n">}; separator="\n">
 
 -- <numRolesEnabled> RoleEnabled
 <enabledRoles:{r|<r> : boolean;}; separator="\n">
-- 
GitLab