diff --git a/src/main/java/de/tlc4b/Log.java b/src/main/java/de/tlc4b/Log.java new file mode 100644 index 0000000000000000000000000000000000000000..431fd6681fbd9f88469e9a5b526c06679b056ca0 --- /dev/null +++ b/src/main/java/de/tlc4b/Log.java @@ -0,0 +1,61 @@ +package de.tlc4b; + +import static de.tlc4b.util.StopWatch.Watches.PARSING_TIME; + +import java.util.ArrayList; + +import de.tlc4b.tlc.TLCResults; +import de.tlc4b.util.StopWatch; +import de.tlc4b.util.StopWatch.Watches; + +public class Log { + + private ArrayList<String> fieldNames = new ArrayList<>(); + private ArrayList<String> fieldValues = new ArrayList<>(); + + public Log(TLC4B tlc4b, TLCResults tlcResults) { + + fieldNames.add("Machine File"); + String machineFile = tlc4b.getMainFile().getAbsolutePath(); + fieldValues.add(machineFile); + + fieldNames.add("TLC Model Checking Time (s)"); + int tlcModelCheckingTime = tlcResults.getModelCheckingTime(); + fieldValues.add(String.valueOf(tlcModelCheckingTime)); + + fieldNames.add("Parsing Time Of B machine (ms)"); + long parseTime = StopWatch.getRunTime(PARSING_TIME); + fieldValues.add(String.valueOf(parseTime)); + + fieldNames.add("Translation Time (ms)"); + long translationTime = StopWatch.getRunTime(Watches.TRANSLATION_TIME); + fieldValues.add(String.valueOf(translationTime)); + + fieldNames.add("Model Checking Time (ms)"); + long modelCheckingTime = StopWatch + .getRunTime(Watches.MODEL_CHECKING_TIME); + fieldValues.add(String.valueOf(modelCheckingTime)); + + } + + public String getCSVValueLine() { + return getCSVLine(fieldValues); + } + + public String getCSVFieldNamesLine() { + return getCSVLine(fieldNames); + } + + private String getCSVLine(ArrayList<String> list) { + StringBuilder sb = new StringBuilder(); + for (int i = 0; i < list.size(); i++) { + sb.append(list.get(i)); + if (i < list.size() - 1) { + sb.append(";"); + } + } + sb.append("\n"); + return sb.toString(); + } + +} diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java index 667c8a5726e916229993580ea0bdb4d88bd76dc7..ed6d4f79766d717a0398f0f8109307b71ea16fd6 100644 --- a/src/main/java/de/tlc4b/TLC4B.java +++ b/src/main/java/de/tlc4b/TLC4B.java @@ -5,6 +5,7 @@ import java.io.File; import java.io.FileInputStream; import java.io.FileNotFoundException; import java.io.FileOutputStream; +import java.io.FileWriter; import java.io.IOException; import java.io.InputStream; import java.io.OutputStreamWriter; @@ -30,6 +31,7 @@ public class TLC4B { private File mainfile; private String machineFileNameWithoutFileExtension; // e.g. Test of file foo/bar/Test.mch + private String logFileString; private File buildDir; @@ -67,10 +69,11 @@ public class TLC4B { TLCRunner.runTLC(tlc4b.machineFileNameWithoutFileExtension, tlc4b.buildDir); - TLCResults results = new TLCResults(tlc4b.tlcOutputInfo); results.evalResults(); tlc4b.printResults(results, TLC4BGlobals.isCreateTraceFile()); + Log log = new Log(tlc4b, results); + tlc4b.createLogFile(log); System.exit(0); } catch (NoClassDefFoundError e) { @@ -219,7 +222,6 @@ public class TLC4B { TLCResults results = new TLCResults(tlc4b.tlcOutputInfo); results.evalResults(); tlc4b.printResults(results, false); - System.exit(0); } } @@ -259,6 +261,14 @@ public class TLC4B { TLC4BGlobals.setDeleteOnExit(true); } else if (args[index].toLowerCase().equals("-parinveval")) { TLC4BGlobals.setPartialInvariantEvaluation(true); + } else if (args[index].toLowerCase().equals("-log")) { + index = index + 1; + if (index == args.length) { + throw new TLC4BIOException( + "Error: File requiered after option '-log'."); + } + logFileString = args[index]; + } else if (args[index].toLowerCase().equals("-maxint")) { index = index + 1; if (index == args.length) { @@ -382,6 +392,26 @@ public class TLC4B { } } + private void createLogFile(Log log) { + if (logFileString != null) { + File logFile = new File(logFileString); + FileWriter fw; + boolean fileExists = logFile.exists(); + try { + fw = new FileWriter(logFile, true); // the true will append the + // new data + if (!fileExists) { + fw.write(log.getCSVFieldNamesLine()); + } + fw.write(log.getCSVValueLine()); + fw.close(); + println("Log file: " + logFile.getAbsolutePath()); + } catch (IOException e) { + new TLC4BIOException(e.getLocalizedMessage()); + } + } + } + private void createFiles() { boolean dirCreated = buildDir.mkdir(); if (dirCreated && TLC4BGlobals.isDeleteOnExit()) { @@ -403,6 +433,7 @@ public class TLC4B { println("Configuration file '" + configFile.getAbsolutePath() + "' created."); } + createStandardModules(); } @@ -501,4 +532,8 @@ public class TLC4B { return machineFileNameWithoutFileExtension; } + public File getMainFile(){ + return this.mainfile; + } + } diff --git a/src/main/java/de/tlc4b/TLCRunner.java b/src/main/java/de/tlc4b/TLCRunner.java index 3087b77672e5bdada5265796b408989aab3c2d6f..d90fbef8607fc2af0b00f0a85de709df035437be 100644 --- a/src/main/java/de/tlc4b/TLCRunner.java +++ b/src/main/java/de/tlc4b/TLCRunner.java @@ -1,5 +1,7 @@ package de.tlc4b; +import static de.tlc4b.util.StopWatch.Watches.MODEL_CHECKING_TIME; + import java.io.BufferedReader; import java.io.File; import java.io.FileNotFoundException; @@ -13,6 +15,7 @@ import java.util.HashSet; import java.util.List; import java.util.Set; +import de.tlc4b.util.StopWatch; import util.SimpleFilenameToStream; import util.ToolIO; import tlc2.TLC; @@ -90,6 +93,7 @@ public class TLCRunner { } public static void runTLC(String machineName, File path) { + StopWatch.start(MODEL_CHECKING_TIME); MP.println("--------------------------------"); MP.TLCOutputStream.changeOutputStream(); ToolIO.setMode(ToolIO.SYSTEM); @@ -134,6 +138,7 @@ public class TLCRunner { // return messages; MP.TLCOutputStream.resetOutputStream(); MP.println("--------------------------------"); + StopWatch.stop(MODEL_CHECKING_TIME); } private static void closeThreads() { diff --git a/src/main/java/de/tlc4b/util/StopWatch.java b/src/main/java/de/tlc4b/util/StopWatch.java index d93065fd9fb72250bdab09b20c465df95dbf282d..b978519b87e94dea1c21db1a338940d5bc2cb50e 100644 --- a/src/main/java/de/tlc4b/util/StopWatch.java +++ b/src/main/java/de/tlc4b/util/StopWatch.java @@ -9,7 +9,7 @@ public class StopWatch { private static final Hashtable<Watches, Long> runTime = new Hashtable<Watches, Long>(); public enum Watches{ - PARSING_TIME, TRANSLATION_TIME, TLC_TIME, OVERALL_TIME + PARSING_TIME, TRANSLATION_TIME, TLC_TIME, OVERALL_TIME, MODEL_CHECKING_TIME } public static void start(Watches watch){