diff --git a/prism/src/cex/CexPathAsBDDs.java b/prism/src/cex/CexPathAsBDDs.java index 018869fa..b653aee7 100644 --- a/prism/src/cex/CexPathAsBDDs.java +++ b/prism/src/cex/CexPathAsBDDs.java @@ -31,11 +31,13 @@ import java.util.ArrayList; import jdd.JDD; import jdd.JDDNode; import parser.State; +import simulator.PathFullInfo;; /** - * Class to store a single-path counterexample, as a list of BDDs. + * Class to store a single-path, non-probabilistic counterexample, as a list of BDDs. + * This is just a sequence of states, no more. */ -public class CexPathAsBDDs +public class CexPathAsBDDs implements PathFullInfo { protected prism.Model model; protected ArrayList states; @@ -68,6 +70,118 @@ public class CexPathAsBDDs } } + // ACCESSORS (for PathFullInfo) + + @Override + public int size() + { + return states.size() - 1; + } + + @Override + public State getState(int step) + { + return model.convertBddToState(states.get(step)); + } + + @Override + public double getStateReward(int step, int rsi) + { + return 0.0; + } + + @Override + public double getCumulativeTime(int step) + { + return 0.0; + } + + @Override + public double getCumulativeReward(int step, int rsi) + { + return 0.0; + } + + @Override + public double getTime(int step) + { + return 0.0; + } + + @Override + public int getChoice(int step) + { + return 0; + } + + @Override + public int getModuleOrActionIndex(int step) + { + return 0; + } + + @Override + public String getModuleOrAction(int step) + { + return ""; + } + + @Override + public double getTransitionReward(int step, int rsi) + { + return 0.0; + } + + @Override + public boolean isLooping() + { + return false; + } + + @Override + public int loopStart() + { + return 0; + } + + @Override + public int loopEnd() + { + return 0; + } + + @Override + public boolean hasRewardInfo() + { + return false; + } + + @Override + public boolean hasChoiceInfo() + { + return false; + } + + @Override + public boolean hasActionInfo() + { + return false; + } + + @Override + public boolean hasTimeInfo() + { + return false; + } + + @Override + public boolean hasLoopInfo() + { + return false; + } + + // Standard method + @Override public String toString() {