From 17b4d063d118fc09d613ae77cbfb7a7c690ec13f Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 5 May 2010 13:04:09 +0000 Subject: [PATCH] Simulator supports labels git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1880 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/NOTES | 15 ----- prism/NOTES-SIM | 10 +-- prism/examples/ctmdp/NOTES | 3 + prism/examples/explicit/NOTES | 2 + prism/examples/pta/brp/brp.pm | 2 +- prism/src/parser/ast/ASTElement.java | 11 +++ prism/src/parser/visitor/ExpandLabels.java | 78 ++++++++++++++++++++++ prism/src/simulator/SimulatorEngine.java | 6 +- 8 files changed, 103 insertions(+), 24 deletions(-) create mode 100644 prism/src/parser/visitor/ExpandLabels.java diff --git a/prism/NOTES b/prism/NOTES index 5b7c8ddd..23c9f7fd 100644 --- a/prism/NOTES +++ b/prism/NOTES @@ -20,21 +20,6 @@ See also: ----------------------------------------------------------------------- -Fixes/tidying needed before release to Kim: - -Processing TODOs: -Check STPGAR carefully (and then PTAAR subclass) -CTL stuff (even if only disable?) in NonProbMC -Tidy up, disable and/or remove PTA rewards stuff - -disable simulator neatly? - -and to Holger et al.: - -CTMDP stuff - ------------------------------------------------------------------------ - Filters, property semantics, etc. TODO: diff --git a/prism/NOTES-SIM b/prism/NOTES-SIM index a919cc01..a3a8319d 100644 --- a/prism/NOTES-SIM +++ b/prism/NOTES-SIM @@ -2,19 +2,15 @@ NOW/NEXT: -work on Sampler classes -need to get property constants sorted out -should be specified when passed to sim engine, like for models -but when are props passed to sim engine? diff for pathgen/sampling? -what about experiments, e.g. F<=t for t=...? - looping TODO: -explicitbuildtest doesn't handle dupes in mdps (e.fg. consensus) +add support "deadlock" and "init" (new EvaluationContext, model *and* state dependent) + +explicitbuildtest doesn't handle dupes in mdps (e.g. consensus) explicit build doesn't handle multiple initial states diff --git a/prism/examples/ctmdp/NOTES b/prism/examples/ctmdp/NOTES index 62803015..59d6821b 100644 --- a/prism/examples/ctmdp/NOTES +++ b/prism/examples/ctmdp/NOTES @@ -4,3 +4,6 @@ java -cp classes explicit.CTMDPModelChecker examples/ctmdp/Neu10.{tra,lab} targe java -cp classes explicit.CTMDPModelChecker examples/ctmdp/jsp.{tra,lab} done 10 -max + +prism examples/ctmdp/cluster.sm -csl 'const double T; P=? [ true U<=T !"minimum" ]' -const N=4,T=1000 +prism examples/ctmdp/cluster.sm -csl 'const double T; P=? [ true U<=T !"minimum" {"crit"} ]' -const N=4,T=1000 diff --git a/prism/examples/explicit/NOTES b/prism/examples/explicit/NOTES index d2510613..a9cd3f37 100644 --- a/prism/examples/explicit/NOTES +++ b/prism/examples/explicit/NOTES @@ -110,6 +110,8 @@ prism polling/poll5.sm -fixdl -exporttrans polling/poll5.tra -exportstates polli prism-ar polling/poll2 last_polled -ctmc -noopt prism-ar polling/poll5 last_polled -ctmc -noopt + prism-ar polling/poll2 last_polled -ctmc -noopt -exactcheck + -ctmc -probreachbnd=1 #================================================ diff --git a/prism/examples/pta/brp/brp.pm b/prism/examples/pta/brp/brp.pm index eae82496..09945670 100644 --- a/prism/examples/pta/brp/brp.pm +++ b/prism/examples/pta/brp/brp.pm @@ -10,7 +10,7 @@ const int MAX; // max time to send a message (transition delay) const int TD; // time out limit (greater than TD+TD - the max time to send a message and receive an ack) -const int TIME_OUT; +const int TIME_OUT = 2*TD + 1; module sender diff --git a/prism/src/parser/ast/ASTElement.java b/prism/src/parser/ast/ASTElement.java index a00471b0..56569874 100644 --- a/prism/src/parser/ast/ASTElement.java +++ b/prism/src/parser/ast/ASTElement.java @@ -316,6 +316,17 @@ public abstract class ASTElement return evaluatePartially(new EvaluateContextValues(null, varValues)); } + /** + * Expand labels, return result. + * Special labels "deadlock", "init" and any not in list are left. + * @param labelList: The LabelList for label definitions + */ + public ASTElement expandLabels(LabelList labelList) throws PrismLangException + { + ExpandLabels visitor = new ExpandLabels(labelList); + return (ASTElement) accept(visitor); + } + /** * Check for type-correctness and compute type. */ diff --git a/prism/src/parser/visitor/ExpandLabels.java b/prism/src/parser/visitor/ExpandLabels.java new file mode 100644 index 00000000..5a09c113 --- /dev/null +++ b/prism/src/parser/visitor/ExpandLabels.java @@ -0,0 +1,78 @@ +//============================================================================== +// +// 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 labels, return result. + * Special labels "deadlock", "init" and any not in list are left. + */ +public class ExpandLabels extends ASTTraverseModify +{ + // The LabelList for label definitions + private LabelList labelList; + + public ExpandLabels(LabelList labelList) + { + 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 the corresponding expression + expr = labelList.getLabel(i); + // 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) + expr = Expression.Parenth(expr); + // This is probably being done before type-checking so + // don't really need to preserve type, 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/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index 0f9a1355..d2c56bbc 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -611,8 +611,12 @@ public class SimulatorEngine */ public int addProperty(Expression prop, PropertiesFile pf) throws PrismException { - // Take a copy, get rid of any constants and simplify + // Take a copy Expression propNew = prop.deepCopy(); + // Combine label lists from model/property file, then remove labels from property + LabelList combinedLabelList = (pf == null) ? modulesFile.getLabelList() : pf.getCombinedLabelList(); + propNew = (Expression) propNew.expandLabels(combinedLabelList); + // Then get rid of any constants and simplify propNew = (Expression) propNew.replaceConstants(constants); if (pf != null) { propNew = (Expression) propNew.replaceConstants(pf.getConstantValues());