s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Tidy up of export-to-Dot functionality, plus new "dot" option for exporting strategy (explicit engine only, currently). 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8110 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 13 years ago
parent
7b8b7832a4
commit
21748bcaa4
14 changed files with 329 additions and 225 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 28
      prism/src/explicit/DTMCExplicit.java
  2. 6
      prism/src/explicit/MDP.java
  3. 90
      prism/src/explicit/MDPExplicit.java
  4. 10
      prism/src/explicit/Model.java
  5. 28
      prism/src/explicit/ModelExplicit.java
  6. 8
      prism/src/explicit/NondetModel.java
  7. 52
      prism/src/explicit/STPGAbstrSimple.java
  8. 274
      prism/src/explicit/SubNondetModel.java
  9. 12
      prism/src/param/ParamModel.java
  10. 14
      prism/src/prism/Prism.java
  11. 2
      prism/src/prism/PrismCL.java
  12. 6
      prism/src/strat/MDStrategyArray.java
  13. 19
      prism/src/strat/MDStrategyIV.java
  14. 5
      prism/src/strat/Strategy.java

28
prism/src/explicit/DTMCExplicit.java
View File

@ -96,27 +96,21 @@ public abstract class DTMCExplicit extends ModelExplicit implements DTMC
} }
@Override @Override
public void exportToDotFile(String filename, BitSet mark) throws PrismException
public void exportToDotFile(PrismLog out, BitSet mark)
{ {
int i; int i;
try {
FileWriter out = new FileWriter(filename);
out.write("digraph " + getModelType() + " {\nsize=\"8,5\"\nnode [shape=box];\n");
for (i = 0; i < numStates; i++) {
if (mark != null && mark.get(i))
out.write(i + " [style=filled fillcolor=\"#cccccc\"]\n");
Iterator<Map.Entry<Integer, Double>> iter = getTransitionsIterator(i);
while (iter.hasNext()) {
Map.Entry<Integer, Double> e = iter.next();
out.write(i + " -> " + e.getKey() + " [ label=\"");
out.write(e.getValue() + "\" ];\n");
}
out.print("digraph " + getModelType() + " {\nsize=\"8,5\"\nnode [shape=box];\n");
for (i = 0; i < numStates; i++) {
if (mark != null && mark.get(i))
out.print(i + " [style=filled fillcolor=\"#cccccc\"]\n");
Iterator<Map.Entry<Integer, Double>> iter = getTransitionsIterator(i);
while (iter.hasNext()) {
Map.Entry<Integer, Double> e = iter.next();
out.print(i + " -> " + e.getKey() + " [ label=\"");
out.print(e.getValue() + "\" ];\n");
} }
out.write("}\n");
out.close();
} catch (IOException e) {
throw new PrismException("Could not write " + getModelType() + " to file \"" + filename + "\"" + e);
} }
out.print("}\n");
} }
@Override @Override

6
prism/src/explicit/MDP.java
View File

@ -31,7 +31,6 @@ import java.util.Iterator;
import java.util.List; import java.util.List;
import java.util.Map.Entry; import java.util.Map.Entry;
import prism.PrismException;
import explicit.rewards.MCRewards; import explicit.rewards.MCRewards;
import explicit.rewards.MDPRewards; import explicit.rewards.MDPRewards;
@ -277,9 +276,4 @@ public interface MDP extends NondetModel
* @param dest Vector to write result to. * @param dest Vector to write result to.
*/ */
public void mvMultRight(int[] states, int[] strat, double[] source, double[] dest); public void mvMultRight(int[] states, int[] strat, double[] source, double[] dest);
/**
* Export to a dot file, highlighting states in 'mark' and choices for a (memoryless) strategy.
*/
public void exportToDotFileWithStrat(String filename, BitSet mark, int strat[]) throws PrismException;
} }

90
prism/src/explicit/MDPExplicit.java
View File

