diff --git a/prism-tests/functionality/export/vector/exportvector.prism.args b/prism-tests/functionality/export/vector/exportvector.prism.args index d885285b..031d5fa5 100644 --- a/prism-tests/functionality/export/vector/exportvector.prism.args +++ b/prism-tests/functionality/export/vector/exportvector.prism.args @@ -1,4 +1,4 @@ -ex -#-m +-m -s -h diff --git a/prism/src/prism/StateAndValueConsumer.java b/prism/src/prism/StateAndValueConsumer.java new file mode 100644 index 00000000..8107ce78 --- /dev/null +++ b/prism/src/prism/StateAndValueConsumer.java @@ -0,0 +1,48 @@ +//============================================================================== +// +// Copyright (c) 2018- +// Authors: +// * Joachim Klein (TU Dresden) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package prism; + +/** + * Functional interface for a consumer of (state, value) pairs, + * used in iteration over a StateValues vector, e.g., printing. + */ +@FunctionalInterface +public interface StateAndValueConsumer +{ + + /** + * Accept a state/value pair. + *
+ * The values of the state variables are provided as integers, + * with boolean values mapped to 0 and 1, respectively. + * @param varValues an integer array with the state variable values + * @param value the value for this state + * @param stateIndex the state index (-1 indicates that no index information is available) + */ + void accept(int[] varValues, double value, long stateIndex); + +} diff --git a/prism/src/prism/StateAndValuePrinter.java b/prism/src/prism/StateAndValuePrinter.java new file mode 100644 index 00000000..95443a08 --- /dev/null +++ b/prism/src/prism/StateAndValuePrinter.java @@ -0,0 +1,128 @@ +//============================================================================== +// +// Copyright (c) 2018- +// Authors: +// * Joachim Klein (TU Dresden) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package prism; + +import parser.VarList; +import parser.type.TypeInt; + +/** + * StateValueConsumer that formats the state/value pairs + * and prints them to a PrismLog. + */ +class StateAndValuePrinter implements StateAndValueConsumer +{ + /** The log for output */ + private PrismLog outputLog; + /** The VarList (for the type information on the variables) */ + private VarList varList; + + /** Flag: printSparse (only non-zero values) */ + boolean printSparse = true; + /** Flag: printMatlab */ + boolean printMatlab = false; + /** Flag: printStates (variable values on the model) */ + boolean printStates = true; + /** Flag: printIndizes (indizes for the states) */ + boolean printIndices = true; + + /** Flag: Did we print at least one line? */ + private boolean hadOutput = false; + + /** + * Constructor. + * @param outputLog The log for output + * @param varList The VarList (for the type information) + * @param printSparse Print only non-zero values? + * @param printMatlab Print in Matlab format? + * @param printStates Print the state variable values? + * @param printIndices Print the state indices? + */ + public StateAndValuePrinter(PrismLog outputLog, VarList varList, boolean printSparse, boolean printMatlab, boolean printStates, boolean printIndices) + { + this.outputLog = outputLog; + this.varList = varList; + + this.printSparse = printSparse; + this.printMatlab = printMatlab; + this.printStates = printStates; + this.printIndices = printIndices; + } + + @Override + public void accept(int[] varValues, double value, long stateIndex) + { + if (printSparse && value == 0) { + // skip zeroes + return; + } + + hadOutput = true; + + // Matlab + if (printMatlab) { + if (printSparse) { + outputLog.println("v(" + (stateIndex + 1) + ")=" + value + ";"); + } else { + outputLog.println(value); + } + return; + } + + // PRISM format + if (printIndices) { + outputLog.print(stateIndex + ":"); + } + if (printStates) { + outputLog.print("("); + int n = varList.getNumVars(); + for (int i = 0; i < n; i++) { + if (i > 0) + outputLog.print(","); + + // integer variable + if (varList.getType(i) instanceof TypeInt) { + outputLog.print(varValues[i]); + } + // boolean variable + else { + outputLog.print(varValues[i] == 1); + } + } + outputLog.print(")"); + } + if (printIndices || printStates) + outputLog.print("="); + outputLog.println(value); + } + + /** Return true if we printed at least one state/value pair. */ + public boolean hadOutput() + { + return hadOutput; + } + +} diff --git a/prism/src/prism/StateValues.java b/prism/src/prism/StateValues.java index aba84ffb..ba105f89 100644 --- a/prism/src/prism/StateValues.java +++ b/prism/src/prism/StateValues.java @@ -221,7 +221,10 @@ public interface StateValues extends StateVector /** * Print vector to a log/file (non-zero entries only) */ - void print(PrismLog log) throws PrismException; + default void print(PrismLog log) throws PrismException + { + print(log, true, false, true, true); + } /** * Print vector to a log/file. @@ -230,7 +233,10 @@ public interface StateValues extends StateVector * @param printMatlab Print in Matlab format? * @param printStates Print states (variable values) for each element? */ - void print(PrismLog log, boolean printSparse, boolean printMatlab, boolean printStates) throws PrismException; + default void print(PrismLog log, boolean printSparse, boolean printMatlab, boolean printStates) throws PrismException + { + print(log, printSparse, printMatlab, printStates, true); + } /** * Print vector to a log/file. @@ -248,7 +254,10 @@ public interface StateValues extends StateVector * @param log The log * @param filter A BDD specifying which states to print for. */ - void printFiltered(PrismLog log, JDDNode filter) throws PrismException; + default void printFiltered(PrismLog log, JDDNode filter) throws PrismException + { + printFiltered(log, filter, true, false, true); + } /** * Print part of a vector to a log/file (non-zero entries only). @@ -259,7 +268,39 @@ public interface StateValues extends StateVector * @param printMatlab Print in Matlab format? * @param printStates Print states (variable values) for each element? */ - void printFiltered(PrismLog log, JDDNode filter, boolean printSparse, boolean printMatlab, boolean printStates) throws PrismException; + default void printFiltered(PrismLog log, JDDNode filter, boolean printSparse, boolean printMatlab, boolean printStates) throws PrismException + { + printFiltered(log, filter, printSparse, printMatlab, printStates, true); + } + + /** + * Print part of a vector to a log/file (non-zero entries only). + *
[ DEREFS: none ] + * @param log The log + * @param filter A BDD specifying which states to print for. + * @param printSparse Print non-zero elements only? + * @param printMatlab Print in Matlab format? + * @param printStates Print states (variable values) for each element? + * @param printIndices Print state indices for each element? + */ + void printFiltered(PrismLog log, JDDNode filter, boolean printSparse, boolean printMatlab, boolean printStates, boolean printIndices) throws PrismException; + + /** + * Iterate over all state/value pairs + * and call {@code consumer.accept()} for each. + * @param consumer the consumer + * @param sparse only call accept for non-zero values + */ + void iterate(StateAndValueConsumer consumer, boolean sparse); + + /** + * Iterate over all state/value pairs + * where the state is included in the filter DD and + * call {@code consumer.accept()} for each. + * @param consumer the consumer + * @param sparse only call accept for non-zero values + */ + void iterateFiltered(JDDNode filter, StateAndValueConsumer consumer, boolean sparse); /** * Make a (deep) copy of this vector diff --git a/prism/src/prism/StateValuesDV.java b/prism/src/prism/StateValuesDV.java index 80e7dc8f..c856a233 100644 --- a/prism/src/prism/StateValuesDV.java +++ b/prism/src/prism/StateValuesDV.java @@ -33,7 +33,6 @@ import jdd.*; import odd.*; import parser.VarList; import parser.ast.RelOp; -import parser.type.*; /** * Class for state-indexed vectors of (integer or double) values, @@ -56,25 +55,6 @@ public class StateValuesDV implements StateValues /** The VarList of the underlying model*/ VarList varList; - // stuff to keep track of variable values in print method - int[] varSizes; - int[] varValues; - int currentVar; - int currentVarLevel; - int counter; - - /** Log for output from print method */ - PrismLog outputLog; - - /** Flag: printSparse (only non-zero values) */ - boolean printSparse = true; - /** Flag: printMatlab */ - boolean printMatlab = false; - /** Flag: printStates (variable values on the model) */ - boolean printStates = true; - /** Flag: printIndizes (indizes for the states) */ - boolean printIndices = true; - // CONSTRUCTORS /** @@ -114,13 +94,6 @@ public class StateValuesDV implements StateValues numVars = vars.n(); odd = model.getODD(); varList = model.getVarList(); - - // initialise arrays - varSizes = new int[varList.getNumVars()]; - for (int i = 0; i < varList.getNumVars(); i++) { - varSizes[i] = varList.getRangeLogTwo(i); - } - varValues = new int[varList.getNumVars()]; } @Override @@ -386,29 +359,9 @@ public class StateValuesDV implements StateValues // PRINTING STUFF - @Override - public void print(PrismLog log) throws PrismException - { - print(log, true, false, true, true); - } - - @Override - public void print(PrismLog log, boolean printSparse, boolean printMatlab, boolean printStates) throws PrismException - { - print(log, printSparse, printMatlab, printStates, true); - } - @Override public void print(PrismLog log, boolean printSparse, boolean printMatlab, boolean printStates, boolean printIndices) throws PrismException { - int i; - - // store flags - this.printSparse = printSparse; - this.printMatlab = printMatlab; - this.printStates = printStates; - this.printIndices = printIndices; - // header for matlab format if (printMatlab) log.println(!printSparse ? "v = [" : "v = sparse(" + values.getSize() + ",1);"); @@ -420,89 +373,13 @@ public class StateValuesDV implements StateValues } // set up and call recursive print - outputLog = log; - for (i = 0; i < varList.getNumVars(); i++) { - varValues[i] = 0; - } - currentVar = 0; - currentVarLevel = 0; - printRec(0, odd, 0); + iterate(new StateAndValuePrinter(log, varList, printSparse, printMatlab, printStates, printIndices), printSparse); // footer for matlab format if (printMatlab && !printSparse) log.println("];"); } - /** - * 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) - */ - private void printRec(int level, ODDNode o, int n) - { - double d; - - // base case - at bottom - if (level == numVars) { - d = values.getElement(n); - printLine(n, d); - return; - } - // recurse - else { - if (o.getEOff() > 0) { - currentVarLevel++; - if (currentVarLevel == varSizes[currentVar]) { - currentVar++; - currentVarLevel = 0; - } - printRec(level + 1, o.getElse(), n); - currentVarLevel--; - if (currentVarLevel == -1) { - currentVar--; - currentVarLevel = varSizes[currentVar] - 1; - } - } - if (o.getTOff() > 0) { - varValues[currentVar] += (1 << (varSizes[currentVar] - 1 - currentVarLevel)); - currentVarLevel++; - if (currentVarLevel == varSizes[currentVar]) { - currentVar++; - currentVarLevel = 0; - } - printRec(level + 1, o.getThen(), (int) (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, false, true, true); - } - - @Override - public void printFiltered(PrismLog log, JDDNode filter, boolean printSparse, boolean printMatlab, boolean printStates) throws PrismException - { - printFiltered(log, filter, printSparse, printMatlab, printStates, true); - } - /** * Print part of a vector to a log/file (non-zero entries only). * @param log The log @@ -515,32 +392,15 @@ public class StateValuesDV implements StateValues public void printFiltered(PrismLog log, JDDNode filter, boolean printSparse, boolean printMatlab, boolean printStates, boolean printIndices) throws PrismException { - int i; - - // store flags - this.printSparse = printSparse; - this.printMatlab = printMatlab; - this.printStates = printStates; - this.printIndices = printIndices; - // header for matlab format if (printMatlab) log.println(!printSparse ? "v = [" : "v = sparse(" + values.getSize() + ",1);"); - // set up a counter so we can check if there were no non-zero elements - counter = 0; + StateAndValuePrinter printer = new StateAndValuePrinter(log, varList, printSparse, printMatlab, printStates, printIndices); + iterateFiltered(filter, printer, printSparse); - // set up and call recursive print - outputLog = log; - for (i = 0; i < varList.getNumVars(); i++) { - varValues[i] = 0; - } - currentVar = 0; - currentVarLevel = 0; - printFilteredRec(0, odd, 0, filter); - - // check if all zero - if (printSparse && !printMatlab && counter == 0) { + // check if all zero + if (printSparse && !printMatlab && !printer.hadOutput()) { log.println("(all zero)"); return; } @@ -550,111 +410,195 @@ public class StateValuesDV implements StateValues log.println("];"); } - /** - * Recursive part of printFiltered method. - * - * So we need to traverse filter too. - * See also notes above for printRec. - */ - private void printFilteredRec(int level, ODDNode o, int n, JDDNode filter) + @Override + public void iterate(StateAndValueConsumer consumer, boolean sparse) { - double d; - JDDNode newFilter; + if (!sparse) { + StateAndValuesIterator it = new StateAndValuesIterator(consumer); + it.iterate(); + } else { + StateAndValueConsumer sparseConsumer = (int varValues[], double value, long stateIndex) -> { + if (value != 0) { + consumer.accept(varValues, value, stateIndex); + } + }; + StateAndValuesIterator it = new StateAndValuesIterator(sparseConsumer); + it.iterate(); + } + } - // don't print if the filter is zero - if (filter.equals(JDD.ZERO)) { - return; + @Override + public void iterateFiltered(JDDNode filter, StateAndValueConsumer consumer, boolean sparse) + { + if (!sparse) { + StateAndValuesIterator it = new StateAndValuesIterator(consumer); + it.iterateFiltered(filter); + } else { + StateAndValueConsumer sparseConsumer = (int varValues[], double value, long stateIndex) -> { + if (value != 0) { + consumer.accept(varValues, value, stateIndex); + } + }; + StateAndValuesIterator it = new StateAndValuesIterator(sparseConsumer); + it.iterateFiltered(filter); } + } - // base case - at bottom - if (level == numVars) { - d = values.getElement(n); - printLine(n, d); - return; + private class StateAndValuesIterator { + private int[] varSizes; + private int[] varValues; + private int currentVar; + private int currentVarLevel; + + private StateAndValueConsumer consumer; + + public StateAndValuesIterator(StateAndValueConsumer consumer) + { + this.consumer = consumer; + + varValues = new int[varList.getNumVars()]; + for (int i = 0; i < varList.getNumVars(); i++) { + varValues[i] = varList.getLow(i); + } + + varSizes = new int[varList.getNumVars()]; + for (int i = 0; i < varList.getNumVars(); i++) { + varSizes[i] = varList.getRangeLogTwo(i); + } + + currentVar = 0; + currentVarLevel = 0; } - // recurse - else { - if (o.getEOff() > 0) { - currentVarLevel++; - if (currentVarLevel == varSizes[currentVar]) { - currentVar++; - currentVarLevel = 0; - } - JDD.Ref(filter); - JDD.Ref(vars.getVar(level)); - newFilter = JDD.Apply(JDD.TIMES, filter, JDD.Not(vars.getVar(level))); - printFilteredRec(level + 1, o.getElse(), n, newFilter); - JDD.Deref(newFilter); - currentVarLevel--; - if (currentVarLevel == -1) { - currentVar--; - currentVarLevel = varSizes[currentVar] - 1; - } + + public void iterate() + { + iterateRec(0, odd, 0); + } + + public void iterateFiltered(JDDNode filter) + { + iterateRecFiltered(0, odd, 0, filter); + } + + /** + * Recursive part of state/value iteration. + * + * (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) + */ + private void iterateRec(int level, ODDNode o, int n) + { + double d; + + // base case - at bottom + if (level == numVars) { + d = values.getElement(n); + consumer.accept(varValues, d, n); + return; } - if (o.getTOff() > 0) { - varValues[currentVar] += (1 << (varSizes[currentVar] - 1 - currentVarLevel)); - currentVarLevel++; - if (currentVarLevel == varSizes[currentVar]) { - currentVar++; - currentVarLevel = 0; + // recurse + else { + if (o.getEOff() > 0) { + currentVarLevel++; + if (currentVarLevel == varSizes[currentVar]) { + currentVar++; + currentVarLevel = 0; + } + iterateRec(level + 1, o.getElse(), n); + currentVarLevel--; + if (currentVarLevel == -1) { + currentVar--; + currentVarLevel = varSizes[currentVar] - 1; + } } - JDD.Ref(filter); - JDD.Ref(vars.getVar(level)); - newFilter = JDD.Apply(JDD.TIMES, filter, vars.getVar(level)); - printFilteredRec(level + 1, o.getThen(), (int) (n + o.getEOff()), newFilter); - JDD.Deref(newFilter); - currentVarLevel--; - if (currentVarLevel == -1) { - currentVar--; - currentVarLevel = varSizes[currentVar] - 1; + if (o.getTOff() > 0) { + varValues[currentVar] += (1 << (varSizes[currentVar] - 1 - currentVarLevel)); + currentVarLevel++; + if (currentVarLevel == varSizes[currentVar]) { + currentVar++; + currentVarLevel = 0; + } + iterateRec(level + 1, o.getThen(), (int) (n + o.getEOff())); + currentVarLevel--; + if (currentVarLevel == -1) { + currentVar--; + currentVarLevel = varSizes[currentVar] - 1; + } + varValues[currentVar] -= (1 << (varSizes[currentVar] - 1 - currentVarLevel)); } - varValues[currentVar] -= (1 << (varSizes[currentVar] - 1 - currentVarLevel)); } } - } - private void printLine(int n, double d) - { - int i, j; - // increment counter (used in printFiltered) - if (d > 0) - counter++; - // do printing - if (!printSparse || d != 0) { - if (printMatlab) { - if (printSparse) { - outputLog.println("v(" + (n + 1) + ")=" + d + ";"); - } else { - outputLog.println(d); - } - } else { - if (printIndices) { - outputLog.print(n + ":"); + /** + * Recursive part of filtered state/value iteration. + * + * So we need to traverse filter too. + * See also notes above for iterateRec. + */ + private void iterateRecFiltered(int level, ODDNode o, int n, JDDNode filter) + { + double d; + JDDNode newFilter; + + // skip if the filter is zero + if (filter.equals(JDD.ZERO)) { + return; + } + + // base case - at bottom + if (level == numVars) { + d = values.getElement(n); + consumer.accept(varValues, d, n); + return; + } + // recurse + else { + if (o.getEOff() > 0) { + currentVarLevel++; + if (currentVarLevel == varSizes[currentVar]) { + currentVar++; + currentVarLevel = 0; + } + JDD.Ref(filter); + JDD.Ref(vars.getVar(level)); + newFilter = JDD.Apply(JDD.TIMES, filter, JDD.Not(vars.getVar(level))); + iterateRecFiltered(level + 1, o.getElse(), n, newFilter); + JDD.Deref(newFilter); + currentVarLevel--; + if (currentVarLevel == -1) { + currentVar--; + currentVarLevel = varSizes[currentVar] - 1; + } } - if (printStates) { - outputLog.print("("); - 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(","); + if (o.getTOff() > 0) { + varValues[currentVar] += (1 << (varSizes[currentVar] - 1 - currentVarLevel)); + currentVarLevel++; + if (currentVarLevel == varSizes[currentVar]) { + currentVar++; + currentVarLevel = 0; } - outputLog.print(")"); + JDD.Ref(filter); + JDD.Ref(vars.getVar(level)); + newFilter = JDD.Apply(JDD.TIMES, filter, vars.getVar(level)); + iterateRecFiltered(level + 1, o.getThen(), (int) (n + o.getEOff()), newFilter); + JDD.Deref(newFilter); + currentVarLevel--; + if (currentVarLevel == -1) { + currentVar--; + currentVarLevel = varSizes[currentVar] - 1; + } + varValues[currentVar] -= (1 << (varSizes[currentVar] - 1 - currentVarLevel)); } - if (printIndices || printStates) - outputLog.print("="); - outputLog.println(d); } - //return true; - } else { - //return false; } } diff --git a/prism/src/prism/StateValuesMTBDD.java b/prism/src/prism/StateValuesMTBDD.java index 1b9baefe..f8418515 100644 --- a/prism/src/prism/StateValuesMTBDD.java +++ b/prism/src/prism/StateValuesMTBDD.java @@ -35,7 +35,6 @@ import jdd.*; import odd.*; import parser.VarList; import parser.ast.RelOp; -import parser.type.*; /** * Class for state-indexed vectors of (integer or double) values, represented by an MTBDD @@ -60,15 +59,6 @@ public class StateValuesMTBDD implements StateValues /** The VarList of the underlying model*/ VarList varList; - // stuff to keep track of variable values in print method - int[] varSizes; - int[] varValues; - int currentVar; - int currentVarLevel; - - /** log for output from print method */ - PrismLog outputLog; - // CONSTRUCTOR /** @@ -96,13 +86,6 @@ public class StateValuesMTBDD implements StateValues numVars = vars.n(); odd = model.getODD(); varList = model.getVarList(); - - // initialise arrays - varSizes = new int[varList.getNumVars()]; - for (int i = 0; i < varList.getNumVars(); i++) { - varSizes[i] = varList.getRangeLogTwo(i); - } - varValues = new int[varList.getNumVars()]; } @Override @@ -574,28 +557,6 @@ public class StateValuesMTBDD implements StateValues // PRINTING STUFF - @Override - public void print(PrismLog log) - { - int i; - - // check if all zero - if (values.equals(JDD.ZERO)) { - log.println("(all zero)"); - return; - } - - // set up and call recursive print - outputLog = log; - for (i = 0; i < varList.getNumVars(); i++) { - varValues[i] = 0; - } - currentVar = 0; - currentVarLevel = 0; - printRec(values, 0, odd, 0); - //log.println(); - } - /** * Print the state values for a JDDNode, representing an MTBDD over the row vars of a model. *
[ REFS: none, DEREFS: value ] @@ -604,7 +565,7 @@ public class StateValuesMTBDD implements StateValues * @param model the Model (for the variable information) * @param description an optional description for printing (may be {@code null}) */ - public static void print(PrismLog log, JDDNode values, Model model, String description) + public static void print(PrismLog log, JDDNode values, Model model, String description) throws PrismException { StateValuesMTBDD sv = null; try { @@ -617,135 +578,281 @@ public class StateValuesMTBDD implements StateValues } } - @Override - public void print(PrismLog log, boolean printSparse, boolean printMatlab, boolean printStates) throws PrismException - { - print(log, printSparse, printMatlab, printStates, true); - } - @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 + if (odd == null) { + if (printMatlab && printSparse) { + throw new PrismNotSupportedException("Cannot print in sparse Matlab format, as there is no ODD"); + } + // we have no index information -> can't print state index + printIndices = false; + } + + // header for matlab format + if (printMatlab) + log.println(!printSparse ? "v = [" : "v = sparse(" + getSize() + ",1);"); + + // check if all zero + if (printSparse && !printMatlab && values.equals(JDD.ZERO)) { + log.println("(all zero)"); + return; + } + + // set up and call recursive print + StateIterator it = new StateIterator(new StateAndValuePrinter(log, varList, printSparse, printMatlab, printStates, printIndices)); + if (printSparse) { + it.iterateSparse(values); + } else { + it.iterateFiltered(model.getReach(), values); + } + + // footer for matlab format + if (printMatlab && !printSparse) + log.println("];"); } - /** - * 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) - */ - private void printRec(JDDNode dd, int level, ODDNode o, long n) - { - int i, j; - JDDNode e, t; + private class StateIterator { + private int[] varSizes; + private int[] varValues; + private int currentVar; + private int currentVarLevel; - // zero constant - bottom out of recursion - if (dd.equals(JDD.ZERO)) return; + private StateAndValueConsumer consumer; - // base case - at bottom (nonzero terminal) - if (level == numVars) { - - if (o != null) { - outputLog.print(n + ":("); - } else { - // we have no index - outputLog.print("("); + public StateIterator(StateAndValueConsumer consumer) + { + this.consumer = consumer; + + varValues = new int[varList.getNumVars()]; + for (int i = 0; i < varList.getNumVars(); i++) { + varValues[i] = varList.getLow(i); } - 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(","); + varSizes = new int[varList.getNumVars()]; + for (int i = 0; i < varList.getNumVars(); i++) { + varSizes[i] = varList.getRangeLogTwo(i); } - outputLog.print(")=" + dd.getValue()); - outputLog.println(); - return; + currentVar = 0; + currentVarLevel = 0; } - - // select 'else' and 'then' branches - else if (dd.getIndex() > vars.getVarIndex(level)) { - e = t = dd; + + public void iterateSparse(JDDNode dd) + { + // if we don't have an ODD, we set the index to -1 + long stateIndex = (odd == null ? -1 : 0); + iterateSparseRec(dd, 0, odd, stateIndex); } - else { - e = dd.getElse(); - t = dd.getThen(); + + /** + * Iterate over all state/value pairs in ddValue that + * are included in the 0/1-DD ddFilter. + * + * @param ddFilter 0/1-DD for the states that should be considered + * @param ddValue the values for the states (has to be zero for all states not in ddFilter) + */ + public void iterateFiltered(JDDNode ddFilter, JDDNode ddValue) + { + // if we don't have an ODD, we set the index to -1 + long stateIndex = (odd == null ? -1 : 0); + iterateRec(ddFilter, ddValue, 0, odd, stateIndex); } - ODDNode oe = (o != null ? o.getElse() : null); - ODDNode ot = (o != null ? o.getThen() : null); - long eoff = (o != null ? o.getEOff() : 0); + /** + * Recursive part of iteration (only non-zero values). + * + * (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) + */ + private void iterateSparseRec(JDDNode dd, int level, ODDNode o, long stateIndex) + { + JDDNode e, t; + + // zero constant - bottom out of recursion + if (dd.equals(JDD.ZERO)) return; + + // base case - at bottom (nonzero terminal) + if (level == numVars) { + consumer.accept(varValues, dd.getValue(), stateIndex); + return; + } - // then recurse... - currentVarLevel++; if (currentVarLevel == varSizes[currentVar]) { currentVar++; currentVarLevel=0; } - printRec(e, level+1, oe, 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; } - printRec(t, level+1, ot, n + eoff); - currentVarLevel--; if (currentVarLevel == -1) { currentVar--; currentVarLevel=varSizes[currentVar]-1; } - varValues[currentVar] -= (1 << (varSizes[currentVar]-1-currentVarLevel)); + // select 'else' and 'then' branches + else if (dd.getIndex() > vars.getVarIndex(level)) { + e = t = dd; + } + else { + e = dd.getElse(); + t = dd.getThen(); + } + + ODDNode oe = (o != null ? o.getElse() : null); + ODDNode ot = (o != null ? o.getThen() : null); + long eoff = (o != null ? o.getEOff() : 0); + + // then recurse... + currentVarLevel++; if (currentVarLevel == varSizes[currentVar]) { currentVar++; currentVarLevel=0; } + iterateSparseRec(e, level+1, oe, stateIndex); + currentVarLevel--; if (currentVarLevel == -1) { currentVar--; currentVarLevel=varSizes[currentVar]-1; } + varValues[currentVar] += (1 << (varSizes[currentVar]-1-currentVarLevel)); + currentVarLevel++; if (currentVarLevel == varSizes[currentVar]) { currentVar++; currentVarLevel=0; } + iterateSparseRec(t, level+1, ot, stateIndex + eoff); + currentVarLevel--; if (currentVarLevel == -1) { currentVar--; currentVarLevel=varSizes[currentVar]-1; } + varValues[currentVar] -= (1 << (varSizes[currentVar]-1-currentVarLevel)); + } + + /** + * Recursive part of iteration (all elements, + * including where the value is zero). + * + * @param ddFilter 0/1-DD for the states that should be considered + * @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 iterateRec(JDDNode ddFilter, JDDNode ddValue, int level, ODDNode o, long stateIndex) + { + /* + * (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) + */ + + // ddFilter is zero - bottom out of recursion + if (ddFilter.equals(JDD.ZERO)) return; + + // base case - at bottom (nonzero terminal) + if (level == numVars) { + consumer.accept(varValues, ddValue.getValue(), stateIndex); + return; + } + + JDDNode eFilter, tFilter, eValue, tValue; + + // 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(); + } + + ODDNode oe = (o != null ? o.getElse() : null); + ODDNode ot = (o != null ? o.getThen() : null); + long eoff = (o != null ? o.getEOff() : 0); + + // then recurse... + currentVarLevel++; if (currentVarLevel == varSizes[currentVar]) { currentVar++; currentVarLevel=0; } + iterateRec(eFilter, eValue, level+1, oe, stateIndex); + currentVarLevel--; if (currentVarLevel == -1) { currentVar--; currentVarLevel=varSizes[currentVar]-1; } + varValues[currentVar] += (1 << (varSizes[currentVar]-1-currentVarLevel)); + currentVarLevel++; if (currentVarLevel == varSizes[currentVar]) { currentVar++; currentVarLevel=0; } + iterateRec(tFilter, tValue, level+1, ot, stateIndex + eoff); + currentVarLevel--; if (currentVarLevel == -1) { currentVar--; currentVarLevel=varSizes[currentVar]-1; } + varValues[currentVar] -= (1 << (varSizes[currentVar]-1-currentVarLevel)); + } + } + + @Override + public void iterate(StateAndValueConsumer consumer, boolean sparse) + { + StateIterator it = new StateIterator(consumer); + if (sparse) { + it.iterateSparse(values); + } else { + it.iterateFiltered(reach, values); + } + } + + @Override + public void iterateFiltered(JDDNode filter, StateAndValueConsumer consumer, boolean sparse) + { + // filter out + JDDNode tmp = JDD.Apply(JDD.TIMES, values.copy(), filter.copy()); + + StateIterator it = new StateIterator(consumer); + + if (sparse) { + it.iterateSparse(tmp); + } else { + it.iterateFiltered(filter, tmp); + } + + JDD.Deref(tmp); } @Override - public void printFiltered(PrismLog log, JDDNode filter) throws PrismException + public void printFiltered(PrismLog log, JDDNode filter, boolean printSparse, boolean printMatlab, boolean printStates, boolean printIndices) throws PrismException { - int i; JDDNode tmp; - + + if (odd == null) { + if (printMatlab && printSparse) { + throw new PrismNotSupportedException("Cannot print in sparse Matlab format, as there is no ODD"); + } + // we have no index information -> can't print state index + printIndices = false; + } + // filter out JDD.Ref(values); JDD.Ref(filter); tmp = JDD.Apply(JDD.TIMES, values, filter); - + + // header for matlab format + if (printMatlab) + log.println(!printSparse ? "v = [" : "v = sparse(" + getSize() + ",1);"); + // check if all zero - if (tmp.equals(JDD.ZERO)) { + if (printSparse && !printMatlab && tmp.equals(JDD.ZERO)) { JDD.Deref(tmp); log.println("(all zero)"); return; } - + // set up and call recursive print - outputLog = log; - for (i = 0; i < varList.getNumVars(); i++) { - varValues[i] = 0; + StateIterator it = new StateIterator(new StateAndValuePrinter(log, varList, printSparse, printMatlab, printStates, printIndices)); + if (printSparse) { + it.iterateSparse(tmp); + } else { + it.iterateFiltered(filter, tmp); } - currentVar = 0; - currentVarLevel = 0; - printRec(tmp, 0, odd, 0); + + // footer for matlab format + if (printMatlab && !printSparse) + log.println("];"); + //log.println(); JDD.Deref(tmp); } - @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 - } - /** * Make a (deep) copy of this vector */ diff --git a/prism/src/prism/StateValuesVoid.java b/prism/src/prism/StateValuesVoid.java index e231cdf7..99292383 100644 --- a/prism/src/prism/StateValuesVoid.java +++ b/prism/src/prism/StateValuesVoid.java @@ -239,31 +239,25 @@ public class StateValuesVoid implements StateValues } @Override - public void print(PrismLog log) throws PrismException - { - throw new UnsupportedOperationException(); - } - - @Override - public void print(PrismLog log, boolean printSparse, boolean printMatlab, boolean printStates) throws PrismException + public void print(PrismLog log, boolean printSparse, boolean printMatlab, boolean printStates, boolean printIndices) throws PrismException { throw new UnsupportedOperationException(); } @Override - public void print(PrismLog log, boolean printSparse, boolean printMatlab, boolean printStates, boolean printIndices) throws PrismException + public void printFiltered(PrismLog log, JDDNode filter, boolean printSparse, boolean printMatlab, boolean printStates, boolean printIndizes) throws PrismException { throw new UnsupportedOperationException(); } @Override - public void printFiltered(PrismLog log, JDDNode filter) throws PrismException + public void iterate(StateAndValueConsumer consumer, boolean sparse) { throw new UnsupportedOperationException(); } @Override - public void printFiltered(PrismLog log, JDDNode filter, boolean printSparse, boolean printMatlab, boolean printStates) throws PrismException + public void iterateFiltered(JDDNode filter, StateAndValueConsumer consumer, boolean sparse) { throw new UnsupportedOperationException(); }