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

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
master
Dave Parker 15 years ago
parent
2654125531
commit
4ca846889f
5 changed files with 142 additions and 0 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 8
      prism/include/JDD.h
  2. 2
      prism/include/dd_export.h
  3. 83
      prism/src/dd/dd_export.cc
  4. 17
      prism/src/jdd/JDD.cc
  5. 32
      prism/src/jdd/JDD.java

8
prism/include/JDD.h
View File

@ -639,6 +639,14 @@ JNIEXPORT void JNICALL Java_jdd_JDD_DD_1ExportDDToDotFileLabelled
JNIEXPORT void JNICALL Java_jdd_JDD_DD_1ExportMatrixToPPFile JNIEXPORT void JNICALL Java_jdd_JDD_DD_1ExportMatrixToPPFile
(JNIEnv *, jclass, jlong, jlong, jint, jlong, jint, jstring); (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 * Class: jdd_JDD
* Method: DD_ExportMatrixToMatlabFile * Method: DD_ExportMatrixToMatlabFile

2
prism/include/dd_export.h
View File

@ -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_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, char *filename);
void DD_ExportMatrixToPPFile(DdManager *ddman, DdNode *dd, DdNode **rvars, int num_rvars, DdNode **cvars, int num_cvars, FILE *fp_out); 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, char *filename);
void DD_ExportMatrixToSpyFile(DdManager *ddman, DdNode *dd, DdNode **rvars, int num_rvars, DdNode **cvars, int num_cvars, int depth, FILE *fp_out); void DD_ExportMatrixToSpyFile(DdManager *ddman, DdNode *dd, DdNode **rvars, int num_rvars, DdNode **cvars, int num_cvars, int depth, FILE *fp_out);

83
prism/src/dd/dd_export.cc
View File

@ -3,6 +3,7 @@
// Copyright (c) 2002- // Copyright (c) 2002-
// Authors: // Authors:
// * Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford, formerly University of Birmingham) // * Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford, formerly University of Birmingham)
// * Vojtech Forejt <vojtech.forejt@cs.ox.ac.uk> (University of Oxford)
// Description: DD export functions // 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 void DD_ExportMatrixToSpyFile
( (
DdManager *ddman, DdManager *ddman,

17
prism/src/jdd/JDD.cc
View File

@ -3,6 +3,7 @@
// Copyright (c) 2002- // Copyright (c) 2002-
// Authors: // Authors:
// * Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford, formerly University of Birmingham) // * Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford, formerly University of Birmingham)
// * Vojtech Forejt <vojtech.forejt@cs.ox.ac.uk> (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) 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); const char *str1 = env->GetStringUTFChars(name, 0);

32
prism/src/jdd/JDD.java
View File

@ -3,6 +3,7 @@
// Copyright (c) 2002- // Copyright (c) 2002-
// Authors: // Authors:
// * Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford, formerly University of Birmingham) // * Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford, formerly University of Birmingham)
// * Vojtech Forejt <vojtech.forejt@cs.ox.ac.uk> (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_ExportDDToDotFile(long dd, String filename);
private static native void DD_ExportDDToDotFileLabelled(long dd, String filename, List<String> var_names); private static native void DD_ExportDDToDotFileLabelled(long dd, String filename, List<String> 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_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_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); private static native void DD_ExportMatrixToSpyFile(long dd, long rvars, int num_rvars, long cvars, int num_cvars, int depth, String filename);
@ -953,6 +955,36 @@ public class JDD
DD_ExportMatrixToPPFile(dd.ptr(), rvars.array(), rvars.n(), cvars.array(), cvars.n(), filename); 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: <none>, DEREFS: <none> ]
*/
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 // export matrix dd to a matlab file
// [ REFS: <none>, DEREFS: <none> ] // [ REFS: <none>, DEREFS: <none> ]

Write Preview
Loading…
Cancel
Save