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

Some refactoring of the RelOp and ModelType enums. [from Steffen Marcker]] 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10616 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 11 years ago
parent
11c1a65260
commit
ce6131636e
2 changed files with 230 additions and 212 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. 197
      prism/src/parser/ast/RelOp.java
  2. 245
      prism/src/prism/ModelType.java

197
prism/src/parser/ast/RelOp.java
View File

@ -1,35 +1,121 @@
package parser.ast; package parser.ast;
import java.util.HashMap;
import java.util.Iterator;
import java.util.Map;
import java.util.Map.Entry;
import prism.PrismLangException; import prism.PrismLangException;
/** /**
* Class to represent a relational operator (or similar) found in a P/R/S operator. * Class to represent a relational operator (or similar) found in a P/R/S operator.
*/ */
public enum RelOp {
GT, GEQ, MIN, LEQ, LT, MAX, EQ;
protected static Map<RelOp, String> symbols;
static {
symbols = new HashMap<RelOp, String>();
symbols.put(RelOp.GT, ">");
symbols.put(RelOp.GEQ, ">=");
symbols.put(RelOp.MIN, "min=");
symbols.put(RelOp.LT, "<");
symbols.put(RelOp.LEQ, "<=");
symbols.put(RelOp.MAX, "max=");
symbols.put(RelOp.EQ, "=");
public enum RelOp
{
GT(">") {
@Override
public boolean isLowerBound()
{
return true;
}
@Override
public boolean isStrict()
{
return true;
}
@Override
public RelOp negate() throws PrismLangException
{
return LEQ;
}
},
GEQ(">=") {
@Override
public boolean isLowerBound()
{
return true;
}
@Override
public RelOp negate() throws PrismLangException
{
return LT;
}
},
MIN("min=") {
@Override
public boolean isMin()
{
return true;
}
@Override
public RelOp negate() throws PrismLangException
{
return MAX;
}
},
LT("<") {
@Override
public boolean isUpperBound()
{
return true;
}
@Override
public boolean isStrict()
{
return true;
}
@Override
public RelOp negate() throws PrismLangException
{
return GEQ;
}
},
LEQ("<=") {
@Override
public boolean isUpperBound()
{
return true;
}
@Override
public RelOp negate() throws PrismLangException
{
return GT;
}
},
MAX("max=") {
@Override
public boolean isMax()
{
return false;
}
@Override
public RelOp negate() throws PrismLangException
{
return MIN;
}
},
EQ("=") {
@Override
public RelOp negate() throws PrismLangException
{
throw new PrismLangException("Cannot negate " + this);
}
};
private final String symbol;
private RelOp(String symbol)
{
this.symbol = symbol;
} }
@Override @Override
public String toString() public String toString()
{ {
return symbols.get(this);
return symbol;
} }
/** /**
@ -38,13 +124,7 @@ public enum RelOp {
*/ */
public boolean isLowerBound() public boolean isLowerBound()
{ {
switch (this) {
case GT:
case GEQ:
return true;
default:
return false;
}
return false;
} }
/** /**
@ -53,13 +133,7 @@ public enum RelOp {
*/ */
public boolean isUpperBound() public boolean isUpperBound()
{ {
switch (this) {
case LT:
case LEQ:
return true;
default:
return false;
}
return false;
} }
/** /**
@ -67,13 +141,7 @@ public enum RelOp {
*/ */
public boolean isStrict() public boolean isStrict()
{ {
switch (this) {
case GT:
case LT:
return true;
default:
return false;
}
return false;
} }
/** /**
@ -81,12 +149,7 @@ public enum RelOp {
*/ */
public boolean isMin() public boolean isMin()
{ {
switch (this) {
case MIN:
return true;
default:
return false;
}
return false;
} }
/** /**
@ -94,38 +157,13 @@ public enum RelOp {
*/ */
public boolean isMax() public boolean isMax()
{ {
switch (this) {
case MAX:
return true;
default:
return false;
}
return false;
} }
/** /**
* Returns the negated form of this operator. * Returns the negated form of this operator.
*/ */
public RelOp negate() throws PrismLangException
{
switch (this) {
case GT:
return RelOp.LEQ;
case GEQ:
return RelOp.LT;
case MIN:
return RelOp.MAX;
case LT:
return RelOp.GEQ;
case LEQ:
return RelOp.GT;
case MAX:
return RelOp.MIN;
case EQ:
throw new PrismLangException("Cannot negate =");
default:
throw new PrismLangException("Cannot negate " + this);
}
}
public abstract RelOp negate() throws PrismLangException;
/** /**
* Returns the RelOp object corresponding to a (string) symbol, * Returns the RelOp object corresponding to a (string) symbol,
@ -135,12 +173,11 @@ public enum RelOp {
*/ */
public static RelOp parseSymbol(String symbol) public static RelOp parseSymbol(String symbol)
{ {
Iterator<Entry<RelOp, String>> it = symbols.entrySet().iterator();
while (it.hasNext()) {
Map.Entry<RelOp, String> e = it.next();
if (e.getValue().equals(symbol))
return e.getKey();
for (RelOp relop : RelOp.values()) {
if (relop.toString().equals(symbol)) {
return relop;
}
} }
return null; return null;
} }
}
}

245
prism/src/prism/ModelType.java
View File

