Bug fix in DTMCFromMDPAndMDStrategy, related to recent changes to successors info in explicit engine.

davexparker · davexparker · commit 748c097907c2 · 2017-12-27T01:13:49.000Z
diff --git a/prism/src/explicit/DTMCFromMDPAndMDStrategy.java b/prism/src/explicit/DTMCFromMDPAndMDStrategy.java
@@ -123,7 +123,11 @@ public int getNumTransitions()
 
 	public SuccessorsIterator getSuccessors(final int s)
 	{
-		return mdp.getSuccessors(s, strat.getChoiceIndex(s));
+		if (strat.isChoiceDefined(s)) {
+			return mdp.getSuccessors(s, strat.getChoiceIndex(s));
+		} else {
+			return SuccessorsIterator.empty();
+		}
 	}
 
 	public int getNumChoices(int s)

Original file line number	Diff line number	Diff line change
`@@ -123,7 +123,11 @@ public int getNumTransitions()`
`123`	`123`
`124`	`124`	`public SuccessorsIterator getSuccessors(final int s)`
`125`	`125`	`{`
`126`		`- return mdp.getSuccessors(s, strat.getChoiceIndex(s));`
	`126`	`+ if (strat.isChoiceDefined(s)) {`
	`127`	`+ return mdp.getSuccessors(s, strat.getChoiceIndex(s));`
	`128`	`+ } else {`
	`129`	`+ return SuccessorsIterator.empty();`
	`130`	`+ }`
`127`	`131`	`}`
`128`	`132`
`129`	`133`	`public int getNumChoices(int s)`