Commit 9a951e34 authored by Jonathan Shahen's avatar Jonathan Shahen

Intermediate commit: role mapping file produced to make it easier to...

Intermediate commit: role mapping file produced to make it easier to understand the NuSMV file (role mapping to come)
parent b3e355df
......@@ -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");
......
......@@ -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, ",");
}
......
......@@ -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">
......
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