Commit 1ed60a31 authored by Jonathan Shahen's avatar Jonathan Shahen

More comments and a better system for writing out the SMV auxiliary files

parent e72f835b
......@@ -16,6 +16,12 @@ import mohawk.global.timing.MohawkTiming;
public class ConvertToNuSMV extends ConvertTo {
public static final Logger logger = Logger.getLogger("mohawk");
/**
* If {@link ConvertToNuSMV#convertedFile} has the parameter {@code writeToFile} set to TRUE, then this field will
* be updated with the file that contains the converted SMV string.
*/
public File convertedFile = null;
public ConvertToNuSMV(MohawkTiming timing) {
super(timing);
tPrefix = "ConvertToNuSMV";
......@@ -40,6 +46,9 @@ public class ConvertToNuSMV extends ConvertTo {
public String convert(MohawkT m, File file, Boolean writeToFile) {
try {
/* Timing */timing.startTimer(tPrefix + "_" + "sortRolesReduceTimeslots");
//////////////////////////////////////////////////////////////////////////////////////////
// REDUCTION
// Reduce Roles to Integers
m.roleHelper.allowZeroRole = false;// roles start from 1 NOT 0!
m.roleHelper.setupSortedRoles();
......@@ -50,7 +59,10 @@ public class ConvertToNuSMV extends ConvertTo {
/* Timing */timing.stopTimer(tPrefix + "_" + "sortRolesReduceTimeslots");
m.indexAllRules();
//////////////////////////////////////////////////////////////////////////////////////////
//////////////////////////////////////////////////////////////////////////////////////////
// GATHER TEMPLATE VARIABLE INFORMATION
Set<Role> adminRoles = RoleHelper.getAdministratorRoles(m.getAllRules(), false);
Integer caRuleCount = m.canAssign.numberOfRules();
......@@ -84,8 +96,10 @@ public class ConvertToNuSMV extends ConvertTo {
/* Timing */timing.startTimer(tPrefix + "_" + "roleMappingString");
String roleMappingStr = roleTimeslotMapping(m);
/* Timing */timing.stopTimer(tPrefix + "_" + "roleMappingString");
//////////////////////////////////////////////////////////////////////////////////////////
// Generate the Converted String
//////////////////////////////////////////////////////////////////////////////////////////
// GENERATE THE CONVERTED STRING
/* Timing */timing.startTimer(tPrefix + "_" + "template");
String template = ConvertTo.readFile(this.getClass().getResource("nusmvTemplate.st"));
ST st = new ST(template);
......@@ -119,11 +133,17 @@ public class ConvertToNuSMV extends ConvertTo {
convertedStr = st.render();
/* Timing */timing.stopTimer(tPrefix + "_" + "template");
//////////////////////////////////////////////////////////////////////////////////////////
// Write the converted string out to "file + getFileExtenstion()"
//////////////////////////////////////////////////////////////////////////////////////////
/** Write the converted string out to {@link ConvertToNuSMV#convertedFile} */
if (writeToFile) {
/* Timing */timing.startTimer(tPrefix + "_" + "Files.write");
File convertedFile = new File(file.getAbsolutePath() + getFileExtenstion());
if (file.getAbsolutePath().endsWith(getFileExtenstion())) {
convertedFile = file;
} else {
convertedFile = new File(file.getAbsolutePath() + getFileExtenstion());
}
if (!convertedFile.exists()) {
convertedFile.createNewFile();
......@@ -132,24 +152,26 @@ public class ConvertToNuSMV extends ConvertTo {
Files.write(convertedFile.toPath(), convertedStr.getBytes());
// Rule Mapping file
convertedFile = new File(file.getAbsolutePath() + getFileExtenstion() + ".rulemapping");
File ruleMapFile = new File(convertedFile.getAbsolutePath() + ".rulemapping");
if (!convertedFile.exists()) {
convertedFile.createNewFile();
if (!ruleMapFile.exists()) {
ruleMapFile.createNewFile();
}
logger.info("Writing Rule Mapping file to:" + convertedFile.getAbsolutePath());
Files.write(convertedFile.toPath(), ruleMappingStr.getBytes());
logger.info("Writing Rule Mapping file to:" + ruleMapFile.getAbsolutePath());
Files.write(ruleMapFile.toPath(), ruleMappingStr.getBytes());
// Role Mapping file
convertedFile = new File(file.getAbsolutePath() + getFileExtenstion() + ".roletimemapping");
File roleMapFile = new File(convertedFile.getAbsolutePath() + ".roletimemapping");
if (!convertedFile.exists()) {
convertedFile.createNewFile();
if (!roleMapFile.exists()) {
roleMapFile.createNewFile();
}
logger.info("Writing Role Mapping file to:" + convertedFile.getAbsolutePath());
Files.write(convertedFile.toPath(), roleMappingStr.getBytes());
logger.info("Writing Role Mapping file to:" + roleMapFile.getAbsolutePath());
Files.write(roleMapFile.toPath(), roleMappingStr.getBytes());
/* Timing */timing.stopTimer(tPrefix + "_" + "Files.write");
}
//////////////////////////////////////////////////////////////////////////////////////////
lastError = null;
} catch (Exception e) {
StringWriter errors = new StringWriter();
......
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