From d7a2d4ac2d46ae699cb03a2dfac7d3012c35ebbd Mon Sep 17 00:00:00 2001
From: Jonathan Shahen <jonathan.shahen@gmail.com>
Date: Thu, 20 Oct 2016 23:49:00 -0400
Subject: [PATCH] HOTFIX: fixing compilation error - got a working positive,
 need to test negatives and more positives

---
 .../converter/to/nusmv/ConvertToNuSMV.java    |  8 ++++--
 .../converter/to/nusmv/nusmvTemplate.st       | 28 +++++++++----------
 2 files changed, 19 insertions(+), 17 deletions(-)

diff --git a/src/mohawk/converter/to/nusmv/ConvertToNuSMV.java b/src/mohawk/converter/to/nusmv/ConvertToNuSMV.java
index 04c3754..f2337df 100644
--- a/src/mohawk/converter/to/nusmv/ConvertToNuSMV.java
+++ b/src/mohawk/converter/to/nusmv/ConvertToNuSMV.java
@@ -88,9 +88,11 @@ public class ConvertToNuSMV extends ConvertTo {
             st.add("goalRoles", RoleTimeSlot.grabAll(m.query._roles, m.query._timeslot, m.timeIntervalHelper,
                     m.roleHelper));
 
-            st.add("caruleslist", stringList("CA", caRuleCount));
-            st.add("crruleslist", stringList("CR", crRuleCount));
-            st.add("ceruleslist", stringList("CE", ceRuleCount));
+            st.add("caruleslist", stringList("CA", caRuleCount)
+                    + ((caRuleCount > 0 & (crRuleCount > 0 | ceRuleCount > 0 | cdRuleCount > 0)) ? "," : ""));
+            st.add("crruleslist", stringList("CR", crRuleCount)
+                    + ((crRuleCount > 0 & (ceRuleCount > 0 | cdRuleCount > 0)) ? "," : ""));
+            st.add("ceruleslist", stringList("CE", ceRuleCount) + ((ceRuleCount > 0 & (cdRuleCount > 0)) ? "," : ""));
             st.add("cdruleslist", stringList("CD", cdRuleCount));
 
             st.add("users", users);
diff --git a/src/mohawk/converter/to/nusmv/nusmvTemplate.st b/src/mohawk/converter/to/nusmv/nusmvTemplate.st
index 0518f14..f657311 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|U1<r.string> = TRUE}; separator=" & ">)
+LTLSPEC G !(<goalRoles:{r|u[1]<r.string> = TRUE}; separator=" & ">)
 
 VAR
 rule : {
@@ -24,10 +24,10 @@ rule : {
 user : 1 .. numusers;
 admin: 1 .. numusers;
 
-U : array 1..numusers of 
+u : array 1..numusers of 
     array 1..numroles of 
     array 1..numtimeslots of boolean;
-RE : array 1..numroles of 
+e : array 1..numroles of 
      array 1..numtimeslots of boolean;
 
 ASSIGN
@@ -39,11 +39,11 @@ ASSIGN
 -- User <u>, Role <r.role> Assign/Revoke 
 <r.timeslots:{ts|
 <if(ts.cases)>
-next(U[<u>][<r.role>][<ts.timeslot>]) := case
-<ts.cases:{c|<\t>user=<u> & <c.condition> : <if(c.trueResult)>TRUE<else>FALSE<endif>}; separator="\n">
-<\t>TRUE : U[<u>][<r.role>][<ts.timeslot>];
+next(u[<u>][<r.role>][<ts.timeslot>]) := case
+<ts.cases:{c|<\t>user=<u> & <c.condition> : <if(c.trueResult)>TRUE<else>FALSE<endif>;}; separator="\n">
+<\t>TRUE : u[<u>][<r.role>][<ts.timeslot>];
 esac;
-<else>next(U[<u>][<r.role>][<ts.timeslot>]) := U[<u>][<r.role>][<ts.timeslot>];
+<else>next(u[<u>][<r.role>][<ts.timeslot>]) := u[<u>][<r.role>][<ts.timeslot>];
 <endif>
 }; separator="\n">
 <else>-- Skipping <r.role>
@@ -57,11 +57,11 @@ esac;
 -- Role <r.role> Enable/Disable
 <r.timeslots:{ts|
 <if(ts.cases)>
-next(RE[<r.role>][<ts.timeslot>]) := case
-<ts.cases:{c|<\t><c.condition> : <if(c.trueResult)>TRUE<else>FALSE<endif>}; separator="\n">
-<\t>TRUE : RE[<r.role>][<ts.timeslot>];
+next(e[<r.role>][<ts.timeslot>]) := case
+<ts.cases:{c|<\t><c.condition> : <if(c.trueResult)>TRUE<else>FALSE<endif>;}; separator="\n">
+<\t>TRUE : e[<r.role>][<ts.timeslot>];
 esac;
-<else>next(RE[<r.role>][<ts.timeslot>]) := RE[<r.role>][<ts.timeslot>];
+<else>next(e[<r.role>][<ts.timeslot>]) := e[<r.role>][<ts.timeslot>];
 <endif>
 }; separator="\n">
 <else>-- Skipping <r.role>
@@ -77,13 +77,13 @@ VAR
 <users:{u|<roleTimeslots:{rt|U<u><rt.string> : boolean;}; separator="  ">}; separator="\n">
 
 -- <numRolesEnabled> RoleEnabled
-<enabledRoles:{rt|RE<rt.string> : boolean;}; separator="  ">
+<enabledRoles:{rt|e<rt.string> : boolean;}; separator="  ">
 ------------------------------------------------------------
 !>
 
 ASSIGN
 -- Disabling User Role Assignments
-<users:{u|<roleTimeslots:{rt|init(U[<u>]<rt.string>) := FALSE;}; separator="  ">}; separator="\n">
+<users:{u|<roleTimeslots:{rt|init(u[<u>]<rt.string>) := FALSE;}; separator="  ">}; separator="\n">
 
 -- Disabling Roles
-<enabledRoles:{rt|init(RE<rt.string>) := FALSE;}; separator="  ">
\ No newline at end of file
+<enabledRoles:{rt|init(e<rt.string>) := FALSE;}; separator="  ">
\ No newline at end of file
-- 
GitLab