From 4ca846889ffac7f0a7d543cbd2bf1a990aa3a1c4 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 8 Jul 2011 07:05:53 +0000 Subject: [PATCH] Extra DD-to-PP file export functionality for 3D matrices (from Vojta). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3234 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/include/JDD.h | 8 ++++ prism/include/dd_export.h | 2 + prism/src/dd/dd_export.cc | 83 +++++++++++++++++++++++++++++++++++++++ prism/src/jdd/JDD.cc | 17 ++++++++ prism/src/jdd/JDD.java | 32 +++++++++++++++ 5 files changed, 142 insertions(+) diff --git a/prism/include/JDD.h b/prism/include/JDD.h index 5d79e704..8451d5f1 100644 --- a/prism/include/JDD.h +++ b/prism/include/JDD.h @@ -639,6 +639,14 @@ JNIEXPORT void JNICALL Java_jdd_JDD_DD_1ExportDDToDotFileLabelled JNIEXPORT void JNICALL Java_jdd_JDD_DD_1ExportMatrixToPPFile (JNIEnv *, jclass, jlong, jlong, jint, jlong, jint, jstring); +/* + * Class: jdd_JDD + * Method: DD_Export3dMatrixToPPFile + * Signature: (JJIJIJILjava/lang/String;)V + */ +JNIEXPORT void JNICALL Java_jdd_JDD_DD_1Export3dMatrixToPPFile + (JNIEnv *, jclass, jlong, jlong, jint, jlong, jint, jlong, jint, jstring); + /* * Class: jdd_JDD * Method: DD_ExportMatrixToMatlabFile diff --git a/prism/include/dd_export.h b/prism/include/dd_export.h index 3db0b7f2..2eec9d3c 100644 --- a/prism/include/dd_export.h +++ b/prism/include/dd_export.h @@ -42,6 +42,8 @@ void DD_ExportMatrixToMatlabFile(DdManager *ddman, DdNode *dd, DdNode **rvars, i void DD_ExportMatrixToMatlabFile(DdManager *ddman, DdNode *dd, DdNode **rvars, int num_rvars, DdNode **cvars, int num_cvars, char *name, FILE *fp_out); void DD_ExportMatrixToPPFile(DdManager *ddman, DdNode *dd, DdNode **rvars, int num_rvars, DdNode **cvars, int num_cvars, char *filename); void DD_ExportMatrixToPPFile(DdManager *ddman, DdNode *dd, DdNode **rvars, int num_rvars, DdNode **cvars, int num_cvars, FILE *fp_out); +void DD_Export3dMatrixToPPFile(DdManager *ddman, DdNode *dd, DdNode **rvars, int num_rvars, DdNode **cvars, int num_cvars, DdNode **nvars, int num_nvars, char *filename); +void DD_Export3dMatrixToPPFile(DdManager *ddman, DdNode *dd, DdNode **rvars, int num_rvars, DdNode **cvars, int num_cvars, DdNode **nvars, int num_nvars, FILE *fp); void DD_ExportMatrixToSpyFile(DdManager *ddman, DdNode *dd, DdNode **rvars, int num_rvars, DdNode **cvars, int num_cvars, int depth, char *filename); void DD_ExportMatrixToSpyFile(DdManager *ddman, DdNode *dd, DdNode **rvars, int num_rvars, DdNode **cvars, int num_cvars, int depth, FILE *fp_out); diff --git a/prism/src/dd/dd_export.cc b/prism/src/dd/dd_export.cc index dcd363e8..c52209c0 100644 --- a/prism/src/dd/dd_export.cc +++ b/prism/src/dd/dd_export.cc @@ -3,6 +3,7 @@ // Copyright (c) 2002- // Authors: // * Dave Parker (University of Oxford, formerly University of Birmingham) +// * Vojtech Forejt (University of Oxford) // Description: DD export functions // //------------------------------------------------------------------------------ @@ -460,6 +461,88 @@ int cstart //------------------------------------------------------------------------------ +// Given a BDD that represents a MDP transition matrices, this method +// outputs one matrix for every action. +// note that the output is in fact not a PP file, but +// several PP files concatenated into one file. +// +// For example, for a model with the variable +// x : [0..2]; +// and transitions +// [a] (x=0) -> 0.3:(x'=1) + 0.7:(x'=2); +// [b] (x=0) -> 1:(x'=2); +// [a] (x=2) -> (x'=1); +// [a] (x=1) -> (x'=0); +// the output would be (e.g.) +// 4 +// 4 +// 0 2 1.000000 +// 4 +// 0 1 0.300000 +// 1 0 1.000000 +// 0 2 0.700000 +// 2 1 1.000000 +// 4 +void DD_Export3dMatrixToPPFile +( + DdManager *ddman, + DdNode *dd, + DdNode **rvars, + int num_rvars, + DdNode **cvars, + int num_cvars, + DdNode **nvars, + int num_nvars, + char *filename + ) +{ + FILE *fp = fopen(filename, "w"); + if (fp == NULL) { + // crash out + return; + } + DD_Export3dMatrixToPPFile(ddman, dd, rvars, num_rvars, cvars, num_cvars, nvars, num_nvars, fp); + fclose(fp); +} + +void DD_Export3dMatrixToPPFile +( + DdManager *ddman, + DdNode *dd, + DdNode **rvars, + int num_rvars, + DdNode **cvars, + int num_cvars, + DdNode **nvars, + int num_nvars, + FILE *fp + ) +{ + DdNode *n, *s; + if (num_nvars == 0) + { //base step: if there are no nondeterministic variables, print output as for normal PP file + fprintf(fp, "%d\n", (int)pow(2.0, num_rvars)); + DD_ExportMatrixToPPFile(ddman, dd, rvars, num_rvars, cvars, num_cvars, fp, 0, 0); + } + else + { //if there are some nondeterministic variables, we remove one of them, splitting into two cases + Cudd_Ref(dd); + Cudd_Ref(nvars[0]); + n = DD_Restrict(ddman, dd, DD_Not(ddman, nvars[0])); + Cudd_Ref(dd); + Cudd_Ref(nvars[0]); + s = DD_Restrict(ddman, dd, nvars[0]); + + DD_Export3dMatrixToPPFile(ddman, n, rvars, num_rvars, cvars, num_cvars, &nvars[1], num_nvars-1, fp); + DD_Export3dMatrixToPPFile(ddman, s, rvars, num_rvars, cvars, num_cvars, &nvars[1], num_nvars-1, fp); + + Cudd_RecursiveDeref(ddman, n); + Cudd_RecursiveDeref(ddman, s); + } +} + +//------------------------------------------------------------------------------ + void DD_ExportMatrixToSpyFile ( DdManager *ddman, diff --git a/prism/src/jdd/JDD.cc b/prism/src/jdd/JDD.cc index 7ac0f1e8..455cea10 100644 --- a/prism/src/jdd/JDD.cc +++ b/prism/src/jdd/JDD.cc @@ -3,6 +3,7 @@ // Copyright (c) 2002- // Authors: // * Dave Parker (University of Oxford, formerly University of Birmingham) +// * Vojtech Forejt (University of Oxford) // //------------------------------------------------------------------------------ // @@ -728,6 +729,22 @@ JNIEXPORT void JNICALL Java_jdd_JDD_DD_1ExportMatrixToPPFile(JNIEnv *env, jclass //------------------------------------------------------------------------------ +JNIEXPORT void JNICALL Java_jdd_JDD_DD_1Export3dMatrixToPPFile(JNIEnv *env, jclass cls, jlong __jlongpointer dd, jlong __jlongpointer rvars, jint num_rvars, jlong __jlongpointer cvars, jint num_cvars, jlong __jlongpointer nvars, jint num_nvars, jstring filename) +{ + const char *str = env->GetStringUTFChars(filename, 0); + DD_Export3dMatrixToPPFile( + ddman, jlong_to_DdNode(dd), + jlong_to_DdNode_array(rvars), num_rvars, + jlong_to_DdNode_array(cvars), num_cvars, + jlong_to_DdNode_array(nvars), num_nvars, + (char *)str + ); + env->ReleaseStringUTFChars(filename, str); +} + +//------------------------------------------------------------------------------ + + JNIEXPORT void JNICALL Java_jdd_JDD_DD_1ExportMatrixToMatlabFile(JNIEnv *env, jclass cls, jlong __jlongpointer dd, jlong __jlongpointer rvars, jint num_rvars, jlong __jlongpointer cvars, jint num_cvars, jstring name, jstring filename) { const char *str1 = env->GetStringUTFChars(name, 0); diff --git a/prism/src/jdd/JDD.java b/prism/src/jdd/JDD.java index e754ec2e..a2bb16f3 100644 --- a/prism/src/jdd/JDD.java +++ b/prism/src/jdd/JDD.java @@ -3,6 +3,7 @@ // Copyright (c) 2002- // Authors: // * Dave Parker (University of Oxford, formerly University of Birmingham) +// * Vojtech Forejt (University of Oxford) // //------------------------------------------------------------------------------ // @@ -113,6 +114,7 @@ public class JDD private static native void DD_ExportDDToDotFile(long dd, String filename); private static native void DD_ExportDDToDotFileLabelled(long dd, String filename, List var_names); private static native void DD_ExportMatrixToPPFile(long dd, long rvars, int num_rvars, long cvars, int num_cvars, String filename); + private static native void DD_Export3dMatrixToPPFile(long dd, long rvars, int num_rvars, long cvars, int num_cvars, long nvars, int num_nvars, String filename); private static native void DD_ExportMatrixToMatlabFile(long dd, long rvars, int num_rvars, long cvars, int num_cvars, String name, String filename); private static native void DD_ExportMatrixToSpyFile(long dd, long rvars, int num_rvars, long cvars, int num_cvars, int depth, String filename); @@ -952,6 +954,36 @@ public class JDD { DD_ExportMatrixToPPFile(dd.ptr(), rvars.array(), rvars.n(), cvars.array(), cvars.n(), filename); } + + /** + * Given a BDD that represents transition matrices of an MDP, this method + * outputs one matrix for every action. Note that the output is in fact + * not a PP file, but several PP files concatenated into one file. + * + * For example, for a model with the variable + * x : [0..2]; + * and transitions + * [a] (x=0) -> 0.3:(x'=1) + 0.7:(x'=2); + * [b] (x=0) -> 1:(x'=2); + * [a] (x=2) -> (x'=1); + * [a] (x=1) -> (x'=0); + * the output would be (e.g.) + * 4 + * 4 + * 0 2 1.000000 + * 4 + * 0 1 0.300000 + * 1 0 1.000000 + * 0 2 0.700000 + * 2 1 1.000000 + * 4 + * + * [ REFS: , DEREFS: ] + */ + public static void Export3dMatrixToPPFile(JDDNode dd, JDDVars rvars, JDDVars cvars, JDDVars nvars, String filename) + { + DD_Export3dMatrixToPPFile(dd.ptr(), rvars.array(), rvars.n(), cvars.array(), cvars.n(), nvars.array(), nvars.n(), filename); + } // export matrix dd to a matlab file // [ REFS: , DEREFS: ]