updated gradle file

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)

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();

src/main/java/de/tlc4b/TLCRunner.java

@@ -107,7 +107,7 @@ public class TLCRunner {
 		if (TLC4BGlobals.isPrintCoverage()) {
 			list.add("-nowarning");
 			list.add("-coverage");
-			list.add(""+ 100);
+			list.add("" + 60);
 		}
 
 		// list.add("-config");

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;

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() {