Browse Source

Minor refactoring (allow PrismLangException to thrown instead of PrismException). [from Steffen Marcker]

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10606 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 11 years ago
parent
commit
7f3862e636
  1. 5
      prism/src/parser/ast/ExpressionProb.java
  2. 8
      prism/src/prism/OpRelOpBound.java

5
prism/src/parser/ast/ExpressionProb.java

@ -30,7 +30,6 @@ import parser.EvaluateContext;
import parser.Values; import parser.Values;
import parser.visitor.ASTVisitor; import parser.visitor.ASTVisitor;
import prism.OpRelOpBound; import prism.OpRelOpBound;
import prism.PrismException;
import prism.PrismLangException; import prism.PrismLangException;
public class ExpressionProb extends ExpressionQuant public class ExpressionProb extends ExpressionQuant
@ -80,12 +79,12 @@ public class ExpressionProb extends ExpressionQuant
} }
@Override @Override
public OpRelOpBound getRelopBoundInfo(Values constantValues) throws PrismException
public OpRelOpBound getRelopBoundInfo(Values constantValues) throws PrismLangException
{ {
if (getBound() != null) { if (getBound() != null) {
double boundVal = getBound().evaluateDouble(constantValues); double boundVal = getBound().evaluateDouble(constantValues);
if (boundVal < 0 || boundVal > 1) if (boundVal < 0 || boundVal > 1)
throw new PrismException("Invalid probability bound " + boundVal + " in P operator");
throw new PrismLangException("Invalid probability bound " + boundVal + " in P operator");
return new OpRelOpBound("P", getRelOp(), boundVal); return new OpRelOpBound("P", getRelOp(), boundVal);
} else { } else {
return new OpRelOpBound("P", getRelOp(), null); return new OpRelOpBound("P", getRelOp(), null);

8
prism/src/prism/OpRelOpBound.java

@ -78,21 +78,21 @@ public class OpRelOpBound
return false; return false;
} }
public MinMax getMinMax(ModelType modelType) throws PrismException
public MinMax getMinMax(ModelType modelType) throws PrismLangException
{ {
return getMinMax(modelType, true); return getMinMax(modelType, true);
} }
public MinMax getMinMax(ModelType modelType, boolean forAll) throws PrismException
public MinMax getMinMax(ModelType modelType, boolean forAll) throws PrismLangException
{ {
MinMax minMax = MinMax.blank(); MinMax minMax = MinMax.blank();
if (modelType.nondeterministic()) { if (modelType.nondeterministic()) {
if (!(modelType == ModelType.MDP || modelType == ModelType.CTMDP)) { if (!(modelType == ModelType.MDP || modelType == ModelType.CTMDP)) {
throw new PrismException("Don't know how to model check " + getTypeOfOperator() + " properties for " + modelType + "s");
throw new PrismLangException("Don't know how to model check " + getTypeOfOperator() + " properties for " + modelType + "s");
} }
if (isNumeric()) { if (isNumeric()) {
if (relOp == RelOp.EQ) { if (relOp == RelOp.EQ) {
throw new PrismException("Can't use \"" + op + "=?\" for nondeterministic models; use e.g. \"" + op + "min=?\" or \"" + op + "max=?\"");
throw new PrismLangException("Can't use \"" + op + "=?\" for nondeterministic models; use e.g. \"" + op + "min=?\" or \"" + op + "max=?\"");
} }
minMax = relOp.isMin() ? MinMax.min() : MinMax.max(); minMax = relOp.isMin() ? MinMax.min() : MinMax.max();
} else { } else {

Loading…
Cancel
Save