diff --git a/prism/include/PrismSparse.h b/prism/include/PrismSparse.h index 788fd220..eb3012cc 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;JJIJIJIJJZLstrat/MDStrategyNative;)J + * Signature: (JJLjava/util/List;JJIJIJIJJZ)J */ JNIEXPORT jlong JNICALL Java_sparse_PrismSparse_PS_1NondetUntil - (JNIEnv *, jclass, jlong, jlong, jobject, jlong, jlong, jint, jlong, jint, jlong, jint, jlong, jlong, jboolean, jobject); + (JNIEnv *, jclass, jlong, jlong, jobject, jlong, jlong, jint, jlong, jint, jlong, jint, jlong, jlong, jboolean); /* * Class: sparse_PrismSparse diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index b7e7f05f..106ae3d6 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -27,17 +27,13 @@ package explicit; import java.io.File; -import java.util.BitSet; -import java.util.List; -import java.util.Map; +import java.util.*; -import parser.ast.Expression; -import parser.ast.ExpressionTemporal; -import parser.ast.ExpressionUnaryOp; +import prism.*; +import explicit.StateValues; +import explicit.rewards.*; +import parser.ast.*; 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 314c53a5..2e5d007b 100644 --- a/prism/src/prism/Makefile +++ b/prism/src/prism/Makefile @@ -29,9 +29,6 @@ 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) @@ -48,8 +45,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) $(O_FILES_EXT) - $(LD) $(SHARED) $(LDFLAGS) -o $@ $(O_FILES) $(O_FILES_EXT) $(LIBRARIES) +$(PRISM_DIR_REL)/$(LIB_DIR)/$(LIBPREFIX)prism$(LIBSUFFIX): $(O_FILES) + $(LD) $(SHARED) $(LDFLAGS) -o $@ $(O_FILES) $(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 0936e348..5482cd25 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -42,7 +42,6 @@ import jdd.*; import dv.*; import mtbdd.*; import sparse.*; -import strat.MDStrategyNative; import hybrid.*; import parser.ast.*; import parser.visitor.ASTTraverse; @@ -1964,16 +1963,7 @@ public class NondetModelChecker extends NonProbModelChecker probs = new StateValuesMTBDD(probsMTBDD, model); break; case Prism.SPARSE: - 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(); - } + probsDV = PrismSparse.NondetUntil(tr, tra, model.getSynchs(), odd, allDDRowVars, allDDColVars, allDDNondetVars, yes, maybe, min); 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 83c2077c..d8eb7ca2 100644 --- a/prism/src/sparse/PS_NondetUntil.cc +++ b/prism/src/sparse/PS_NondetUntil.cc @@ -57,8 +57,7 @@ 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) -jobject md_strat // storage for an MD strategy +jboolean min // min or max probabilities (true = min, false = max) ) { // cast function parameters @@ -217,19 +216,6 @@ jobject md_strat // storage for an MD strategy 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 af5b5424..a395c93c 100644 --- a/prism/src/sparse/PrismSparse.java +++ b/prism/src/sparse/PrismSparse.java @@ -30,7 +30,6 @@ import java.io.FileNotFoundException; import java.util.List; import prism.*; -import strat.MDStrategyNative; import jdd.*; import dv.*; import odd.*; @@ -203,10 +202,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, 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 + 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 { - 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); + 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); if (ptr == 0) throw new PrismException(getErrorMessage()); return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff())); }