Simulator supports labels

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1880 bbc10eb1-c90d-0410-af57-cb519fbb1720

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:

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
 

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

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
 
 #================================================

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
 

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.
 	 */

prism/src/parser/visitor/ExpandLabels.java

@@ -0,0 +1,78 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <david.parker@comlab.ox.ac.uk> (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;
+	}
+}
+

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());