Browse Source

Export to string array option in StateList (unused) + tidy.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1440 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 17 years ago
parent
commit
2efea0dda6
  1. 3
      prism/src/prism/StateList.java
  2. 64
      prism/src/prism/StateListMTBDD.java

3
prism/src/prism/StateList.java

@ -26,6 +26,8 @@
package prism; package prism;
import java.util.List;
import jdd.*; import jdd.*;
import parser.Values; import parser.Values;
@ -38,6 +40,7 @@ public interface StateList
void print(PrismLog log); void print(PrismLog log);
void printMatlab(PrismLog log); void printMatlab(PrismLog log);
void printDot(PrismLog log); void printDot(PrismLog log);
public List<String> exportToStringList();
void print(PrismLog log, int n); void print(PrismLog log, int n);
void printMatlab(PrismLog log, int n); void printMatlab(PrismLog log, int n);
boolean includes(JDDNode state); boolean includes(JDDNode state);

64
prism/src/prism/StateListMTBDD.java

@ -26,11 +26,12 @@
package prism; package prism;
import java.util.*;
import jdd.*; import jdd.*;
import odd.*; import odd.*;
import parser.Values; import parser.Values;
import parser.VarList; import parser.VarList;
import parser.ast.Expression;
import parser.type.*; import parser.type.*;
// list of states (mtbdd) // list of states (mtbdd)
@ -61,8 +62,11 @@ public class StateListMTBDD implements StateList
// log for output from print method // log for output from print method
PrismLog outputLog; PrismLog outputLog;
// string array when exporting
List<String> strList;
// output format // output format
enum OutputFormat { NORMAL, MATLAB, DOT };
enum OutputFormat { NORMAL, MATLAB, DOT, STRINGS };
OutputFormat outputFormat = OutputFormat.NORMAL; OutputFormat outputFormat = OutputFormat.NORMAL;
// constructor // constructor
@ -103,50 +107,64 @@ public class StateListMTBDD implements StateList
return (size > Long.MAX_VALUE) ? "" + size : "" + Math.round(size); return (size > Long.MAX_VALUE) ? "" + size : "" + Math.round(size);
} }
// print whole list
// print/export whole list
public void print(PrismLog log) public void print(PrismLog log)
{ {
outputFormat = OutputFormat.NORMAL;
limit = false; limit = false;
count = 0;
doPrint(log);
outputLog = log;
doPrint();
} }
public void printMatlab(PrismLog log) public void printMatlab(PrismLog log)
{ {
outputFormat = OutputFormat.MATLAB; outputFormat = OutputFormat.MATLAB;
print(log);
outputFormat = OutputFormat.NORMAL;
limit = false;
outputLog = log;
doPrint();
} }
public void printDot(PrismLog log) public void printDot(PrismLog log)
{ {
outputFormat = OutputFormat.DOT; outputFormat = OutputFormat.DOT;
print(log);
outputFormat = OutputFormat.NORMAL;
limit = false;
outputLog = log;
doPrint();
}
public List<String> exportToStringList()
{
strList = new ArrayList<String>((int)size);
outputFormat = OutputFormat.STRINGS;
limit = false;
doPrint();
return strList;
} }
// print first n states of list // print first n states of list
public void print(PrismLog log, int n) public void print(PrismLog log, int n)
{ {
outputFormat = OutputFormat.NORMAL;
limit = true; limit = true;
numToPrint = n; numToPrint = n;
count = 0;
doPrint(log);
outputLog = log;
doPrint();
} }
public void printMatlab(PrismLog log, int n) public void printMatlab(PrismLog log, int n)
{ {
outputFormat = OutputFormat.MATLAB; outputFormat = OutputFormat.MATLAB;
print(log, n);
outputFormat = OutputFormat.NORMAL;
limit = true;
numToPrint = n;
outputLog = log;
doPrint();
} }
// printing method // printing method
public void doPrint(PrismLog log)
public void doPrint()
{ {
int i; int i;
outputLog = log;
count = 0;
for (i = 0; i < varList.getNumVars(); i++) { for (i = 0; i < varList.getNumVars(); i++) {
varValues[i] = 0; varValues[i] = 0;
} }
@ -168,6 +186,7 @@ public class StateListMTBDD implements StateList
{ {
int i, j; int i, j;
JDDNode e, t; JDDNode e, t;
String varsString;
// if we've printed enough states, stop // if we've printed enough states, stop
if (limit) if (count >= numToPrint) return; if (limit) if (count >= numToPrint) return;
@ -184,23 +203,24 @@ public class StateListMTBDD implements StateList
case DOT: outputLog.print(n + " [label=\"" + n + "\\n("); break; case DOT: outputLog.print(n + " [label=\"" + n + "\\n("); break;
} }
j = varList.getNumVars(); j = varList.getNumVars();
varsString = "";
for (i = 0; i < j; i++) { for (i = 0; i < j; i++) {
// integer variable // integer variable
if (varList.getType(i) instanceof TypeInt) { if (varList.getType(i) instanceof TypeInt) {
outputLog.print(varValues[i]+varList.getLow(i));
varsString += varValues[i]+varList.getLow(i);
} }
// boolean variable // boolean variable
else { else {
outputLog.print(varValues[i] == 1);
varsString += (varValues[i] == 1);
} }
if (i < j-1) outputLog.print(",");
if (i < j-1) varsString += ",";
} }
switch (outputFormat) { switch (outputFormat) {
case NORMAL: outputLog.print(")"); break;
case MATLAB: break;
case DOT: outputLog.print(")\"];"); break;
case NORMAL: outputLog.println(varsString + ")"); break;
case MATLAB: outputLog.println(varsString); break;
case DOT: outputLog.println(varsString + ")\"];"); break;
case STRINGS: strList.add(varsString);
} }
outputLog.println();
count++; count++;
return; return;

Loading…
Cancel
Save