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

Explicit models: Move exportToPrismLanguage methods to default implementations in interfaces.

accumulation-v4.7
Dave Parker 6 years ago
parent
d4cf7a59ee
commit
6ee3395544
13 changed files with 100 additions and 208 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 6
      prism/src/automata/LTSFromDA.java
  2. 35
      prism/src/explicit/DTMC.java
  3. 50
      prism/src/explicit/DTMCExplicit.java
  4. 7
      prism/src/explicit/LTS.java
  5. 7
      prism/src/explicit/LTSExplicit.java
  6. 42
      prism/src/explicit/MDP.java
  7. 53
      prism/src/explicit/MDPExplicit.java
  8. 3
      prism/src/explicit/ModelExplicit.java
  9. 7
      prism/src/explicit/STPG.java
  10. 7
      prism/src/explicit/STPGAbstrSimple.java
  11. 10
      prism/src/explicit/STPGExplicit.java
  12. 38
      prism/src/explicit/modelviews/DTMCView.java
  13. 43
      prism/src/explicit/modelviews/MDPView.java

6
prism/src/automata/LTSFromDA.java
View File

@ -133,12 +133,6 @@ public class LTSFromDA extends ModelExplicit implements LTS
throw new RuntimeException("Not implemented yet");
}
@Override
public void exportToPrismLanguage(String filename) throws PrismException
{
throw new RuntimeException("Not implemented yet");
}
// Methods to implement NondetModel
@Override

35
prism/src/explicit/DTMC.java
View File

