diff --git a/prism/include/PrismSparse.h b/prism/include/PrismSparse.h index eb3012cc..756b525d 100644 --- a/prism/include/PrismSparse.h +++ b/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 diff --git a/prism/src/dv/IntegerVector.java b/prism/src/dv/IntegerVector.java index 5cc2c746..5dd453be 100644 --- a/prism/src/dv/IntegerVector.java +++ b/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; diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 5482cd25..c8942041 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/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: diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index 2589d3f0..556d1c2b 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/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(); } /** diff --git a/prism/src/sparse/PS_NondetUntil.cc b/prism/src/sparse/PS_NondetUntil.cc index d8eb7ca2..2e3d008c 100644 --- a/prism/src/sparse/PS_NondetUntil.cc +++ b/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&&(d2d1))) { 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); diff --git a/prism/src/sparse/PrismSparse.java b/prism/src/sparse/PrismSparse.java index a395c93c..d25f7ca7 100644 --- a/prism/src/sparse/PrismSparse.java +++ b/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 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 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 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 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())); } diff --git a/prism/src/strat/MDStrategyIV.java b/prism/src/strat/MDStrategyIV.java new file mode 100644 index 00000000..d0e9f724 --- /dev/null +++ b/prism/src/strat/MDStrategyIV.java @@ -0,0 +1,101 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (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 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; + } +} diff --git a/prism/src/strat/Makefile b/prism/src/strat/Makefile new file mode 100644 index 00000000..2f4e62e2 --- /dev/null +++ b/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 + +#################################################