Commit 32b8e4bb authored by Jonathan Shahen's avatar Jonathan Shahen

Formatting Changes to new formatter

parent 5e919184
......@@ -83,18 +83,18 @@ public class ConverterCUI {
public static void printCommonCommands() {
System.out.println("\n\n--- Common Commands ---");
System.out.println(OptionString.TO_ALL.c()
+ OptionString.SPECFILE.c("data/Mohawk/mixednocr/test04.mohawk.mohawk.T") + OptionString.LOGLEVEL.c()
+ "debug !exit");
System.out.println(
OptionString.TO_ALL.c() + OptionString.SPECFILE.c("data/Mohawk/mixednocr/test04.mohawk.mohawk.T")
+ OptionString.LOGLEVEL.c() + "debug !exit");
System.out.println(OptionString.TO_ALL.c() + OptionString.SPECFILE.c() + "data/regressiontests/positive2.spec "
+ OptionString.LOGLEVEL.c() + "debug !exit");
System.out.println(OptionString.TO_ALL.c() + OptionString.SPECFILE.c() + "data/regressiontests/positive3.spec "
+ OptionString.LOGLEVEL.c() + "debug !exit");
System.out.println(OptionString.TO_ALL.c() + OptionString.SPECFILE.c() + "data/regressiontests/positive4.spec "
+ OptionString.LOGLEVEL.c() + "debug !exit");
System.out.println(OptionString.TO_ALL.c()
+ OptionString.SPECFILE.c("data/Mohawk/positive/test01.mohawk.mohawk.T")
+ OptionString.LOGLEVEL.c("debug") + "!exit");
System.out.println(
OptionString.TO_ALL.c() + OptionString.SPECFILE.c("data/Mohawk/positive/test01.mohawk.mohawk.T")
+ OptionString.LOGLEVEL.c("debug") + "!exit");
System.out.println("");
System.out.println(OptionString.TO_ALL.c() + OptionString.SPECFILE.c("data/Mohawk/positive/")
......@@ -111,9 +111,9 @@ public class ConverterCUI {
System.out.println(OptionString.TO_ALL.c() + OptionString.SPECFILE.c("data/TestsuiteC") + OptionString.BULK.c()
+ OptionString.LOGLEVEL.c("debug") + OptionString.SPECEXT.c(fileExt.Mohawk_T) + "!exit");
System.out.println("");
System.out.println(OptionString.TO_MOHAWK.c() + OptionString.SPECFILE.c("data/TestsuiteC/split1")
+ OptionString.BULK.c() + OptionString.LOGLEVEL.c("debug") + OptionString.SPECEXT.c(fileExt.Mohawk_T)
+ "!exit");
System.out.println(
OptionString.TO_MOHAWK.c() + OptionString.SPECFILE.c("data/TestsuiteC/split1") + OptionString.BULK.c()
+ OptionString.LOGLEVEL.c("debug") + OptionString.SPECEXT.c(fileExt.Mohawk_T) + "!exit");
System.out.println("");
System.out.println(OptionString.TO_TROLE.c() + OptionString.SPECFILE.c("data/Mahesh/easy/")
......
package mohawk.converter;
public enum OptionString {
/** Outputs the authors who have contributed code to this project. Does not allow any other actions to occur. */
AUTHORS("authors"),
BULK("bulk"),
/** Outputs the authors who have contributed code to this project. Does not allow any other actions to occur. */
AUTHORS("authors"), BULK("bulk"),
/** Outputs whether NuSMV could be found. Does not allow any other actions to occur. */
CHECKNUSMV("checknusmv"),
/** Outputs the help menu. Does not allow any other actions to occur. */
HELP("help"),
LINESTR("linstr"),
LOGLEVEL("loglevel"),
LOGFILE("logfile"),
LOGFOLDER("logfolder"),
MAXW("maxw"),
NOHEADER("noheader"),
ONLYREDUCTION("only"),
RESULTSFILE("output"),
SPECFILE("input"),
SPECEXT("specext"),
SHORT_ROLENAMES("shortnames"),
TO_ALL("to_all"),
TO_ASAPTIME_NSA("to_asaptime_nsa"),
TO_ASAPTIME_SA("to_asaptime_sa"),
TO_MOHAWK("to_mohawk"),
HELP("help"), LINESTR("linstr"), LOGLEVEL("loglevel"), LOGFILE("logfile"), LOGFOLDER("logfolder"), MAXW("maxw"), NOHEADER("noheader"), ONLYREDUCTION("only"), RESULTSFILE("output"), SPECFILE("input"), SPECEXT("specext"), SHORT_ROLENAMES("shortnames"), TO_ALL("to_all"), TO_ASAPTIME_NSA("to_asaptime_nsa"), TO_ASAPTIME_SA("to_asaptime_sa"), TO_MOHAWK("to_mohawk"),
/** Takes in a potentially messy Mohawk+T policy and outputs a well nice formatted Mohawk+T policy. */
TO_MOHAWK_T("to_mohawk_t"),
/** Converts a Mohawk+T policy to a NuSMV/NuXMV model. */
TO_NUSMV("to_nusmv"),
TO_TROLE("to_trole"),
TO_TRULE("to_trule"),
/** Outputs the current version of this code repository. Does not allow any other actions to occur.*/
TO_NUSMV("to_nusmv"), TO_TROLE("to_trole"), TO_TRULE("to_trule"),
/** Outputs the current version of this code repository. Does not allow any other actions to occur. */
VERSION("version");
private String _str;
......@@ -43,20 +25,18 @@ public enum OptionString {
return _str;
}
/**
* Returns the commandline equivalent with the hyphen and a space following: AUTHORS -> "-authors "
/** Returns the commandline equivalent with the hyphen and a space following: AUTHORS -> "-authors "
*
* @return
*/
* @return */
public String c() {
return "-" + _str + " ";
}
/**
* Returns the commandline equivalent with the hyphen and a space following: LOGLEVEL("debug") -> "-loglevel debug "
/** Returns the commandline equivalent with the hyphen and a space following: LOGLEVEL("debug") -> "-loglevel debug
* "
*
* @param param
* @return
*/
* @return */
public String c(String param) {
return "-" + _str + " " + param + " ";
}
......
......@@ -84,8 +84,8 @@ public class SpecHelper {
}
if (bulk) {
nusmvFile = new File(new File(smvFilepath).getAbsolutePath() + File.pathSeparator + specFile2.getName()
+ ".smv");
nusmvFile = new File(
new File(smvFilepath).getAbsolutePath() + File.pathSeparator + specFile2.getName() + ".smv");
} else {
nusmvFile = new File(smvFilepath);
}
......
......@@ -17,12 +17,9 @@ import mohawk.global.parser.BooleanErrorListener;
import mohawk.global.parser.mohawkT.MohawkTARBACParser;
import mohawk.global.pieces.*;
/**
* Run these JUnit tests before adding any branch to master
/** Run these JUnit tests before adding any branch to master
*
* @author Jonathan Shahen
*
*/
* @author Jonathan Shahen */
public class ConverterRegressionTests {
public final Logger logger = Logger.getLogger("mohawk");
......
......@@ -25,23 +25,21 @@ public class ConvertTo {
this.timing = timing;
}
/**
* Takes in a Mohawk+T Policy and converts it to an equivalent problem instance. Has the ability to then write that
/** Takes in a Mohawk+T Policy and converts it to an equivalent problem instance. Has the ability to then write that
* instance out to a file, when {@code writeToFile} is TRUE.
*
* @param m Input Mohawk+T policy to convert
* @param f can be <b>NULL</b> if {@code writeToFile} is FALSE
* @param writeToFile TRUE to write the instance out to the file {@code f}
* @return the equivalent instance string
*/
* @param writeToFile TRUE to write the instance out to the file {@code f}
* @return the equivalent instance string */
public String convert(MohawkT m, File f, Boolean writeToFile) {
return null;
}
/**
* Returns the file extension that {@link ConvertTo#convert(MohawkT, File, Boolean)} will append to the file when
/** Returns the file extension that {@link ConvertTo#convert(MohawkT, File, Boolean)} will append to the file when
* writing out
* @return
*/
*
* @return */
public String getFileExtenstion() {
return null;
}
......
......@@ -97,8 +97,7 @@ public class ConvertToASAPTimeNSA extends ConvertTo {
return convertedStr;
}
/**
* Directly converts the Query's timeslot to the reduced timeslot and then it copies the Goal Role is there is only
/** Directly converts the Query's timeslot to the reduced timeslot and then it copies the Goal Role is there is only
* 1. If there is more than 1 Goal Role in the Query then it will create a new Goal Role that is unique and create a
* new Rule such that only someone who has reached the Goal Roles in the original Query can assign this new Goal
* Role and thus make the system REACHABLE.
......@@ -111,8 +110,7 @@ public class ConvertToASAPTimeNSA extends ConvertTo {
* @param rules
* @param roleHelper
* @param timeIntervalHelper
* @return
*/
* @return */
public ASAPTimeNSA_Query toASAPTimeNSA_Query(Query query, ArrayList<ASAPTimeNSA_Rule> rules, RoleHelper roleHelper,
TimeIntervalHelper timeIntervalHelper) {
ASAPTimeNSA_Query q = new ASAPTimeNSA_Query();
......@@ -147,13 +145,10 @@ public class ConvertToASAPTimeNSA extends ConvertTo {
return q;
}
/**
*
* @param rule
/** @param rule
* @param roleHelper
* @param timeIntervalHelper
* @return
*/
* @return */
public ArrayList<ASAPTimeNSA_Rule> toASAPTimeNSA_Rules(Rule rule, RoleHelper roleHelper,
TimeIntervalHelper timeIntervalHelper) {
ArrayList<ASAPTimeNSA_Rule> rules = new ArrayList<ASAPTimeNSA_Rule>();
......
......@@ -42,13 +42,13 @@ public class ConvertToASAPTimeSA extends ConvertTo {
/* Timing */timing.startTimer(tPrefix + "_removeEnableDisableRules");
// Reduction (3)
switch (canEnableVersion) {
case 1:
workableRules = roleHelper.removeEnableDisableRules(m.getAllRules());
break;
case 1 :
workableRules = roleHelper.removeEnableDisableRules(m.getAllRules());
break;
case 2:
workableRules = roleHelper.removeEnableDisableRulesv2(m.getAllRules());
break;
case 2 :
workableRules = roleHelper.removeEnableDisableRulesv2(m.getAllRules());
break;
}
/* Timing */timing.stopTimer(tPrefix + "_removeEnableDisableRules");
......@@ -118,19 +118,18 @@ public class ConvertToASAPTimeSA extends ConvertTo {
Files.write(convertedFile.toPath(), convertedStr.getBytes());
/** Legacy code: use if the Template Files are not working
Charset charset = Charset.forName("US-ASCII");
try (BufferedWriter writer = Files.newBufferedWriter(convertedFile.toPath(), charset)) {
writer.write(convertedStr);
for (ASAPTimeSA_Rule r : newRules) {
writer.write(r.getString() + "\n");
}
writer.flush();
writer.close();
} catch (IOException x) {
System.err.format("IOException: %s%n", x);
}
*/
* Charset charset = Charset.forName("US-ASCII");
* try (BufferedWriter writer = Files.newBufferedWriter(convertedFile.toPath(), charset)) {
* writer.write(convertedStr);
*
* for (ASAPTimeSA_Rule r : newRules) {
* writer.write(r.getString() + "\n");
* }
* writer.flush();
* writer.close();
* } catch (IOException x) {
* System.err.format("IOException: %s%n", x);
* } */
/* Timing */timing.stopTimer(tPrefix + "_" + "Files.write");
}
......@@ -147,8 +146,7 @@ public class ConvertToASAPTimeSA extends ConvertTo {
return convertedStr;
}
/**
* Directly converts the Query's timeslot to the reduced timeslot and then it copies the Goal Role is there is only
/** Directly converts the Query's timeslot to the reduced timeslot and then it copies the Goal Role is there is only
* 1. If there is more than 1 Goal Role in the Query then it will create a new Goal Role that is unique and create a
* new Rule such that only someone who has reached the Goal Roles in the original Query can assign this new Goal
* Role and thus make the system REACHABLE.
......@@ -161,8 +159,7 @@ public class ConvertToASAPTimeSA extends ConvertTo {
* @param rules
* @param roleHelper
* @param timeIntervalHelper
* @return
*/
* @return */
public ASAPTimeSA_Query toASAPTimeSA_Query(Query query, ArrayList<Rule> rules, RoleHelper roleHelper,
TimeIntervalHelper timeIntervalHelper) {
ASAPTimeSA_Query q = new ASAPTimeSA_Query();
......@@ -195,13 +192,10 @@ public class ConvertToASAPTimeSA extends ConvertTo {
return q;
}
/**
*
* @param rule
/** @param rule
* @param roleHelper
* @param timeIntervalHelper
* @return
*/
* @return */
public ArrayList<ASAPTimeSA_Rule> toASAPTimeSA_Rules(Rule rule, RoleHelper roleHelper,
TimeIntervalHelper timeIntervalHelper) {
......
......@@ -46,13 +46,13 @@ public class ConvertToMohawk extends ConvertTo {
/* Timing */timing.startTimer(tPrefix + "_removeEnableDisableRules");
// Reduction (3)
switch (canEnableVersion) {
case 1:
workableRules = roleHelper.removeEnableDisableRules(m.getAllRules());
break;
case 1 :
workableRules = roleHelper.removeEnableDisableRules(m.getAllRules());
break;
case 2:
workableRules = roleHelper.removeEnableDisableRulesv2(m.getAllRules());
break;
case 2 :
workableRules = roleHelper.removeEnableDisableRulesv2(m.getAllRules());
break;
}
/* Timing */timing.stopTimer(tPrefix + "_removeEnableDisableRules");
......@@ -135,13 +135,13 @@ public class ConvertToMohawk extends ConvertTo {
st.add("roles", roleHelperTemporality.getArrayShortNames());
st.add("adminuser", "AU");
st.add("adminrole", "A");
st.add("users", new String[] { "AU", "User" });
st.add("users", new String[]{"AU", "User"});
st.add("specuser", "User");// Can't use 'U'
} else {
st.add("roles", roleHelperTemporality.getArray());
st.add("adminuser", "AdminUser");
st.add("adminrole", "AdminRole");
st.add("users", new String[] { "AdminUser", "User" });
st.add("users", new String[]{"AdminUser", "User"});
st.add("specuser", "User");
}
st.add("specrole", query.specRole);
......
......@@ -16,10 +16,8 @@ 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.
*/
/** 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) {
......@@ -37,11 +35,10 @@ public class ConvertToNuSMV extends ConvertTo {
return ".smv";
}
/**
* Converts Mohawk+T policies to equivalent NuSMV Model Checker instances
* <br/><br/>
* {@inheritDoc}
*/
/** Converts Mohawk+T policies to equivalent NuSMV Model Checker instances
* <br/>
* <br/>
* {@inheritDoc} */
@Override
public String convert(MohawkT m, File file, Boolean writeToFile) {
try {
......@@ -109,8 +106,8 @@ public class ConvertToNuSMV extends ConvertTo {
st.add("numTimeSlots", m.timeIntervalHelper.sizeReduced());
st.add("queryStr", m.query.getString());
st.add("goalRoles", RoleTimeSlot.grabAll(m.query._roles, m.query._timeslot, m.timeIntervalHelper,
m.roleHelper));
st.add("goalRoles",
RoleTimeSlot.grabAll(m.query._roles, m.query._timeslot, m.timeIntervalHelper, m.roleHelper));
st.add("numCARules", caRuleCount);
st.add("numCRRules", crRuleCount);
......
......@@ -44,13 +44,13 @@ public class ConvertToTRole extends ConvertTo {
/* Timing */timing.startTimer(tPrefix + "_removeEnableDisableRules");
// Reduction (3)
switch (canEnableVersion) {
case 1:
workableRules = roleHelper.removeEnableDisableRules(m.getAllRules());
break;
case 1 :
workableRules = roleHelper.removeEnableDisableRules(m.getAllRules());
break;
case 2:
workableRules = roleHelper.removeEnableDisableRulesv2(m.getAllRules());
break;
case 2 :
workableRules = roleHelper.removeEnableDisableRulesv2(m.getAllRules());
break;
}
/* Timing */timing.stopTimer(tPrefix + "_removeEnableDisableRules");
......@@ -145,8 +145,7 @@ public class ConvertToTRole extends ConvertTo {
return convertedStr;
}
/**
* This function creates a new goal role and create a Can Assign rule to assign this new goal role to anyone who
/** This function creates a new goal role and create a Can Assign rule to assign this new goal role to anyone who
* satisfies the original Query's preconditions C and timeslot l. The query returned stored the Mohawk-T version of
* the Goal Role and thus after the Role Helper converts the Roles into Integer references this query must call it's
* finalize() method to convert the goal role into it's integer form.
......@@ -159,8 +158,7 @@ public class ConvertToTRole extends ConvertTo {
* @param rules
* @param roleHelper
* @param timeIntervalHelper
* @return
*/
* @return */
public TRole_Query toTRole_Query(Query query, ArrayList<Rule> rules, RoleHelper roleHelper,
TimeIntervalHelper timeIntervalHelper) {
// Checking Conditions
......
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