@ -26,6 +26,8 @@
package explicit;
import java.io.FileWriter;
import java.io.IOException;
import java.util.*;
import java.util.Map.Entry;
import java.util.PrimitiveIterator.OfInt;
@ -101,6 +103,39 @@ public interface DTMC extends Model
}
}
@Override
default void exportToPrismLanguage(final String filename) throws PrismException
{
try (FileWriter out = new FileWriter(filename)) {
out.write(getModelType().keyword() + "\n");
out.write("module M\nx : [0.." + (getNumStates() - 1) + "];\n");
final TreeMap<Integer, Double> sorted = new TreeMap<Integer, Double>();
for (int state = 0, max = getNumStates(); state < max; state++) {
// Extract transitions and sort by destination state index (to match PRISM-exported files)
for (Iterator<Entry<Integer, Double>> transitions = getTransitionsIterator(state); transitions.hasNext();) {
final Entry<Integer, Double> transition = transitions.next();
sorted.put(transition.getKey(), transition.getValue());
}
// Print out (sorted) transitions
out.write("[]x=" + state + "->");
boolean first = true;
for (Entry<Integer, Double> transition : sorted.entrySet()) {
if (first)
first = false;
else
out.write("+");
// Note use of PrismUtils.formatDouble to match PRISM-exported files
out.write(PrismUtils.formatDouble(transition.getValue()) + ":(x'=" + transition.getKey() + ")");
}
out.write(";\n");
sorted.clear();
}
out.write("endmodule\n");
} catch (IOException e) {
throw new PrismException("Could not export " + getModelType() + " to file \"" + filename + "\"" + e);
}
}
// Accessors
/**

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

@ -26,68 +26,18 @@
package explicit;
import java.io.FileWriter;
import java.io.IOException;
import java.util.AbstractMap;
import java.util.Iterator;
import java.util.Map;
import java.util.TreeMap;
import java.util.Map.Entry;
import explicit.graphviz.Decorator;
import prism.Pair;
import prism.PrismException;
import prism.PrismLog;
import prism.PrismUtils;
/**
* Base class for explicit-state representations of a DTMC.
*/
public abstract class DTMCExplicit extends ModelExplicit implements DTMC
{
// Accessors (for Model)
@Override
public void exportToPrismLanguage(String filename) throws PrismException
{
int i;
boolean first;
FileWriter out;
TreeMap<Integer, Double> sorted;
try {
// Output transitions to PRISM language file
out = new FileWriter(filename);
out.write(getModelType().keyword() + "\n");
out.write("module M\nx : [0.." + (numStates - 1) + "];\n");
sorted = new TreeMap<Integer, Double>();
for (i = 0; i < numStates; i++) {
// Extract transitions and sort by destination state index (to match PRISM-exported files)
Iterator<Map.Entry<Integer, Double>> iter = getTransitionsIterator(i);
while (iter.hasNext()) {
Map.Entry<Integer, Double> e = iter.next();
sorted.put(e.getKey(), e.getValue());
}
// Print out (sorted) transitions
out.write("[]x=" + i + "->");
first = true;
for (Map.Entry<Integer, Double> e : sorted.entrySet()) {
if (first)
first = false;
else
out.write("+");
// Note use of PrismUtils.formatDouble to match PRISM-exported files
out.write(PrismUtils.formatDouble(e.getValue()) + ":(x'=" + e.getKey() + ")");
}
out.write(";\n");
sorted.clear();
}
out.write("endmodule\n");
out.close();
} catch (IOException e) {
throw new PrismException("Could not export " + getModelType() + " to file \"" + filename + "\"" + e);
}
}
// Accessors (for DTMC)
@Override

7
prism/src/explicit/LTS.java
View File

@ -30,6 +30,7 @@ import java.util.BitSet;
import java.util.Iterator;
import prism.ModelType;
import prism.PrismException;
import prism.PrismLog;
/**
@ -61,6 +62,12 @@ public interface LTS extends NondetModel
}
}
@Override
default void exportToPrismLanguage(String filename) throws PrismException
{
throw new UnsupportedOperationException();
}
// Accessors (for NondetModel) - default implementations
@Override

7
prism/src/explicit/LTSExplicit.java
View File

@ -168,11 +168,4 @@ public class LTSExplicit extends ModelExplicit implements LTS
{
throw new UnsupportedOperationException();
}
@Override
public void exportToPrismLanguage(String filename) throws PrismException
{
throw new UnsupportedOperationException();
}
}

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

@ -26,6 +26,8 @@
package explicit;
import java.io.FileWriter;
import java.io.IOException;
import java.util.ArrayList;
import java.util.BitSet;
import java.util.Iterator;
@ -41,6 +43,7 @@ import explicit.graphviz.Decorator;
import explicit.rewards.MCRewards;
import explicit.rewards.MDPRewards;
import prism.ModelType;
import prism.PrismException;
import prism.PrismLog;
import prism.PrismUtils;
@ -135,6 +138,45 @@ public interface MDP extends MDPGeneric<Double>
}
}
@Override
default void exportToPrismLanguage(final String filename) throws PrismException
{
try (FileWriter out = new FileWriter(filename)) {
// Output transitions to PRISM language file
out.write(getModelType().keyword() + "\n");
final int numStates = getNumStates();
out.write("module M\nx : [0.." + (numStates - 1) + "];\n");
final TreeMap<Integer, Double> sorted = new TreeMap<Integer, Double>();
for (int state = 0; state < numStates; state++) {
for (int choice = 0, numChoices = getNumChoices(state); choice < numChoices; choice++) {
// Extract transitions and sort by destination state index (to match PRISM-exported files)
for (Iterator<Entry<Integer, Double>> transitions = getTransitionsIterator(state, choice); transitions.hasNext();) {
final Entry<Integer, Double> trans = transitions.next();
sorted.put(trans.getKey(), trans.getValue());
}
// Print out (sorted) transitions
final Object action = getAction(state, choice);
out.write(action != null ? ("[" + action + "]") : "[]");
out.write("x=" + state + "->");
boolean first = true;
for (Entry<Integer, Double> e : sorted.entrySet()) {
if (first)
first = false;
else
out.write("+");
// Note use of PrismUtils.formatDouble to match PRISM-exported files
out.write(PrismUtils.formatDouble(e.getValue()) + ":(x'=" + e.getKey() + ")");
}
out.write(";\n");
sorted.clear();
}
}
out.write("endmodule\n");
} catch (IOException e) {
throw new PrismException("Could not export " + getModelType() + " to file \"" + filename + "\"" + e);
}
}
// Accessors (for NondetModel) - default implementations
@Override

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

@ -27,14 +27,8 @@
package explicit;
import java.io.FileWriter;
import java.io.IOException;
import java.util.HashSet;
import java.util.Iterator;
import java.util.Map;
import java.util.TreeMap;
import prism.PrismException;
import prism.PrismUtils;
import strat.MDStrategy;
@ -67,53 +61,6 @@ public abstract class MDPExplicit extends ModelExplicit implements MDP
return s;
}
@Override
public void exportToPrismLanguage(String filename) throws PrismException
{
int i, j, numChoices;
boolean first;
FileWriter out;
TreeMap<Integer, Double> sorted;
Object action;
try {
// Output transitions to PRISM language file
out = new FileWriter(filename);
out.write(getModelType().keyword() + "\n");
out.write("module M\nx : [0.." + (numStates - 1) + "];\n");
sorted = new TreeMap<Integer, Double>();
for (i = 0; i < numStates; i++) {
numChoices = getNumChoices(i);
for (j = 0; j < numChoices; j++) {
// Extract transitions and sort by destination state index (to match PRISM-exported files)
Iterator<Map.Entry<Integer, Double>> iter = getTransitionsIterator(i, j);
while (iter.hasNext()) {
Map.Entry<Integer, Double> e = iter.next();
sorted.put(e.getKey(), e.getValue());
}
// Print out (sorted) transitions
action = getAction(i, j);
out.write(action != null ? ("[" + action + "]") : "[]");
out.write("x=" + i + "->");
first = true;
for (Map.Entry<Integer, Double> e : sorted.entrySet()) {
if (first)
first = false;
else
out.write("+");
// Note use of PrismUtils.formatDouble to match PRISM-exported files
out.write(PrismUtils.formatDouble(e.getValue()) + ":(x'=" + e.getKey() + ")");
}
out.write(";\n");
sorted.clear();
}
}
out.write("endmodule\n");
out.close();
} catch (IOException e) {
throw new PrismException("Could not export " + getModelType() + " to file \"" + filename + "\"" + e);
}
}
// Accessors (for NondetModel)
@Override

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

@ -355,9 +355,6 @@ public abstract class ModelExplicit implements Model
@Override
public abstract void checkForDeadlocks(BitSet except) throws PrismException;
@Override
public abstract void exportToPrismLanguage(String filename) throws PrismException;
@Override
public void exportStates(int exportType, VarList varList, PrismLog log) throws PrismException
{

7
prism/src/explicit/STPG.java
View File

@ -35,6 +35,7 @@ import java.util.Map.Entry;
import explicit.rewards.STPGRewards;
import prism.ModelType;
import prism.PrismException;
import prism.PrismLog;
import prism.PrismUtils;
@ -95,6 +96,12 @@ public interface STPG extends NondetModel
}
}
@Override
default void exportToPrismLanguage(final String filename) throws PrismException
{
throw new UnsupportedOperationException();
}
// Accessors
/**

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

@ -35,7 +35,6 @@ import common.IterableStateSet;
import explicit.rewards.STPGRewards;
import prism.PrismException;
import prism.PrismNotSupportedException;
import prism.PrismLog;
import prism.PrismUtils;
import strat.MDStrategy;
@ -390,12 +389,6 @@ public class STPGAbstrSimple extends ModelExplicit implements STPG, NondetModelS
throw new RuntimeException("Not yet supported");
}
@Override
public void exportToPrismLanguage(String filename) throws PrismException
{
throw new PrismNotSupportedException("Export to STPG PRISM models not supported");
}
@Override
public String infoString()
{

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

@ -36,6 +36,7 @@ import java.util.Map.Entry;
import explicit.rewards.MDPRewards;
import explicit.rewards.STPGRewards;
import prism.ModelType;
import prism.PrismException;
import prism.PrismLog;
/**
@ -43,7 +44,7 @@ import prism.PrismLog;
*/
public class STPGExplicit extends MDPSimple implements STPG
{
/** Which player owns each state, i.e. stateOwners[i] is owned by player i (1 or 2) */
/** Which player owns each state,fl i.e. stateOwners[i] is owned by player i (1 or 2) */
protected List<Integer> stateOwners;
// Constructors
@ -163,6 +164,13 @@ public class STPGExplicit extends MDPSimple implements STPG
STPG.super.exportToPrismExplicitTra(out);
}
@Override
public void exportToPrismLanguage(final String filename) throws PrismException
{
// Resolve conflict: STPG interface does not (currently) extend MDP
STPG.super.exportToPrismLanguage(filename);
}
// Accessors (for STPG)
@Override

38
prism/src/explicit/modelviews/DTMCView.java
View File

@ -27,13 +27,10 @@
package explicit.modelviews;
import java.io.FileWriter;
import java.io.IOException;
import java.util.AbstractMap;
import java.util.Iterator;
import java.util.Map.Entry;
import java.util.PrimitiveIterator;
import java.util.TreeMap;
import java.util.function.IntFunction;
import common.IterableStateSet;
@ -43,8 +40,6 @@ import explicit.DTMC;
import explicit.Distribution;
import explicit.SuccessorsIterator;
import prism.Pair;
import prism.PrismException;
import prism.PrismUtils;
/**
* Base class for a DTMC view, i.e., a virtual DTMC that is obtained
@ -117,39 +112,6 @@ public abstract class DTMCView extends ModelView implements DTMC, Cloneable
}, true);
}
@Override
public void exportToPrismLanguage(final String filename) throws PrismException
{
try (FileWriter out = new FileWriter(filename)) {
out.write(getModelType().keyword() + "\n");
out.write("module M\nx : [0.." + (getNumStates() - 1) + "];\n");
final TreeMap<Integer, Double> sorted = new TreeMap<Integer, Double>();
for (int state = 0, max = getNumStates(); state < max; state++) {
// Extract transitions and sort by destination state index (to match PRISM-exported files)
for (Iterator<Entry<Integer, Double>> transitions = getTransitionsIterator(state); transitions.hasNext();) {
final Entry<Integer, Double> transition = transitions.next();
sorted.put(transition.getKey(), transition.getValue());
}
// Print out (sorted) transitions
out.write("[]x=" + state + "->");
boolean first = true;
for (Entry<Integer, Double> transition : sorted.entrySet()) {
if (first)
first = false;
else
out.write("+");
// Note use of PrismUtils.formatDouble to match PRISM-exported files
out.write(PrismUtils.formatDouble(transition.getValue()) + ":(x'=" + transition.getKey() + ")");
}
out.write(";\n");
sorted.clear();
}
out.write("endmodule\n");
} catch (IOException e) {
throw new PrismException("Could not export " + getModelType() + " to file \"" + filename + "\"" + e);
}
}
@Override
public String infoString()
{

43
prism/src/explicit/modelviews/MDPView.java
View File

@ -27,13 +27,10 @@
package explicit.modelviews;
import java.io.FileWriter;
import java.io.IOException;
import java.util.HashSet;
import java.util.Iterator;
import java.util.Map.Entry;
import java.util.PrimitiveIterator;
import java.util.TreeMap;
import common.IteratorTools;
import explicit.DTMCFromMDPAndMDStrategy;
@ -41,7 +38,6 @@ import explicit.Distribution;
import explicit.MDP;
import explicit.Model;
import explicit.SuccessorsIterator;
import prism.PrismException;
import prism.PrismUtils;
import strat.MDStrategy;
@ -107,45 +103,6 @@ public abstract class MDPView extends ModelView implements MDP, Cloneable
return numTransitions;
}
@Override
public void exportToPrismLanguage(final String filename) throws PrismException
{
try (FileWriter out = new FileWriter(filename)) {
// Output transitions to PRISM language file
out.write(getModelType().keyword() + "\n");
final int numStates = getNumStates();
out.write("module M\nx : [0.." + (numStates - 1) + "];\n");
final TreeMap<Integer, Double> sorted = new TreeMap<Integer, Double>();
for (int state = 0; state < numStates; state++) {
for (int choice = 0, numChoices = getNumChoices(state); choice < numChoices; choice++) {
// Extract transitions and sort by destination state index (to match PRISM-exported files)
for (Iterator<Entry<Integer, Double>> transitions = getTransitionsIterator(state, choice); transitions.hasNext();) {
final Entry<Integer, Double> trans = transitions.next();
sorted.put(trans.getKey(), trans.getValue());
}
// Print out (sorted) transitions
final Object action = getAction(state, choice);
out.write(action != null ? ("[" + action + "]") : "[]");
out.write("x=" + state + "->");
boolean first = true;
for (Entry<Integer, Double> e : sorted.entrySet()) {
if (first)
first = false;
else
out.write("+");
// Note use of PrismUtils.formatDouble to match PRISM-exported files
out.write(PrismUtils.formatDouble(e.getValue()) + ":(x'=" + e.getKey() + ")");
}
out.write(";\n");
sorted.clear();
}
}
out.write("endmodule\n");
} catch (IOException e) {
throw new PrismException("Could not export " + getModelType() + " to file \"" + filename + "\"" + e);
}
}
@Override
public String infoString()
{

Write Preview
Loading…
Cancel
Save