@ -108,75 +108,63 @@ public abstract class MDPExplicit extends ModelExplicit implements MDP
} }
@Override @Override
public void exportToDotFile(String filename, BitSet mark) throws PrismException
public void exportToDotFile(PrismLog out, BitSet mark)
{ {
int i, j, numChoices; int i, j, numChoices;
String nij; String nij;
Object action; Object action;
try {
FileWriter out = new FileWriter(filename);
out.write("digraph " + getModelType() + " {\nsize=\"8,5\"\nnode [shape=box];\n");
for (i = 0; i < numStates; i++) {
if (mark != null && mark.get(i))
out.write(i + " [style=filled fillcolor=\"#cccccc\"]\n");
numChoices = getNumChoices(i);
for (j = 0; j < numChoices; j++) {
action = getAction(i, j);
nij = "n" + i + "_" + j;
out.write(i + " -> " + nij + " [ arrowhead=none,label=\"" + j);
if (action != null)
out.write(":" + action);
out.write("\" ];\n");
out.write(nij + " [ shape=point,width=0.1,height=0.1,label=\"\" ];\n");
Iterator<Map.Entry<Integer, Double>> iter = getTransitionsIterator(i, j);
while (iter.hasNext()) {
Map.Entry<Integer, Double> e = iter.next();
out.write(nij + " -> " + e.getKey() + " [ label=\"" + e.getValue() + "\" ];\n");
}
out.print("digraph " + getModelType() + " {\nsize=\"8,5\"\nnode [shape=box];\n");
for (i = 0; i < numStates; i++) {
if (mark != null && mark.get(i))
out.print(i + " [style=filled fillcolor=\"#cccccc\"]\n");
numChoices = getNumChoices(i);
for (j = 0; j < numChoices; j++) {
action = getAction(i, j);
nij = "n" + i + "_" + j;
out.print(i + " -> " + nij + " [ arrowhead=none,label=\"" + j);
if (action != null)
out.print(":" + action);
out.print("\" ];\n");
out.print(nij + " [ shape=point,width=0.1,height=0.1,label=\"\" ];\n");
Iterator<Map.Entry<Integer, Double>> iter = getTransitionsIterator(i, j);
while (iter.hasNext()) {
Map.Entry<Integer, Double> e = iter.next();
out.print(nij + " -> " + e.getKey() + " [ label=\"" + e.getValue() + "\" ];\n");
} }
} }
out.write("}\n");
out.close();
} catch (IOException e) {
throw new PrismException("Could not write " + getModelType() + " to file \"" + filename + "\"" + e);
} }
out.print("}\n");
} }
@Override @Override
public void exportToDotFileWithStrat(String filename, BitSet mark, int strat[]) throws PrismException
public void exportToDotFileWithStrat(PrismLog out, BitSet mark, int strat[])
{ {
int i, j, numChoices; int i, j, numChoices;
String nij; String nij;
Object action; Object action;
String style; String style;
try {
FileWriter out = new FileWriter(filename);
out.write("digraph " + getModelType() + " {\nsize=\"8,5\"\nnode [shape=box];\n");
for (i = 0; i < numStates; i++) {
if (mark != null && mark.get(i))
out.write(i + " [style=filled fillcolor=\"#cccccc\"]\n");
numChoices = getNumChoices(i);
for (j = 0; j < numChoices; j++) {
style = (strat[i] == j) ? ",color=\"#ff0000\",fontcolor=\"#ff0000\"" : "";
action = getAction(i, j);
nij = "n" + i + "_" + j;
out.write(i + " -> " + nij + " [ arrowhead=none,label=\"" + j);
if (action != null)
out.write(":" + action);
out.write("\"" + style + " ];\n");
out.write(nij + " [ shape=point,height=0.1,label=\"\"" + style + " ];\n");
Iterator<Map.Entry<Integer, Double>> iter = getTransitionsIterator(i, j);
while (iter.hasNext()) {
Map.Entry<Integer, Double> e = iter.next();
out.write(nij + " -> " + e.getKey() + " [ label=\"" + e.getValue() + "\"" + style + " ];\n");
}
out.print("digraph " + getModelType() + " {\nsize=\"8,5\"\nnode [shape=box];\n");
for (i = 0; i < numStates; i++) {
if (mark != null && mark.get(i))
out.print(i + " [style=filled fillcolor=\"#cccccc\"]\n");
numChoices = getNumChoices(i);
for (j = 0; j < numChoices; j++) {
style = (strat[i] == j) ? ",color=\"#ff0000\",fontcolor=\"#ff0000\"" : "";
action = getAction(i, j);
nij = "n" + i + "_" + j;
out.print(i + " -> " + nij + " [ arrowhead=none,label=\"" + j);
if (action != null)
out.print(":" + action);
out.print("\"" + style + " ];\n");
out.print(nij + " [ shape=point,height=0.1,label=\"\"" + style + " ];\n");
Iterator<Map.Entry<Integer, Double>> iter = getTransitionsIterator(i, j);
while (iter.hasNext()) {
Map.Entry<Integer, Double> e = iter.next();
out.print(nij + " -> " + e.getKey() + " [ label=\"" + e.getValue() + "\"" + style + " ];\n");
} }
} }
out.write("}\n");
out.close();
} catch (IOException e) {
throw new PrismException("Could not write " + getModelType() + " to file \"" + filename + "\"" + e);
} }
out.print("}\n");
} }
@Override @Override

10
prism/src/explicit/Model.java
View File

@ -203,6 +203,16 @@ public interface Model
*/ */
public void exportToDotFile(String filename, BitSet mark) throws PrismException; public void exportToDotFile(String filename, BitSet mark) throws PrismException;
/**
* Export to a dot file.
*/
public void exportToDotFile(PrismLog out);
/**
* Export to a dot file, highlighting states in 'mark'.
*/
public void exportToDotFile(PrismLog out, BitSet mark);
/** /**
* Export to a equivalent PRISM language model description. * Export to a equivalent PRISM language model description.
*/ */

