Commit 0eb562b8 authored by Jonathan Shahen's avatar Jonathan Shahen

starting work on the toolchain for the reduction to NuSMV

parent 8b9c12df
package mohawk.converter.to.nusmv;
import java.io.File;
import java.io.PrintWriter;
import java.io.StringWriter;
import java.nio.file.Files;
import java.util.logging.Logger;
import org.stringtemplate.v4.ST;
import mohawk.converter.to.ConvertTo;
import mohawk.global.pieces.MohawkT;
import mohawk.global.timing.MohawkTiming;
public class ConvertToNuSMV extends ConvertTo {
public static final Logger logger = Logger.getLogger("mohawk");
public ConvertToNuSMV(MohawkTiming timing) {
super(timing);
tPrefix = "ConvertToNuSMV";
}
@Override
public String convert(MohawkT m, File file, Boolean writeToFile) {
try {
// Generate the Converted String
/* Timing */timing.startTimer(tPrefix + "_" + "template");
String template = ConvertTo.readFile(this.getClass().getResource("ASAPTimeNSATemplate.st"));
ST st = new ST(template);
/*
st.add("numRoles", roleHelper.numberOfRoles());
st.add("numTimeslots", timeIntervalHelper.sizeReduced());
st.add("goalRole", query.goalRole);
st.add("goalTimeslot", query.goalTimeslot);
st.add("rules_nsa", rules);
*/
convertedStr = st.render();
/* Timing */timing.stopTimer(tPrefix + "_" + "template");
// Write the converted string out to "file + getFileExtenstion()"
if (writeToFile) {
/* Timing */timing.startTimer(tPrefix + "_" + "Files.write");
File convertedFile = new File(file.getAbsolutePath() + getFileExtenstion());
if (!convertedFile.exists()) {
convertedFile.createNewFile();
}
Files.write(convertedFile.toPath(), convertedStr.getBytes());
/* Timing */timing.stopTimer(tPrefix + "_" + "Files.write");
}
lastError = null;
} catch (Exception e) {
StringWriter errors = new StringWriter();
e.printStackTrace(new PrintWriter(errors));
logger.fine(errors.toString());
logger.warning("[ERROR] Unable to convert to Ranise: " + e.getMessage());
lastError = "Error ConvertToRanise.convert.Exception #1";
}
return convertedStr;
}
}
<! Roles role0 role1 role2 role3; !>
Roles <roles:{r|<r.Name>}; separator=" "> <adminrole>;
<! Users user0 user1 user2 user3 user4; !>
Users <users; separator=" ">;
<! UA <user4,Admin>; !>
UA \<<adminuser>,<adminrole>>;
<! CR <Admin,role0> <Admin,role2>; !>
CR <canrevoke:{cr|\<<adminrole>,<cr.role>>}; separator="\n\t">;
<! CA <role3,role2,role0> <role3,role2&role1,role0> <role3,role2&role0,role1> <role3,TRUE,role1> <role3,role0,role1>; !>
CA <canassign:{ca|\<<adminrole>,<if(ca.precondition)><ca.precondition; separator="&"><else>TRUE<endif>,<ca.role>>}; separator="\n\t">;
<! ADMIN user4; !>
ADMIN <adminuser>;
<! SPEC user0 role1; !>
SPEC <specuser> <specrole>;
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