Skip to content

GitLab

mohawk-t-conversion-tool
mohawk-t-conversion-tool
Commit 52531b36 authored by Jonathan Shahen's avatar Jonathan Shahen
Browse files
Options

intermediate commit: pipeline works for converting to NuSMV, progress made on... 

intermediate commit: pipeline works for converting to NuSMV, progress made on the template but more work still needed
parent 6b72b2d9
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 788 additions and 827 deletions
Mohawk+T notepad++ language 0 → 100644
View file @ 52531b36
<NotepadPlus>
<UserLang name="Mohawk+T" ext=".mohawkt" udlVersion="2.1">
<Settings>
<Global caseIgnored="yes" allowFoldOfComments="yes" foldCompact="no" forcePureLC="0" decimalSeparator="0" />
<Prefix Keywords1="yes" Keywords2="no" Keywords3="no" Keywords4="no" Keywords5="no" Keywords6="no" Keywords7="no" Keywords8="no" />
</Settings>
<KeywordLists>
<Keywords name="Comments">00// 01 02 03/* 04*/</Keywords>
<Keywords name="Numbers, prefix1">t</Keywords>
<Keywords name="Numbers, prefix2"></Keywords>
<Keywords name="Numbers, extras1"></Keywords>
<Keywords name="Numbers, extras2"></Keywords>
<Keywords name="Numbers, suffix1"></Keywords>
<Keywords name="Numbers, suffix2"></Keywords>
<Keywords name="Numbers, range"></Keywords>
<Keywords name="Operators1">~ &amp; &lt; &gt; , { }</Keywords>
<Keywords name="Operators2">NOT TRUE</Keywords>
<Keywords name="Folders in code1, open">{</Keywords>
<Keywords name="Folders in code1, middle"></Keywords>
<Keywords name="Folders in code1, close">}</Keywords>
<Keywords name="Folders in code2, open"></Keywords>
<Keywords name="Folders in code2, middle"></Keywords>
<Keywords name="Folders in code2, close"></Keywords>
<Keywords name="Folders in comment, open"></Keywords>
<Keywords name="Folders in comment, middle"></Keywords>
<Keywords name="Folders in comment, close"></Keywords>
<Keywords name="Keywords1">CanAssign CanRevoke CanDisable CanEnable Query Expected</Keywords>
<Keywords name="Keywords2">UNKNOWN GOAL_REACHABLE REACHABLE</Keywords>
<Keywords name="Keywords3">GOAL_UNREACHABLE UNREACHABLE</Keywords>
<Keywords name="Keywords4"></Keywords>
<Keywords name="Keywords5"></Keywords>
<Keywords name="Keywords6"></Keywords>
<Keywords name="Keywords7"></Keywords>
<Keywords name="Keywords8"></Keywords>
<Keywords name="Delimiters">00 01 02 03 04 05 06 07 08 09 10 11 12 13 14 15 16 17 18 19 20 21 22 23</Keywords>
</KeywordLists>
<Styles>
<WordsStyle name="DEFAULT" fgColor="000000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
<WordsStyle name="COMMENTS" fgColor="00A600" bgColor="FFFFFF" fontName="" fontStyle="2" nesting="256" />
<WordsStyle name="LINE COMMENTS" fgColor="00A600" bgColor="FFFFFF" fontName="" fontStyle="2" nesting="0" />
<WordsStyle name="NUMBERS" fgColor="FF8000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
<WordsStyle name="KEYWORDS1" fgColor="C8002A" bgColor="FFFFFF" fontName="" fontStyle="1" nesting="0" />
<WordsStyle name="KEYWORDS2" fgColor="2A00FF" bgColor="FFFFFF" fontName="" fontStyle="4" nesting="0" />
<WordsStyle name="KEYWORDS3" fgColor="D75D00" bgColor="FFFFFF" fontName="" fontStyle="4" nesting="0" />
<WordsStyle name="KEYWORDS4" fgColor="000000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
<WordsStyle name="KEYWORDS5" fgColor="000000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
<WordsStyle name="KEYWORDS6" fgColor="000000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
<WordsStyle name="KEYWORDS7" fgColor="000000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
<WordsStyle name="KEYWORDS8" fgColor="000000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
<WordsStyle name="OPERATORS" fgColor="7F0055" bgColor="FFFFFF" fontName="" fontStyle="1" nesting="0" />
<WordsStyle name="FOLDER IN CODE1" fgColor="000000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
<WordsStyle name="FOLDER IN CODE2" fgColor="000000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
<WordsStyle name="FOLDER IN COMMENT" fgColor="000000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
<WordsStyle name="DELIMITERS1" fgColor="000000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
<WordsStyle name="DELIMITERS2" fgColor="000000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
<WordsStyle name="DELIMITERS3" fgColor="000000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
<WordsStyle name="DELIMITERS4" fgColor="000000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
<WordsStyle name="DELIMITERS5" fgColor="000000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
<WordsStyle name="DELIMITERS6" fgColor="000000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
<WordsStyle name="DELIMITERS7" fgColor="000000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
<WordsStyle name="DELIMITERS8" fgColor="000000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
</Styles>
</UserLang>
</NotepadPlus>
src/mohawk/converter/ConverterCUI.java
View file @ 52531b36
......@@ -54,7 +54,7 @@ public class ConverterCUI {
break;
}
if (cmd.equals("!prev")) {
if (cmd.equals("!p")) {
argv.clear();
argv.addAll(Arrays.asList(previousCmd.split(" ")));
break;
......@@ -67,7 +67,7 @@ public class ConverterCUI {
System.out.println("Commands: " + argv);
try {
if (!cmd.equals("!prev")) {
if (!cmd.equals("!p")) {
FileWriter fw;
fw = new FileWriter(previousCommandFilename, false);
fw.write(fullCommand.toString());
......@@ -147,13 +147,15 @@ public class ConverterCUI {
+ OptionString.LOGLEVEL.c("quiet") + "!exit");
System.out.println(OptionString.TO_MOHAWK.c() + OptionString.SPECFILE.c("data/bug/11-CA-no-role3.mohawk.T")
+ OptionString.LOGLEVEL.c("quiet") + "!exit");
System.out.println("");
System.out.println(OptionString.TO_NUSMV.c() + OptionString.SPECFILE.c("data/nusmv/test01.mohawkt") + "!exit");
System.out.println("");
try {
BufferedReader bfr = new BufferedReader(new FileReader(previousCommandFilename));
previousCmd = bfr.readLine();
bfr.close();
System.out.println("Previous Command ('!prev' to use the previous command): " + previousCmd);
System.out.println("Previous Command ('!p' to use the previous command): " + previousCmd);
} catch (IOException e) {
System.out.println("[ERROR] Unable to load previous command!");
}
......
src/mohawk/converter/ConverterInstance.java
View file @ 52531b36
This diff is collapsed.
src/mohawk/converter/to/nusmv/ConvertToNuSMV.java
View file @ 52531b36
package mohawk.converter.to.nusmv;
import java.io.File;
import java.io.*;
import java.nio.file.Files;
import java.util.*;
import java.util.logging.Logger;
import org.stringtemplate.v4.ST;
import mohawk.converter.to.ConvertTo;
import mohawk.global.pieces.MohawkT;
import mohawk.global.helper.RoleHelper;
import mohawk.global.helper.TimeIntervalHelper;
import mohawk.global.pieces.*;
import mohawk.global.timing.MohawkTiming;
public class ConvertToNuSMV extends ConvertTo {
public static final Logger logger = Logger.getLogger("mohawk");
/** Change this number to change from Reduction 2 to Reduction 3. */
public static final Integer reduction = 3;
public boolean shortRolenames = false;
public ConvertToNuSMV(MohawkTiming timing) {
super(timing);
tPrefix = "ConvertToNuSMV";
}
@Override
public String getFileExtenstion() {
return ".smv";
}
@Override
public String convert(MohawkT m, File file, Boolean writeToFile) {
logger.warning("[ERROR] Pick a specific Reduction to NuSMV");
lastError = "Pick a specific Reduction to NuSMV";
try {
// Deep Copy Helpers
/* Timing */timing.startTimer(tPrefix + "_" + "deepcopy");
RoleHelper roleHelper = new RoleHelper(m.roleHelper);
TimeIntervalHelper timeIntervalHelper = new TimeIntervalHelper(m.timeIntervalHelper);
Query workableQuery = new Query(m.query);
/* Timing */timing.stopTimer(tPrefix + "_" + "deepcopy");
/* Timing */timing.startTimer(tPrefix + "_" + "sortRolesReduceTimeslots");
// Reduce Roles to Integers
roleHelper.allowZeroRole = false;// roles start from 1 NOT 0!
roleHelper.setupSortedRoles();
// Reduce TimeIntervals to Timeslots
timeIntervalHelper.allowZeroTimeslot = false;// time-slots start from t1 NOT t0!
// Reduction (2)
timeIntervalHelper.reduceToTimeslots();
/* Timing */timing.stopTimer(tPrefix + "_" + "sortRolesReduceTimeslots");
Set<Role> adminRoles = RoleHelper.getAdministratorRoles(m.getAllRules(), false);
Integer caRuleCount = m.canAssign.numberOfRules();
Integer crRuleCount = m.canRevoke.numberOfRules();
Integer ceRuleCount = m.canEnable.numberOfRules();
Integer cdRuleCount = m.canDisable.numberOfRules();
/* Generate a list of users (roles + 1) to loop through */
ArrayList<Integer> users = new ArrayList<>(roleHelper.numberOfRoles() + 1);
for (int i = 1; i <= roleHelper.numberOfRoles() + 1; i++) {
users.add(i);
}
Set<RoleTimeSlot> roleTimeslots = new HashSet<>();
for (Rule r : m.canAssign.getRules()) {
roleTimeslots.addAll(RoleTimeSlot.grabAll(r));
}
// 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("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("caruleslist", stringList("CA", caRuleCount));
st.add("crruleslist", stringList("CR", crRuleCount));
st.add("ceruleslist", stringList("CE", ceRuleCount));
st.add("cdruleslist", stringList("CD", cdRuleCount));
st.add("users", users);
st.add("roleTimeslots", roleTimeslots);
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;
}
private String stringList(String prefix, Integer count) {
return stringList(prefix, count, ",");
}
private String stringList(String prefix, Integer count, String suffix) {
StringBuilder sb = new StringBuilder((prefix.length() + count.toString().length()) * count);
for (int i = 1; i <= count - 1; i++) {
sb.append(prefix).append(i).append(suffix);
}
/*Add the last one*/
sb.append(prefix).append(count);
return sb.toString();
}
}
src/mohawk/converter/to/nusmv/ConvertToNuSMVReduction2.java deleted 100644 → 0
View file @ 6b72b2d9
package mohawk.converter.to.nusmv;
import java.io.*;
import java.nio.file.Files;
import java.util.logging.Logger;
import org.stringtemplate.v4.ST;
import mohawk.converter.to.ConvertTo;
import mohawk.global.helper.RoleHelper;
import mohawk.global.helper.TimeIntervalHelper;
import mohawk.global.pieces.MohawkT;
import mohawk.global.pieces.Query;
import mohawk.global.timing.MohawkTiming;
public class ConvertToNuSMVReduction2 extends ConvertToNuSMV {
public static final Logger logger = Logger.getLogger("mohawk");
public ConvertToNuSMVReduction2(MohawkTiming timing) {
super(timing);
tPrefix = "ConvertToNuSMV";
}
@Override
public String convert(MohawkT m, File file, Boolean writeToFile) {
try {
// Deep Copy Helpers
/* Timing */timing.startTimer(tPrefix + "_" + "deepcopy");
RoleHelper roleHelper = new RoleHelper(m.roleHelper);
TimeIntervalHelper timeIntervalHelper = new TimeIntervalHelper(m.timeIntervalHelper);
Query workableQuery = new Query(m.query);
/* Timing */timing.stopTimer(tPrefix + "_" + "deepcopy");
/* Timing */timing.startTimer(tPrefix + "_" + "sortRolesReduceTimeslots");
// Reduce Roles to Integers
roleHelper.allowZeroRole = false;// roles start from 1 NOT 0!
roleHelper.setupSortedRoles();
// Reduce TimeIntervals to Timeslots
timeIntervalHelper.allowZeroTimeslot = false;// time-slots start from t1 NOT t0!
// Reduction (2)
timeIntervalHelper.reduceToTimeslots();
/* Timing */timing.stopTimer(tPrefix + "_" + "sortRolesReduceTimeslots");
// 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("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;
}
}
src/mohawk/converter/to/nusmv/ConvertToNuSMVReduction3.java deleted 100644 → 0
View file @ 6b72b2d9
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 ConvertToNuSMVReduction3 extends ConvertToNuSMV {
public static final Logger logger = Logger.getLogger("mohawk");
public ConvertToNuSMVReduction3(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;
}
}
src/mohawk/converter/to/nusmv/nusmvTemplate.st
View file @ 52531b36
MODULE main
DEFINE
numroles := 4;
numadminroles := 3; -- Might be used later as a optimization
numusers := numroles + 1;
numtimeslots := 4;
numroles := <numRoles>;
numadminroles := <numAdminRoles>; -- Might be used later as a optimization
numusers := <numUsers>; -- should be = numroles + 1
numtimeslots := <numTimeSlots>;
VAR
RoleEnabled : array 1..numroles of
array 1..numtimeslots of boolean;
-- 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=" & ">)
rule : {CA01, CA02, CA03, ..., CR01, CR02, ..., CE01, ..., CD01, ...};
VAR
rule : {
-- CanAssign
<caruleslist>
-- CanRevoke
<crruleslist>
-- CanEnable
<ceruleslist>
-- CanDisable
<cdruleslist>
};
user : 1 .. numusers;
admin: 1 .. numusers;
-- Users Variable
U01R01T01 : boolean;
-- Continue Above...
ASSIGN
VAR
-- <numUsers> Users Variable
<users:{u|<roleTimeslots:{rt|U<u>R<rt.role>T<rt.time> : boolean;}; separator="\n">}; separator="\n">
-- RoleEnabled
RE01T01 : boolean
-- Continue Above...
-- <numRolesEnabled> RoleEnabled
<enabledRoles:{r|<r> : boolean;}; separator="\n">
ASSIGN
-- Disabling User Role Assignments
init(U01R01T01) := FALSE;
-- Continue Above...
<users:{u|init(<u>):=FALSE;}; separator="\n">
-- Disabling Roles
init(RE01T01) := FALSE;
-- Continue Above...
\ No newline at end of file
<enabledRoles:{r|init(<r>) := FALSE;}; separator="\n">
\ No newline at end of file
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