28
prism/src/explicit/ModelExplicit.java
View File

@ -288,21 +288,13 @@ public abstract class ModelExplicit implements Model
@Override @Override
public void exportToPrismExplicitTra(String filename) throws PrismException public void exportToPrismExplicitTra(String filename) throws PrismException
{ {
PrismLog tmpLog = new PrismFileLog(filename);
if (!tmpLog.ready()) {
throw new PrismException("Could not open file \"" + filename + "\" for output");
}
exportToPrismExplicitTra(tmpLog);
exportToPrismExplicitTra(PrismFileLog.create(filename));
} }
@Override @Override
public void exportToPrismExplicitTra(File file) throws PrismException public void exportToPrismExplicitTra(File file) throws PrismException
{ {
PrismLog tmpLog = new PrismFileLog(file.getPath());
if (!tmpLog.ready()) {
throw new PrismException("Could not open file \"" + file + "\" for output");
}
exportToPrismExplicitTra(new PrismFileLog(file.getPath()));
exportToPrismExplicitTra(PrismFileLog.create(file.getPath()));
} }
@Override @Override
@ -311,11 +303,23 @@ public abstract class ModelExplicit implements Model
@Override @Override
public void exportToDotFile(String filename) throws PrismException public void exportToDotFile(String filename) throws PrismException
{ {
exportToDotFile(filename, null);
exportToDotFile(PrismFileLog.create(filename), null);
}
@Override
public void exportToDotFile(String filename, BitSet mark) throws PrismException
{
exportToDotFile(PrismFileLog.create(filename), mark);
}
@Override
public void exportToDotFile(PrismLog out)
{
exportToDotFile(out, null);
} }
@Override @Override
public abstract void exportToDotFile(String filename, BitSet mark) throws PrismException;
public abstract void exportToDotFile(PrismLog out, BitSet mark);
@Override @Override
public abstract void exportToPrismLanguage(String filename) throws PrismException; public abstract void exportToPrismLanguage(String filename) throws PrismException;

8
prism/src/explicit/NondetModel.java
View File

@ -30,6 +30,9 @@ import java.util.BitSet;
import java.util.Iterator; import java.util.Iterator;
import java.util.Map.Entry; import java.util.Map.Entry;
import prism.PrismException;
import prism.PrismLog;
import strat.MDStrategy; import strat.MDStrategy;
/** /**
@ -91,4 +94,9 @@ public interface NondetModel extends Model
* @param strat (Memoryless) strategy to use * @param strat (Memoryless) strategy to use
*/ */
public Model constructInducedModel(MDStrategy strat); public Model constructInducedModel(MDStrategy strat);
/**
* Export to a dot file, highlighting states in 'mark' and choices for a (memoryless) strategy.
*/
public void exportToDotFileWithStrat(PrismLog out, BitSet mark, int strat[]);
} }

52
prism/src/explicit/STPGAbstrSimple.java
View File

