Add "type" option to -exportstrat (explicit engine only) + a few changes in Strategy classes.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7602 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/explicit/DTMCExplicit.java

@@ -72,7 +72,7 @@ public abstract class DTMCExplicit extends ModelExplicit implements DTMC
 	}
 	
 	@Override
-	public void exportToPrismExplicitTra(PrismLog out) throws PrismException
+	public void exportToPrismExplicitTra(PrismLog out)
 	{
 		int i;
 		TreeMap<Integer, Double> sorted;

prism/src/explicit/DTMCFromMDPAndMDStrategy.java

@@ -0,0 +1,260 @@
+//==============================================================================
+//	
+//	Copyright (c) 2013-
+//	Authors:
+//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package explicit;
+
+import java.util.*;
+import java.util.Map.Entry;
+
+import explicit.rewards.MCRewards;
+import parser.State;
+import parser.Values;
+import prism.ModelType;
+import prism.PrismException;
+import strat.MDStrategy;
+
+/**
+* Explicit-state representation of a DTMC, constructed (implicitly)
+* from an MDP and a memoryless deterministic (MD) adversary.
+* This class is read-only: most of the data is pointers to other model info.
+*/
+public class DTMCFromMDPAndMDStrategy extends DTMCExplicit
+{
+	// Parent MDP
+	protected MDP mdp;
+	// MD strategy
+	protected MDStrategy strat;
+
+	/**
+	 * Constructor: create from MDP and memoryless adversary.
+	 */
+	public DTMCFromMDPAndMDStrategy(MDP mdp, MDStrategy strat)
+	{
+		this.mdp = mdp;
+		this.numStates = mdp.getNumStates();
+		this.strat = strat;
+	}
+
+	@Override
+	public void buildFromPrismExplicit(String filename) throws PrismException
+	{
+		throw new PrismException("Not supported");
+	}
+
+	// Accessors (for Model)
+
+	public ModelType getModelType()
+	{
+		return ModelType.DTMC;
+	}
+
+	public int getNumStates()
+	{
+		return mdp.getNumStates();
+	}
+
+	public int getNumInitialStates()
+	{
+		return mdp.getNumInitialStates();
+	}
+
+	public Iterable<Integer> getInitialStates()
+	{
+		return mdp.getInitialStates();
+	}
+
+	public int getFirstInitialState()
+	{
+		return mdp.getFirstInitialState();
+	}
+
+	public boolean isInitialState(int i)
+	{
+		return mdp.isInitialState(i);
+	}
+
+	public boolean isDeadlockState(int i)
+	{
+		return mdp.isDeadlockState(i);
+	}
+
+	public List<State> getStatesList()
+	{
+		return mdp.getStatesList();
+	}
+
+	public Values getConstantValues()
+	{
+		return mdp.getConstantValues();
+	}
+
+	public int getNumTransitions()
+	{
+		int numTransitions = 0;
+		for (int s = 0; s < numStates; s++)
+			if (strat.isChoiceDefined(s))
+				numTransitions += mdp.getNumTransitions(s, strat.getChoiceIndex(s));
+		return numTransitions;
+	}
+
+	public Iterator<Integer> getSuccessorsIterator(final int s)
+	{
+		throw new RuntimeException("Not implemented yet");
+	}
+
+	public boolean isSuccessor(int s1, int s2)
+	{
+		throw new RuntimeException("Not implemented yet");
+	}
+
+	public boolean allSuccessorsInSet(int s, BitSet set)
+	{
+		throw new RuntimeException("Not implemented yet");
+	}
+
+	public boolean someSuccessorsInSet(int s, BitSet set)
+	{
+		throw new RuntimeException("Not implemented yet");
+	}
+
+	public int getNumChoices(int s)
+	{
+		// Always 1 for a DTMC
+		return 1;
+	}
+
+	public void findDeadlocks(boolean fix) throws PrismException
+	{
+		// No deadlocks by definition
+	}
+
+	public void checkForDeadlocks() throws PrismException
+	{
+		// No deadlocks by definition
+	}
+
+	public void checkForDeadlocks(BitSet except) throws PrismException
+	{
+		// No deadlocks by definition
+	}
+
+	@Override
+	public String infoString()
+	{
+		return mdp.infoString() + " + " + "???"; // TODO
+	}
+
+	@Override
+	public String infoStringTable()
+	{
+		return mdp.infoString() + " + " + "???\n"; // TODO
+	}
+
+	// Accessors (for DTMC)
+
+	public double getNumTransitions(int s)
+	{
+		return strat.isChoiceDefined(s) ? mdp.getNumTransitions(s, strat.getChoiceIndex(s)) : 0;
+	}
+
+	public Iterator<Entry<Integer, Double>> getTransitionsIterator(int s)
+	{
+		if (strat.isChoiceDefined(s)) {
+			return mdp.getTransitionsIterator(s, strat.getChoiceIndex(s));
+		} else {
+			// Empty iterator
+			return new Iterator<Entry<Integer, Double>>()
+			{
+				@Override
+				public boolean hasNext()
+				{
+					return false;
+				}
+
+				@Override
+				public Entry<Integer, Double> next()
+				{
+					return null;
+				}
+
+				@Override
+				public void remove()
+				{
+					throw new UnsupportedOperationException();
+				}
+			};
+		}
+	}
+
+	public void prob0step(BitSet subset, BitSet u, BitSet result)
+	{
+		// TODO
+		throw new Error("Not yet supported");
+	}
+
+	public void prob1step(BitSet subset, BitSet u, BitSet v, BitSet result)
+	{
+		// TODO
+		throw new Error("Not yet supported");
+	}
+
+	@Override
+	public double mvMultSingle(int s, double vect[])
+	{
+		return strat.isChoiceDefined(s) ? mdp.mvMultSingle(s, strat.getChoiceIndex(s), vect) : 0;
+	}
+
+	@Override
+	public double mvMultJacSingle(int s, double vect[])
+	{
+		return strat.isChoiceDefined(s) ? mdp.mvMultJacSingle(s, strat.getChoiceIndex(s), vect) : 0;
+	}
+
+	@Override
+	public double mvMultRewSingle(int s, double vect[], MCRewards mcRewards)
+	{
+		throw new RuntimeException("Not implemented yet");
+		//return mdp.mvMultRewSingle(s, adv[s], vect);
+	}
+
+	@Override
+	public void vmMult(double vect[], double result[])
+	{
+		throw new RuntimeException("Not implemented yet");
+	}
+
+	@Override
+	public String toString()
+	{
+		throw new RuntimeException("Not implemented yet");
+	}
+
+	@Override
+	public boolean equals(Object o)
+	{
+		throw new RuntimeException("Not implemented yet");
+	}
+}

prism/src/explicit/MDPExplicit.java

@@ -38,6 +38,7 @@ import prism.ModelType;
 import prism.PrismException;
 import prism.PrismLog;
 import prism.PrismUtils;
+import strat.MDStrategy;
 import explicit.rewards.MDPRewards;
 
 /**
@@ -76,7 +77,7 @@ public abstract class MDPExplicit extends ModelExplicit implements MDP
 	}
 
 	@Override
-	public void exportToPrismExplicitTra(PrismLog out) throws PrismException
+	public void exportToPrismExplicitTra(PrismLog out)
 	{
 		int i, j, numChoices;
 		Object action;
@@ -339,4 +340,10 @@ public abstract class MDPExplicit extends ModelExplicit implements MDP
 		}*/
 		return maxDiff;
 	}
