From 19d8e743ebc3f7306f555bc917246ae195115366 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Fri, 12 Oct 2018 14:26:31 +0200
Subject: [PATCH] imported patch predecessor-restrict-diagnostics.patch

---
 prism/src/explicit/ECComputerDefault.java | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/prism/src/explicit/ECComputerDefault.java b/prism/src/explicit/ECComputerDefault.java
index 63b0ce29..f513a882 100644
--- a/prism/src/explicit/ECComputerDefault.java
+++ b/prism/src/explicit/ECComputerDefault.java
@@ -169,13 +169,19 @@ public class ECComputerDefault extends ECComputer
 		BitSet initialStates = new BitSet();
 		initialStates.set(states.nextSetBit(0));
 
+		int iterations = 0;
+		int checks = 0;
+		long start = System.currentTimeMillis();
+
 		boolean changed = true;
 		while (changed) {
+			iterations++;
 			changed = false;
 			actions.clear();
 			for (int i = 0; i < model.getNumStates(); i++) {
 				BitSet act = new BitSet();
 				if (states.get(i)) {
+					checks++;
 					for (int j = 0; j < model.getNumChoices(i); j++) {
 						if (model.allSuccessorsInSet(i, j, states)) {
 							act.set(j);
@@ -189,6 +195,7 @@ public class ECComputerDefault extends ECComputer
 				}
 			}
 		}
+		getLog().println("Restrict precomputations took "+iterations+" iterations, "+checks+" checks and "+(System.currentTimeMillis()-start)+"ms.");
 
 		return new SubNondetModel(model, states, actions, initialStates);
 	}