From 37a8adbe4164327ab078b610a55ac146fc4d17ee Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Fri, 12 Oct 2018 14:26:41 +0200
Subject: [PATCH] (TODO) IncomingChoiceRelation: calculatePreStar

TODO: optimize data types (Stack, BitSets)?
---
 .../src/explicit/IncomingChoiceRelation.java  | 81 +++++++++++++++++++
 1 file changed, 81 insertions(+)

diff --git a/prism/src/explicit/IncomingChoiceRelation.java b/prism/src/explicit/IncomingChoiceRelation.java
index a65214fb..784c7546 100644
--- a/prism/src/explicit/IncomingChoiceRelation.java
+++ b/prism/src/explicit/IncomingChoiceRelation.java
@@ -27,8 +27,12 @@
 package explicit;
 
 import java.util.ArrayList;
+import java.util.BitSet;
 import java.util.Iterator;
 import java.util.List;
+import java.util.Stack;
+
+import common.IterableBitSet;
 import prism.PrismComponent;
 
 /**
@@ -187,4 +191,81 @@ public class IncomingChoiceRelation
 		return pre;
 	}
 
+
+	/**
+	 * Computes the set Pre*(target) via a DFS, i.e., all states that
+	 * are in {@code target} or can reach {@code target} via one or more transitions
+	 * from states contained in {@code remain} and via the enabled choices in {@code enabledChoices}.
+	 * <br/>
+	 * If the parameter {@code remain} is {@code null}, then
+	 * {@code remain} is considered to include all states in the model.
+	 * <br/>
+	 * If the parameter {@code enabledChoices} is {@code null}, then
+	 * {@code enabledChoices} is considered to include all choices in the model.
+	 * <br/>
+	 * If the parameter {@code absorbing} is not {@code null},
+	 * then the states in {@code absorbing} are considered to be absorbing,
+	 * i.e., to have a single self-loop, disregarding other outgoing edges.
+
+	 * @param remain restriction on the states that may occur
+	 *               on the path to target, {@code null} = all states
+	 * @param target The set of target states
+	 * @param absorbing (optional) set of states that should be considered to be absorbing,
+	 *               i.e., their outgoing edges are ignored, {@code null} = no states
+	 * @param enabledChoices a mask providing information which choices are considered to be enabled
+	 * @return the set of states Pre*(target)
+	 */
+	public BitSet calculatePreStar(BitSet remain, BitSet target, BitSet absorbing, ChoicesMask enabledChoices)
+	{
+		BitSet result;
+
+		// all target states are in Pre*
+		result = (BitSet)target.clone();
+
+		// the stack of states whose predecessors have to be considered
+		Stack<Integer> todo = new Stack<Integer>();
+
+		// initial todo: all the target states
+		for (Integer s : IterableBitSet.getSetBits(target)) {
+			todo.add(s);
+		};
+
+		// the set of states that are finished
+		BitSet done = new BitSet();
+
+		while (!todo.isEmpty()) {
+			int s = todo.pop();
+			// already considered?
+			if (done.get(s)) continue;
+
+			done.set(s);
+
+			// for each predecessor in the graph
+			for (Choice choice : getIncomingChoices(s)) {
+				// check that choice is actually enabled
+				if (enabledChoices != null &&
+				    !enabledChoices.isEnabled(choice.getState(), choice.getChoice())) {
+					continue;
+				}
+
+				int p = choice.getState();
+				if (absorbing != null && absorbing.get(p)) {
+					// predecessor is absorbing, thus the edge is considered to not exist
+					continue;
+				}
+
+				if (remain == null || remain.get(p)) {
+					// can reach result (and is in remain)
+					result.set(p);
+					if (!done.get(p)) {
+						// add to stack
+						todo.add(p);
+					}
+				}
+			}
+		}
+
+		return result;
+	}
+
 }