diff --git a/prism/src/parser/ast/ASTElement.java b/prism/src/parser/ast/ASTElement.java index 96135932..ff73c623 100644 --- a/prism/src/parser/ast/ASTElement.java +++ b/prism/src/parser/ast/ASTElement.java @@ -410,6 +410,16 @@ public abstract class ASTElement return (ASTElement) accept(visitor); } + /** + * Compute (maximum) number of nested probabilistic operators (P, S, R). + */ + public int computeProbNesting() throws PrismLangException + { + ComputeProbNesting visitor = new ComputeProbNesting(); + accept(visitor); + return visitor.getMaxNesting(); + } + /** * Convert to string showing tree representation. */ diff --git a/prism/src/parser/visitor/ComputeProbNesting.java b/prism/src/parser/visitor/ComputeProbNesting.java new file mode 100644 index 00000000..90142f96 --- /dev/null +++ b/prism/src/parser/visitor/ComputeProbNesting.java @@ -0,0 +1,84 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Oxford) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package parser.visitor; + +import parser.ast.*; +import prism.PrismLangException; + +/** + * Compute (maximum) number of nested probabilistic operators (P, S, R). + */ +public class ComputeProbNesting extends ASTTraverse +{ + private int currentNesting; + private int maxNesting; + + public ComputeProbNesting() + { + currentNesting = 0; + maxNesting = 0; + } + + public int getMaxNesting() + { + return maxNesting; + } + + public void visitPre(ExpressionProb e) throws PrismLangException + { + currentNesting++; + maxNesting = Math.max(maxNesting, currentNesting); + } + + public void visitPost(ExpressionProb e) throws PrismLangException + { + currentNesting--; + } + + public void visitPre(ExpressionReward e) throws PrismLangException + { + currentNesting++; + maxNesting = Math.max(maxNesting, currentNesting); + } + + public void visitPost(ExpressionReward e) throws PrismLangException + { + currentNesting--; + } + + public void visitPre(ExpressionSS e) throws PrismLangException + { + currentNesting++; + maxNesting = Math.max(maxNesting, currentNesting); + } + + public void visitPost(ExpressionSS e) throws PrismLangException + { + currentNesting--; + } +} + diff --git a/prism/src/pta/DigitalClocks.java b/prism/src/pta/DigitalClocks.java index 973d65dc..b0d88877 100644 --- a/prism/src/pta/DigitalClocks.java +++ b/prism/src/pta/DigitalClocks.java @@ -119,17 +119,14 @@ public class DigitalClocks { if (e.getOperand1().getType() instanceof TypeClock) { if (e.getOperand2().getType() instanceof TypeClock) { - throw new PrismLangException( - "Diagonal clock constraints are not allowed when using the digital clocks method", e); + throw new PrismLangException("Diagonal clock constraints are not allowed when using the digital clocks method", e); } else { if (e.getOperator() == ExpressionBinaryOp.GT || e.getOperator() == ExpressionBinaryOp.LT) - throw new PrismLangException( - "Strict clock constraints are not allowed when using the digital clocks method", e); + throw new PrismLangException("Strict clock constraints are not allowed when using the digital clocks method", e); } } else if (e.getOperand2().getType() instanceof TypeClock) { if (e.getOperator() == ExpressionBinaryOp.GT || e.getOperator() == ExpressionBinaryOp.LT) - throw new PrismLangException( - "Strict clock constraints are not allowed when using the digital clocks method", e); + throw new PrismLangException("Strict clock constraints are not allowed when using the digital clocks method", e); } } }; @@ -137,6 +134,14 @@ public class DigitalClocks if (propertiesFile != null) propertiesFile.accept(astt); + // Check that there are no nested probabilistic operators + // TODO: should be checking on individual properties really + if (propertiesFile != null) { + if (propertiesFile.computeProbNesting() > 1) { + throw new PrismLangException("Nested P operators are not allowed when using the digital clocks method"); + } + } + // Choose a new action label to represent time timeAction = "time"; while (modulesFile.getSynchs().contains(timeAction)) { @@ -165,8 +170,7 @@ public class DigitalClocks if (e.getDeclType() instanceof DeclarationClock) { int cMax = cci.getScaledClockMax(e.getName()); if (cMax < 0) - throw new PrismLangException("Clock " + e.getName() - + " is unbounded since there are no references to it in the model"); + throw new PrismLangException("Clock " + e.getName() + " is unbounded since there are no references to it in the model"); DeclarationType declType = new DeclarationInt(Expression.Int(0), Expression.Int(cMax + 1)); Declaration decl = new Declaration(e.getName(), declType); return decl; @@ -281,8 +285,7 @@ public class DigitalClocks continue; // TODO: handle this case if (rs.getNumTransItems() > 0) - throw new PrismLangException( - "Translation of reward structures with both state/transition items is not yet supported"); + throw new PrismLangException("Translation of reward structures with both state/transition items is not yet supported"); n = rs.getNumItems(); for (i = 0; i < n; i++) { RewardStructItem rsi = rs.getRewardStructItem(i); diff --git a/prism/src/pta/PTAModelChecker.java b/prism/src/pta/PTAModelChecker.java index e704f099..c30f849f 100644 --- a/prism/src/pta/PTAModelChecker.java +++ b/prism/src/pta/PTAModelChecker.java @@ -31,7 +31,9 @@ import java.util.*; import parser.*; import parser.ast.*; import parser.type.*; +import parser.visitor.ASTTraverseModify; import prism.*; +import simulator.sampler.Sampler; import explicit.*; /** @@ -49,7 +51,7 @@ public class PTAModelChecker private PropertiesFile propertiesFile; // Constants from model private Values constantValues; - // Label list + // Label list (combined: model/properties file) private LabelList labelList; // PTA private PTA pta; @@ -115,8 +117,28 @@ public class PTAModelChecker pta = m2pta.translate(); mainLog.println("\nPTA: " + pta.infoString()); + // Check for references to clocks - not allowed (yet) + // (do this before modifications below for better error reporting) + expr.accept(new ASTTraverseModify() + { + public Object visit(ExpressionVar e) throws PrismLangException + { + if (e.getType() instanceof TypeClock) { + throw new PrismLangException("Properties cannot contain references to clocks", e); + } else { + return e; + } + } + }); + + // Take a copy of property, since will modify + expr = expr.deepCopy(); + // Remove labels from property, using combined label list + expr = (Expression) expr.expandLabels(labelList); // Evaluate constants in property (easier to do now) - expr = (Expression) expr.deepCopy().replaceConstants(constantValues); + expr = (Expression) expr.replaceConstants(constantValues); + // Also simplify expression to optimise model checking + expr = (Expression) expr.simplify(); // Do model checking res = checkExpression(expr); @@ -177,9 +199,9 @@ public class PTAModelChecker if (!(expr.getExpression() instanceof ExpressionTemporal)) throw new PrismException("PTA model checking currently only supports the F path operator"); exprTemp = (ExpressionTemporal) expr.getExpression(); - if (exprTemp.getOperator() != ExpressionTemporal.P_F) + if (exprTemp.getOperator() != ExpressionTemporal.P_F || !exprTemp.isSimplePathFormula()) throw new PrismException("PTA model checking currently only supports the F path operator"); - + // Determine locations satisfying target exprTarget = exprTemp.getOperand2(); targetLocs = checkLocationExpression(exprTarget); @@ -314,6 +336,7 @@ public class PTAModelChecker /** * Determine which locations in the PTA satisfy a (Boolean) expression. * Note: This is rather inefficiently at the moment. + * TODO: potentially use explicit.StateMC on dummy model eventually */ private BitSet checkLocationExpression(Expression expr) throws PrismException { @@ -321,6 +344,7 @@ public class PTAModelChecker BitSet res; // Labels - expand and recurse + // (note: currently not used - these are expanded earlier) if (expr instanceof ExpressionLabel) { ExpressionLabel exprLabel = (ExpressionLabel) expr; if (exprLabel.getName().equals("deadlock")) diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index 86db159a..f7121c9a 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -33,7 +33,6 @@ import simulator.sampler.*; import parser.*; import parser.ast.*; import parser.type.*; -import parser.visitor.ASTTraverse; import prism.*; /** @@ -1081,41 +1080,20 @@ public class SimulatorEngine { // Simulator can only be applied to P=? or R=? properties boolean ok = true; - Expression expr = null; if (!(prop instanceof ExpressionProb || prop instanceof ExpressionReward)) ok = false; else if (prop instanceof ExpressionProb) { if ((((ExpressionProb) prop).getProb() != null)) ok = false; - expr = ((ExpressionProb) prop).getExpression(); } else if (prop instanceof ExpressionReward) { if ((((ExpressionReward) prop).getReward() != null)) ok = false; - expr = ((ExpressionReward) prop).getExpression(); } if (!ok) throw new PrismException("Simulator can only handle P=? or R=? properties"); // Check that there are no nested probabilistic operators - try { - expr.accept(new ASTTraverse() - { - public void visitPre(ExpressionProb e) throws PrismLangException - { - throw new PrismLangException(""); - } - - public void visitPre(ExpressionReward e) throws PrismLangException - { - throw new PrismLangException(""); - } - - public void visitPre(ExpressionSS e) throws PrismLangException - { - throw new PrismLangException(""); - } - }); - } catch (PrismLangException e) { + if (prop.computeProbNesting() > 1) { throw new PrismException("Simulator cannot handle nested P, R or S operators"); } }