From 2604e2044793274b536bba2696c1ba6fd1e2ac24 Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Mon, 1 Jun 2015 12:08:20 +0200
Subject: [PATCH] print coverage statistics
---
src/main/java/de/tlc4b/TLC4BGlobals.java | 10 ++++++++++
src/main/java/de/tlc4b/TLCRunner.java | 6 ++++++
src/main/java/de/tlc4b/Translator.java | 10 +++++++---
src/main/java/de/tlc4b/analysis/MachineContext.java | 4 ++++
4 files changed, 27 insertions(+), 3 deletions(-)
diff --git a/src/main/java/de/tlc4b/TLC4BGlobals.java b/src/main/java/de/tlc4b/TLC4BGlobals.java
index faf0db7..88abc39 100644
--- a/src/main/java/de/tlc4b/TLC4BGlobals.java
+++ b/src/main/java/de/tlc4b/TLC4BGlobals.java
@@ -14,6 +14,7 @@ public class TLC4BGlobals {
private static boolean proBconstantsSetup;
private static boolean partialInvariantEvaluation;
private static boolean useSymmetry;
+ private static boolean printCoverage;
private static boolean deleteFilesOnExit;
@@ -49,6 +50,7 @@ public class TLC4BGlobals {
checkWD = false;
partialInvariantEvaluation = false;
useSymmetry = false;
+ printCoverage = false;
setForceTLCToEvalConstants(true);
setProBconstantsSetup(false);
@@ -247,5 +249,13 @@ public class TLC4BGlobals {
public static void setSymmetryUse(boolean b) {
useSymmetry = b;
}
+
+ public static void setPrintCoverage(boolean b){
+ printCoverage = b;
+ }
+
+ public static boolean isPrintCoverage(){
+ return printCoverage;
+ }
}
diff --git a/src/main/java/de/tlc4b/TLCRunner.java b/src/main/java/de/tlc4b/TLCRunner.java
index 8be4aad..9e67b65 100644
--- a/src/main/java/de/tlc4b/TLCRunner.java
+++ b/src/main/java/de/tlc4b/TLCRunner.java
@@ -103,6 +103,12 @@ public class TLCRunner {
list.add("-workers");
list.add("" + TLC4BGlobals.getWorkers());
}
+
+ if(TLC4BGlobals.isPrintCoverage()){
+ list.add("-nowarning");
+ list.add("-coverage");
+ list.add(""+ 100);
+ }
//list.add("-config");
//list.add(machineName + ".cfg");
diff --git a/src/main/java/de/tlc4b/Translator.java b/src/main/java/de/tlc4b/Translator.java
index 135c9f0..efc50e4 100644
--- a/src/main/java/de/tlc4b/Translator.java
+++ b/src/main/java/de/tlc4b/Translator.java
@@ -111,6 +111,10 @@ public class Translator {
MachineContext machineContext = new MachineContext(machineName, start,
ltlFormula, constantsSetup);
this.machineName = machineContext.getMachineName();
+ if(machineContext
+ .machineContainsOperations()){
+ TLC4BGlobals.setPrintCoverage(true);
+ }
Typechecker typechecker = new Typechecker(machineContext);
UnchangedVariablesFinder unchangedVariablesFinder = new UnchangedVariablesFinder(
@@ -155,7 +159,8 @@ public class Translator {
TLAPrinter printer = new TLAPrinter(machineContext, typechecker,
unchangedVariablesFinder, precedenceCollector, usedModules,
typeRestrictor, generator.getTlaModule(),
- generator.getConfigFile(), primedNodesMarker, renamer, invariantPreservationAnalysis);
+ generator.getConfigFile(), primedNodesMarker, renamer,
+ invariantPreservationAnalysis);
printer.start();
moduleString = printer.getStringbuilder().toString();
configString = printer.getConfigString().toString();
@@ -197,9 +202,8 @@ public class Translator {
return usedStandardModules;
}
- public String getTranslatedLTLFormula(){
+ public String getTranslatedLTLFormula() {
return translatedLTLFormula;
}
-
}
diff --git a/src/main/java/de/tlc4b/analysis/MachineContext.java b/src/main/java/de/tlc4b/analysis/MachineContext.java
index 0db6b07..2002c16 100644
--- a/src/main/java/de/tlc4b/analysis/MachineContext.java
+++ b/src/main/java/de/tlc4b/analysis/MachineContext.java
@@ -1090,6 +1090,10 @@ public class MachineContext extends DepthFirstAdapter {
return invariantMachineClause;
}
+ public boolean machineContainsOperations() {
+ return operations.size() > 0;
+ }
+
public AInitialisationMachineClause getInitialisationMachineClause() {
return initialisationMachineClause;
}
--
GitLab