Commit 43e64ae5 authored by Jonathan Shahen's avatar Jonathan Shahen

Init commit to fix some of the errors that got introduced after the conference paper:

 * The long time on AGTUniv10 is due to a simple System.out.prinln printing too much text to the screen. The fix is to reduce the amount that is outputted.
 * The CR Error did not appear in the conference paper because it was an assert that was old and should have been removed, but asserts are ignored in Java, except in debugging mode, so the conference code did not have this problem. Between the conference code and now I converted all asserts to IF statements with throws, but this assert should have been removed

More testing is required before version increase and merging into master
parent d32fba51
......@@ -12,6 +12,14 @@ import java.util.logging.Handler;
import java.util.logging.Level;
import java.util.logging.Logger;
import org.apache.commons.cli.BasicParser;
import org.apache.commons.cli.CommandLine;
import org.apache.commons.cli.CommandLineParser;
import org.apache.commons.cli.HelpFormatter;
import org.apache.commons.cli.OptionBuilder;
import org.apache.commons.cli.Options;
import org.apache.commons.lang3.StringUtils;
import mohawk.converter.generated.MohawkTARBACParser;
import mohawk.converter.helper.SpecHelper;
import mohawk.converter.logging.MohawkCSVFileFormatter;
......@@ -24,14 +32,6 @@ import mohawk.global.FileExtensions;
import mohawk.global.pieces.MohawkT;
import mohawk.global.timing.MohawkTiming;
import org.apache.commons.cli.BasicParser;
import org.apache.commons.cli.CommandLine;
import org.apache.commons.cli.CommandLineParser;
import org.apache.commons.cli.HelpFormatter;
import org.apache.commons.cli.OptionBuilder;
import org.apache.commons.cli.Options;
import org.apache.commons.lang3.StringUtils;
public class ConverterInstance {
private static final String VERSION = "v1.1.2";
private static final String AUTHORS = "Jonathan Shahen <jmshahen@uwaterloo.ca>";
......@@ -163,8 +163,8 @@ public class ConverterInstance {
if (toTRole.lastError == null) {
logger.info("[SUCCESS] Successfully converted to TRole Input Format");
} else {
logger.warning("[FAILURE] Failed to convert to TRole Input Format; Error code "
+ toTRole.lastError);
logger.warning(
"[FAILURE] Failed to convert to TRole Input Format; Error code " + toTRole.lastError);
}
/* Timing */timing.stopTimer("convertToTRole (" + i + ")");
......@@ -233,7 +233,7 @@ public class ConverterInstance {
logger.info("[EOF] Converter Instance done running");
for (Handler h : logger.getHandlers()) {
h.close(); //must call h.close or a .LCK file will remain.
h.close();//must call h.close or a .LCK file will remain.
}
return 0;
}
......@@ -256,8 +256,9 @@ public class ConverterInstance {
public void printHelp(Options options, int maxw) {
HelpFormatter f = new HelpFormatter();
f.printHelp(maxw, "mohawk-converter", StringUtils.repeat("-", maxw) + "\nAuthors: " + AUTHORS + "\n"
+ StringUtils.repeat("-", 20), options, StringUtils.repeat("-", maxw), true);
f.printHelp(maxw, "mohawk-converter",
StringUtils.repeat("-", maxw) + "\nAuthors: " + AUTHORS + "\n" + StringUtils.repeat("-", 20), options,
StringUtils.repeat("-", maxw), true);
}
@SuppressWarnings("static-access")
......@@ -270,37 +271,31 @@ public class ConverterInstance {
"Checks that NuSMV is on the system and displays which version is installed");
// Add Logging Level Options
options.addOption(OptionBuilder
.withArgName("quiet|debug|verbose")
.withDescription(
"Be extra quiet only errors are shown; " + "Show debugging information; "
+ "extra information is given for Verbose; " + "default is warning level").hasArg()
.create(OptionString.LOGLEVEL.toString()));
options.addOption(OptionBuilder
.withArgName("logfile|'n'|'u'")
.withDescription(
"The filepath where the log file should be created; "
+ "No file will be created when equal to 'n'; "
+ "A unique filename will be created when equal to 'u'; "
+ "default it creates a log called '" + Logger_filepath + "'").hasArg()
.create(OptionString.LOGFILE.toString()));
options.addOption(OptionBuilder
.withArgName("folder path")
.withDescription(
"The path to the location that the logs should be placed, "
+ "default it puts the logs in the folder '" + Logger_folderpath + "'").hasArg()
.create(OptionString.LOGFOLDER.toString()));
options.addOption(OptionBuilder.withArgName("quiet|debug|verbose")
.withDescription("Be extra quiet only errors are shown; " + "Show debugging information; "
+ "extra information is given for Verbose; " + "default is between debug and verbose level")
.hasArg().create(OptionString.LOGLEVEL.toString()));
options.addOption(OptionBuilder.withArgName("logfile|'n'|'u'")
.withDescription("The filepath where the log file should be created; "
+ "No file will be created when equal to 'n'; "
+ "A unique filename will be created when equal to 'u'; " + "default it creates a log called '"
+ Logger_filepath + "'")
.hasArg().create(OptionString.LOGFILE.toString()));
options.addOption(OptionBuilder.withArgName("folder path")
.withDescription("The path to the location that the logs should be placed, "
+ "default it puts the logs in the folder '" + Logger_folderpath + "'")
.hasArg().create(OptionString.LOGFOLDER.toString()));
options.addOption(OptionString.NOHEADER.toString(), false,
"Does not write the CSV file header to the output log");
options.addOption(OptionBuilder.withArgName("csvfile")
.withDescription("The file where the result should be stored").hasArg()
.create(OptionString.RESULTSFILE.toString()));
options.addOption(
OptionBuilder.withArgName("csvfile").withDescription("The file where the result should be stored")
.hasArg().create(OptionString.RESULTSFILE.toString()));
// custom Console Logging Options
options.addOption(OptionBuilder.withArgName("num")
.withDescription("The maximum width of the console (default 120)").hasArg()
.create(OptionString.MAXW.toString()));
options.addOption(
OptionBuilder.withArgName("num").withDescription("The maximum width of the console (default 120)")
.hasArg().create(OptionString.MAXW.toString()));
options.addOption(OptionBuilder.withArgName("string")
.withDescription("The new line string when wrapping a long line (default '\\n ')").hasArg()
.create(OptionString.LINESTR.toString()));
......@@ -310,11 +305,11 @@ public class ConverterInstance {
.withDescription("Path to the Mohawk-T Spec File, or Folder if the 'bulk' option is set").hasArg()
.create(OptionString.SPECFILE.toString()));
options.addOption(OptionBuilder
.withArgName("extension")
options.addOption(OptionBuilder.withArgName("extension")
.withDescription(
"File extention used when searching for SPEC files when the 'bulk' option is used. Default:'"
+ specHelper.specFileExt + "'").hasArg().create(OptionString.SPECEXT.toString()));
+ specHelper.specFileExt + "'")
.hasArg().create(OptionString.SPECEXT.toString()));
// Add Functional Options
options.addOption(OptionString.BULK.toString(), false,
......@@ -345,7 +340,7 @@ public class ConverterInstance {
// Logging Level
logger.setUseParentHandlers(false);
consoleHandler.setFormatter(new MohawkConsoleFormatter());
setLoggerLevel(Level.FINE); // Default Level
setLoggerLevel(Level.FINE);// Default Level
if (cmd.hasOption(OptionString.LOGLEVEL.toString())) {
String loglevel = cmd.getOptionValue(OptionString.LOGLEVEL.toString());
if (loglevel.equalsIgnoreCase("quiet")) {
......@@ -383,8 +378,8 @@ public class ConverterInstance {
} else {
try {
// Create a log file with a specific name
File logfile = new File(Logger_folderpath + File.separator
+ cmd.getOptionValue(OptionString.LOGFILE.toString()));
File logfile = new File(
Logger_folderpath + File.separator + cmd.getOptionValue(OptionString.LOGFILE.toString()));
if (!logfile.exists()) {
logfile.createNewFile();
......@@ -392,7 +387,7 @@ public class ConverterInstance {
Logger_filepath = logfile.getAbsolutePath();
if (WriteCSVFileHeader) {
FileOutputStream writer = new FileOutputStream(logfile, true); // Always append!
FileOutputStream writer = new FileOutputStream(logfile, true);// Always append!
writer.write(MohawkCSVFileFormatter.csvHeaders().getBytes());
writer.flush();
writer.close();
......
......@@ -9,6 +9,8 @@ import java.util.SortedSet;
import java.util.TreeSet;
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;
......@@ -21,10 +23,8 @@ import mohawk.global.pieces.reduced.query.ASAPTimeNSA_Query;
import mohawk.global.pieces.reduced.rules.ASAPTimeNSA_Rule;
import mohawk.global.timing.MohawkTiming;
import org.stringtemplate.v4.ST;
public class ConvertToASAPTimeNSA extends ConvertTo {
public static final Logger logger = Logger.getGlobal();
public static final Logger logger = Logger.getLogger("mohawk");
public ConvertToASAPTimeNSA(MohawkTiming timing) {
super(timing);
......@@ -45,10 +45,10 @@ public class ConvertToASAPTimeNSA extends ConvertTo {
/* Timing */timing.startTimer(tPrefix + "_" + "sortRolesReduceTimeslots");
// Reduce Roles to Integers
roleHelper.allowZeroRole = false; // roles start from 1 NOT 0!
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!
timeIntervalHelper.allowZeroTimeslot = false;// time-slots start from t1 NOT t0!
timeIntervalHelper.reduceToTimeslots();
/* Timing */timing.stopTimer(tPrefix + "_" + "sortRolesReduceTimeslots");
......@@ -64,8 +64,8 @@ public class ConvertToASAPTimeNSA extends ConvertTo {
// Stats and logging
numberOfRules = rules.size();
logger.finest("Rules: " + m.getAllRules());
logger.finest("Reduced Rules: " + rules);
logger.fine("Rules: " + m.getAllRules());
logger.fine("Reduced Rules: " + rules);
// Generate the Converted String
/* Timing */timing.startTimer(tPrefix + "_" + "template");
......@@ -125,11 +125,18 @@ public class ConvertToASAPTimeNSA extends ConvertTo {
// Set the Goal Timeslot
SortedSet<Integer> goalTimeslots = timeIntervalHelper.indexOfReduced(query._timeslot);
assert (goalTimeslots.size() == 1) : "The reduced query must have only one timeslot";
if (goalTimeslots.size() != 1) {
logger.severe("goalTimeslots size: " + goalTimeslots.size());
throw new IllegalArgumentException("The reduced query must have only one timeslot");
}
q.goalTimeslot = goalTimeslots.first();
// Set the Goal Role
assert (query._roles.size() > 0) : "The query must have atleast one Goal Role";
if (query._roles.size() == 0) {
logger.severe("query._roles size: " + query._roles.size());
throw new IllegalArgumentException("The query must have atleast one Goal Role");
}
if (query._roles.size() == 1) {
q.goalRole = roleHelper.indexOf(query._roles.get(0));
} else {
......
......@@ -10,6 +10,8 @@ import java.util.TreeSet;
import java.util.logging.Level;
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;
......@@ -22,8 +24,6 @@ import mohawk.global.pieces.reduced.query.ASAPTimeSA_Query;
import mohawk.global.pieces.reduced.rules.ASAPTimeSA_Rule;
import mohawk.global.timing.MohawkTiming;
import org.stringtemplate.v4.ST;
public class ConvertToASAPTimeSA extends ConvertTo {
public static final Logger logger = Logger.getLogger("mohawk");
......@@ -50,19 +50,25 @@ public class ConvertToASAPTimeSA extends ConvertTo {
workableRules = roleHelper.removeEnableDisableRules(m.getAllRules());
/* Timing */timing.stopTimer(tPrefix + "_" + "removeEnableDisableRules");
logger.fine("[STEPWISE] Query Before roleHelper.alwaysOnRules Conversion: " + workableQuery);
logger.fine("[STEPWISE] Rules Before roleHelper.alwaysOnRules Conversion: " + workableRules);
/* Timing */timing.startTimer(tPrefix + "_" + "alwaysOnRules");
workableRules = roleHelper.alwaysOnRules(workableRules, workableQuery, timeIntervalHelper);
/* Timing */timing.stopTimer(tPrefix + "_" + "alwaysOnRules");
/* Timing */timing.startTimer(tPrefix + "_" + "reduceToTimeslots");
// Reduce TimeIntervals to Timeslots
timeIntervalHelper.allowZeroTimeslot = false; // time-slots start from t1 NOT t0!
timeIntervalHelper.reduceToTimeslots();
// Reduce Roles to Integers
roleHelper.allowZeroRole = false; // roles start from 1 NOT 0!
roleHelper.setupSortedRoles();
timeIntervalHelper.allowZeroTimeslot = false;// time-slots start from t1 NOT t0!
timeIntervalHelper.reduceToTimeslots();// Reduce TimeIntervals to Timeslots
roleHelper.allowZeroRole = false;// roles start from 1 NOT 0!
roleHelper.setupSortedRoles();// Reduce Roles to Integers
/* Timing */timing.stopTimer(tPrefix + "_" + "reduceToTimeslots");
logger.fine("[STEPWISE] Query Before ASAPTimeSA_Query Conversion: " + workableQuery);
logger.fine("[STEPWISE] Rules Before toASAPTimeSA_Rules Conversion: " + workableRules);
// Convert Query to Reduced ASAPTime SA Query and add any extra rules as needed
ASAPTimeSA_Query query = toASAPTimeSA_Query(workableQuery, workableRules, roleHelper, timeIntervalHelper);
......@@ -75,8 +81,8 @@ public class ConvertToASAPTimeSA extends ConvertTo {
// Stats and logging
numberOfRules = newRules.size();
logger.finest("Rules: " + m.getAllRules());
logger.finest("Reduced Rules: " + newRules);
logger.fine("Rules: " + m.getAllRules());
logger.fine("Reduced Rules: " + newRules);
// Generate the Converted String
/* Timing */timing.startTimer(tPrefix + "_" + "template");
......@@ -104,7 +110,7 @@ public class ConvertToASAPTimeSA extends ConvertTo {
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");
}
......@@ -152,11 +158,18 @@ public class ConvertToASAPTimeSA extends ConvertTo {
// Set the Goal Timeslot
SortedSet<Integer> goalTimeslots = timeIntervalHelper.indexOfReduced(query._timeslot);
assert (goalTimeslots.size() == 1) : "The reduced query must have only one timeslot";
if (goalTimeslots.size() != 1) {
logger.severe("goalTimeslots size: " + goalTimeslots.size());
throw new IllegalArgumentException("The reduced query must have only one timeslot");
}
q.goalTimeslot = goalTimeslots.first();
// Set the Goal Role
assert (query._roles.size() > 0) : "The query must have atleast one Goal Role";
if (query._roles.size() == 0) {
logger.severe("query._roles size: " + query._roles.size());
throw new IllegalArgumentException("The query must have atleast one Goal Role");
}
if (query._roles.size() == 1) {
q.goalRole = roleHelper.indexOf(query._roles.get(0));
} else {
......
......@@ -8,6 +8,8 @@ import java.util.ArrayList;
import java.util.Arrays;
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;
......@@ -22,10 +24,8 @@ import mohawk.global.pieces.reduced.rules.MohawkCA_Rule;
import mohawk.global.pieces.reduced.rules.MohawkCR_Rule;
import mohawk.global.timing.MohawkTiming;
import org.stringtemplate.v4.ST;
public class ConvertToMohawk extends ConvertTo {
public static final Logger logger = Logger.getLogger("mohawk-converter");
public static final Logger logger = Logger.getLogger("mohawk");
public ConvertToMohawk(MohawkTiming timing) {
super(timing);
......@@ -47,32 +47,43 @@ public class ConvertToMohawk extends ConvertTo {
/* Timing */timing.stopTimer(tPrefix + "_deepcopy");
/* Timing */timing.startTimer(tPrefix + "_removeEnableDisableRules");
workableRules = roleHelper.removeEnableDisableRules(m.getAllRules()); // (3)
workableRules = roleHelper.removeEnableDisableRules(m.getAllRules());
// (3)
/* Timing */timing.stopTimer(tPrefix + "_removeEnableDisableRules");
// Convert Query to Reduced ASAPTime SA Query and add any extra rules as needed
//Mohawk_Query query = toMohawk_Query(workableQuery, workableRules, roleHelper, timeIntervalHelper);
/* Timing */timing.startTimer(tPrefix + "_alwaysOnRules");
workableRules = roleHelper.alwaysOnRules(workableRules, workableQuery, timeIntervalHelper); // (4)
workableRules = roleHelper.alwaysOnRules(workableRules, workableQuery, timeIntervalHelper);
// (4)
/* Timing */timing.stopTimer(tPrefix + "_alwaysOnRules");
// Convert Query to Reduced ASAPTime SA Query and add any extra rules as needed
Mohawk_Query query = toMohawk_Query(workableQuery, workableRules, roleHelper, timeIntervalHelper);
/* Timing */timing.startTimer(tPrefix + "_removeUninvokablePrecondtions");
workableRules = roleHelper.removeUninvokablePrecondtions(workableRules, false); // (6)
workableRules = roleHelper.removeUninvokablePrecondtions(workableRules, false);
// (6)
/* Timing */timing.stopTimer(tPrefix + "_removeUninvokablePrecondtions");
logger.fine("[STEPWISE] Rules Before roleHelperTemporality.removePrecondtionsCanRevoke Conversion: "
+ workableRules);
/* Timing */timing.startTimer(tPrefix + "_removePrecondtionsCanRevoke");
workableRules = roleHelper.removePrecondtionsCanRevoke(workableRules, false); // (6)
workableRules = roleHelper.removePrecondtionsCanRevoke(workableRules, false);
// (6)
/* Timing */timing.stopTimer(tPrefix + "_removePrecondtionsCanRevoke");
logger.fine("[STEPWISE] Rules Before roleHelperTemporality.removeTemporality Conversion: " + workableRules);
/* Timing */timing.startTimer(tPrefix + "_removeTemporality");
RoleHelper roleHelperTemporality = new RoleHelper(roleHelper);
ArrayList<Object> reducedRules = roleHelperTemporality.removeTemporality(workableRules, timeIntervalHelper);
/* Timing */timing.stopTimer(tPrefix + "_removeTemporality");
logger.fine("[STEPWISE] Rules Before CA and CR Conversion: " + workableRules);
// Convert Rules into Reduced Mohawk CA and CR Rules (5)
/* Timing */timing.startTimer(tPrefix + "_convertRules");
for (Object r : reducedRules) {
......
......@@ -12,6 +12,8 @@ import java.util.ArrayList;
import java.util.Arrays;
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;
......@@ -25,10 +27,8 @@ import mohawk.global.pieces.reduced.query.TRole_Query;
import mohawk.global.pieces.reduced.rules.TRole_Rule;
import mohawk.global.timing.MohawkTiming;
import org.stringtemplate.v4.ST;
public class ConvertToTRole extends ConvertTo {
public static final Logger logger = Logger.getGlobal();
public static final Logger logger = Logger.getLogger("mohawk");
public ConvertToTRole(MohawkTiming timing) {
super(timing);
......@@ -57,7 +57,7 @@ public class ConvertToTRole extends ConvertTo {
/* Timing */timing.stopTimer(tPrefix + "_" + "alwaysOnRules");
// Reduce Roles to Integers
roleHelper.allowZeroRole = false; // roles start from 1 NOT 0!
roleHelper.allowZeroRole = false;// roles start from 1 NOT 0!
roleHelper.setupSortedRoles();
// Convert Query to Reduced ASAPTime SA Query and add any extra rules as needed
......@@ -87,7 +87,7 @@ public class ConvertToTRole extends ConvertTo {
/*
File convertedFile = new File(file.getAbsolutePath() + getFileExtenstion());
FileOutputStream out = new FileOutputStream(convertedFile);
out.write(header.getBytes());
// Convert Rules into Reduced ASAPTime NSA Rules
for (Rule r : workableRules) {
......@@ -99,8 +99,8 @@ public class ConvertToTRole extends ConvertTo {
*/
Charset charset = Charset.forName("US-ASCII");
try (BufferedWriter writer = Files.newBufferedWriter(
Paths.get(file.getAbsolutePath() + getFileExtenstion()), charset)) {
try (BufferedWriter writer = Files
.newBufferedWriter(Paths.get(file.getAbsolutePath() + getFileExtenstion()), charset)) {
writer.write(header);
// Convert Rules into Reduced ASAPTime NSA Rules
for (Rule r : workableRules) {
......@@ -158,7 +158,10 @@ public class ConvertToTRole extends ConvertTo {
public TRole_Query toTRole_Query(Query query, ArrayList<Rule> rules, RoleHelper roleHelper,
TimeIntervalHelper timeIntervalHelper) {
// Checking Conditions
assert (query._roles.size() > 0) : "The query must have atleast one Goal Role";
if (query._roles.size() == 0) {
logger.severe("The query must have atleast one Goal Role: " + query);
throw new IllegalArgumentException("The query must have atleast one Goal Role");
}
Role newGoalRole = roleHelper.addUniqueRole("goalRole");
TRole_Query q = new TRole_Query(newGoalRole);
......
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