+	
+	@Override
+	public Model constructInducedModel(MDStrategy strat)
+	{
+		return new DTMCFromMDPAndMDStrategy(this, strat);
+	}
 }

prism/src/explicit/Model.java

@@ -185,7 +185,7 @@ public interface Model
 	/**
 	 * Export transition matrix to explicit format readable by PRISM (i.e. a .tra file).
 	 */
-	public void exportToPrismExplicitTra(PrismLog log) throws PrismException;
+	public void exportToPrismExplicitTra(PrismLog log);
 	
 	/**
 	 * Export to a dot file.

prism/src/explicit/ModelExplicit.java

@@ -258,17 +258,25 @@ public abstract class ModelExplicit implements Model
 	@Override
 	public void exportToPrismExplicitTra(String filename) throws PrismException
 	{
-		exportToPrismExplicitTra(new PrismFileLog(filename));
+		PrismLog tmpLog = new PrismFileLog(filename);
+		if (!tmpLog.ready()) {
+			throw new PrismException("Could not open file \"" + filename + "\" for output");
+		}
+		exportToPrismExplicitTra(tmpLog);
 	}
 
 	@Override
 	public void exportToPrismExplicitTra(File file) throws PrismException
 	{
+		PrismLog tmpLog = new PrismFileLog(file.getPath());
+		if (!tmpLog.ready()) {
+			throw new PrismException("Could not open file \"" + file + "\" for output");
+		}
 		exportToPrismExplicitTra(new PrismFileLog(file.getPath()));
 	}
 
 	@Override
-	public abstract void exportToPrismExplicitTra(PrismLog out) throws PrismException;
+	public abstract void exportToPrismExplicitTra(PrismLog out);
 
 	@Override
 	public void exportToDotFile(String filename) throws PrismException

prism/src/explicit/NondetModel.java

@@ -30,6 +30,8 @@ import java.util.BitSet;
 import java.util.Iterator;
 import java.util.Map.Entry;
 
+import strat.MDStrategy;
+
 /**
  * Interface for (abstract) classes that provide (read-only) access to an explicit-state model with nondeterminism.
  */
