Changes to DTMC/MDP/STPG interface.

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

prism/src/pta/PTAAbstractRefine.java

@@ -166,7 +166,7 @@ public class PTAAbstractRefine extends STPGAbstractRefine
 
 		// Check for deadlocks in the constructed STPG
 		// (should never occur because of the restrictions we impose on PTAs)
-		if (((STPG) abstraction).steps.get(src).size() == 0) {
+		if (abstraction.getNumChoices(src) == 0) {
 			throw new PrismException("STPG has deadlock in state #" + src + ":" + graph.states.get(src));
 		}
 	}
@@ -298,7 +298,7 @@ public class PTAAbstractRefine extends STPGAbstractRefine
 			for (int in : choiceList) {
 				// If using BitSets for action labels (i.e. have not cached zones for reuse)
 				// need to build the corresponding zone
-				action = ((STPG) abstraction).steps.get(splitState).get(in).action;
+				action = ((STPG) abstraction).getChoice(splitState, in).action;
 				if (!storeValidZones) {
 					actionBitSet = (BitSet) action;
 					List<SymbolicTransition> sts = graph.trans.get(splitState);

prism/src/pta/PTAExpected.java

@@ -332,7 +332,7 @@ public class PTAExpected
 				if (distr.isEmpty())
 					continue;
 				// Add distribution
-				choice = mdp.addDistribution(src, distr);
+				choice = mdp.addChoice(src, distr);
 				// Compute reward
 				if (min) {
 					rewSum = 0.0;
@@ -406,7 +406,7 @@ public class PTAExpected
 		// Add transition + reward
 		distr = new Distribution();
 		distr.add(initialStates.get(0), 1.0);
-		mdp.addDistribution(src, distr);
+		mdp.addChoice(src, distr);
 		if (!min)
 			mdp.setTransitionReward(src, 0, getMinMaxForZone(graph.states.get(initialStates.get(0)).zone, someClock,
 					min));

prism/src/pta/ReachabilityGraph.java

@@ -198,7 +198,7 @@ public class ReachabilityGraph
 					distr.add(dest, edge.getProbability());
 				}
 				if (!distr.isEmpty())
-					mdp.addDistribution(src, distr);
+					mdp.addChoice(src, distr);
 			}
 		}