diff --git a/prism/src/parser/visitor/SemanticCheck.java b/prism/src/parser/visitor/SemanticCheck.java index 8a3d43cf..c1399e7d 100644 --- a/prism/src/parser/visitor/SemanticCheck.java +++ b/prism/src/parser/visitor/SemanticCheck.java @@ -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()); }