Browse Source

PrismSparse.exportMDP: sanity check

tud-infrastructure-2018-10-12
Joachim Klein 7 years ago
parent
commit
4d672db58b
  1. 4
      prism/src/sparse/PrismSparse.java

4
prism/src/sparse/PrismSparse.java

@ -32,6 +32,7 @@ import java.util.List;
import jdd.JDD;
import jdd.JDDNode;
import jdd.JDDVars;
import jdd.SanityJDD;
import odd.ODDNode;
import prism.NativeIntArray;
import prism.OpsAndBoundsList;
@ -600,6 +601,9 @@ public class PrismSparse
public static void ExportMDP(JDDNode mdp, JDDNode transActions, List<String> synchs, String name, JDDVars rows, JDDVars cols, JDDVars nondet, ODDNode odd, int exportType, String filename) throws FileNotFoundException, PrismException
{
checkNumStates(odd);
if (SanityJDD.enabled) {
SanityJDD.checkIsDDOverVars(mdp, rows, cols, nondet);
}
int res = PS_ExportMDP(mdp.ptr(), (transActions == null) ? 0 : transActions.ptr(), synchs, name, rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), odd.ptr(), exportType, filename);
if (res == -1) {

Loading…
Cancel
Save