First (partial) connection of sparse adversary generation to Strategy classes and -exportstrat.

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

prism/include/PrismSparse.h

@@ -106,10 +106,10 @@ JNIEXPORT jlong JNICALL Java_sparse_PrismSparse_PS_1NondetBoundedUntil
 /*
  * Class:     sparse_PrismSparse
  * Method:    PS_NondetUntil
- * Signature: (JJLjava/util/List;JJIJIJIJJZ)J
+ * Signature: (JJLjava/util/List;JJIJIJIJJZJ)J
  */
 JNIEXPORT jlong JNICALL Java_sparse_PrismSparse_PS_1NondetUntil
-  (JNIEnv *, jclass, jlong, jlong, jobject, jlong, jlong, jint, jlong, jint, jlong, jint, jlong, jlong, jboolean);
+  (JNIEnv *, jclass, jlong, jlong, jobject, jlong, jlong, jint, jlong, jint, jlong, jint, jlong, jlong, jboolean, jlong);
 
 /*
  * Class:     sparse_PrismSparse

prism/src/dv/IntegerVector.java

@@ -54,13 +54,21 @@ public class IntegerVector
 	// instance variables/methods
 	//------------------------------------------------------------------------------
 
-	// data
-	private long v; // vector (actually a C/C++ pointer cast to a long)
-	private int n; // size
+	/**
+	 * Vector contents (C/C++ pointer cast to a long)
+	 */
+	private long v;
+	/**
+	 * Size of vector
+	 */
+	private int n;
 	
 	// constructors
 	
-	private native long IV_CreateZeroVector(int n);
+	/**
+	 * Create a new IntegerVector of size {@code size} with all entries set to 0.
+	 * @throws PrismException if there is insufficient memory to create the array.
+	 */
 	public IntegerVector(int size) throws PrismException
 	{
 		v = IV_CreateZeroVector(size);
@@ -68,6 +76,11 @@ public class IntegerVector
 		n = size;
 	}
 	
