From 926f3d5a495ea97739e6b0b923b02dac682cea90 Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Tue, 2 Jun 2015 10:43:38 +0200
Subject: [PATCH] updated gradle file
---
build.gradle | 6 +-
src/main/java/de/tlc4b/TLC4B.java | 21 +++++
src/main/java/de/tlc4b/TLCRunner.java | 10 +--
src/main/java/de/tlc4b/tlc/TLCOutputInfo.java | 2 +-
src/main/java/de/tlc4b/tlc/TLCResults.java | 81 ++++++++++++++++++-
5 files changed, 112 insertions(+), 8 deletions(-)
diff --git a/build.gradle b/build.gradle
index 1473342..7639ef0 100644
--- a/build.gradle
+++ b/build.gradle
@@ -19,11 +19,15 @@ configurations { // configuration that holds jars to copy into lib
releaseJars
}
+configurations.all {
+ resolutionStrategy.cacheChangingModulesFor 0, 'seconds'
+}
+
def parser_version = '2.4.36-SNAPSHOT'
dependencies {
//compile (group: 'com.microsoft', name: 'tla2tools', version: '1.4.6')
- compile (group: 'de.tla', name: 'tlatools', version: '1.0.0-SNAPSHOT')
+ compile (group: 'de.tla', name: 'tlatools', version: '1.0.0-SNAPSHOT', changing: true)
compile (group: 'de.prob', name: 'prologlib', version: parser_version)
compile (group: 'de.prob', name: 'parserbase', version: parser_version)
diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java
index d95d1da..30a634d 100644
--- a/src/main/java/de/tlc4b/TLC4B.java
+++ b/src/main/java/de/tlc4b/TLC4B.java
@@ -9,6 +9,10 @@ import java.io.IOException;
import java.io.InputStream;
import java.io.OutputStreamWriter;
import java.io.UnsupportedEncodingException;
+import java.util.LinkedHashMap;
+import java.util.Map;
+import java.util.Set;
+import java.util.Map.Entry;
import tlc2.TLCGlobals;
import de.be4.classicalb.core.parser.exceptions.BException;
@@ -72,6 +76,7 @@ public class TLC4B {
}
private void printResults(TLCResults results, boolean createTraceFile) {
+ printOperationsCount(results);
// options
System.out.println("Used Options");
System.out.println("| Number of workers: " + TLC4BGlobals.getWorkers());
@@ -129,6 +134,22 @@ public class TLC4B {
}
+ private void printOperationsCount(TLCResults results) {
+ LinkedHashMap<String, Long> operationCount = results
+ .getOperationCount();
+ if (TLC4BGlobals.isPrintCoverage() && operationCount != null) {
+ System.out.println("---------- Coverage statistics ----------");
+
+ for (Entry<String, Long> entry : operationCount.entrySet()) {
+ String key = entry.getKey();
+ String value = entry.getValue().toString();
+ System.out.println(key + ": " + value);
+ }
+ System.out
+ .println("---------- End of coverage statistics ----------");
+ }
+ }
+
public static void test(String[] args, boolean deleteFiles)
throws Exception {
TLC4BGlobals.resetGlobals();
diff --git a/src/main/java/de/tlc4b/TLCRunner.java b/src/main/java/de/tlc4b/TLCRunner.java
index 9e67b65..611bd49 100644
--- a/src/main/java/de/tlc4b/TLCRunner.java
+++ b/src/main/java/de/tlc4b/TLCRunner.java
@@ -103,15 +103,15 @@ public class TLCRunner {
list.add("-workers");
list.add("" + TLC4BGlobals.getWorkers());
}
-
- if(TLC4BGlobals.isPrintCoverage()){
+
+ if (TLC4BGlobals.isPrintCoverage()) {
list.add("-nowarning");
list.add("-coverage");
- list.add(""+ 100);
+ list.add("" + 60);
}
- //list.add("-config");
- //list.add(machineName + ".cfg");
+ // list.add("-config");
+ // list.add(machineName + ".cfg");
list.add(machineName);
ToolIO.setUserDir(path.getPath());
String[] args = list.toArray(new String[list.size()]);
diff --git a/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java b/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
index 1e3932f..ef0c9e7 100644
--- a/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
+++ b/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
@@ -17,7 +17,7 @@ import de.tlc4b.tla.config.ModelValueAssignment;
public class TLCOutputInfo {
- Hashtable<String, String> namesMapping;
+ public Hashtable<String, String> namesMapping;
Hashtable<String, BType> typesTable;
Set<String> constants;
boolean constantSetup = false;
diff --git a/src/main/java/de/tlc4b/tlc/TLCResults.java b/src/main/java/de/tlc4b/tlc/TLCResults.java
index a2d4ad2..cfc8ad3 100644
--- a/src/main/java/de/tlc4b/tlc/TLCResults.java
+++ b/src/main/java/de/tlc4b/tlc/TLCResults.java
@@ -2,21 +2,35 @@ package de.tlc4b.tlc;
import java.util.ArrayList;
import java.util.Date;
+import java.util.Hashtable;
+import java.util.LinkedHashMap;
+import java.util.Map.Entry;
+import java.util.Set;
import de.tlc4b.TLC4BGlobals;
import static de.tlc4b.tlc.TLCResults.TLCResult.*;
+import tla2sany.semantic.ExprNode;
+import tla2sany.semantic.ExprOrOpArgNode;
+import tla2sany.semantic.ModuleNode;
+import tla2sany.semantic.OpApplNode;
+import tla2sany.semantic.OpDefNode;
+import tla2sany.semantic.SymbolNode;
+import tla2sany.st.Location;
import tlc2.output.EC;
import static tlc2.output.MP.*;
import tlc2.output.Message;
import tlc2.output.OutputCollector;
+import tlc2.tool.BuiltInOPs;
import tlc2.tool.TLCStateInfo;
+import tlc2.tool.ToolGlobals;
-public class TLCResults {
+public class TLCResults implements ToolGlobals {
private TLCResult tlcResult;
private String violatedDefinition;
private Date startTime;
private Date endTime;
+ private LinkedHashMap<String, Long> operationsCount;
private int lengthOfTrace;
private String traceString;
@@ -34,6 +48,10 @@ public class TLCResults {
return lengthOfTrace > 0;
}
+ public LinkedHashMap<String, Long> getOperationCount() {
+ return operationsCount;
+ }
+
public TLCResults(TLCOutputInfo tlcOutputInfo) {
this.tlcOutputInfo = tlcOutputInfo;
this.lengthOfTrace = 0;
@@ -78,6 +96,67 @@ public class TLCResults {
tlcResult = InitialStateError;
}
+ if (TLC4BGlobals.isPrintCoverage() && OutputCollector.lineCount != null) {
+ evalCoverage();
+ }
+ }
+
+ private void evalCoverage() {
+ Hashtable<Integer, Long> lineCount = new Hashtable<Integer, Long>();
+ Set<Entry<Location, Long>> entrySet = OutputCollector.lineCount
+ .entrySet();
+ for (Entry<Location, Long> entry : entrySet) {
+ int endline = entry.getKey().endLine();
+ if (lineCount.containsKey(endline)) {
+ lineCount.put(endline,
+ Math.max(lineCount.get(endline), entry.getValue()));
+ } else {
+ lineCount.put(endline, entry.getValue());
+ }
+ }
+ ArrayList<OpDefNode> defs = findOperations(OutputCollector.moduleNode);
+ operationsCount = new LinkedHashMap<String, Long>();
+ for (OpDefNode opDefNode : defs) {
+ String operationName = opDefNode.getName().toString();
+ Long count = lineCount.get(opDefNode.getLocation().endLine());
+ if (count == null) {
+ count = 0L;
+ }
+ operationsCount.put(operationName, count);
+ }
+ }
+
+ private ArrayList<OpDefNode> findOperations(ModuleNode moduleNode) {
+
+ OpDefNode[] opDefs = moduleNode.getOpDefs();
+ ExprNode pred = null;
+ for (int i = opDefs.length - 1; i > 0; i--) {
+ OpDefNode def = opDefs[i];
+ if (def.getName().toString().equals("Next")) {
+ pred = def.getBody();
+ break;
+ }
+ }
+ OpApplNode dis = (OpApplNode) pred;
+ ArrayList<OpDefNode> operations = new ArrayList<OpDefNode>();
+ for (int i = 0; i < dis.getArgs().length; i++) {
+ operations.add(findOperation(dis.getArgs()[i]));
+ }
+ return operations;
+ }
+
+ private OpDefNode findOperation(ExprOrOpArgNode arg) {
+ OpApplNode op1 = (OpApplNode) arg;
+ SymbolNode opNode = op1.getOperator();
+ int opcode = BuiltInOPs.getOpCode(opNode.getName());
+ if (opcode == OPCODE_be) { // BoundedExists
+ return findOperation(op1.getArgs()[0]);
+ } else if (opNode instanceof OpDefNode) {
+ OpDefNode def = (OpDefNode) opNode;
+ return def;
+ } else {
+ throw new RuntimeException("Unkown Node");
+ }
}
private void evalTrace() {
--
GitLab