@ -394,41 +394,41 @@ public class STPGAbstrSimple extends ModelExplicit implements STPG, NondetModelS
} }
@Override @Override
public void exportToDotFile(String filename, BitSet mark) throws PrismException
public void exportToDotFile(PrismLog out, BitSet mark)
{ {
int i, j, k; int i, j, k;
String nij, nijk; String nij, nijk;
try {
FileWriter out = new FileWriter(filename);
out.write("digraph " + getModelType() + " {\nsize=\"8,5\"\nnode [shape=box];\n");
for (i = 0; i < numStates; i++) {
if (mark != null && mark.get(i))
out.write(i + " [style=filled fillcolor=\"#cccccc\"]\n");
j = -1;
for (DistributionSet distrs : trans.get(i)) {
j++;
nij = "n" + i + "_" + j;
out.write(i + " -> " + nij + " [ arrowhead=none,label=\"" + j + "\" ];\n");
out.write(nij + " [ shape=circle,width=0.1,height=0.1,label=\"\" ];\n");
k = -1;
for (Distribution distr : distrs) {
k++;
nijk = "n" + i + "_" + j + "_" + k;
out.write(nij + " -> " + nijk + " [ arrowhead=none,label=\"" + k + "\" ];\n");
out.write(nijk + " [ shape=point,label=\"\" ];\n");
for (Map.Entry<Integer, Double> e : distr) {
out.write(nijk + " -> " + e.getKey() + " [ label=\"" + e.getValue() + "\" ];\n");
}
out.print("digraph " + getModelType() + " {\nsize=\"8,5\"\nnode [shape=box];\n");
for (i = 0; i < numStates; i++) {
if (mark != null && mark.get(i))
out.print(i + " [style=filled fillcolor=\"#cccccc\"]\n");
j = -1;
for (DistributionSet distrs : trans.get(i)) {
j++;
nij = "n" + i + "_" + j;
out.print(i + " -> " + nij + " [ arrowhead=none,label=\"" + j + "\" ];\n");
out.print(nij + " [ shape=circle,width=0.1,height=0.1,label=\"\" ];\n");
k = -1;
for (Distribution distr : distrs) {
k++;
nijk = "n" + i + "_" + j + "_" + k;
out.print(nij + " -> " + nijk + " [ arrowhead=none,label=\"" + k + "\" ];\n");
out.print(nijk + " [ shape=point,label=\"\" ];\n");
for (Map.Entry<Integer, Double> e : distr) {
out.print(nijk + " -> " + e.getKey() + " [ label=\"" + e.getValue() + "\" ];\n");
} }
} }
} }
out.write("}\n");
out.close();
} catch (IOException e) {
throw new PrismException("Could not write " + getModelType() + " to file \"" + filename + "\"" + e);
} }
out.print("}\n");
} }
@Override
public void exportToDotFileWithStrat(PrismLog out, BitSet mark, int strat[])
{
throw new RuntimeException("Not yet supported");
}
@Override @Override
public void exportToPrismLanguage(String filename) throws PrismException public void exportToPrismLanguage(String filename) throws PrismException
{ {

274
prism/src/explicit/SubNondetModel.java
View File

@ -44,113 +44,125 @@ import prism.PrismException;
import prism.PrismLog; import prism.PrismLog;
import strat.MDStrategy; import strat.MDStrategy;
/*
/**
* Class for creating a sub-model of any NondetModel, please note the translate* methods * Class for creating a sub-model of any NondetModel, please note the translate* methods
* used to translate between state ids for model and sub-model. Created sub-model will have new * used to translate between state ids for model and sub-model. Created sub-model will have new
* state numbering from 0 to number of states in the sub model. * state numbering from 0 to number of states in the sub model.
*
*/ */
public class SubNondetModel implements NondetModel {
public class SubNondetModel implements NondetModel
{
private NondetModel model = null; private NondetModel model = null;
private BitSet states = null; private BitSet states = null;
private Map<Integer,BitSet> actions = null;
private Map<Integer, BitSet> actions = null;
private BitSet initialStates = null; private BitSet initialStates = null;
private List<State> statesList = null; private List<State> statesList = null;
private Map<Integer,Integer> stateLookupTable = new HashMap<Integer,Integer>();
private Map<Integer,Map<Integer,Integer>> actionLookupTable = new HashMap<Integer,Map<Integer,Integer>>();
private Map<Integer,Integer> inverseStateLookupTable = new HashMap<Integer,Integer>();
private Map<Integer, Integer> stateLookupTable = new HashMap<Integer, Integer>();
private Map<Integer, Map<Integer, Integer>> actionLookupTable = new HashMap<Integer, Map<Integer, Integer>>();
private Map<Integer, Integer> inverseStateLookupTable = new HashMap<Integer, Integer>();
private int numTransitions = 0; private int numTransitions = 0;
private int maxNumChoices = 0; private int maxNumChoices = 0;
private int numChoices = 0; private int numChoices = 0;
public SubNondetModel(NondetModel model, BitSet states, Map<Integer,BitSet> actions, BitSet initialStates) {
public SubNondetModel(NondetModel model, BitSet states, Map<Integer, BitSet> actions, BitSet initialStates)
{
this.model = model; this.model = model;
this.states = states; this.states = states;
this.actions = actions; this.actions = actions;
this.initialStates = initialStates; this.initialStates = initialStates;
generateStatistics(); generateStatistics();
generateLookupTable(states, actions); generateLookupTable(states, actions);
} }
@Override @Override
public ModelType getModelType() {
public ModelType getModelType()
{
return model.getModelType(); return model.getModelType();
} }
@Override @Override
public int getNumStates() {
public int getNumStates()
{
return states.cardinality(); return states.cardinality();
} }
@Override @Override
public int getNumInitialStates() {
public int getNumInitialStates()
{
return initialStates.cardinality(); return initialStates.cardinality();
} }
@Override @Override
public Iterable<Integer> getInitialStates() {
public Iterable<Integer> getInitialStates()
{
List<Integer> is = new ArrayList<Integer>(); List<Integer> is = new ArrayList<Integer>();
for(int i=initialStates.nextSetBit(0); i>=0; i=initialStates.nextSetBit(i+1)) {
for (int i = initialStates.nextSetBit(0); i >= 0; i = initialStates.nextSetBit(i + 1)) {
is.add(translateState(i)); is.add(translateState(i));
} }
return is; return is;
} }
@Override @Override
public int getFirstInitialState() {
public int getFirstInitialState()
{
return translateState(initialStates.nextSetBit(0)); return translateState(initialStates.nextSetBit(0));
} }
@Override @Override
public boolean isInitialState(int i) {
public boolean isInitialState(int i)
{
return initialStates.get(translateState(i)); return initialStates.get(translateState(i));
} }
@Override @Override
public int getNumDeadlockStates() {
public int getNumDeadlockStates()
{
throw new UnsupportedOperationException(); throw new UnsupportedOperationException();
} }
@Override @Override
public Iterable<Integer> getDeadlockStates() {
public Iterable<Integer> getDeadlockStates()
{
throw new UnsupportedOperationException(); throw new UnsupportedOperationException();
} }
@Override @Override
public StateValues getDeadlockStatesList() {
public StateValues getDeadlockStatesList()
{
throw new UnsupportedOperationException(); throw new UnsupportedOperationException();
} }
@Override @Override
public int getFirstDeadlockState() {
public int getFirstDeadlockState()
{
throw new UnsupportedOperationException(); throw new UnsupportedOperationException();
} }
@Override @Override
public boolean isDeadlockState(int i) {
public boolean isDeadlockState(int i)
{
throw new UnsupportedOperationException(); throw new UnsupportedOperationException();
} }
@Override @Override
public List<State> getStatesList() {
public List<State> getStatesList()
{
//We use lazy generation because in many cases the state list is not //We use lazy generation because in many cases the state list is not
//needed //needed
if(statesList == null) {
if (statesList == null) {
statesList = generateSubStateList(states); statesList = generateSubStateList(states);
} }
return statesList; return statesList;
} }
private List<State> generateSubStateList(BitSet states) {
private List<State> generateSubStateList(BitSet states)
{
List<State> statesList = new ArrayList<State>(); List<State> statesList = new ArrayList<State>();
for(int i=0;i<model.getNumStates();i++) {
if(states.get(i)) {
for (int i = 0; i < model.getNumStates(); i++) {
if (states.get(i)) {
statesList.add(model.getStatesList().get(i)); statesList.add(model.getStatesList().get(i));
} }
} }
@ -158,29 +170,33 @@ public class SubNondetModel implements NondetModel {
} }
@Override @Override
public Values getConstantValues() {
public Values getConstantValues()
{
throw new UnsupportedOperationException(); throw new UnsupportedOperationException();
} }
@Override @Override
public BitSet getLabelStates(String name) {
public BitSet getLabelStates(String name)
{
throw new UnsupportedOperationException(); throw new UnsupportedOperationException();
} }
@Override @Override
public int getNumTransitions() {
public int getNumTransitions()
{
return numTransitions; return numTransitions;
} }
@Override @Override
public Iterator<Integer> getSuccessorsIterator(int s) {
public Iterator<Integer> getSuccessorsIterator(int s)
{
s = translateState(s); s = translateState(s);
List<Integer> succ = new ArrayList<Integer>(); List<Integer> succ = new ArrayList<Integer>();
for(int i=0;i<model.getNumChoices(s);i++) {
if(actions.get(s).get(i)) {
Iterator<Entry<Integer,Double>> it = model.getTransitionsIterator(s,i);
while(it.hasNext()) {
for (int i = 0; i < model.getNumChoices(s); i++) {
if (actions.get(s).get(i)) {
Iterator<Entry<Integer, Double>> it = model.getTransitionsIterator(s, i);
while (it.hasNext()) {
int succc = it.next().getKey(); int succc = it.next().getKey();
succ.add(inverseTranslateState(succc)); succ.add(inverseTranslateState(succc));
} }
@ -188,114 +204,148 @@ public class SubNondetModel implements NondetModel {
} }
return succ.iterator(); return succ.iterator();
} }
@Override @Override
public boolean isSuccessor(int s1, int s2) {
public boolean isSuccessor(int s1, int s2)
{
s1 = translateState(s1); s1 = translateState(s1);
s2 = translateState(s2); s2 = translateState(s2);
return model.isSuccessor(s1, s2); return model.isSuccessor(s1, s2);
} }
@Override @Override
public boolean allSuccessorsInSet(int s, BitSet set) {
public boolean allSuccessorsInSet(int s, BitSet set)
{
throw new UnsupportedOperationException(); throw new UnsupportedOperationException();
} }
@Override @Override
public boolean someSuccessorsInSet(int s, BitSet set) {
public boolean someSuccessorsInSet(int s, BitSet set)
{
throw new UnsupportedOperationException(); throw new UnsupportedOperationException();
} }
@Override @Override
public void findDeadlocks(boolean fix) throws PrismException {
public void findDeadlocks(boolean fix) throws PrismException
{
throw new UnsupportedOperationException(); throw new UnsupportedOperationException();
} }
@Override @Override
public void checkForDeadlocks() throws PrismException {
public void checkForDeadlocks() throws PrismException
{
throw new UnsupportedOperationException(); throw new UnsupportedOperationException();
} }
@Override @Override
public void checkForDeadlocks(BitSet except) throws PrismException {
public void checkForDeadlocks(BitSet except) throws PrismException
{
throw new UnsupportedOperationException(); throw new UnsupportedOperationException();
} }
@Override @Override
public void exportToPrismExplicit(String baseFilename)
throws PrismException {
public void exportToPrismExplicit(String baseFilename) throws PrismException
{
throw new UnsupportedOperationException(); throw new UnsupportedOperationException();
} }
@Override @Override
public void exportToPrismExplicitTra(String filename) throws PrismException {
public void exportToPrismExplicitTra(String filename) throws PrismException
{
throw new UnsupportedOperationException(); throw new UnsupportedOperationException();
} }
@Override @Override
public void exportToPrismExplicitTra(File file) throws PrismException {
public void exportToPrismExplicitTra(File file) throws PrismException
{
throw new UnsupportedOperationException(); throw new UnsupportedOperationException();
} }
@Override @Override
public void exportToPrismExplicitTra(PrismLog log) {
public void exportToPrismExplicitTra(PrismLog log)
{
throw new UnsupportedOperationException(); throw new UnsupportedOperationException();
} }
@Override @Override
public void exportToDotFile(String filename) throws PrismException {
public void exportToDotFile(String filename) throws PrismException
{
throw new UnsupportedOperationException(); throw new UnsupportedOperationException();
} }
@Override @Override
public void exportToDotFile(String filename, BitSet mark)
throws PrismException {
public void exportToDotFile(String filename, BitSet mark) throws PrismException
{
throw new UnsupportedOperationException(); throw new UnsupportedOperationException();
} }
@Override @Override
public void exportToPrismLanguage(String filename) throws PrismException {
public void exportToDotFile(PrismLog out)
{
throw new UnsupportedOperationException(); throw new UnsupportedOperationException();
} }
@Override @Override
public void exportStates(int exportType, VarList varList, PrismLog log)
throws PrismException {
public void exportToDotFile(PrismLog out, BitSet mark)
{
throw new UnsupportedOperationException(); throw new UnsupportedOperationException();
} }
@Override @Override
public String infoString() {
public void exportToDotFileWithStrat(PrismLog out, BitSet mark, int strat[])
{
throw new UnsupportedOperationException();
}
@Override
public void exportToPrismLanguage(String filename) throws PrismException
{
throw new UnsupportedOperationException();
}
@Override
public void exportStates(int exportType, VarList varList, PrismLog log) throws PrismException
{
throw new UnsupportedOperationException();
}
@Override
public String infoString()
{
throw new UnsupportedOperationException(); throw new UnsupportedOperationException();
} }
@Override @Override
public String infoStringTable() {
public String infoStringTable()
{
throw new UnsupportedOperationException(); throw new UnsupportedOperationException();
} }
@Override @Override
public int getNumChoices(int s) {
public int getNumChoices(int s)
{
s = translateState(s); s = translateState(s);
return actions.get(s).cardinality(); return actions.get(s).cardinality();
} }
@Override @Override
public int getMaxNumChoices() {
public int getMaxNumChoices()
{
return maxNumChoices; return maxNumChoices;
} }
@Override @Override
public int getNumChoices() {
public int getNumChoices()
{
return numChoices; return numChoices;
} }
@Override @Override
public Object getAction(int s, int i) {
public Object getAction(int s, int i)
{
s = translateState(s); s = translateState(s);
i = translateAction(s, i); i = translateAction(s, i);
return model.getAction(s, i); return model.getAction(s, i);
} }
@ -306,7 +356,8 @@ public class SubNondetModel implements NondetModel {
} }
@Override @Override
public boolean allSuccessorsInSet(int s, int i, BitSet set) {
public boolean allSuccessorsInSet(int s, int i, BitSet set)
{
s = translateState(s); s = translateState(s);
i = translateAction(s, i); i = translateAction(s, i);
set = translateSet(set); set = translateSet(set);
@ -315,37 +366,41 @@ public class SubNondetModel implements NondetModel {
} }
@Override @Override
public boolean someSuccessorsInSet(int s, int i, BitSet set) {
public boolean someSuccessorsInSet(int s, int i, BitSet set)
{
s = translateState(s); s = translateState(s);
i = translateAction(s, i); i = translateAction(s, i);
set = translateSet(set); set = translateSet(set);
return model.someSuccessorsInSet(s, i, set); return model.someSuccessorsInSet(s, i, set);
} }
private BitSet translateSet(BitSet set) {
private BitSet translateSet(BitSet set)
{
BitSet translatedBitSet = new BitSet(); BitSet translatedBitSet = new BitSet();
for (int i = set.nextSetBit(0); i >= 0; i = set.nextSetBit(i+1)) {
translatedBitSet.set(translateState(i));
}
return translatedBitSet;
for (int i = set.nextSetBit(0); i >= 0; i = set.nextSetBit(i + 1)) {
translatedBitSet.set(translateState(i));
}
return translatedBitSet;
} }
private void generateStatistics() {
for(int i=0;i<model.getNumStates();i++) {
if(states.get(i)) {
private void generateStatistics()
{
for (int i = 0; i < model.getNumStates(); i++) {
if (states.get(i)) {
numTransitions += getTransitions(i); numTransitions += getTransitions(i);
numChoices += actions.get(i).cardinality(); numChoices += actions.get(i).cardinality();
maxNumChoices = Math.max(maxNumChoices, model.getNumChoices(i)); maxNumChoices = Math.max(maxNumChoices, model.getNumChoices(i));
} }
} }
} }
private int getTransitions(int state) {
private int getTransitions(int state)
{
int transitions = 0; int transitions = 0;
for(int i=0;i<model.getNumChoices(state);i++) {
Iterator<Entry<Integer,Double>> it = model.getTransitionsIterator(state, i);
while(it.hasNext()) {
for (int i = 0; i < model.getNumChoices(state); i++) {
Iterator<Entry<Integer, Double>> it = model.getTransitionsIterator(state, i);
while (it.hasNext()) {
it.next(); it.next();
transitions += 1; transitions += 1;
} }
@ -354,51 +409,56 @@ public class SubNondetModel implements NondetModel {
} }
@Override @Override
public Iterator<Entry<Integer, Double>> getTransitionsIterator(int s, int i) {
public Iterator<Entry<Integer, Double>> getTransitionsIterator(int s, int i)
{
s = translateState(s); s = translateState(s);
i = translateAction(s, i); i = translateAction(s, i);
Map<Integer,Double> distrs = new HashMap<Integer, Double>();
Iterator<Entry<Integer,Double>> it = model.getTransitionsIterator(s, i);
while(it.hasNext()) {
Map<Integer, Double> distrs = new HashMap<Integer, Double>();
Iterator<Entry<Integer, Double>> it = model.getTransitionsIterator(s, i);
while (it.hasNext()) {
Entry<Integer, Double> e = it.next(); Entry<Integer, Double> e = it.next();
int succ = inverseTranslateState(e.getKey()); int succ = inverseTranslateState(e.getKey());
distrs.put(succ, e.getValue()); distrs.put(succ, e.getValue());
} }
return distrs.entrySet().iterator(); return distrs.entrySet().iterator();
} }
@Override @Override
public Model constructInducedModel(MDStrategy strat) public Model constructInducedModel(MDStrategy strat)
{ {
throw new RuntimeException("Not implemented"); throw new RuntimeException("Not implemented");
} }
private void generateLookupTable(BitSet states, Map<Integer,BitSet> actions) {
for(int i=0;i < model.getNumStates();i++) {
if(states.get(i)) {
private void generateLookupTable(BitSet states, Map<Integer, BitSet> actions)
{
for (int i = 0; i < model.getNumStates(); i++) {
if (states.get(i)) {
inverseStateLookupTable.put(i, stateLookupTable.size()); inverseStateLookupTable.put(i, stateLookupTable.size());
stateLookupTable.put(stateLookupTable.size(),i);
Map<Integer,Integer> r = new HashMap<Integer,Integer>();
for(int j=0;j<model.getNumChoices(i);j++) {
if(actions.get(i).get(j)) {
r.put(r.size(),j);
stateLookupTable.put(stateLookupTable.size(), i);
Map<Integer, Integer> r = new HashMap<Integer, Integer>();
for (int j = 0; j < model.getNumChoices(i); j++) {
if (actions.get(i).get(j)) {
r.put(r.size(), j);
} }
} }
actionLookupTable.put(actionLookupTable.size(),r);
actionLookupTable.put(actionLookupTable.size(), r);
} }
} }
} }
public int translateState(int s) {
public int translateState(int s)
{
return stateLookupTable.get(s); return stateLookupTable.get(s);
} }
private int inverseTranslateState(int s) {
private int inverseTranslateState(int s)
{
return inverseStateLookupTable.get(s); return inverseStateLookupTable.get(s);
} }
public int translateAction(int s, int i) {
public int translateAction(int s, int i)
{
return actionLookupTable.get(s).get(i); return actionLookupTable.get(s).get(i);
} }
} }

12
prism/src/param/ParamModel.java
View File

@ -195,6 +195,18 @@ final class ParamModel extends ModelExplicit
throw new UnsupportedOperationException(); throw new UnsupportedOperationException();
} }
@Override
public void exportToDotFile(PrismLog out)
{
throw new UnsupportedOperationException();
}
@Override
public void exportToDotFile(PrismLog out, BitSet mark)
{
throw new UnsupportedOperationException();
}
@Override @Override
public void exportToPrismLanguage(String filename) throws PrismException public void exportToPrismLanguage(String filename) throws PrismException
{ {

14
prism/src/prism/Prism.java
View File

@ -155,7 +155,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
// Options for type of strategy export // Options for type of strategy export
public enum StrategyExportType { public enum StrategyExportType {
ACTIONS, INDICES, INDUCED_MODEL;
ACTIONS, INDICES, INDUCED_MODEL, DOT_FILE;
public String description() public String description()
{ {
switch (this) { switch (this) {
@ -165,6 +165,8 @@ public class Prism extends PrismComponent implements PrismSettingsListener
return "as indices"; return "as indices";
case INDUCED_MODEL: case INDUCED_MODEL:
return "as an induced model"; return "as an induced model";
case DOT_FILE:
return "as a dot file";
default: default:
return this.toString(); return this.toString();
} }
@ -2158,7 +2160,9 @@ public class Prism extends PrismComponent implements PrismSettingsListener
currentModelExpl.exportToPrismExplicitTra(tmpLog); currentModelExpl.exportToPrismExplicitTra(tmpLog);
break; break;
case Prism.EXPORT_MATLAB: case Prism.EXPORT_MATLAB:
throw new PrismException("Export not yet supported");
case Prism.EXPORT_DOT: case Prism.EXPORT_DOT:
currentModelExpl.exportToDotFile(tmpLog);
case Prism.EXPORT_MRMC: case Prism.EXPORT_MRMC:
case Prism.EXPORT_ROWS: case Prism.EXPORT_ROWS:
case Prism.EXPORT_DOT_STATES: case Prism.EXPORT_DOT_STATES:
@ -2997,6 +3001,9 @@ public class Prism extends PrismComponent implements PrismSettingsListener
case INDUCED_MODEL: case INDUCED_MODEL:
strat.exportInducedModel(tmpLog); strat.exportInducedModel(tmpLog);
break; break;
case DOT_FILE:
strat.exportDotFile(tmpLog);
break;
} }
if (file != null) if (file != null)
tmpLog.close(); tmpLog.close();
@ -3475,10 +3482,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
// create new file log or use main log // create new file log or use main log
PrismLog tmpLog; PrismLog tmpLog;
if (file != null) { if (file != null) {
tmpLog = new PrismFileLog(file.getPath(), append);
if (!tmpLog.ready()) {
throw new PrismException("Could not open file \"" + file + "\" for output");
}
tmpLog = PrismFileLog.create(file.getPath(), append);
} else { } else {
tmpLog = mainLog; tmpLog = mainLog;
} }

2
prism/src/prism/PrismCL.java
View File

@ -1825,6 +1825,8 @@ public class PrismCL implements PrismModelListener
exportStratType = StrategyExportType.INDICES; exportStratType = StrategyExportType.INDICES;
else if (optVal.equals("induced")) else if (optVal.equals("induced"))
exportStratType = StrategyExportType.INDUCED_MODEL; exportStratType = StrategyExportType.INDUCED_MODEL;
else if (optVal.equals("dot"))
exportStratType = StrategyExportType.DOT_FILE;
else else
throw new PrismException("Unknown value \"" + optVal + "\" provided for \"type\" option of -exportstrat"); throw new PrismException("Unknown value \"" + optVal + "\" provided for \"type\" option of -exportstrat");
} }

6
prism/src/strat/MDStrategyArray.java
View File

@ -103,6 +103,12 @@ public class MDStrategyArray extends MDStrategy
dtmcInd.exportToPrismExplicitTra(out); dtmcInd.exportToPrismExplicitTra(out);
} }
@Override
public void exportDotFile(PrismLog out)
{
model.exportToDotFileWithStrat(out, null, choices);
}
@Override @Override
public void clear() public void clear()
{ {

19
prism/src/strat/MDStrategyIV.java
View File

@ -26,9 +26,12 @@
package strat; package strat;
import java.io.FileNotFoundException;
import java.util.List; import java.util.List;
import prism.Model; import prism.Model;
import prism.Prism;
import prism.PrismException;
import prism.PrismLog; import prism.PrismLog;
import dv.IntegerVector; import dv.IntegerVector;
@ -42,7 +45,7 @@ public class MDStrategyIV extends MDStrategy
// Other model info // Other model info
private int numStates; private int numStates;
private List<String> actions; private List<String> actions;
// Array storing MD strategy (action index for each state)
// Array storing MD strategy: *action* index (not choice index) for each state
private IntegerVector iv; private IntegerVector iv;
/** /**
@ -106,6 +109,20 @@ public class MDStrategyIV extends MDStrategy
{ {
// TODO // TODO
} }
@Override
public void exportDotFile(PrismLog out)
{
try {
model.exportToFile(Prism.EXPORT_DOT, true, new java.io.File("a.dot"));
} catch (FileNotFoundException e) {
// TODO Auto-generated catch block
e.printStackTrace();
} catch (PrismException e) {
// TODO Auto-generated catch block
e.printStackTrace();
}
}
@Override @Override
public void clear() public void clear()

5
prism/src/strat/Strategy.java
View File

@ -54,6 +54,11 @@ public interface Strategy
*/ */
public void exportInducedModel(PrismLog out); public void exportInducedModel(PrismLog out);
/**
* Export the strategy to a dot file (of the model showing the strategy).
*/
public void exportDotFile(PrismLog out);
/** /**
* Initialise the strategy, based on an initial model state. * Initialise the strategy, based on an initial model state.
* @param s Initial state of the model * @param s Initial state of the model

Write Preview
Loading…
Cancel
Save