+	private native long IV_CreateZeroVector(int n);
+	
+	/**
+	 * Create a new IntegerVector from a pointer {@code vect} to an existing native integer array of size {@code size}.
+	 */
 	public IntegerVector(long vector, int size)
 	{
 		v = vector;

prism/src/prism/NondetModelChecker.java

@@ -29,11 +29,8 @@
 
 package prism;
 
-import java.io.BufferedWriter;
 import java.io.File;
 import java.io.FileNotFoundException;
-import java.io.FileWriter;
-import java.io.IOException;
 import java.util.*;
 
 import odd.ODDUtils;
@@ -42,6 +39,7 @@ import jdd.*;
 import dv.*;
 import mtbdd.*;
 import sparse.*;
+import strat.MDStrategyIV;
 import hybrid.*;
 import parser.ast.*;
 import parser.visitor.ASTTraverse;
@@ -1963,7 +1961,17 @@ public class NondetModelChecker extends NonProbModelChecker
 					probs = new StateValuesMTBDD(probsMTBDD, model);
 					break;
 				case Prism.SPARSE:
-					probsDV = PrismSparse.NondetUntil(tr, tra, model.getSynchs(), odd, allDDRowVars, allDDColVars, allDDNondetVars, yes, maybe, min);
+					IntegerVector strat = null;
+					if (genStrat) {
+						strat = new IntegerVector((int) model.getNumStates());
+					}
+					probsDV = PrismSparse.NondetUntil(tr, tra, model.getSynchs(), odd, allDDRowVars, allDDColVars, allDDNondetVars, yes, maybe, min, strat);
+					if (genStrat) {
+						mainLog.println();
+						MDStrategyIV strategy = new MDStrategyIV(model, strat);
+						strategy.exportActions(mainLog);
+						strategy.clear();
+					}
 					probs = new StateValuesDV(probsDV, model);
 					break;
 				case Prism.HYBRID:

prism/src/prism/StateModelChecker.java

@@ -76,6 +76,8 @@ public class StateModelChecker implements ModelChecker
 	protected double termCritParam;
 	// Verbose mode?
 	protected boolean verbose;
+	// Generate/store a strategy during model checking?
+	protected boolean genStrat = false;
 
 	// Constructor
 
@@ -107,6 +109,7 @@ public class StateModelChecker implements ModelChecker
 		engine = prism.getEngine();
 		termCritParam = prism.getTermCritParam();
 		verbose = prism.getVerbose();
+		genStrat = prism.getGenStrat();
 	}
 
 	/**

prism/src/sparse/PS_NondetUntil.cc

@@ -57,7 +57,8 @@ jlong __jlongpointer ndv,	// nondet vars
 jint num_ndvars,
 jlong __jlongpointer y,		// 'yes' states
 jlong __jlongpointer m,		// 'maybe' states
-jboolean min				// min or max probabilities (true = min, false = max)
+jboolean min,				// min or max probabilities (true = min, false = max)
+jlong _strat				// strategy storage
 )
 {
 	// cast function parameters
@@ -69,6 +70,7 @@ jboolean min				// min or max probabilities (true = min, false = max)
 	DdNode **ndvars = jlong_to_DdNode_array(ndv);	// nondet vars
 	DdNode *yes = jlong_to_DdNode(y);				// 'yes' states
 	DdNode *maybe = jlong_to_DdNode(m); 			// 'maybe' states
+	int *strat = (int *)jlong_to_ptr(_strat);		// strategy storage
 
 	// mtbdds
 	DdNode *a = NULL, *tmp = NULL;
@@ -139,7 +141,7 @@ jboolean min				// min or max probabilities (true = min, false = max)
 	
 	// if needed, and if info is available, build a vector of action indices for the MDP
 	actions = NULL;
-	if (export_adv_enabled != EXPORT_ADV_NONE) {
+	if (export_adv_enabled != EXPORT_ADV_NONE || strat != NULL) {
 		if (trans_actions != NULL) {
 			PS_PrintToMainLog(env, "Building action information... ");
 			// first need to filter out unwanted rows
@@ -175,9 +177,9 @@ jboolean min				// min or max probabilities (true = min, false = max)
 	PS_PrintMemoryToMainLog(env, "[2 x ", kb, "]\n");
 	
 	// if required, create storage for adversary and initialise
-	if (export_adv_enabled != EXPORT_ADV_NONE) {
+	if (export_adv_enabled != EXPORT_ADV_NONE || strat != NULL) {
 		PS_PrintToMainLog(env, "Allocating adversary vector... ");
-		adv = new int[n];
+		adv = (strat == NULL) ? new int[n] : strat;
 		kb = n*sizeof(int)/1024.0;
 		kbt += kb;
 		PS_PrintMemoryToMainLog(env, "[", kb, "]\n");
@@ -249,7 +251,7 @@ jboolean min				// min or max probabilities (true = min, false = max)
 				if (first || (min&&(d2<d1)) || (!min&&(d2>d1))) {
 					d1 = d2;
 					// if adversary generation is enabled, remember optimal choice
-					if (export_adv_enabled != EXPORT_ADV_NONE) {
+					if (export_adv_enabled != EXPORT_ADV_NONE || strat != NULL) {
 						// for max, only remember strictly better choices
 						// (this resolves problems with end components)
 						if (!min) {
@@ -340,6 +342,13 @@ jboolean min				// min or max probabilities (true = min, false = max)
 		fclose(fp_adv);
 		PS_PrintToMainLog(env, "\nAdversary written to file \"%s\".\n", export_adv_filename);
 	}
+		
+	// convert strategy indices from choices to actions
+	if (strat != NULL) {
+		for (i = 0; i < n; i++) {
+			if (adv[i] > 0) strat[i] = actions[adv[i]] - 1;
+		}
+	}
 	
 	// catch exceptions: register error, free memory
 	} catch (std::bad_alloc e) {
@@ -353,7 +362,7 @@ jboolean min				// min or max probabilities (true = min, false = max)
 	if (ndsm) delete ndsm;
 	if (yes_vec) delete[] yes_vec;
 	if (soln2) delete[] soln2;
-	if (adv) delete[] adv;
+	//if (strat == NULL && adv) delete[] adv;
 	if (actions != NULL) {
 		delete[] actions;
 		release_string_array_from_java(env, action_names_jstrings, action_names, num_actions);

prism/src/sparse/PrismSparse.java

@@ -30,6 +30,7 @@ import java.io.FileNotFoundException;
 import java.util.List;
 
 import prism.*;
+import strat.MDStrategyIV;
 import jdd.*;
 import dv.*;
 import odd.*;
@@ -202,10 +203,10 @@ public class PrismSparse
 	}
 	
 	// pctl until (nondeterministic/mdp)
-	private static native long PS_NondetUntil(long trans, long trans_actions, List<String> synchs, long odd, long rv, int nrv, long cv, int ncv, long ndv, int nndv, long yes, long maybe, boolean minmax);
-	public static DoubleVector NondetUntil(JDDNode trans, JDDNode transActions, List<String> synchs, ODDNode odd, JDDVars rows, JDDVars cols, JDDVars nondet, JDDNode yes, JDDNode maybe, boolean minmax) throws PrismException
+	private static native long PS_NondetUntil(long trans, long trans_actions, List<String> synchs, long odd, long rv, int nrv, long cv, int ncv, long ndv, int nndv, long yes, long maybe, boolean minmax, long strat);
+	public static DoubleVector NondetUntil(JDDNode trans, JDDNode transActions, List<String> synchs, ODDNode odd, JDDVars rows, JDDVars cols, JDDVars nondet, JDDNode yes, JDDNode maybe, boolean minmax, IntegerVector strat) throws PrismException
 	{
-		long ptr = PS_NondetUntil(trans.ptr(), (transActions == null) ? 0 : transActions.ptr(), synchs, odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), yes.ptr(), maybe.ptr(), minmax);
+		long ptr = PS_NondetUntil(trans.ptr(), (transActions == null) ? 0 : transActions.ptr(), synchs, odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), yes.ptr(), maybe.ptr(), minmax, (strat == null) ? 0 : strat.getPtr());
 		if (ptr == 0) throw new PrismException(getErrorMessage());
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}

prism/src/strat/MDStrategyIV.java

@@ -0,0 +1,101 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	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 strat;
+
+import java.util.List;
+
+import dv.IntegerVector;
+
+import prism.Model;
+
+/**
+ * Class to store a memoryless deterministic (MD) strategy, as a IntegerVector (i.e. stored natively as an array).
+ */
+public class MDStrategyIV extends MDStrategy
+{
+	// Model associated with the strategy
+	private Model model;
+	
+	private IntegerVector iv;
+	
+	private List<String> actions;
+	
+	private int numStates;
+	private long ptr;
+	
+	/**
+	 * Creates...
+	 */
+	public MDStrategyIV(Model model)
+	{
+		this.model = model;
+		numStates = (int) model.getNumStates();
+		actions = model.getSynchs();
+	}
+	
+	/**
+	 * Creates...
+	 */
+	public MDStrategyIV(Model model, IntegerVector iv)
+	{
+		this.model = model;
+		numStates = (int) model.getNumStates();
+		actions = model.getSynchs();
+		this.iv = iv;
+	}
+	
+	public void setPointer(long ptr)
+	{
+		this.ptr = ptr;
+	}
+	
+	@Override
+	public int getNumStates()
+	{
+		return numStates;
+	}
+	
+	@Override
+	public int getChoice(int s)
+	{
+		return 99;
+	}
+	
+	@Override
+	public Object getChoiceAction(int s)
+	{
+		int c = iv.getElement(s);
+		//return ""+c; //c >= 0 ? actions.get(c) : "?";
+		return c >= 0 ? actions.get(c) : c == -1 ? "?" : c == -2 ? "*" : "-";
+	}
+	
+	public void clear()
+	{
+		iv.clear();
+		iv = null;
+	}
+}

