diff --git a/prism/src/parser/ast/RelOp.java b/prism/src/parser/ast/RelOp.java index 5dabb017..a4eb9843 100644 --- a/prism/src/parser/ast/RelOp.java +++ b/prism/src/parser/ast/RelOp.java @@ -1,35 +1,121 @@ package parser.ast; -import java.util.HashMap; -import java.util.Iterator; -import java.util.Map; -import java.util.Map.Entry; - import prism.PrismLangException; /** * 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 symbols; - static { - symbols = new HashMap(); - 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 public String toString() { - return symbols.get(this); + return symbol; } /** @@ -38,13 +124,7 @@ public enum RelOp { */ 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() { - switch (this) { - case LT: - case LEQ: - return true; - default: - return false; - } + return false; } /** @@ -67,13 +141,7 @@ public enum RelOp { */ 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() { - switch (this) { - case MIN: - return true; - default: - return false; - } + return false; } /** @@ -94,38 +157,13 @@ public enum RelOp { */ public boolean isMax() { - switch (this) { - case MAX: - return true; - default: - return false; - } + return false; } /** * 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, @@ -135,12 +173,11 @@ public enum RelOp { */ public static RelOp parseSymbol(String symbol) { - Iterator> it = symbols.entrySet().iterator(); - while (it.hasNext()) { - Map.Entry 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; } -} +} \ No newline at end of file diff --git a/prism/src/prism/ModelType.java b/prism/src/prism/ModelType.java index eaf85373..e112f2e6 100644 --- a/prism/src/prism/ModelType.java +++ b/prism/src/prism/ModelType.java @@ -26,36 +26,114 @@ package prism; -public enum ModelType { - +public enum ModelType +{ // 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. */ 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() { - 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() { - 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; } /** - * Are time delay continuous for this model type? + * Are time delays continuous for this model type? */ 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() { - 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; } @@ -154,20 +174,7 @@ public enum ModelType { */ 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() { - switch (this) { - case LTS: - return false; - default: - return true; - } + return true; } - + /** * Does this model have probabilities or rates? * Returns "Probability" or "Rate", accordingly (or "" if there are neither) */ 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) { - 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; + } } -} +} \ No newline at end of file