diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index c0ffdecc..e040c763 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -2691,7 +2691,7 @@ public class Prism implements PrismSettingsListener tmpLog = getPrismLogForFile(file); // Export - strat.export(tmpLog); + strat.exportActions(tmpLog); // Tidy up if (file != null) diff --git a/prism/src/strat/MDStrategy.java b/prism/src/strat/MDStrategy.java index 9f5cf38a..51a21352 100644 --- a/prism/src/strat/MDStrategy.java +++ b/prism/src/strat/MDStrategy.java @@ -34,15 +34,28 @@ import prism.PrismLog; */ public abstract class MDStrategy implements Strategy { + /** + * Get the number of states of the model associated with this strategy. + */ public abstract int getNumStates(); - public abstract int getChoice(int i); - public abstract Object getChoiceAction(int i); - public void export(PrismLog out) + /** + * Get the index of the choice taken in state s. + * The index is defined with respect to a particular model, stored locally. + */ + public abstract int getChoice(int s); + + /** + * Get the action taken in state s. + */ + public abstract Object getChoiceAction(int s); + + @Override + public void exportActions(PrismLog out) { int n = getNumStates(); - for (int i = 0; i < n; i++) { - out.println(i + ":" + getChoice(i)); + for (int s = 0; s < n; s++) { + out.println(s + ":" + getChoiceAction(s)); } } } diff --git a/prism/src/strat/MDStrategyArray.java b/prism/src/strat/MDStrategyArray.java index 76ff5e6d..9eb1d64d 100644 --- a/prism/src/strat/MDStrategyArray.java +++ b/prism/src/strat/MDStrategyArray.java @@ -32,34 +32,34 @@ package strat; */ public class MDStrategyArray extends MDStrategy { - private explicit.Model model; + private explicit.NondetModel model; private int choices[]; /** * Creates an MDStrategyArray from an integer array of choices. * The array may later be modified/delete - take a copy if you want to keep it. */ - public MDStrategyArray(explicit.Model model, int choices[]) + public MDStrategyArray(explicit.NondetModel model, int choices[]) { this.model = model; this.choices = choices; } + @Override public int getNumStates() { - // Need? - return choices.length; + return model.getNumStates(); } @Override - public int getChoice(int i) + public int getChoice(int s) { - return choices[i]; + return choices[s]; } @Override - public Object getChoiceAction(int i) + public Object getChoiceAction(int s) { - return "";//model.getAction(choices[i]); + return model.getAction(s, choices[s]); } } diff --git a/prism/src/strat/Strategy.java b/prism/src/strat/Strategy.java index 8348fa87..d5902e27 100644 --- a/prism/src/strat/Strategy.java +++ b/prism/src/strat/Strategy.java @@ -35,7 +35,7 @@ import prism.PrismLog; public interface Strategy { /** - * Export the strategy to a PrismLog. + * Export the strategy to a PrismLog, displaying strategy choices as action names. */ - public void export(PrismLog out); + public void exportActions(PrismLog out); }