From 7f1315dfc1166d390c5c71f77b83ff3bf5c22157 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 18 Jun 2015 08:19:29 +0000 Subject: [PATCH] Do not allow any ExpressionQuant modifiers for now. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10035 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/visitor/SemanticCheck.java | 9 +++++++++ 1 file changed, 9 insertions(+) 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()); }