prism/src/strat/Makefile

@@ -0,0 +1,54 @@
+################################################
+#  NB: This Makefile is designed to be called  #
+#      from the main PRISM Makefile. It won't  #
+#      work on its own because it needs        #
+#      various options to be passed in         #
+################################################
+
+.SUFFIXES: .o .c .cc
+
+# Reminder: $@ = target, $* = target without extension, $< = dependency
+
+THIS_DIR = strat
+PRISM_DIR_REL = ../..
+
+INCLUDES = \
+-I$(PRISM_DIR_REL)/$(CUDD_DIR)/include \
+-I"$(JAVA_JNI_H_DIR)" \
+-I"$(JAVA_JNI_MD_H_DIR)" \
+-I$(PRISM_DIR_REL)/$(INCLUDE_DIR)
+
+LIBRARIES = \
+-L$(PRISM_DIR_REL)/$(LIB_DIR) \
+-lodd \
+-ldd \
+$(LIBMATH)
+
+JAVA_FILES_ALL = $(wildcard *.java)
+JAVA_FILES = $(subst package-info.java,,$(JAVA_FILES_ALL))
+CLASS_FILES = $(JAVA_FILES:%.java=$(PRISM_DIR_REL)/$(CLASSES_DIR)/$(THIS_DIR)/%.class)
+
+PRISM_CLASSPATH = "$(THIS_DIR)/$(PRISM_DIR_REL)/$(CLASSES_DIR)$(CLASSPATHSEP)$(THIS_DIR)/$(PRISM_DIR_REL)/lib/*"
+
+default: all
+
+all: checks $(CLASS_FILES)
+
+# Try and prevent accidental makes (i.e. called manually, not from top-level Makefile)
+checks:
+	@if [ "$(SRC_DIR)" = "" ]; then \
+	  (echo "Error: This Makefile is designed to be called from the main PRISM Makefile"; exit 1) \
+	fi; 
+
+$(PRISM_DIR_REL)/$(CLASSES_DIR)/$(THIS_DIR)/%.class: %.java
+	(cd ..; $(JAVAC) -sourcepath $(THIS_DIR)/$(PRISM_DIR_REL)/$(SRC_DIR) -classpath $(PRISM_CLASSPATH) -d $(THIS_DIR)/$(PRISM_DIR_REL)/$(CLASSES_DIR) $(THIS_DIR)/$<)
+
+$(PRISM_DIR_REL)/$(OBJ_DIR)/$(THIS_DIR)/%.o: %.cc
+	$(CPP) $(CPPFLAGS) -c $< -o $@ $(INCLUDES)
+
+clean: checks
+	@rm -f $(CLASS_FILES) $(O_FILES)
+
+celan: clean
+
+#################################################