s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Undo last commit 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7075 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 13 years ago
parent
2c5a9de4f8
commit
026359ea2f
6 changed files with 14 additions and 46 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 4
      prism/include/PrismSparse.h
  2. 14
      prism/src/explicit/DTMCModelChecker.java
  3. 7
      prism/src/prism/Makefile
  4. 12
      prism/src/prism/NondetModelChecker.java
  5. 16
      prism/src/sparse/PS_NondetUntil.cc
  6. 7
      prism/src/sparse/PrismSparse.java

4
prism/include/PrismSparse.h
View File

@ -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

14
prism/src/explicit/DTMCModelChecker.java
View File

@ -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).

7
prism/src/prism/Makefile
View File

@ -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)

12
prism/src/prism/NondetModelChecker.java
View File

@ -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:

16
prism/src/sparse/PS_NondetUntil.cc
View File

@ -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

7
prism/src/sparse/PrismSparse.java
View File

@ -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<String> 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<String> 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<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
{
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()));
}

Write Preview
Loading…
Cancel
Save