@@ -77,4 +79,11 @@ public interface NondetModel extends Model
 	 * Get an iterator over the transitions of state s and action i.
 	 */
 	public Iterator<Entry<Integer, Double>> getTransitionsIterator(int s, int i);
+	
+	/**
+	 * Construct a model that is induced by applying strategy {@code strat} to this model.
+	 * Note that the "new" model may be just an implicit (read-only) representation. 
+	 * @param strat (Memoryless) strategy to use
+	 */
+	public Model constructInducedModel(MDStrategy strat);
 }

prism/src/explicit/STPGAbstrSimple.java

@@ -36,6 +36,7 @@ import prism.ModelType;
 import prism.PrismException;
 import prism.PrismLog;
 import prism.PrismUtils;
+import strat.MDStrategy;
 
 /**
  * Simple explicit-state representation of a stochastic two-player game (STPG),
@@ -363,7 +364,7 @@ public class STPGAbstrSimple extends ModelExplicit implements STPG, NondetModelS
 	}
 
 	@Override
-	public void exportToPrismExplicitTra(PrismLog out) throws PrismException
+	public void exportToPrismExplicitTra(PrismLog out)
 	{
 		int i, j, k;
 		TreeMap<Integer, Double> sorted;
@@ -521,6 +522,12 @@ public class STPGAbstrSimple extends ModelExplicit implements STPG, NondetModelS
 		return null;
 	}
 
+	@Override
+	public Model constructInducedModel(MDStrategy strat)
+	{
+		throw new RuntimeException("Not implemented");
+	}
+	
 	@Override
 	public boolean isChoiceNested(int s, int i)
 	{

prism/src/explicit/SubNondetModel.java

@@ -28,7 +28,6 @@
 package explicit;
 
 import java.io.File;
-import java.io.NotSerializableException;
 import java.util.ArrayList;
 import java.util.BitSet;
 import java.util.HashMap;
@@ -36,7 +35,6 @@ import java.util.Iterator;
 import java.util.List;
 import java.util.Map;
 import java.util.Map.Entry;
-import java.util.NoSuchElementException;
 
 import parser.State;
 import parser.Values;
@@ -44,6 +42,7 @@ import parser.VarList;
 import prism.ModelType;
 import prism.PrismException;
 import prism.PrismLog;
+import strat.MDStrategy;
 
 /*
  * Class for creating a sub-model of any NondetModel, please note the translate* methods
@@ -235,7 +234,7 @@ public class SubNondetModel implements NondetModel {
 	}
 
 	@Override
-	public void exportToPrismExplicitTra(PrismLog log) throws PrismException {
+	public void exportToPrismExplicitTra(PrismLog log) {
 		throw new UnsupportedOperationException();
 	}
 
@@ -358,6 +357,12 @@ public class SubNondetModel implements NondetModel {
 		return distrs.entrySet().iterator();
 	}
 	
+	@Override
+	public Model constructInducedModel(MDStrategy strat)
+	{
+		throw new RuntimeException("Not implemented");
+	}
+	
 	private void generateLookupTable(BitSet states, Map<Integer,BitSet> actions) {
 		for(int i=0;i < model.getNumStates();i++) {
 			if(states.get(i)) {

prism/src/param/ParamModel.java

@@ -178,7 +178,7 @@ final class ParamModel extends ModelExplicit
 	}
 
 	@Override
-	public void exportToPrismExplicitTra(PrismLog log) throws PrismException
+	public void exportToPrismExplicitTra(PrismLog log)
 	{
 		throw new UnsupportedOperationException();
 	}

prism/src/prism/Prism.java

@@ -153,6 +153,24 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 	public static final int LOCKSTEP = 2;
 	public static final int SCCFIND = 3;
 
+	// Options for type of strategy export
+	public enum StrategyExportType {
+		ACTIONS, INDICES, INDUCED_MODEL;
+		public String description()
+		{
+			switch (this) {
+			case ACTIONS:
+				return "as actions";
+			case INDICES:
+				return "as indices";
+			case INDUCED_MODEL:
+				return "as an induced model";
+			default:
+				return this.toString();
+			}
+		}
+	}
+	
 	//------------------------------------------------------------------------------
 	// Settings / flags / options
 	//------------------------------------------------------------------------------
@@ -2918,27 +2936,34 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 	}
 	
 	/**
-	 * Export a strategy (for the currently loaded model);
-	 * TODO: is it necessarily loaded?
+	 * Export a strategy. The associated model should be attached to the strategy.
+	 * Strictly, speaking that does not need to be the currently loaded model,
+	 * but it would probably have been discarded if that was not the case.
 	 * @param strat The strategy
+	 * @param exportType The type of output
 	 * @param file File to output the path to (stdout if null)
 	 */
