From fbf968e060bc79145ea64659a5e2ddb74b119cfb Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Wed, 29 Jul 2015 10:12:11 +0000 Subject: [PATCH] JDD: add PrintMinterms methods for debugging git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10453 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/jdd/JDD.java | 153 ++++++++++++++++++++++++++++++++++++++++- 1 file changed, 152 insertions(+), 1 deletion(-) diff --git a/prism/src/jdd/JDD.java b/prism/src/jdd/JDD.java index def08360..1423e905 100644 --- a/prism/src/jdd/JDD.java +++ b/prism/src/jdd/JDD.java @@ -30,6 +30,9 @@ package jdd; import java.util.*; +import prism.PrismException; +import prism.PrismLog; + public class JDD { // dd library functions @@ -1013,7 +1016,155 @@ public class JDD } return new JDDNode(DD_MatrixMultiply(dd1.ptr(), dd2.ptr(), vars.array(), vars.n(), method)); } - + + /** + * Print the minterms for a JDDNode (using the support of dd as variables). + *
+ * Positive variables are marked with 1, negatives with 0 and don't cares are marked with - + *
[ REFS: none, DEREFS: dd ] + * + * @param log the output log + * @param dd the MTBDD + */ + public static void PrintMinterms(PrismLog log, JDDNode dd) + { + PrintMinterms(log, dd, null); + } + + /** + * Print the minterms for a JDDNode (using the support of dd as variables). + *
+ * Positive variables are marked with 1, negatives with 0 and don't cares are marked with - + *
[ REFS: none, DEREFS: dd ] + * + * @param log the output log + * @param dd the MTBDD + * @param name an optional description to be printed ({@code null} for none) + */ + public static void PrintMinterms(PrismLog log, JDDNode dd, String description) + { + JDDNode csSupport = GetSupport(dd); + JDDVars vars = JDDVars.fromCubeSet(csSupport); + PrintMinterms(log, dd, vars, description); + vars.derefAll(); + } + + /** + * Print the minterms for a JDDNode over the variables {@code vars}. + *
+ * Positive variables are marked with 1, negatives with 0 and don't cares are marked with - + *
+ * {@code vars} has to be ordered with increasing variable indizes and + * has to contain all variables in the support of {@code dd}. + *
[ REFS: none, DEREFS: dd ] + * + * @param log the output log + * @param dd the MTBDD + * @param vars JDDVars of the relevant variables + * @param description an optional description to be printed ({@code null} for none) + * @throws IllegalArgumentException if {@code vars} does not fullfil the constraints + */ + public static void PrintMinterms(PrismLog log, JDDNode dd, JDDVars vars, String description) + { + try { + if (description != null) + log.println(description+":"); + log.print(" Variables: ("); + boolean first = true; + for (JDDNode var : vars) { + if (!first) log.print(","); + first = false; + log.print(var.getIndex()); + } + log.println(")"); + char[] minterm = new char[vars.n()]; + for (int i = 0; i< minterm.length; i++) { + minterm[i] = '-'; + } + PrintMintermsRec(log, dd, vars, 0, minterm); + } finally { + JDD.Deref(dd); + } + } + + /** + * Recursively print the minterms for a JDDNode over the variables {@code vars}. + *
+ * Positive variables are marked with 1, negatives with 0 and don't cares are marked with - + *
+ * {@code vars} has to be ordered with increasing variable indizes and + * has to contain all variables in the support of {@code dd}. + *
[ REFS: none, DEREFS: none ] + * + * @param log the output log + * @param dd the MTBDD + * @param vars JDDVars of the relevant variables + * @param cur_index the current index into {@code vars} + * @param minterm character array of length {@code vars.n()} storing the current (partial) minterm + * @throws IllegalArgumentException if {@code vars} does not fullfil the constraints + */ + private static void PrintMintermsRec(PrismLog log, JDDNode dd, JDDVars vars, int cur_index, char[] minterm) + { + if (dd.isConstant()) { + // base case: we are at the ZERO sink, don't print + if (dd.equals(JDD.ZERO)) + return; + + // print the current minterm buffer + log.print(" |"); + for (char c : minterm) { + log.print(c); + } + // ... and the constant value + log.println("| = " +dd.getValue()); + } else { + // Get the current variable index + int index = dd.getIndex(); + // As long as there are variables left in vars + while (cur_index < vars.n()) { + int var_index = vars.getVar(cur_index).getIndex(); + // We are at the level of the next var in vars + if (var_index == index) { + // Recurse for else + minterm[cur_index]='0'; + PrintMintermsRec(log, dd.getElse(), vars, cur_index+1, minterm); + // Recurse for then + minterm[cur_index]='1'; + PrintMintermsRec(log, dd.getThen(), vars, cur_index+1, minterm); + // ... and we are done + minterm[cur_index]='-'; + return; + } else if (var_index < index) { + // The next variable in vars is less then the current dd index + // -> don't care + minterm[cur_index]='-'; + // Go to next variable in vars + ++cur_index; + // ... and continue + continue; + } else { + // var_index > index + // Either the vars are not ordered correctly or + // the dd has relevant variables not included in vars + // To help with debugging, differentiate between the two cases... + for (JDDNode var : vars) { + if (var.getIndex() == index) { + // There is a var with the current index in vars, but + // not at the correct position + throw new IllegalArgumentException("PrintMinterms: vars array does not appear to be sorted correctly (DD index = "+index+", var index = "+var_index+")"); + } + } + // otherwise, the dd depends on a variable not in vars + throw new IllegalArgumentException("PrintMinterms: MTBDD depends on variable "+index+", not included in vars"); + } + } + if (vars.n() == 0) { + throw new IllegalArgumentException("PrintMinterms: MTBDD depends on variable "+index+", not included in vars"); + } + throw new UnsupportedOperationException("PrintMinterms: Implementation error"); + } + } + /** * prints out vector dd *
[ REFS: none, DEREFS: none ]