@ -26,36 +26,114 @@
package prism; package prism;
public enum ModelType {
public enum ModelType
{
// List of model types (ordered alphabetically) // List of model types (ordered alphabetically)
CTMC, CTMDP, DTMC, LTS, MDP, PTA, STPG, SMG;
CTMC("continuous-time Markov chain") {
@Override
public boolean choicesSumToOne()
{
return false;
}
@Override
public boolean continuousTime()
{
return true;
}
@Override
public boolean nondeterministic()
{
return false;
}
@Override
public String probabilityOrRate()
{
return RATE;
}
},
CTMDP("continuous-time Markov decision process") {
@Override
public boolean choicesSumToOne()
{
return false;
}
@Override
public boolean continuousTime()
{
return true;
}
@Override
public String probabilityOrRate()
{
return RATE;
}
},
DTMC("discrete-time Markov chain") {
@Override
public boolean nondeterministic()
{
return false;
}
},
LTS("labelled transition system") {
@Override
public boolean isProbabilistic()
{
return false;
}
@Override
public String probabilityOrRate()
{
return NEITHER;
}
},
MDP("Markov decision process") {
},
PTA("probabilistic timed automaton") {
@Override
public boolean continuousTime()
{
return true;
}
},
STPG("stochastic two-player game") {
@Override
public boolean multiplePlayers()
{
return true;
}
},
SMG("stochastic multi-player game") {
@Override
public boolean multiplePlayers()
{
return true;
}
};
private static final String PROBABILITY = "Probability";
private static final String RATE = "Rate";
private static final String NEITHER = "";
private final String fullName;
ModelType(final String fullName) {
this.fullName = fullName;
}
/** /**
* Get the full name, in words, of the this model type. * Get the full name, in words, of the this model type.
*/ */
public String fullName() public String fullName()
{ {
switch (this) {
case CTMC:
return "continuous-time Markov chain";
case CTMDP:
return "continuous-time Markov decision process";
case DTMC:
return "discrete-time Markov chain";
case LTS:
return "labelled transition system";
case MDP:
return "Markov decision process";
case PTA:
return "probabilistic timed automaton";
case STPG:
return "stochastic two-player game";
case SMG:
return "stochastic multi-player game";
}
// Should never happen
return "";
return fullName;
} }
/** /**
@ -63,26 +141,7 @@ public enum ModelType {
*/ */
public String keyword() public String keyword()
{ {
switch (this) {
case CTMC:
return "ctmc";
case CTMDP:
return "ctmdp";
case DTMC:
return "dtmc";
case LTS:
return "lts";
case MDP:
return "mdp";
case PTA:
return "pta";
case STPG:
return "stpg";
case SMG:
return "smg";
}
// Should never happen
return "";
return this.name().toLowerCase();
} }
/** /**
@ -91,41 +150,15 @@ public enum ModelType {
*/ */
public boolean choicesSumToOne() public boolean choicesSumToOne()
{ {
switch (this) {
case DTMC:
case LTS:
case MDP:
case PTA:
case STPG:
case SMG:
return true;
case CTMC:
case CTMDP:
return false;
}
// Should never happen
return true; return true;
} }
/** /**
* Are time delay continuous for this model type?
* Are time delays continuous for this model type?
*/ */
public boolean continuousTime() public boolean continuousTime()
{ {
switch (this) {
case DTMC:
case LTS:
case MDP:
case STPG:
case SMG:
return false;
case PTA:
case CTMC:
case CTMDP:
return true;
}
// Should never happen
return true;
return false;
} }
/** /**
@ -133,19 +166,6 @@ public enum ModelType {
*/ */
public boolean nondeterministic() public boolean nondeterministic()
{ {
switch (this) {
case DTMC:
case CTMC:
return false;
case LTS:
case MDP:
case STPG:
case SMG:
case PTA:
case CTMDP:
return true;
}
// Should never happen
return true; return true;
} }
@ -154,20 +174,7 @@ public enum ModelType {
*/ */
public boolean multiplePlayers() public boolean multiplePlayers()
{ {
switch (this) {
case DTMC:
case CTMC:
case LTS:
case MDP:
case PTA:
case CTMDP:
return false;
case STPG:
case SMG:
return true;
}
// Should never happen
return true;
return false;
} }
/** /**
@ -175,50 +182,24 @@ public enum ModelType {
*/ */
public boolean isProbabilistic() public boolean isProbabilistic()
{ {
switch (this) {
case LTS:
return false;
default:
return true;
}
return true;
} }
/** /**
* Does this model have probabilities or rates? * Does this model have probabilities or rates?
* Returns "Probability" or "Rate", accordingly (or "" if there are neither) * Returns "Probability" or "Rate", accordingly (or "" if there are neither)
*/ */
public String probabilityOrRate() public String probabilityOrRate()
{ {
switch (this) {
case CTMC:
case CTMDP:
return "Rate";
case LTS:
return "";
default:
return "Probability";
}
return PROBABILITY;
} }
public static ModelType parseName(String name) public static ModelType parseName(String name)
{ {
if ("ctmc".equals(name))
return CTMC;
else if ("ctmdp".equals(name))
return CTMDP;
else if ("dtmc".equals(name))
return DTMC;
else if ("mdp".equals(name))
return MDP;
else if ("lts".equals(name))
return LTS;
else if ("pta".equals(name))
return PTA;
else if ("stpg".equals(name))
return STPG;
else if ("smg".equals(name))
return SMG;
else
try {
return valueOf(name.toUpperCase());
} catch (IllegalArgumentException e) {
return null; return null;
}
} }
}
}
Write Preview
Loading…
Cancel
Save