-	public void exportStrategy(Strategy strat, File file) throws FileNotFoundException, PrismException
+	public void exportStrategy(Strategy strat, StrategyExportType exportType, File file) throws FileNotFoundException, PrismException
 	{
 		PrismLog tmpLog;
 
 		// Print message
-		mainLog.print("\nExporting strategy ");
-		//mainLog.print(getStringForExportType(exportType) + " ");
+		mainLog.print("\nExporting strategy " + exportType.description() + " ");
 		mainLog.println(getDestinationStringForFile(file));
 
-		// Create new file log or use main log
+		// Export to file (or use main log)
 		tmpLog = getPrismLogForFile(file);
-
-		// Export
-		strat.exportActions(tmpLog);
-
-		// Tidy up
+		switch (exportType) {
+		case ACTIONS:
+			strat.exportActions(tmpLog);
+			break;
+		case INDICES:
+			strat.exportIndices(tmpLog);
+			break;
+		case INDUCED_MODEL:
+			strat.exportInducedModel(tmpLog);
+			break;
+		}
 		if (file != null)
 			tmpLog.close();
 	}

prism/src/prism/PrismCL.java

@@ -38,6 +38,7 @@ import parser.ast.ExpressionReward;
 import parser.ast.ModulesFile;
 import parser.ast.PropertiesFile;
 import parser.ast.Property;
+import prism.Prism.StrategyExportType;
 import simulator.GenerateSimulationPath;
 import simulator.method.ACIconfidence;
 import simulator.method.ACIiterations;
@@ -188,6 +189,9 @@ public class PrismCL implements PrismModelListener
 	private boolean simManual = false;
 	private SimulationMethod simMethod = null;
 
+	// strategy export info
+	private Prism.StrategyExportType exportStratType = StrategyExportType.ACTIONS;
+	
 	// parametric analysis info
 	private String[] paramLowerBounds = null;
 	private String[] paramUpperBounds = null;
