|
|
|
@ -441,6 +441,9 @@ public class SemanticCheck extends ASTTraverse |
|
|
|
|
|
|
|
public void visitPost(ExpressionProb e) throws PrismLangException |
|
|
|
{ |
|
|
|
if (e.getModifier() != null) { |
|
|
|
throw new PrismLangException("Modifier \"" + e.getModifier() + "\" not supported for P operator"); |
|
|
|
} |
|
|
|
if (e.getProb() != null && !e.getProb().isConstant()) { |
|
|
|
throw new PrismLangException("P operator probability bound is not constant", e.getProb()); |
|
|
|
} |
|
|
|
@ -448,6 +451,9 @@ public class SemanticCheck extends ASTTraverse |
|
|
|
|
|
|
|
public void visitPost(ExpressionReward e) throws PrismLangException |
|
|
|
{ |
|
|
|
if (e.getModifier() != null) { |
|
|
|
throw new PrismLangException("Modifier \"" + e.getModifier() + "\" not supported for P operator"); |
|
|
|
} |
|
|
|
if (e.getRewardStructIndex() != null) { |
|
|
|
if (e.getRewardStructIndex() instanceof Expression) { |
|
|
|
Expression rsi = (Expression) e.getRewardStructIndex(); |
|
|
|
@ -481,6 +487,9 @@ public class SemanticCheck extends ASTTraverse |
|
|
|
|
|
|
|
public void visitPost(ExpressionSS e) throws PrismLangException |
|
|
|
{ |
|
|
|
if (e.getModifier() != null) { |
|
|
|
throw new PrismLangException("Modifier \"" + e.getModifier() + "\" not supported for P operator"); |
|
|
|
} |
|
|
|
if (e.getProb() != null && !e.getProb().isConstant()) { |
|
|
|
throw new PrismLangException("S operator probability bound is not constant", e.getProb()); |
|
|
|
} |
|
|
|
|