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

JDD: Switch to JDDNode ptrToNode(long ptr) as a single point for converting from a DD long pointer to a referenced JDDNode. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10471 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Joachim Klein 11 years ago
parent
32e6c16015
commit
379918beea
4 changed files with 84 additions and 74 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. 16
      prism/src/dv/DoubleVector.java
  2. 94
      prism/src/jdd/JDD.java
  3. 46
      prism/src/mtbdd/PrismMTBDD.java
  4. 2
      prism/src/odd/ODDUtils.java

16
prism/src/dv/DoubleVector.java
View File

@ -293,22 +293,22 @@ public class DoubleVector
switch (relOp) {
case GEQ:
sol = new JDDNode(
sol = JDD.ptrToNode(
DV_BDDGreaterThanEquals(v, bound, vars.array(), vars.n(), odd.ptr())
);
break;
case GT:
sol = new JDDNode(
sol = JDD.ptrToNode(
DV_BDDGreaterThan(v, bound, vars.array(), vars.n(), odd.ptr())
);
break;
case LEQ:
sol = new JDDNode(
sol = JDD.ptrToNode(
DV_BDDLessThanEquals(v, bound, vars.array(), vars.n(), odd.ptr())
);
break;
case LT:
sol = new JDDNode(
sol = JDD.ptrToNode(
DV_BDDLessThan(v, bound, vars.array(), vars.n(), odd.ptr())
);
break;
@ -331,7 +331,7 @@ public class DoubleVector
{
JDDNode sol;
sol = new JDDNode(
sol = JDD.ptrToNode(
DV_BDDInterval(v, lo, hi, vars.array(), vars.n(), odd.ptr())
);
@ -347,7 +347,7 @@ public class DoubleVector
{
JDDNode sol;
sol = new JDDNode(
sol = JDD.ptrToNode(
DV_BDDCloseValueAbs(v, value, epsilon, vars.array(), vars.n(), odd.ptr())
);
@ -363,7 +363,7 @@ public class DoubleVector
{
JDDNode sol;
sol = new JDDNode(
sol = JDD.ptrToNode(
DV_BDDCloseValueRel(v, value, epsilon, vars.array(), vars.n(), odd.ptr())
);
@ -379,7 +379,7 @@ public class DoubleVector
{
JDDNode sol;
sol = new JDDNode(
sol = JDD.ptrToNode(
DV_ConvertToMTBDD(v, vars.array(), vars.n(), odd.ptr())
);

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

@ -281,7 +281,7 @@ public class JDD
*/
public static JDDNode Create()
{
return new JDDNode(DD_Create());
return ptrToNode(DD_Create());
}
/**
@ -293,7 +293,7 @@ public class JDD
if (Double.isInfinite(value))
return value > 0 ? JDD.PlusInfinity() : JDD.MinusInfinity();
else
return new JDDNode(DD_Constant(value));
return ptrToNode(DD_Constant(value));
}
/**
@ -302,7 +302,7 @@ public class JDD
*/
public static JDDNode PlusInfinity()
{
return new JDDNode(DD_PlusInfinity());
return ptrToNode(DD_PlusInfinity());
}
/**
@ -311,7 +311,7 @@ public class JDD
*/
public static JDDNode MinusInfinity()
{
return new JDDNode(DD_MinusInfinity());
return ptrToNode(DD_MinusInfinity());
}
/**
@ -320,7 +320,7 @@ public class JDD
*/
public static JDDNode Var(int i)
{
return new JDDNode(DD_Var(i));
return ptrToNode(DD_Var(i));
}
/**
@ -331,7 +331,7 @@ public class JDD
{
if (DebugJDD.debugEnabled)
DebugJDD.decrement(dd);
return new JDDNode(DD_Not(dd.ptr()));
return ptrToNode(DD_Not(dd.ptr()));
}
/**
@ -344,7 +344,7 @@ public class JDD
DebugJDD.decrement(dd1);
DebugJDD.decrement(dd2);
}
return new JDDNode(DD_Or(dd1.ptr(), dd2.ptr()));
return ptrToNode(DD_Or(dd1.ptr(), dd2.ptr()));
}
/**
@ -358,7 +358,7 @@ public class JDD
DebugJDD.decrement(dd2);
}
return new JDDNode(DD_And(dd1.ptr(), dd2.ptr()));
return ptrToNode(DD_And(dd1.ptr(), dd2.ptr()));
}
/**
@ -371,7 +371,7 @@ public class JDD
DebugJDD.decrement(dd1);
DebugJDD.decrement(dd2);
}
return new JDDNode(DD_Xor(dd1.ptr(), dd2.ptr()));
return ptrToNode(DD_Xor(dd1.ptr(), dd2.ptr()));
}
/**
@ -384,7 +384,7 @@ public class JDD
DebugJDD.decrement(dd1);
DebugJDD.decrement(dd2);
}
return new JDDNode(DD_Implies(dd1.ptr(), dd2.ptr()));
return ptrToNode(DD_Implies(dd1.ptr(), dd2.ptr()));
}
/**
@ -397,7 +397,7 @@ public class JDD
DebugJDD.decrement(dd1);
DebugJDD.decrement(dd2);
}
return new JDDNode(DD_Apply(op, dd1.ptr(), dd2.ptr()));
return ptrToNode(DD_Apply(op, dd1.ptr(), dd2.ptr()));
}
/**
@ -408,7 +408,7 @@ public class JDD
{
if (DebugJDD.debugEnabled)
DebugJDD.decrement(dd);
return new JDDNode(DD_MonadicApply(op, dd.ptr()));
return ptrToNode(DD_MonadicApply(op, dd.ptr()));
}
/**
@ -421,7 +421,7 @@ public class JDD
DebugJDD.decrement(dd);
DebugJDD.decrement(cube);
}
return new JDDNode(DD_Restrict(dd.ptr(), cube.ptr()));
return ptrToNode(DD_Restrict(dd.ptr(), cube.ptr()));
}
/**
@ -435,7 +435,7 @@ public class JDD
DebugJDD.decrement(dd2);
DebugJDD.decrement(dd3);
}
return new JDDNode(DD_ITE(dd1.ptr(), dd2.ptr(), dd3.ptr()));
return ptrToNode(DD_ITE(dd1.ptr(), dd2.ptr(), dd3.ptr()));
}
/**
@ -482,7 +482,7 @@ public class JDD
{
if (DebugJDD.debugEnabled)
DebugJDD.decrement(dd);
return new JDDNode(DD_PermuteVariables(dd.ptr(), old_vars.array(), new_vars.array(), old_vars.n()));
return ptrToNode(DD_PermuteVariables(dd.ptr(), old_vars.array(), new_vars.array(), old_vars.n()));
}
/**
@ -493,7 +493,7 @@ public class JDD
{
if (DebugJDD.debugEnabled)
DebugJDD.decrement(dd);
return new JDDNode(DD_SwapVariables(dd.ptr(), old_vars.array(), new_vars.array(), old_vars.n()));
return ptrToNode(DD_SwapVariables(dd.ptr(), old_vars.array(), new_vars.array(), old_vars.n()));
}
/**
@ -502,7 +502,7 @@ public class JDD
*/
public static JDDNode VariablesGreaterThan(JDDVars x_vars, JDDVars y_vars)
{
return new JDDNode(DD_VariablesGreaterThan(x_vars.array(), y_vars.array(), x_vars.n()));
return ptrToNode(DD_VariablesGreaterThan(x_vars.array(), y_vars.array(), x_vars.n()));
}
/**
@ -511,7 +511,7 @@ public class JDD
*/
public static JDDNode VariablesGreaterThanEquals(JDDVars x_vars, JDDVars y_vars)
{
return new JDDNode(DD_VariablesGreaterThanEquals(x_vars.array(), y_vars.array(), x_vars.n()));
return ptrToNode(DD_VariablesGreaterThanEquals(x_vars.array(), y_vars.array(), x_vars.n()));
}
/**
@ -520,7 +520,7 @@ public class JDD
*/
public static JDDNode VariablesLessThan(JDDVars x_vars, JDDVars y_vars)
{
return new JDDNode(DD_VariablesLessThan(x_vars.array(), y_vars.array(), x_vars.n()));
return ptrToNode(DD_VariablesLessThan(x_vars.array(), y_vars.array(), x_vars.n()));
}
/**
@ -529,7 +529,7 @@ public class JDD
*/
public static JDDNode VariablesLessThanEquals(JDDVars x_vars, JDDVars y_vars)
{
return new JDDNode(DD_VariablesLessThanEquals(x_vars.array(), y_vars.array(), x_vars.n()));
return ptrToNode(DD_VariablesLessThanEquals(x_vars.array(), y_vars.array(), x_vars.n()));
}
/**
@ -538,7 +538,7 @@ public class JDD
*/
public static JDDNode VariablesEquals(JDDVars x_vars, JDDVars y_vars)
{
return new JDDNode(DD_VariablesEquals(x_vars.array(), y_vars.array(), x_vars.n()));
return ptrToNode(DD_VariablesEquals(x_vars.array(), y_vars.array(), x_vars.n()));
}
// wrapper methods for dd_abstr
@ -551,7 +551,7 @@ public class JDD
{
if (DebugJDD.debugEnabled)
DebugJDD.decrement(dd);
return new JDDNode(DD_ThereExists(dd.ptr(), vars.array(), vars.n()));
return ptrToNode(DD_ThereExists(dd.ptr(), vars.array(), vars.n()));
}
/**
@ -562,7 +562,7 @@ public class JDD
{
if (DebugJDD.debugEnabled)
DebugJDD.decrement(dd);
return new JDDNode(DD_ForAll(dd.ptr(), vars.array(), vars.n()));
return ptrToNode(DD_ForAll(dd.ptr(), vars.array(), vars.n()));
}
/**
@ -573,7 +573,7 @@ public class JDD
{
if (DebugJDD.debugEnabled)
DebugJDD.decrement(dd);
return new JDDNode(DD_SumAbstract(dd.ptr(), vars.array(), vars.n()));
return ptrToNode(DD_SumAbstract(dd.ptr(), vars.array(), vars.n()));
}
/**
@ -584,7 +584,7 @@ public class JDD
{
if (DebugJDD.debugEnabled)
DebugJDD.decrement(dd);
return new JDDNode(DD_ProductAbstract(dd.ptr(), vars.array(), vars.n()));
return ptrToNode(DD_ProductAbstract(dd.ptr(), vars.array(), vars.n()));
}
/**
@ -595,7 +595,7 @@ public class JDD
{
if (DebugJDD.debugEnabled)
DebugJDD.decrement(dd);
return new JDDNode(DD_MinAbstract(dd.ptr(), vars.array(), vars.n()));
return ptrToNode(DD_MinAbstract(dd.ptr(), vars.array(), vars.n()));
}
/**
@ -606,7 +606,7 @@ public class JDD
{
if (DebugJDD.debugEnabled)
DebugJDD.decrement(dd);
return new JDDNode(DD_MaxAbstract(dd.ptr(), vars.array(), vars.n()));
return ptrToNode(DD_MaxAbstract(dd.ptr(), vars.array(), vars.n()));
}
// wrapper methods for dd_term
@ -619,7 +619,7 @@ public class JDD
{
if (DebugJDD.debugEnabled)
DebugJDD.decrement(dd);
return new JDDNode(DD_GreaterThan(dd.ptr(), threshold));
return ptrToNode(DD_GreaterThan(dd.ptr(), threshold));
}
/**
@ -630,7 +630,7 @@ public class JDD
{
if (DebugJDD.debugEnabled)
DebugJDD.decrement(dd);
return new JDDNode(DD_GreaterThanEquals(dd.ptr(), threshold));
return ptrToNode(DD_GreaterThanEquals(dd.ptr(), threshold));
}
/**
@ -641,7 +641,7 @@ public class JDD
{
if (DebugJDD.debugEnabled)
DebugJDD.decrement(dd);
return new JDDNode(DD_LessThan(dd.ptr(), threshold));
return ptrToNode(DD_LessThan(dd.ptr(), threshold));
}
/**
@ -652,7 +652,7 @@ public class JDD
{
if (DebugJDD.debugEnabled)
DebugJDD.decrement(dd);
return new JDDNode(DD_LessThanEquals(dd.ptr(), threshold));
return ptrToNode(DD_LessThanEquals(dd.ptr(), threshold));
}
/**
@ -663,7 +663,7 @@ public class JDD
{
if (DebugJDD.debugEnabled)
DebugJDD.decrement(dd);
return new JDDNode(DD_Equals(dd.ptr(), value));
return ptrToNode(DD_Equals(dd.ptr(), value));
}
/**
@ -674,7 +674,7 @@ public class JDD
{
if (DebugJDD.debugEnabled)
DebugJDD.decrement(dd);
return new JDDNode(DD_Interval(dd.ptr(), lower, upper));
return ptrToNode(DD_Interval(dd.ptr(), lower, upper));
}
/**
@ -685,7 +685,7 @@ public class JDD
{
if (DebugJDD.debugEnabled)
DebugJDD.decrement(dd);
return new JDDNode(DD_RoundOff(dd.ptr(), places));
return ptrToNode(DD_RoundOff(dd.ptr(), places));
}
/**
@ -723,7 +723,7 @@ public class JDD
{
if (DebugJDD.debugEnabled)
DebugJDD.decrement(dd);
return new JDDNode(DD_RestrictToFirst(dd.ptr(), vars.array(), vars.n()));
return ptrToNode(DD_RestrictToFirst(dd.ptr(), vars.array(), vars.n()));
}
// wrapper methods for dd_info
@ -861,7 +861,7 @@ public class JDD
*/
public static JDDNode GetSupport(JDDNode dd)
{
return new JDDNode(DD_GetSupport(dd.ptr()));
return ptrToNode(DD_GetSupport(dd.ptr()));
}
/**
@ -949,7 +949,7 @@ public class JDD
{
if (DebugJDD.debugEnabled)
DebugJDD.decrement(dd);
return new JDDNode(DD_SetVectorElement(dd.ptr(), vars.array(), vars.n(), index, value));
return ptrToNode(DD_SetVectorElement(dd.ptr(), vars.array(), vars.n(), index, value));
}
/**
@ -960,7 +960,7 @@ public class JDD
{
if (DebugJDD.debugEnabled)
DebugJDD.decrement(dd);
return new JDDNode(DD_SetMatrixElement(dd.ptr(), rvars.array(), rvars.n(), cvars.array(), cvars.n(), rindex, cindex, value));
return ptrToNode(DD_SetMatrixElement(dd.ptr(), rvars.array(), rvars.n(), cvars.array(), cvars.n(), rindex, cindex, value));
}
/**
@ -971,7 +971,7 @@ public class JDD
{
if (DebugJDD.debugEnabled)
DebugJDD.decrement(dd);
return new JDDNode(DD_Set3DMatrixElement(dd.ptr(), rvars.array(), rvars.n(), cvars.array(), cvars.n(), lvars.array(), lvars.n(), rindex, cindex, lindex, value));
return ptrToNode(DD_Set3DMatrixElement(dd.ptr(), rvars.array(), rvars.n(), cvars.array(), cvars.n(), lvars.array(), lvars.n(), rindex, cindex, lindex, value));
}
/**
@ -989,7 +989,7 @@ public class JDD
*/
public static JDDNode Identity(JDDVars rvars, JDDVars cvars)
{
return new JDDNode(DD_Identity(rvars.array(), cvars.array(), rvars.n()));
return ptrToNode(DD_Identity(rvars.array(), cvars.array(), rvars.n()));
}
/**
@ -1000,7 +1000,7 @@ public class JDD
{
if (DebugJDD.debugEnabled)
DebugJDD.decrement(dd);
return new JDDNode(DD_Transpose(dd.ptr(), rvars.array(), cvars.array(), rvars.n()));
return ptrToNode(DD_Transpose(dd.ptr(), rvars.array(), cvars.array(), rvars.n()));
}
/**
@ -1013,7 +1013,7 @@ public class JDD
DebugJDD.decrement(dd1);
DebugJDD.decrement(dd2);
}
return new JDDNode(DD_MatrixMultiply(dd1.ptr(), dd2.ptr(), vars.array(), vars.n(), method));
return ptrToNode(DD_MatrixMultiply(dd1.ptr(), dd2.ptr(), vars.array(), vars.n(), method));
}
/**
@ -1333,6 +1333,16 @@ public class JDD
{
DD_ExportMatrixToSpyFile(dd.ptr(), rvars.array(), rvars.n(), cvars.array(), cvars.n(), depth, filename);
}
/**
* Convert a (referenced) ptr returned from Cudd into a JDDNode.
* <br>[ REFS: <i>none</i> ]
*/
public static JDDNode ptrToNode(long ptr)
{
return new JDDNode(ptr);
}
}
//------------------------------------------------------------------------------

46
prism/src/mtbdd/PrismMTBDD.java
View File

@ -139,7 +139,7 @@ public class PrismMTBDD
{
long ptr = PM_Reachability(trans01.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), start.ptr());
//if (ptr == 0) throw new PrismException(getErrorMessage());
return new JDDNode(ptr);
return JDD.ptrToNode(ptr);
}
// pctl until probability 1 precomputation (probabilistic/dtmc)
@ -148,7 +148,7 @@ public class PrismMTBDD
{
long ptr = PM_Prob1(trans01.ptr(), reach.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), b1.ptr(), b2.ptr(), no.ptr());
//if (ptr == 0) throw new PrismException(getErrorMessage());
return new JDDNode(ptr);
return JDD.ptrToNode(ptr);
}
// pctl until probability 0 precomputation (probabilistic/dtmc)
@ -157,7 +157,7 @@ public class PrismMTBDD
{
long ptr = PM_Prob0(trans01.ptr(), reach.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), b1.ptr(), b2.ptr());
//if (ptr == 0) throw new PrismException(getErrorMessage());
return new JDDNode(ptr);
return JDD.ptrToNode(ptr);
}
// pctl until probability 1 precomputation - there exists (nondeterministic/mdp)
@ -166,7 +166,7 @@ public class PrismMTBDD
{
long ptr = PM_Prob1E(trans01.ptr(), reach.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nd.array(), nd.n(), b1.ptr(), b2.ptr(), no.ptr());
//if (ptr == 0) throw new PrismException(getErrorMessage());
return new JDDNode(ptr);
return JDD.ptrToNode(ptr);
}
// pctl until probability 1 precomputation - for all (nondeterministic/mdp)
@ -175,7 +175,7 @@ public class PrismMTBDD
{
long ptr = PM_Prob1A(trans01.ptr(), reach.ptr(), nondetMask.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nd.array(), nd.n(), no.ptr(), b2.ptr());
//if (ptr == 0) throw new PrismException(getErrorMessage());
return new JDDNode(ptr);
return JDD.ptrToNode(ptr);
}
// pctl until probability 0 precomputation - there exists (nondeterministic/mdp)
@ -184,7 +184,7 @@ public class PrismMTBDD
{
long ptr = PM_Prob0E(trans01.ptr(), reach.ptr(), nondetMask.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nd.array(), nd.n(), b1.ptr(), b2.ptr());
//if (ptr == 0) throw new PrismException(getErrorMessage());
return new JDDNode(ptr);
return JDD.ptrToNode(ptr);
}
// pctl until probability 0 precomputation - for all (nondeterministic/mdp)
@ -193,7 +193,7 @@ public class PrismMTBDD
{
long ptr = PM_Prob0A(trans01.ptr(), reach.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nd.array(), nd.n(), b1.ptr(), b2.ptr());
//if (ptr == 0) throw new PrismException(getErrorMessage());
return new JDDNode(ptr);
return JDD.ptrToNode(ptr);
}
//------------------------------------------------------------------------------
@ -206,7 +206,7 @@ public class PrismMTBDD
{
long ptr = PM_ProbBoundedUntil(trans.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), yes.ptr(), maybe.ptr(), bound);
if (ptr == 0) throw new PrismException(getErrorMessage());
return new JDDNode(ptr);
return JDD.ptrToNode(ptr);
}
// pctl until (probabilistic/dtmc)
@ -215,7 +215,7 @@ public class PrismMTBDD
{
long ptr = PM_ProbUntil(trans.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), yes.ptr(), maybe.ptr());
if (ptr == 0) throw new PrismException(getErrorMessage());
return new JDDNode(ptr);
return JDD.ptrToNode(ptr);
}
// pctl cumulative reward (probabilistic/dtmc)
@ -224,7 +224,7 @@ public class PrismMTBDD
{
long ptr = PM_ProbCumulReward(trans.ptr(), sr.ptr(), trr.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), bound);
if (ptr == 0) throw new PrismException(getErrorMessage());
return new JDDNode(ptr);
return JDD.ptrToNode(ptr);
}
// pctl inst reward (probabilistic/dtmc)
@ -233,7 +233,7 @@ public class PrismMTBDD
{
long ptr = PM_ProbInstReward(trans.ptr(), sr.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), time);
if (ptr == 0) throw new PrismException(getErrorMessage());
return new JDDNode(ptr);
return JDD.ptrToNode(ptr);
}
// pctl reach reward (probabilistic/dtmc)
@ -242,7 +242,7 @@ public class PrismMTBDD
{
long ptr = PM_ProbReachReward(trans.ptr(), sr.ptr(), trr.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), goal.ptr(), inf.ptr(), maybe.ptr());
if (ptr == 0) throw new PrismException(getErrorMessage());
return new JDDNode(ptr);
return JDD.ptrToNode(ptr);
}
// transient (probabilistic/dtmc)
@ -251,7 +251,7 @@ public class PrismMTBDD
{
long ptr = PM_ProbTransient(trans.ptr(), odd.ptr(), init.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), time);
if (ptr == 0) throw new PrismException(getErrorMessage());
return new JDDNode(ptr);
return JDD.ptrToNode(ptr);
}
//------------------------------------------------------------------------------
@ -264,7 +264,7 @@ public class PrismMTBDD
{
long ptr = PM_NondetBoundedUntil(trans.ptr(), odd.ptr(), nondetMask.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), yes.ptr(), maybe.ptr(), bound, minmax);
if (ptr == 0) throw new PrismException(getErrorMessage());
return new JDDNode(ptr);
return JDD.ptrToNode(ptr);
}
// pctl until (nondeterministic/mdp)
@ -273,7 +273,7 @@ public class PrismMTBDD
{
long ptr = PM_NondetUntil(trans.ptr(), odd.ptr(), nondetMask.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 JDDNode(ptr);
return JDD.ptrToNode(ptr);
}
// pctl inst reward (nondeterministic/mdp)
@ -282,7 +282,7 @@ public class PrismMTBDD
{
long ptr = PM_NondetInstReward(trans.ptr(), sr.ptr(), odd.ptr(), nondetMask.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), time, minmax, init.ptr());
if (ptr == 0) throw new PrismException(getErrorMessage());
return new JDDNode(ptr);
return JDD.ptrToNode(ptr);
}
// pctl reach reward (nondeterministic/mdp)
@ -291,7 +291,7 @@ public class PrismMTBDD
{
long ptr = PM_NondetReachReward(trans.ptr(), sr.ptr(), trr.ptr(), odd.ptr(), nondetMask.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), goal.ptr(), inf.ptr(), maybe.ptr(), minmax);
if (ptr == 0) throw new PrismException(getErrorMessage());
return new JDDNode(ptr);
return JDD.ptrToNode(ptr);
}
//------------------------------------------------------------------------------
@ -305,7 +305,7 @@ public class PrismMTBDD
long mult = (multProbs == null) ? 0 : multProbs.ptr();
long ptr = PM_StochBoundedUntil(trans.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), yes.ptr(), maybe.ptr(), time, mult);
if (ptr == 0) throw new PrismException(getErrorMessage());
return new JDDNode(ptr);
return JDD.ptrToNode(ptr);
}
// csl cumulative reward (stochastic/ctmc)
@ -314,7 +314,7 @@ public class PrismMTBDD
{
long ptr = PM_StochCumulReward(trans.ptr(), sr.ptr(), trr.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), time);
if (ptr == 0) throw new PrismException(getErrorMessage());
return new JDDNode(ptr);
return JDD.ptrToNode(ptr);
}
// steady state (stochastic/ctmc)
@ -323,7 +323,7 @@ public class PrismMTBDD
{
long ptr = PM_StochSteadyState(trans.ptr(), odd.ptr(), init.ptr(), rows.array(), rows.n(), cols.array(), cols.n());
if (ptr == 0) throw new PrismException(getErrorMessage());
return new JDDNode(ptr);
return JDD.ptrToNode(ptr);
}
// transient (stochastic/ctmc)
@ -332,7 +332,7 @@ public class PrismMTBDD
{
long ptr = PM_StochTransient(trans.ptr(), odd.ptr(), init.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), time);
if (ptr == 0) throw new PrismException(getErrorMessage());
return new JDDNode(ptr);
return JDD.ptrToNode(ptr);
}
//------------------------------------------------------------------------------
@ -382,7 +382,7 @@ public class PrismMTBDD
{
long ptr = PM_Power(odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), a.ptr(), b.ptr(), init.ptr(), transpose);
if (ptr == 0) throw new PrismException(getErrorMessage());
return new JDDNode(ptr);
return JDD.ptrToNode(ptr);
}
// jor method
@ -391,7 +391,7 @@ public class PrismMTBDD
{
long ptr = PM_JOR(odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), a.ptr(), b.ptr(), init.ptr(), transpose, omega);
if (ptr == 0) throw new PrismException(getErrorMessage());
return new JDDNode(ptr);
return JDD.ptrToNode(ptr);
}
//------------------------------------------------------------------------------

2
prism/src/odd/ODDUtils.java
View File

@ -97,7 +97,7 @@ public class ODDUtils
*/
public static JDDNode SingleIndexToDD(int i, ODDNode odd, JDDVars vars)
{
return new JDDNode(ODD_SingleIndexToDD(i, odd.ptr(), vars.array(), vars.n()));
return JDD.ptrToNode(ODD_SingleIndexToDD(i, odd.ptr(), vars.array(), vars.n()));
}
//------------------------------------------------------------------------------

Write Preview
Loading…
Cancel
Save