diff --git a/prism/include/PrismSparse.h b/prism/include/PrismSparse.h index eb3012cc..788fd220 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;JJIJIJIJJZLstrat/MDStrategyNative;)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, jobject); /* * Class: sparse_PrismSparse diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index 106ae3d6..b7e7f05f 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -27,13 +27,17 @@ package explicit; import java.io.File; -import java.util.*; +import java.util.BitSet; +import java.util.List; +import java.util.Map; -import prism.*; -import explicit.StateValues; -import explicit.rewards.*; -import parser.ast.*; +import parser.ast.Expression; +import parser.ast.ExpressionTemporal; +import parser.ast.ExpressionUnaryOp; import parser.type.TypeDouble; +import prism.PrismException; +import prism.PrismUtils; +import explicit.rewards.MCRewards; /** * Explicit-state model checker for discrete-time Markov chains (DTMCs). diff --git a/prism/src/prism/Makefile b/prism/src/prism/Makefile index 2e5d007b..314c53a5 100644 --- a/prism/src/prism/Makefile +++ b/prism/src/prism/Makefile @@ -29,6 +29,9 @@ PRISM_CLASSPATH = "$(THIS_DIR)/$(PRISM_DIR_REL)/$(CLASSES_DIR)$(CLASSPATHSEP)$(T CC_FILES = $(wildcard *.cc) O_FILES = $(CC_FILES:%.cc=$(PRISM_DIR_REL)/$(OBJ_DIR)/$(THIS_DIR)/%.o) +O_FILES_EXT = $(wildcard $(PRISM_DIR_REL)/$(OBJ_DIR)/strat/*.o) + + default: all all: checks $(CLASS_FILES) $(PRISM_DIR_REL)/$(INCLUDE_DIR)/PrismNative.h $(PRISM_DIR_REL)/$(LIB_DIR)/$(LIBPREFIX)prism$(LIBSUFFIX) @@ -45,8 +48,8 @@ $(PRISM_DIR_REL)/$(CLASSES_DIR)/$(THIS_DIR)/%.class: %.java $(PRISM_DIR_REL)/$(INCLUDE_DIR)/PrismNative.h: $(PRISM_DIR_REL)/$(CLASSES_DIR)/$(THIS_DIR)/PrismNative.class ($(JAVAH) -classpath $(PRISM_DIR_REL)/$(CLASSES_DIR) -jni -o $@ $(THIS_DIR).PrismNative; touch $@) -$(PRISM_DIR_REL)/$(LIB_DIR)/$(LIBPREFIX)prism$(LIBSUFFIX): $(O_FILES) - $(LD) $(SHARED) $(LDFLAGS) -o $@ $(O_FILES) $(LIBRARIES) +$(PRISM_DIR_REL)/$(LIB_DIR)/$(LIBPREFIX)prism$(LIBSUFFIX): $(O_FILES) $(O_FILES_EXT) + $(LD) $(SHARED) $(LDFLAGS) -o $@ $(O_FILES) $(O_FILES_EXT) $(LIBRARIES) $(PRISM_DIR_REL)/$(OBJ_DIR)/$(THIS_DIR)/%.o: %.cc $(CPP) $(CPPFLAGS) -c $< -o $@ $(INCLUDES) diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 5482cd25..0936e348 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -42,6 +42,7 @@ import jdd.*; import dv.*; import mtbdd.*; import sparse.*; +import strat.MDStrategyNative; import hybrid.*; import parser.ast.*; import parser.visitor.ASTTraverse; @@ -1963,7 +1964,16 @@ 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); + MDStrategyNative stratNative = null; + if (true) { + stratNative = new MDStrategyNative((int) model.getNumStates()); + } + probsDV = PrismSparse.NondetUntil(tr, tra, model.getSynchs(), odd, allDDRowVars, allDDColVars, allDDNondetVars, yes, maybe, min, stratNative); + if (true) { + mainLog.println(); + stratNative.exportActions(mainLog); + // TODO cexNative.clear(); + } probs = new StateValuesDV(probsDV, model); break; case Prism.HYBRID: diff --git a/prism/src/sparse/PS_NondetUntil.cc b/prism/src/sparse/PS_NondetUntil.cc index d8eb7ca2..83c2077c 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) +jobject md_strat // storage for an MD strategy ) { // cast function parameters @@ -216,6 +217,19 @@ jboolean min // min or max probabilities (true = min, false = max) PS_PrintWarningToMainLog(env, "Adversary generation cancelled (could not open file \"%s\").", export_adv_filename); export_adv_enabled = EXPORT_ADV_NONE; } + + // store... + int i, j; + jclass vn_cls; + jmethodID vn_mid; + + vn_cls = env->GetObjectClass(md_strat); + vn_mid = env->GetMethodID(vn_cls, "setPointer", "(J)V"); + if (vn_mid == 0) { + return; + } + env->CallIntMethod(md_strat, vn_mid, ptr_to_jlong(adv)); + } // store local copies of stuff diff --git a/prism/src/sparse/PrismSparse.java b/prism/src/sparse/PrismSparse.java index a395c93c..af5b5424 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.MDStrategyNative; 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, MDStrategyNative 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, MDStrategyNative 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); if (ptr == 0) throw new PrismException(getErrorMessage()); return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff())); }