From e03cf7dbe5a45e0f1e9af95915970476ea8e3da6 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Fri, 12 Oct 2018 14:26:33 +0200
Subject: [PATCH] imported patch predecessor-ec-computer-use-backward.patch

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

diff --git a/prism/src/explicit/ECComputerDefault.java b/prism/src/explicit/ECComputerDefault.java
index f513a882..91a55d25 100644
--- a/prism/src/explicit/ECComputerDefault.java
+++ b/prism/src/explicit/ECComputerDefault.java
@@ -34,7 +34,10 @@ import java.util.HashSet;
 import java.util.List;
 import java.util.Map;
 import java.util.Set;
+import java.util.Stack;
 
+import common.IterableBitSet;
+import common.IterableStateSet;
 import prism.PrismComponent;
 import prism.PrismException;
 
@@ -163,7 +166,28 @@ public class ECComputerDefault extends ECComputer
 		return L;
 	}
 
+	private BitSet getActionsRemainingInSet(NondetModel model, BitSet states, int s) {
+		BitSet actions = new BitSet();
+
+		for (int j = 0; j < model.getNumChoices(s); j++) {
+			if (model.allSuccessorsInSet(s, j, states)) {
+				actions.set(j);
+			}
+		}
+
+		return actions;
+	}
+
 	private SubNondetModel restrict(NondetModel model, BitSet states)
+	{
+		if (pre != null) {
+			return restrictUsingPre(model, states);
+		} else {
+			return restrictFixpoint(model, states);
+		}
+	}
+	
+	private SubNondetModel restrictFixpoint(NondetModel model, BitSet states)
 	{
 		Map<Integer, BitSet> actions = new HashMap<Integer, BitSet>();
 		BitSet initialStates = new BitSet();
@@ -200,6 +224,56 @@ public class ECComputerDefault extends ECComputer
 		return new SubNondetModel(model, states, actions, initialStates);
 	}
 
+	private SubNondetModel restrictUsingPre(NondetModel model, BitSet states)
+	{
+		Map<Integer, BitSet> actions = new HashMap<Integer, BitSet>();
+		BitSet initialStates = new BitSet();
+		initialStates.set(states.nextSetBit(0));
+
+		Stack<Integer> toCheck = new Stack<Integer>();
+
+		int checks = 0;
+		long start = System.currentTimeMillis();
+
+		for (int i : IterableBitSet.getSetBits(states)) {
+			checks++;
+			BitSet act = getActionsRemainingInSet(model, states, i);
+			if (act.isEmpty()) {
+				states.clear(i);
+
+				for (int j : pre.getPre(i)) {
+					if (states.get(j))
+						toCheck.add(j);
+				}
+			} else {
+				actions.put(i, act);
+			}
+		}
+
+		while (!toCheck.isEmpty()) {
+			int i = toCheck.pop();
+			if (!states.get(i)) continue;  // already removed
+
+			checks++;
+			BitSet act = getActionsRemainingInSet(model, states, i);
+			if (act.isEmpty()) {
+				states.clear(i);
+				actions.remove(i);
+
+				for (int j : pre.getPre(i)) {
+					if (states.get(j))
+						toCheck.add(j);
+				}
+			} else {
+				actions.put(i, act);
+			}
+		}
+
+		getLog().println("Restrict precomputations took "+checks+" checks and "+(System.currentTimeMillis()-start)+"ms.");
+
+		return new SubNondetModel(model, states, actions, initialStates);
+	}
+
 	private List<BitSet> computeSCCs(NondetModel model) throws PrismException
 	{
 		SCCConsumerStore sccs = new SCCConsumerStore();