Browse Source
Refactor symbolic state value printing
Refactor symbolic state value printing
This cleans up and refactors the iteration over state variable valuation/value pairs via StateValues. In particular StateValuesMTBDD learns how to do non-sparse printing. Furthermore, it * introduces generic "iterate" and "iterateFiltered" methods for iterating over the state/values, calling a StateAndValueConsumer object * provides a StateAndValueConsumer implementation (StateAndValuePrinter) that supports printing in the various output styles supported by PRISM * cleans up the convenience "print" method using default methods in StateValues * activates the MTBDD engine for one -exportvector based test Note: Previously, in the StateValuesMTBDD iteration steps, the int[] array with the current values represented the increments to be added to the low values of state variables, with the addition value = low + a[i] happening on output. Now, we initialise the array with low, i.e., the values in the array correspond to the actual variable values.accumulation-v4.7
Joachim Klein
7 years ago
7 changed files with 645 additions and 383 deletions
-
2prism-tests/functionality/export/vector/exportvector.prism.args
-
48prism/src/prism/StateAndValueConsumer.java
-
128prism/src/prism/StateAndValuePrinter.java
-
49prism/src/prism/StateValues.java
-
414prism/src/prism/StateValuesDV.java
-
373prism/src/prism/StateValuesMTBDD.java
-
14prism/src/prism/StateValuesVoid.java
@ -1,4 +1,4 @@ |
|||
-ex |
|||
#-m |
|||
-m |
|||
-s |
|||
-h |
|||
@ -0,0 +1,48 @@ |
|||
//============================================================================== |
|||
// |
|||
// Copyright (c) 2018- |
|||
// Authors: |
|||
// * Joachim Klein <klein@tcs.inf.tu-dresden.de> (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. |
|||
* <br> |
|||
* 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); |
|||
|
|||
} |
|||
@ -0,0 +1,128 @@ |
|||
//============================================================================== |
|||
// |
|||
// Copyright (c) 2018- |
|||
// Authors: |
|||
// * Joachim Klein <klein@tcs.inf.tu-dresden.de> (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; |
|||
} |
|||
|
|||
} |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue