From fbbb87c109c3ee510f4d0de15b95f82651ecd03d Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 12 Oct 2018 14:25:25 +0200 Subject: [PATCH] imported patch printall-symbolic.patch --- prism/src/prism/StateValues.java | 2 +- prism/src/prism/StateValuesMTBDD.java | 154 +++++++++++++++++++++----- 2 files changed, 130 insertions(+), 26 deletions(-) diff --git a/prism/src/prism/StateValues.java b/prism/src/prism/StateValues.java index d334e4b2..d441fe56 100644 --- a/prism/src/prism/StateValues.java +++ b/prism/src/prism/StateValues.java @@ -251,7 +251,7 @@ public interface StateValues extends StateVector void printFiltered(PrismLog log, JDDNode filter) throws PrismException; /** - * Print part of a vector to a log/file (non-zero entries only). + * Print part of a vector to a log/file. *
[ DEREFS: none ] * @param log The log * @param filter A BDD specifying which states to print for. diff --git a/prism/src/prism/StateValuesMTBDD.java b/prism/src/prism/StateValuesMTBDD.java index 65c58488..7504fce6 100644 --- a/prism/src/prism/StateValuesMTBDD.java +++ b/prism/src/prism/StateValuesMTBDD.java @@ -621,29 +621,39 @@ public class StateValuesMTBDD implements StateValues @Override public void print(PrismLog log, boolean printSparse, boolean printMatlab, boolean printStates, boolean printIndices) throws PrismException { - // Because non-sparse output from MTBDD requires a bit more effort... - if (printSparse) print(log); - else throw new PrismException("Not supported"); - // Note we also ignore printMatlab/printStates/printIndices due to laziness + // Note we ignore printMatlab/printStates/printIndices due to laziness + if (printSparse) { + print(log); + } else { + printFiltered(log, model.getReach(), printSparse, printMatlab, printStates); + } + } /** - * Recursive part of print method. - * - * (NB: this would be very easy - i.e. not even - * any recursion - if we didn't want to print - * out the values of the module variables as well - * which requires traversal of the odd as well - * as the vector) - * (NB2: traversal of vector/odd is still quite simple; - * tricky bit is keeping track of variable values - * throughout traversal - we want to be efficient - * and not compute the values from scratch each - * time, but we also want to avoid passing arrays - * into the recursive method) + * Recursive part of print method (non-zero entries only). + * + * @param dd the current node in the DD + * @param level the current variable level + * @param o the current node in the ODD + * @param n the current state index */ private void printRec(JDDNode dd, int level, ODDNode o, long n) { + /* + * (NB: this would be very easy - i.e. not even + * any recursion - if we didn't want to print + * out the values of the module variables as well + * which requires traversal of the odd as well + * as the vector) + * (NB2: traversal of vector/odd is still quite simple; + * tricky bit is keeping track of variable values + * throughout traversal - we want to be efficient + * and not compute the values from scratch each + * time, but we also want to avoid passing arrays + * into the recursive method) + */ + int i, j; JDDNode e, t; @@ -691,19 +701,111 @@ public class StateValuesMTBDD implements StateValues varValues[currentVar] -= (1 << (varSizes[currentVar]-1-currentVarLevel)); } + /** + * Recursive part of print method (all elements, + * including where the value is zero). + * + * @param ddFilter the states for which values should be printed + * @param ddValue the values for the states (has to be zero for all states not in ddFilter) + * @param level the current variable level + * @param o the current node in the ODD + * @param n the current state index + */ + private void printRecNonSparse(JDDNode ddFilter, JDDNode ddValue, int level, ODDNode o, long n) + { + /* + * (NB: this would be very easy - i.e. not even + * any recursion - if we didn't want to print + * out the values of the module variables as well + * which requires traversal of the odd as well + * as the vector) + * (NB2: traversal of vector/odd is still quite simple; + * tricky bit is keeping track of variable values + * throughout traversal - we want to be efficient + * and not compute the values from scratch each + * time, but we also want to avoid passing arrays + * into the recursive method) + */ + + int i, j; + JDDNode eFilter, tFilter, eValue, tValue; + + // ddFilter is zero - bottom out of recursion + if (ddFilter.equals(JDD.ZERO)) return; + + // base case - at bottom (nonzero terminal) + if (level == numVars) { + + outputLog.print(n + ":("); + j = varList.getNumVars(); + for (i = 0; i < j; i++) { + // integer variable + if (varList.getType(i) instanceof TypeInt) { + outputLog.print(varValues[i]+varList.getLow(i)); + } + // boolean variable + else { + outputLog.print(varValues[i] == 1); + } + if (i < j-1) outputLog.print(","); + } + outputLog.print(")=" + ddValue.getValue()); + outputLog.println(); + return; + } + + // select 'else' and 'then' branches ( filter dd ) + if (ddFilter.getIndex() > vars.getVarIndex(level)) { + eFilter = tFilter = ddFilter; + } else { + eFilter = ddFilter.getElse(); + tFilter = ddFilter.getThen(); + } + + // select 'else' and 'then' branches ( value dd ) + if (ddValue.getIndex() > vars.getVarIndex(level)) { + eValue = tValue = ddValue; + } else { + eValue = ddValue.getElse(); + tValue = ddValue.getThen(); + } + + // then recurse... + currentVarLevel++; if (currentVarLevel == varSizes[currentVar]) { currentVar++; currentVarLevel=0; } + printRecNonSparse(eFilter, eValue, level+1, o.getElse(), n); + currentVarLevel--; if (currentVarLevel == -1) { currentVar--; currentVarLevel=varSizes[currentVar]-1; } + varValues[currentVar] += (1 << (varSizes[currentVar]-1-currentVarLevel)); + currentVarLevel++; if (currentVarLevel == varSizes[currentVar]) { currentVar++; currentVarLevel=0; } + printRecNonSparse(tFilter, tValue, level+1, o.getThen(), n+o.getEOff()); + currentVarLevel--; if (currentVarLevel == -1) { currentVar--; currentVarLevel=varSizes[currentVar]-1; } + varValues[currentVar] -= (1 << (varSizes[currentVar]-1-currentVarLevel)); + } + @Override public void printFiltered(PrismLog log, JDDNode filter) throws PrismException + { + printFiltered(log, filter, true); + } + + /** + * Print part of a vector to a log/file. + *
[ DEREFS: none ] + * @param log The log + * @param filter A BDD specifying which states to print for. + * @param printSparse Print non-zero elements only? + */ + public void printFiltered(PrismLog log, JDDNode filter, boolean printSparse) throws PrismException { int i; JDDNode tmp; - + // filter out JDD.Ref(values); JDD.Ref(filter); tmp = JDD.Apply(JDD.TIMES, values, filter); - + // check if all zero - if (tmp.equals(JDD.ZERO)) { + if (printSparse && tmp.equals(JDD.ZERO)) { JDD.Deref(tmp); log.println("(all zero)"); return; @@ -716,7 +818,11 @@ public class StateValuesMTBDD implements StateValues } currentVar = 0; currentVarLevel = 0; - printRec(tmp, 0, odd, 0); + if (printSparse) { + printRec(tmp, 0, odd, 0); + } else { + printRecNonSparse(filter, tmp, 0, odd, 0); + } //log.println(); JDD.Deref(tmp); } @@ -724,10 +830,8 @@ public class StateValuesMTBDD implements StateValues @Override public void printFiltered(PrismLog log, JDDNode filter, boolean printSparse, boolean printMatlab, boolean printStates) throws PrismException { - // Because non-sparse output from MTBDD requires a bit more effort... - if (printSparse) printFiltered(log, filter); - else throw new PrismException("Not supported"); - // Note we also ignore printMatlab/printStates due to laziness + // Note we ignore printMatlab/printStates due to laziness + printFiltered(log, filter, printSparse); } /**