DTMCFromMDPMemorylessAdversary class treats a choice of -1 as "do nothing".

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6906 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/explicit/DTMCFromMDPMemorylessAdversary.java

@@ -44,7 +44,7 @@ public class DTMCFromMDPMemorylessAdversary extends DTMCExplicit
 {
 	// Parent MDP
 	protected MDP mdp;
-	// Adversary
+	// Adversary (array of choice indices; -1 denotes no choice)
 	protected int adv[];
 
 	/**
@@ -114,6 +114,7 @@ public class DTMCFromMDPMemorylessAdversary extends DTMCExplicit
 	{
 		int numTransitions = 0;
 		for (int s = 0; s < numStates; s++)
+			if (adv[s] >= 0)
 				numTransitions += mdp.getNumTransitions(s, adv[s]);
 		return numTransitions;
 	}
@@ -175,12 +176,36 @@ public class DTMCFromMDPMemorylessAdversary extends DTMCExplicit
 
 	public double getNumTransitions(int s)
 	{
-		return mdp.getNumTransitions(s, adv[s]);
+		return adv[s] >= 0 ? mdp.getNumTransitions(s, adv[s]) : 0;
 	}
 
 	public Iterator<Entry<Integer, Double>> getTransitionsIterator(int s)
 	{
+		if (adv[s] >= 0) {
 			return mdp.getTransitionsIterator(s, adv[s]);
+		} else {
+			// Empty iterator
+			return new Iterator<Entry<Integer, Double>>()
+			{
+				@Override
+				public boolean hasNext()
+				{
+					return false;
+				}
+
+				@Override
+				public Entry<Integer, Double> next()
+				{
+					return null;
+				}
+
+				@Override
+				public void remove()
+				{
+					throw new UnsupportedOperationException();
+				}
+			};
+		}
 	}
 
 	public void prob0step(BitSet subset, BitSet u, BitSet result)
@@ -198,13 +223,13 @@ public class DTMCFromMDPMemorylessAdversary extends DTMCExplicit
 	@Override
 	public double mvMultSingle(int s, double vect[])
 	{
-		return mdp.mvMultSingle(s, adv[s], vect);
+		return adv[s] >= 0 ? mdp.mvMultSingle(s, adv[s], vect) : 0;
 	}
 
 	@Override
 	public double mvMultJacSingle(int s, double vect[])
 	{
-		return mdp.mvMultJacSingle(s, adv[s], vect);
+		return adv[s] >= 0 ? mdp.mvMultJacSingle(s, adv[s], vect) : 0;
 	}
 
 	@Override
@@ -217,7 +242,7 @@ public class DTMCFromMDPMemorylessAdversary extends DTMCExplicit
 	@Override
 	public void vmMult(double vect[], double result[])
 	{
-		throw new RuntimeException("Not implemented yet"); // TODO
+		throw new RuntimeException("Not implemented yet");
 	}
 
 	@Override