@@ -377,7 +381,7 @@ public class PrismCL implements PrismModelListener
 						// if a strategy was generated, and we need to export it, do so
 						if (exportstrat && res.getStrategy() != null) {
 							try {
-								prism.exportStrategy(res.getStrategy(), exportStratFilename.equals("stdout") ? null : new File(exportStratFilename));
+								prism.exportStrategy(res.getStrategy(), exportStratType, exportStratFilename.equals("stdout") ? null : new File(exportStratFilename));
 							}
 							// in case of error, report it and proceed
 							catch (FileNotFoundException e) {
@@ -1806,7 +1810,19 @@ public class PrismCL implements PrismModelListener
 			// Ignore ""
 			if (opt.equals("")) {
 			}
-			// TODO: add some options
+			else if (opt.startsWith("type")) {
+				if (!opt.startsWith("type="))
+					throw new PrismException("No value provided for \"type\" option of -exportstrat");
+				String optVal = opt.substring(5);
+				if (optVal.equals("actions"))
+					exportStratType = StrategyExportType.ACTIONS;
+				else if (optVal.equals("indices"))
+					exportStratType = StrategyExportType.INDICES;
+				else if (optVal.equals("induced"))
+					exportStratType = StrategyExportType.INDUCED_MODEL;
+				else
+					throw new PrismException("Unknown value \"" + optVal + "\" provided for \"type\" option of -exportstrat");
+			}
 			// Unknown option
 			else {
 				throw new PrismException("Unknown option \"" + opt + "\" for -exportstrat switch");

prism/src/strat/MDStrategy.java

@@ -44,6 +44,11 @@ public abstract class MDStrategy implements Strategy
 	 */
 	public abstract int getNumStates();
 
+	/**
+	 * Is choice information stored for state s?
+	 */
+	public abstract boolean isChoiceDefined(int s);
+
 	/**
 	 * Get the type of choice information stored for state s.
 	 */
@@ -86,9 +91,18 @@ public abstract class MDStrategy implements Strategy
 	{
 		int n = getNumStates();
 		for (int s = 0; s < n; s++) {
-			// Only print actions for reachable states
-			if (getChoice(s) != Choice.UNREACHABLE)
+			if (isChoiceDefined(s))
 				out.println(s + ":" + getChoiceAction(s));
 		}
 	}
+
+	@Override
+	public void exportIndices(PrismLog out)
+	{
+		int n = getNumStates();
+		for (int s = 0; s < n; s++) {
+			if (isChoiceDefined(s))
+				out.println(s + ":" + getChoiceIndex(s));
+		}
+	}
 }

prism/src/strat/MDStrategyArray.java

@@ -27,6 +27,10 @@
 
 package strat;
 
+import prism.PrismLog;
+import explicit.MDP;
+import explicit.Model;
+
 /**
  * Class to store a memoryless deterministic (MD) strategy, as a (Java) array of choice indices.
  */
@@ -37,7 +41,7 @@ public class MDStrategyArray extends MDStrategy
 	// Index of choice taken in each state (wrt model above) 
 	// Other possible values: -1 (unknown), -2 (arbitrary), -3 (unreachable)
 	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.
@@ -47,15 +51,21 @@ public class MDStrategyArray extends MDStrategy
 		this.model = model;
 		this.choices = choices;
 	}
-	
+
 	// Methods for MDStrategy
-	
+
 	@Override
 	public int getNumStates()
 	{
 		return model.getNumStates();
 	}
-	
+
+	@Override
+	public boolean isChoiceDefined(int s)
+	{
+		return choices[s] >= 0;
+	}
+
 	@Override
 	public Strategy.Choice getChoice(int s)
 	{
@@ -70,13 +80,13 @@ public class MDStrategyArray extends MDStrategy
 			return Choice.INDEX;
 		}
 	}
-	
+
 	@Override
 	public int getChoiceIndex(int s)
 	{
 		return choices[s];
 	}
-	
+
 	@Override
 	public Object getChoiceAction(int s)
 	{
@@ -85,7 +95,14 @@ public class MDStrategyArray extends MDStrategy
 	}
 
 	// Methods for Strategy
-	
+
+	@Override
+	public void exportInducedModel(PrismLog out)
+	{
+		Model dtmcInd = model.constructInducedModel(this);
+		dtmcInd.exportToPrismExplicitTra(out);
+	}
+
 	@Override
 	public void clear()
 	{

prism/src/strat/MDStrategyIV.java

@@ -29,8 +29,10 @@ package strat;
 import java.util.List;
 
 import dv.IntegerVector;
+import explicit.MDP;
 
 import prism.Model;
+import prism.PrismLog;
 import strat.Strategy.Choice;
 
 /**
@@ -65,6 +67,12 @@ public class MDStrategyIV extends MDStrategy
 		return numStates;
 	}
 	
+	@Override
+	public boolean isChoiceDefined(int s)
+	{
+		return iv.getElement(s) >= 0;
+	}
+
 	@Override
 	public Strategy.Choice getChoice(int s)
 	{
@@ -96,6 +104,12 @@ public class MDStrategyIV extends MDStrategy
 	
 	// Methods for Strategy
 	
+	@Override
+	public void exportInducedModel(PrismLog out)
+	{
+		// TODO
+	}
+	
 	@Override
 	public void clear()
 	{

prism/src/strat/Strategy.java

@@ -44,6 +44,16 @@ public interface Strategy
 	 */
 	public void exportActions(PrismLog out);
 	
+	/**
+	 * Export the strategy to a PrismLog, displaying strategy choices as indices.
+	 */
+	public void exportIndices(PrismLog out);
+	
+	/**
+	 * Export the model induced by this strategy to a PrismLog.
+	 */
+	public void exportInducedModel(PrismLog out);
+	
 	/**
 	 * Initialise the strategy, based on an initial model state.
 	 * @param s Initial state of the model