Browse Source

Tidy up of new Strategy classes, and do export in terms of action labels.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7002 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 13 years ago
parent
commit
355c12dcb2
  1. 2
      prism/src/prism/Prism.java
  2. 23
      prism/src/strat/MDStrategy.java
  3. 16
      prism/src/strat/MDStrategyArray.java
  4. 4
      prism/src/strat/Strategy.java

2
prism/src/prism/Prism.java

@ -2691,7 +2691,7 @@ public class Prism implements PrismSettingsListener
tmpLog = getPrismLogForFile(file); tmpLog = getPrismLogForFile(file);
// Export // Export
strat.export(tmpLog);
strat.exportActions(tmpLog);
// Tidy up // Tidy up
if (file != null) if (file != null)

23
prism/src/strat/MDStrategy.java

@ -34,15 +34,28 @@ import prism.PrismLog;
*/ */
public abstract class MDStrategy implements Strategy 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 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(); 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));
} }
} }
} }

16
prism/src/strat/MDStrategyArray.java

@ -32,34 +32,34 @@ package strat;
*/ */
public class MDStrategyArray extends MDStrategy public class MDStrategyArray extends MDStrategy
{ {
private explicit.Model model;
private explicit.NondetModel model;
private int choices[]; private int choices[];
/** /**
* Creates an MDStrategyArray from an integer array of 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. * 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.model = model;
this.choices = choices; this.choices = choices;
} }
@Override
public int getNumStates() public int getNumStates()
{ {
// Need?
return choices.length;
return model.getNumStates();
} }
@Override @Override
public int getChoice(int i)
public int getChoice(int s)
{ {
return choices[i];
return choices[s];
} }
@Override @Override
public Object getChoiceAction(int i)
public Object getChoiceAction(int s)
{ {
return "";//model.getAction(choices[i]);
return model.getAction(s, choices[s]);
} }
} }

4
prism/src/strat/Strategy.java

@ -35,7 +35,7 @@ import prism.PrismLog;
public interface Strategy 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);
} }
Loading…
Cancel
Save