From a3d99e62d01a1faba16ad7f007c5d950ded2609a Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sat, 28 Jan 2012 00:53:31 +0000 Subject: [PATCH] Add property reference support to PTA ans approx model checking. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4507 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/CHANGELOG.txt | 2 +- prism/src/parser/ast/ASTElement.java | 13 +++ .../visitor/ExpandPropRefsAndLabels.java | 110 ++++++++++++++++++ prism/src/pta/PTAModelChecker.java | 4 +- prism/src/simulator/SimulatorEngine.java | 4 +- 5 files changed, 128 insertions(+), 5 deletions(-) create mode 100644 prism/src/parser/visitor/ExpandPropRefsAndLabels.java diff --git a/prism/CHANGELOG.txt b/prism/CHANGELOG.txt index ed6797b0..130891a4 100644 --- a/prism/CHANGELOG.txt +++ b/prism/CHANGELOG.txt @@ -17,12 +17,12 @@ Changes: * GUI on Macs uses Cmd, not Ctrl * Added prominence given to log warning messages in command-line/GUI * Command-line scripts can signal termination via growlnotify/notify-send +* Properties can be named, by prefixing with "name":, and reference each other Ongoing changes: * Need to decide on switch options format for -exportresults * Handling of verbosity in log: PrismLog updated, not used yet -* Properties can be named, by prefixing with "name":, and reference each other * CTL AG/EF ----------------------------------------------------------------------------- diff --git a/prism/src/parser/ast/ASTElement.java b/prism/src/parser/ast/ASTElement.java index 18fdf107..f1e0c390 100644 --- a/prism/src/parser/ast/ASTElement.java +++ b/prism/src/parser/ast/ASTElement.java @@ -379,6 +379,19 @@ public abstract class ASTElement return v; } + /** + * Expand property references and labels, return result. + * Property expansion is done recursively. + * Special labels "deadlock", "init" and any not in label list are left. + * @param propertiesFile The PropertiesFile for property lookup + * @param labelList The LabelList for label definitions + */ + public ASTElement expandPropRefsAndLabels(PropertiesFile propertiesFile, LabelList labelList) throws PrismLangException + { + ExpandPropRefsAndLabels visitor = new ExpandPropRefsAndLabels(propertiesFile, labelList); + return (ASTElement) accept(visitor); + } + /** * Find all references to action labels, check they exist and, if required, * store their index locally (as defined by the containing ModuleFile). diff --git a/prism/src/parser/visitor/ExpandPropRefsAndLabels.java b/prism/src/parser/visitor/ExpandPropRefsAndLabels.java new file mode 100644 index 00000000..27641674 --- /dev/null +++ b/prism/src/parser/visitor/ExpandPropRefsAndLabels.java @@ -0,0 +1,110 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Oxford, formerly University of Birmingham) +// +//------------------------------------------------------------------------------ +// +// 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 parser.type.*; +import prism.PrismLangException; + +/** + * Expand property references and labels, return result. + * Property expansion is done recursively. + * Special labels "deadlock", "init" and any not in label list are left. + */ +public class ExpandPropRefsAndLabels extends ASTTraverseModify +{ + // The PropertiesFile for property lookup + private PropertiesFile propertiesFile; + // The LabelList for label definitions + private LabelList labelList; + + public ExpandPropRefsAndLabels(PropertiesFile propertiesFile, LabelList labelList) + { + this.propertiesFile = propertiesFile; + this.labelList = labelList; + } + + public Object visit(ExpressionLabel e) throws PrismLangException + { + int i; + Type t; + Expression expr; + + // See if identifier corresponds to a label + i = labelList.getLabelIndex(e.getName()); + if (i != -1) { + // If so, replace it with (a copy of) the corresponding expression + expr = labelList.getLabel(i).deepCopy(); + // But also recursively expand that + // (nested labels not currently supported but may be one day) + // (don't clone it to avoid duplication of work) + expr = (Expression)expr.expandLabels(labelList); + // Put in brackets so precedence is preserved + // (for display purposes only; in case of re-parse) + // Also, preserve type (this is probably being done before + // type-checking so unnecessary, but do so just in case) + t = expr.getType(); + expr = Expression.Parenth(expr); + expr.setType(t); + // Return replacement expression + return expr; + } + + // Couldn't find definition - leave unchanged. + return e; + } + + public Object visit(ExpressionProp e) throws PrismLangException + { + Property prop; + Type t; + Expression expr; + + // See if name corresponds to a property + prop = propertiesFile.lookUpPropertyObjectByName(e.getName()); + if (prop != null) { + // If so, replace it with (a copy of) the corresponding expression + expr = prop.getExpression().deepCopy(); + // But also recursively expand that + // (don't clone it to avoid duplication of work) + expr = (Expression)expr.expandPropRefsAndLabels(propertiesFile, labelList); + // Put in brackets so precedence is preserved + // (for display purposes only; in case of re-parse) + // Also, preserve type (this is probably being done before + // type-checking so unnecessary, but do so just in case) + t = expr.getType(); + expr = Expression.Parenth(expr); + expr.setType(t); + // Return replacement expression + return expr; + } + + // Couldn't find definition - leave unchanged. + return e; + } +} + diff --git a/prism/src/pta/PTAModelChecker.java b/prism/src/pta/PTAModelChecker.java index 2cbebb3f..2e39099a 100644 --- a/prism/src/pta/PTAModelChecker.java +++ b/prism/src/pta/PTAModelChecker.java @@ -133,8 +133,8 @@ public class PTAModelChecker // Take a copy of property, since will modify expr = expr.deepCopy(); - // Remove labels from property, using combined label list - expr = (Expression) expr.expandLabels(labelList); + // Remove property refs ands labels from property + expr = (Expression) expr.expandPropRefsAndLabels(propertiesFile, labelList); // Evaluate constants in property (easier to do now) expr = (Expression) expr.replaceConstants(constantValues); // Also simplify expression to optimise model checking diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index 7a52e242..f1d7cecc 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -530,9 +530,9 @@ public class SimulatorEngine { // Take a copy Expression propNew = prop.deepCopy(); - // Combine label lists from model/property file, then remove labels from property + // Combine label lists from model/property file, then expand property refs/labels in property LabelList combinedLabelList = (pf == null) ? modulesFile.getLabelList() : pf.getCombinedLabelList(); - propNew = (Expression) propNew.expandLabels(combinedLabelList); + propNew = (Expression) propNew.expandPropRefsAndLabels(pf, combinedLabelList); // Then get rid of any constants and simplify propNew = (Expression) propNew.replaceConstants(mfConstants); if (pf != null) {