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

Addition of VariablesGreaterThan etc. functions to dd/jdd (used for symmetry). 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 20 years ago
parent
982a966cfd
commit
2e52615489
5 changed files with 290 additions and 1 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. 40
      prism/include/JDD.h
  2. 5
      prism/include/dd_vars.h
  3. 165
      prism/src/dd/dd_vars.cc
  4. 36
      prism/src/jdd/JDD.cc
  5. 45
      prism/src/jdd/JDD.java

40
prism/include/JDD.h
View File

@ -269,6 +269,46 @@ JNIEXPORT jint JNICALL Java_jdd_JDD_DD_1PermuteVariables
JNIEXPORT jint JNICALL Java_jdd_JDD_DD_1SwapVariables
(JNIEnv *, jclass, jint, jint, jint, jint);
/*
* Class: jdd_JDD
* Method: DD_VariablesGreaterThan
* Signature: (III)I
*/
JNIEXPORT jint JNICALL Java_jdd_JDD_DD_1VariablesGreaterThan
(JNIEnv *, jclass, jint, jint, jint);
/*
* Class: jdd_JDD
* Method: DD_VariablesGreaterThanEquals
* Signature: (III)I
*/
JNIEXPORT jint JNICALL Java_jdd_JDD_DD_1VariablesGreaterThanEquals
(JNIEnv *, jclass, jint, jint, jint);
/*
* Class: jdd_JDD
* Method: DD_VariablesLessThan
* Signature: (III)I
*/
JNIEXPORT jint JNICALL Java_jdd_JDD_DD_1VariablesLessThan
(JNIEnv *, jclass, jint, jint, jint);
/*
* Class: jdd_JDD
* Method: DD_VariablesLessThanEquals
* Signature: (III)I
*/
JNIEXPORT jint JNICALL Java_jdd_JDD_DD_1VariablesLessThanEquals
(JNIEnv *, jclass, jint, jint, jint);
/*
* Class: jdd_JDD
* Method: DD_VariablesEquals
* Signature: (III)I
*/
JNIEXPORT jint JNICALL Java_jdd_JDD_DD_1VariablesEquals
(JNIEnv *, jclass, jint, jint, jint);
/*
* Class: jdd_JDD
* Method: DD_ThereExists

5
prism/include/dd_vars.h
View File

@ -34,5 +34,10 @@
DdNode *DD_PermuteVariables(DdManager *ddman, DdNode *dd, DdNode **old_vars, DdNode **new_vars, int num_vars);
DdNode *DD_SwapVariables(DdManager *ddman, DdNode *dd, DdNode **old_vars, DdNode **new_vars, int num_vars);
DdNode *DD_VariablesGreaterThan(DdManager *ddman, DdNode **x_vars, DdNode **y_vars, int num_vars);
DdNode *DD_VariablesGreaterThanEquals(DdManager *ddman, DdNode **x_vars, DdNode **y_vars, int num_vars);
DdNode *DD_VariablesLessThan(DdManager *ddman, DdNode **x_vars, DdNode **y_vars, int num_vars);
DdNode *DD_VariablesLessThanEquals(DdManager *ddman, DdNode **x_vars, DdNode **y_vars, int num_vars);
DdNode *DD_VariablesEquals(DdManager *ddman, DdNode **x_vars, DdNode **y_vars, int num_vars);
//------------------------------------------------------------------------------

165
prism/src/dd/dd_vars.cc
View File

@ -30,6 +30,7 @@
#include <util.h>
#include <cudd.h>
#include "dd_vars.h"
#include "dd_basics.h"
//------------------------------------------------------------------------------
@ -88,3 +89,167 @@ int num_vars
}
//------------------------------------------------------------------------------
// Generates BDD for the function x > y
// where x, y are num_vars-bit numbers encoded by variables x_vars, y_vars
DdNode *DD_VariablesGreaterThan
(
DdManager *ddman,
DdNode **x_vars,
DdNode **y_vars,
int num_vars
)
{
DdNode *tmp, *res;
DdNode **x_bdd_vars, **y_bdd_vars;
int i;
// create bdd vars from add vars
x_bdd_vars = new DdNode*[num_vars];
y_bdd_vars = new DdNode*[num_vars];
for (i = 0; i < num_vars; i++) {
x_bdd_vars[i] = Cudd_bddIthVar(ddman, x_vars[i]->index);
Cudd_Ref(x_bdd_vars[i]);
y_bdd_vars[i] = Cudd_bddIthVar(ddman, y_vars[i]->index);
Cudd_Ref(y_bdd_vars[i]);
}
// call main function
tmp = Cudd_Xgty(ddman, num_vars, NULL, x_bdd_vars, y_bdd_vars);
Cudd_Ref(tmp);
// convert bdd to add
res = Cudd_BddToAdd(ddman, tmp);
Cudd_Ref(res);
Cudd_RecursiveDeref(ddman, tmp);
// free variables
for (i = 0; i < num_vars; i++) {
Cudd_RecursiveDeref(ddman, x_bdd_vars[i]);
Cudd_RecursiveDeref(ddman, y_bdd_vars[i]);
}
delete x_bdd_vars;
delete y_bdd_vars;
return res;
}
//------------------------------------------------------------------------------
// Generates BDD for the function x >= y
// where x, y are num_vars-bit numbers encoded by variables x_vars, y_vars
DdNode *DD_VariablesGreaterThanEquals
(
DdManager *ddman,
DdNode **x_vars,
DdNode **y_vars,
int num_vars
)
{
return DD_Not(ddman, DD_VariablesLessThan(ddman, x_vars, y_vars, num_vars));
}
//------------------------------------------------------------------------------
// Generates BDD for the function x < y
// where x, y are num_vars-bit numbers encoded by variables x_vars, y_vars
DdNode *DD_VariablesLessThan
(
DdManager *ddman,
DdNode **x_vars,
DdNode **y_vars,
int num_vars
)
{
DdNode *tmp, *res;
DdNode **x_bdd_vars, **y_bdd_vars;
int i;
// create bdd vars from add vars
x_bdd_vars = new DdNode*[num_vars];
y_bdd_vars = new DdNode*[num_vars];
for (i = 0; i < num_vars; i++) {
x_bdd_vars[i] = Cudd_bddIthVar(ddman, x_vars[i]->index);
Cudd_Ref(x_bdd_vars[i]);
y_bdd_vars[i] = Cudd_bddIthVar(ddman, y_vars[i]->index);
Cudd_Ref(y_bdd_vars[i]);
}
// call main function
tmp = Cudd_Xgty(ddman, num_vars, NULL, y_bdd_vars, x_bdd_vars);
Cudd_Ref(tmp);
// convert bdd to add
res = Cudd_BddToAdd(ddman, tmp);
Cudd_Ref(res);
Cudd_RecursiveDeref(ddman, tmp);
// free variables
for (i = 0; i < num_vars; i++) {
Cudd_RecursiveDeref(ddman, x_bdd_vars[i]);
Cudd_RecursiveDeref(ddman, y_bdd_vars[i]);
}
delete x_bdd_vars;
delete y_bdd_vars;
return res;
}
//------------------------------------------------------------------------------
// Generates BDD for the function x <= y
// where x, y are num_vars-bit numbers encoded by variables x_vars, y_vars
DdNode *DD_VariablesLessThanEquals
(
DdManager *ddman,
DdNode **x_vars,
DdNode **y_vars,
int num_vars
)
{
return DD_Not(ddman, DD_VariablesGreaterThan(ddman, x_vars, y_vars, num_vars));
}
//------------------------------------------------------------------------------
// Generates BDD for the function x == y
// where x, y are num_vars-bit numbers encoded by variables x_vars, y_vars
DdNode *DD_VariablesEquals
(
DdManager *ddman,
DdNode **x_vars,
DdNode **y_vars,
int num_vars
)
{
DdNode *tmp, *res;
DdNode **x_bdd_vars, **y_bdd_vars;
int i;
// create bdd vars from add vars
x_bdd_vars = new DdNode*[num_vars];
y_bdd_vars = new DdNode*[num_vars];
for (i = 0; i < num_vars; i++) {
x_bdd_vars[i] = Cudd_bddIthVar(ddman, x_vars[i]->index);
Cudd_Ref(x_bdd_vars[i]);
y_bdd_vars[i] = Cudd_bddIthVar(ddman, y_vars[i]->index);
Cudd_Ref(y_bdd_vars[i]);
}
// call main function
tmp = Cudd_Xeqy(ddman, num_vars, x_bdd_vars, y_bdd_vars);
Cudd_Ref(tmp);
// convert bdd to add
res = Cudd_BddToAdd(ddman, tmp);
Cudd_Ref(res);
Cudd_RecursiveDeref(ddman, tmp);
// free variables
for (i = 0; i < num_vars; i++) {
Cudd_RecursiveDeref(ddman, x_bdd_vars[i]);
Cudd_RecursiveDeref(ddman, y_bdd_vars[i]);
}
delete x_bdd_vars;
delete y_bdd_vars;
return res;
}
//------------------------------------------------------------------------------

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

@ -251,12 +251,46 @@ JNIEXPORT jint JNICALL Java_jdd_JDD_DD_1PermuteVariables(JNIEnv *env, jclass cls
//------------------------------------------------------------------------------
JNIEXPORT jint JNICALL Java_jdd_JDD_DD_1SwapVariables(JNIEnv *env, jclass cls, jint dd, jint old_vars, jint new_vars, jint num_vars)
{
return (int)DD_SwapVariables(ddman, (DdNode *)dd, (DdNode **)old_vars, (DdNode **)new_vars, num_vars);
}
//------------------------------------------------------------------------------
JNIEXPORT jint JNICALL Java_jdd_JDD_DD_1VariablesGreaterThan(JNIEnv *env, jclass cls, jint x_vars, jint y_vars, jint num_vars)
{
return (int)DD_VariablesGreaterThan(ddman, (DdNode **)x_vars, (DdNode **)y_vars, num_vars);
}
//------------------------------------------------------------------------------
JNIEXPORT jint JNICALL Java_jdd_JDD_DD_1VariablesGreaterThanEquals(JNIEnv *env, jclass cls, jint x_vars, jint y_vars, jint num_vars)
{
return (int)DD_VariablesGreaterThanEquals(ddman, (DdNode **)x_vars, (DdNode **)y_vars, num_vars);
}
//------------------------------------------------------------------------------
JNIEXPORT jint JNICALL Java_jdd_JDD_DD_1VariablesLessThan(JNIEnv *env, jclass cls, jint x_vars, jint y_vars, jint num_vars)
{
return (int)DD_VariablesLessThan(ddman, (DdNode **)x_vars, (DdNode **)y_vars, num_vars);
}
//------------------------------------------------------------------------------
JNIEXPORT jint JNICALL Java_jdd_JDD_DD_1VariablesLessThanEquals(JNIEnv *env, jclass cls, jint x_vars, jint y_vars, jint num_vars)
{
return (int)DD_VariablesLessThanEquals(ddman, (DdNode **)x_vars, (DdNode **)y_vars, num_vars);
}
//------------------------------------------------------------------------------
JNIEXPORT jint JNICALL Java_jdd_JDD_DD_1VariablesEquals(JNIEnv *env, jclass cls, jint x_vars, jint y_vars, jint num_vars)
{
return (int)DD_VariablesEquals(ddman, (DdNode **)x_vars, (DdNode **)y_vars, num_vars);
}
//==============================================================================
//
// Wrapper functions for dd_abstr

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

@ -65,6 +65,11 @@ public class JDD
// dd_vars
private static native int DD_PermuteVariables(int dd, int old_vars, int new_vars, int num_vars);
private static native int DD_SwapVariables(int dd, int old_vars, int new_vars, int num_vars);
private static native int DD_VariablesGreaterThan(int x_vars, int y_vars, int num_vars);
private static native int DD_VariablesGreaterThanEquals(int x_vars, int y_vars, int num_vars);
private static native int DD_VariablesLessThan(int x_vars, int y_vars, int num_vars);
private static native int DD_VariablesLessThanEquals(int x_vars, int y_vars, int num_vars);
private static native int DD_VariablesEquals(int x_vars, int y_vars, int num_vars);
// dd_abstr
private static native int DD_ThereExists(int dd, int vars, int num_vars);
private static native int DD_ForAll(int dd, int vars, int num_vars);
@ -376,6 +381,46 @@ public class JDD
return new JDDNode(DD_SwapVariables(dd.ptr(), old_vars.array(), new_vars.array(), old_vars.n()));
}
// build x > y for variables x, y
// [ REFS: <result>, DEREFS: <none> ]
public static JDDNode VariablesGreaterThan(JDDVars x_vars, JDDVars y_vars)
{
return new JDDNode(DD_VariablesGreaterThan(x_vars.array(), y_vars.array(), x_vars.n()));
}
// build x >= y for variables x, y
// [ REFS: <result>, DEREFS: <none> ]
public static JDDNode VariablesGreaterThanEquals(JDDVars x_vars, JDDVars y_vars)
{
return new JDDNode(DD_VariablesGreaterThanEquals(x_vars.array(), y_vars.array(), x_vars.n()));
}
// build x < y for variables x, y
// [ REFS: <result>, DEREFS: <none> ]
public static JDDNode VariablesLessThan(JDDVars x_vars, JDDVars y_vars)
{
return new JDDNode(DD_VariablesLessThan(x_vars.array(), y_vars.array(), x_vars.n()));
}
// build x <= y for variables x, y
// [ REFS: <result>, DEREFS: <none> ]
public static JDDNode VariablesLessThanEquals(JDDVars x_vars, JDDVars y_vars)
{
return new JDDNode(DD_VariablesLessThanEquals(x_vars.array(), y_vars.array(), x_vars.n()));
}
// build x == y for variables x, y
// [ REFS: <result>, DEREFS: <none> ]
public static JDDNode VariablesEquals(JDDVars x_vars, JDDVars y_vars)
{
return new JDDNode(DD_VariablesEquals(x_vars.array(), y_vars.array(), x_vars.n()));
}
// wrapper methods for dd_abstr
// existential abstraction of vars from dd

Write Preview
Loading…
Cancel
Save