From 1314f91107ba6acb9c887d771c5370c3584c3f04 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 4 Dec 2014 12:22:45 +0000 Subject: [PATCH] Bugfix in SubNondetModel (from Joachim Klein). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9372 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/SubNondetModel.java | 30 +++++++++++++------------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/prism/src/explicit/SubNondetModel.java b/prism/src/explicit/SubNondetModel.java index 409b1046..be084a78 100644 --- a/prism/src/explicit/SubNondetModel.java +++ b/prism/src/explicit/SubNondetModel.java @@ -352,10 +352,10 @@ public class SubNondetModel implements NondetModel @Override public Object getAction(int s, int i) { - s = translateState(s); - i = translateAction(s, i); + int sOriginal = translateState(s); + int iOriginal = translateAction(s, i); - return model.getAction(s, i); + return model.getAction(sOriginal, iOriginal); } @Override @@ -367,38 +367,38 @@ public class SubNondetModel implements NondetModel @Override public int getNumTransitions(int s, int i) { - s = translateState(s); - i = translateAction(s, i); - return model.getNumTransitions(s, i); + int sOriginal = translateState(s); + int iOriginal = translateAction(s, i); + return model.getNumTransitions(sOriginal, iOriginal); } @Override public boolean allSuccessorsInSet(int s, int i, BitSet set) { - s = translateState(s); - i = translateAction(s, i); + int sOriginal = translateState(s); + int iOriginal = translateAction(s, i); set = translateSet(set); - return model.allSuccessorsInSet(s, i, set); + return model.allSuccessorsInSet(sOriginal, iOriginal, set); } @Override public boolean someSuccessorsInSet(int s, int i, BitSet set) { - s = translateState(s); - i = translateAction(s, i); + int sOriginal = translateState(s); + int iOriginal = translateAction(s, i); set = translateSet(set); - return model.someSuccessorsInSet(s, i, set); + return model.someSuccessorsInSet(sOriginal, iOriginal, set); } @Override public Iterator getSuccessorsIterator(int s, int i) { - s = translateState(s); - i = translateAction(s, i); + int sOriginal = translateState(s); + int iOriginal = translateAction(s, i); List succ = new ArrayList(); - Iterator it = model.getSuccessorsIterator(s, i); + Iterator it = model.getSuccessorsIterator(sOriginal, iOriginal); while (it.hasNext()) { int j = it.next(); succ.add(inverseTranslateState(j));