First bits of code for improved strategy generation.

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

prism/src/explicit/MDPModelChecker.java

@@ -39,6 +39,7 @@ import prism.PrismException;
 import prism.PrismFileLog;
 import prism.PrismLog;
 import prism.PrismUtils;
+import strat.MDStrategyArray;
 import explicit.rewards.MDPRewards;
 
 /**
@@ -191,6 +192,7 @@ public class MDPModelChecker extends ProbModelChecker
 
 		res = computeUntilProbs((MDP) model, b1, b2, min);
 		probs = StateValues.createFromDoubleArray(res.soln, model);
+		result.setStrategy(res.strat);
 
 		return probs;
 	}
@@ -435,6 +437,10 @@ public class MDPModelChecker extends ProbModelChecker
 		timer = System.currentTimeMillis() - timer;
 		mainLog.println("Probabilistic reachability took " + timer / 1000.0 + " seconds.");
 
+		// Store strategy
+		if (genStrat) {
+			res.strat = new MDStrategyArray(strat);
+		}
 		// Export adversary
 		if (genStrat && exportAdv) {
 			// Prune strategy

prism/src/explicit/ModelCheckerResult.java

@@ -26,6 +26,12 @@
 
 package explicit;
 
+import strat.Strategy;
+
+/**
+ * Class storing some info/data from a call to a model checking or
+ * numerical computation method in the explicit engine. 
+ */
 public class ModelCheckerResult
 {
 	// Solution vector
@@ -40,7 +46,9 @@ public class ModelCheckerResult
 	public double timePre = 0.0;
 	// Time taken for Prob0-type precomputation (secs)
 	public double timeProb0 = 0.0;
-	
+	// Strategy
+	public Strategy strat = null;
+
 	/**
 	 * Clear all stored data, including setting of array pointers to null
 	 * (which may be helpful for garbage collection purposes).

prism/src/explicit/ProbModelChecker.java

@@ -70,6 +70,9 @@ public class ProbModelChecker extends StateModelChecker
 	protected boolean exportAdv = false;
 	protected String exportAdvFilename;
 
+	// Additional flags/settings not included in PrismSettings
+	protected boolean getStrat = false;
+	
 	// Enums for flags/settings
 
 	// Method used for numerical solution

prism/src/prism/Prism.java

@@ -176,6 +176,8 @@ public class Prism implements PrismSettingsListener
 	protected String exportProductTransFilename = null;
 	protected boolean exportProductStates = false;
 	protected String exportProductStatesFilename = null;
+	// Generate a strategy during model checking?
+	protected boolean genStrat = false; 
 
 	// A few miscellaneous options (i.e. defunct/hidden/undocumented/etc.)
 	// See constructor below for default values
@@ -558,6 +560,14 @@ public class Prism implements PrismSettingsListener
 		exportProductStatesFilename = s;
 	}
 
+	/**
+	 * Specify whether or not a strategy should be generated during model checking.
+	 */
+	public void setGenStrat(boolean genStrat)
+	{
+		this.genStrat = genStrat;
+	}
+
 	public void setDoReach(boolean b) throws PrismException
 	{
 		doReach = b;
@@ -840,6 +850,14 @@ public class Prism implements PrismSettingsListener
 		return exportProductStatesFilename;
 	}
 
+	/**
+	 * Whether or not a strategy should be generated during model checking.
+	 */
+	public boolean getGenStrat()
+	{
+		return genStrat;
+	}
+
 	public boolean getDoReach()
 	{
 		return doReach;

prism/src/prism/PrismCL.java

@@ -350,6 +350,8 @@ public class PrismCL implements PrismModelListener
 
 						// store result of model checking
 						results[j].setResult(definedMFConstants, definedPFConstants, res.getResult());
+						
+						// if a counterexample was generated, display it
 						Object cex = res.getCounterexample();
 						if (cex != null) {
 							mainLog.println("\nCounterexample/witness:");
@@ -366,6 +368,12 @@ public class PrismCL implements PrismModelListener
 							}
 						}
 
+						// if a strategy was generated, and we need to export it, do so
+						if (res.getStrategy() != null) {
+							mainLog.println("\nExporting strategy...");
+							res.getStrategy().export(mainLog);
+						}
+						
 						// if required, check result against expected value
 						if (test) {
 							try {

prism/src/prism/Result.java

@@ -28,8 +28,12 @@
 
 package prism;
 
+import strat.Strategy;
+
 /**
  * This class stores the result of a single verification/simulation.
+ * It also stores other info/objects that may be passed back to the user,
+ * e.g. an explanation of the result, counterexample, or optimal strategy.
  */
 public class Result
 {
@@ -39,6 +43,8 @@ public class Result
 	private String explanation;
 	// Counterexample (optional)
 	private Object cex;
+	// Strategy (optional)
+	private Strategy strat;
 	
 	/**
 	 * Construct an empty Result object.
@@ -48,6 +54,7 @@ public class Result
 		this.result = null;
 		this.explanation = null;
 		this.cex = null;
+		this.strat = null;
 	}
 	
 	/**
@@ -83,6 +90,14 @@ public class Result
 		this.cex = cex;
 	}
 	
+	/**
+	 * Set the strategy (null denotes n/a).
+	 */
+	public void setStrategy(Strategy strat)
+	{
+		this.strat = strat;
+	}
+	
 	/**
 	 * Get the result.
 	 */
@@ -107,6 +122,14 @@ public class Result
 		return cex;
 	}
 	
+	/**
+	 * Get the strategy (null denotes n/a).
+	 */
+	public Strategy getStrategy()
+	{
+		return strat;
+	}
+	
 	/**
 	 * Get a string of the result and (if present) explanatory text
 	 */

prism/src/strat/MDStrategy.java

@@ -0,0 +1,47 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford)
+//	* Aistis Simaitis <aistis.aimaitis@cs.ox.ac.uk> (University of 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 strat;
+
+import prism.PrismLog;
+
+/**
+ * Classes to store memoryless deterministic (MD) strategies.
+ */
+public abstract class MDStrategy implements Strategy
+{
+	public abstract int getNumStates();
+	public abstract int getChoice(int i);
+	
+	public void export(PrismLog out)
+	{
+		int n = getNumStates();
+		for (int i = 0; i < n; i++) {
+			out.println(i + ":" + getChoice(i));
+		}
+	}
+}

prism/src/strat/MDStrategyArray.java

@@ -0,0 +1,57 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford)
+//	* Aistis Simaitis <aistis.aimaitis@cs.ox.ac.uk> (University of 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 strat;
+
+/**
+ * Class to store a memoryless deterministic (MD) strategy, as a (Java) array of choice indices.
+ */
+public class MDStrategyArray extends MDStrategy
+{
+	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(int choices[])
+	{
+		this.choices = choices;
+	}
+	
+	public int getNumStates()
+	{
+		// Need?
+		return choices.length;
+	}
+	
+	@Override
+	public int getChoice(int i)
+	{
+		return choices[i];
+	}
+}

prism/src/strat/Strategy.java

@@ -0,0 +1,41 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford)
+//	* Aistis Simaitis <aistis.aimaitis@cs.ox.ac.uk> (University of 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 strat;
+
+import prism.PrismLog;
+
+/**
+ * Interface for classes to store strategies (for MDPs, games, etc.)
+ */
+public interface Strategy
+{
+	/**
+	 * Export the strategy to a PrismLog.
+	 */
+	public void export(PrismLog out);
+}

prism/src/strat/package-info.java

@@ -0,0 +1,4 @@
+/**
+ * Classes to represent/manipulate strategies (of MDPs, games, etc.)
+ */
+package strat;