Properties files can use model file formulas. Model files can contain labels.

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

prism/src/parser/ExpressionFormula.java

@@ -98,10 +98,8 @@ public class ExpressionFormula extends Expression
 			// return replacement expression
 			return e;
 		}
-		else {
-			// error (should never happen)
-			throw new PrismException("Formula \"" + name + "\" undefined");
-		}
+		
+		return this;
 	}
 	
 	// create and return a new expression by renaming

prism/src/parser/FormulaList.java

@@ -83,12 +83,18 @@ public class FormulaList
 	// (inside the formulas in this formula list)
 	
 	public void findAllFormulas() throws PrismException
+	{ findAllFormulas(this); }
+
+	// find all formulas (i.e. locate idents which are formulas)
+	// (from the specified formula list)
+	
+	public void findAllFormulas(FormulaList fl) throws PrismException
 	{
 		int i, n;
 		
 		n = formulas.size();
 		for (i = 0; i < n; i++) {
-			formulas.setElementAt(getFormula(i).findAllFormulas(this), i);
+			formulas.setElementAt(getFormula(i).findAllFormulas(fl), i);
 		}
 	}
 
@@ -159,12 +165,15 @@ public class FormulaList
 	// expand any formulas
 	
 	public void expandFormulas() throws PrismException
+	{ expandFormulas(this); }
+	
+	public void expandFormulas(FormulaList fl) throws PrismException
 	{
 		int i, n;
 		
 		n = formulas.size();
 		for (i = 0; i < n; i++) {
-			formulas.setElementAt(getFormula(i).expandFormulas(this), i);
+			formulas.setElementAt(getFormula(i).expandFormulas(fl), i);
 		}
 	}
 

prism/src/parser/LabelList.java

@@ -79,6 +79,35 @@ public class LabelList
 		return names.indexOf(s);
 	}
 
+	// find all formulas (i.e. locate idents which are formulas)
+	// (inside the expressions in this label list)
+	
+	public void findAllFormulas(FormulaList formulaList) throws PrismException
+	{
+		int i, n;
+		Expression e;
+		
+		n = labels.size();
+		for (i = 0; i < n; i++) {
+			e = getLabel(i);
+			labels.setElementAt(e.findAllFormulas(formulaList), i);
+		}
+	}
+
+	// expand any formulas
+	
+	public void expandFormulas(FormulaList formulaList) throws PrismException
+	{
+		int i, n;
+		Expression e;
+		
+		n = labels.size();
+		for (i = 0; i < n; i++) {
+			e = getLabel(i);
+			labels.setElementAt(e.expandFormulas(formulaList), i);
+		}
+	}
+
 	// find all constants (i.e. locate idents which are constants)
 	
 	public void findAllConstants(ConstantList constantList) throws PrismException

prism/src/parser/ModulesFile.java

@@ -43,6 +43,9 @@ public class ModulesFile
 	// formulas (macros)
 	private FormulaList formulaList;
 	
+	// labels (atomic propositions)
+	private LabelList labelList;
+	
 	// constants
 	private ConstantList constantList;
 	
@@ -70,6 +73,7 @@ public class ModulesFile
 	{
 		// initialise
 		formulaList = new FormulaList(); // empty - will be overwritten
+		labelList = new LabelList(); // empty - will be overwritten
 		constantList = new ConstantList(); // empty - will be overwritten
 		type = NONDETERMINISTIC; // default type
 		globals = new Vector();
@@ -87,6 +91,8 @@ public class ModulesFile
 	
 	public void setFormulaList(FormulaList fl) { formulaList = fl; }
 	
+	public void setLabelList(LabelList ll) { labelList = ll; }
+	
 	public void setConstantList(ConstantList cl) { constantList = cl; }
 	
 	public void setType(int t) { type = t; }
@@ -110,6 +116,8 @@ public class ModulesFile
 
 	public FormulaList getFormulaList() { return formulaList; }
 	
+	public LabelList getLabelList() { return labelList; }
+	
 	public ConstantList getConstantList() { return constantList; }
 	
 	public int getType() { return type; }
@@ -222,6 +230,9 @@ public class ModulesFile
 		// sort out any modules defined by renaming
 		sortRenamings();
 		
+		// check label identifiers
+		checkLabelIdents();
+		
 		// check module names
 		checkModuleNames();
 		
@@ -280,6 +291,8 @@ public class ModulesFile
 		
 		// look in formula list
 		formulaList.findAllFormulas();
+		// look in labels
+		labelList.findAllFormulas(formulaList);
 		// look in constants
 		constantList.findAllFormulas(formulaList);
 		// look in globals
@@ -314,6 +327,8 @@ public class ModulesFile
 		// look in formula list
 		// (best to do this first - sorts out any linked formulas)
 		formulaList.expandFormulas();
+		// look in labels
+		labelList.expandFormulas(formulaList);
 		// look in constants
 		constantList.expandFormulas(formulaList);
 		// look in globals
@@ -369,6 +384,29 @@ public class ModulesFile
 		}
 	}
 	
+	// check label identifiers
+	
+	private void checkLabelIdents() throws PrismException
+	{
+		int i, n;
+		String s;
+		Vector labelIdents;
+		
+		// go thru labels
+		n = labelList.size();
+		labelIdents = new Vector();
+		for (i = 0; i < n; i++) {
+			s = labelList.getLabelName(i);
+			// see if ident has been used already for a label
+			if (labelIdents.contains(s)) {
+				throw new PrismException("Duplicated label name \"" + s + "\"");
+			}
+			else {
+				labelIdents.addElement(s);
+			}
+		}
+	}
+
 	// check module names
 	
 	private void checkModuleNames() throws PrismException
@@ -478,6 +516,8 @@ public class ModulesFile
 	{
 		int i, n;
 		
+		// look in labels
+		labelList.findAllConstants(constantList);
 		// look in constants
 		constantList.findAllConstants(constantList);
 		// look in globals
@@ -557,6 +597,8 @@ public class ModulesFile
 		// nb: we even check in places where there shouldn't be vars
 		//     eg. in constant definitions etc.
 		
+		// look in labels
+		labelList.findAllVars(varNames, varTypes);
 		// look in constants
 		constantList.findAllVars(varNames, varTypes);
 		// look in globals
@@ -601,6 +643,9 @@ public class ModulesFile
 		Module module;
 		Vector v;
 		
+		// check labels
+		labelList.check();
+		
 		// check constants
 		constantList.check();
 		// check globals
@@ -809,6 +854,10 @@ public class ModulesFile
 		if (tmp.length() > 0) tmp += "\n";
 		s += tmp;
 		
+		tmp = "" + labelList;
+		if (tmp.length() > 0) tmp += "\n";
+		s += tmp;
+		
 		tmp = "" + constantList;
 		if (tmp.length() > 0) tmp += "\n";
 		s += tmp;

prism/src/parser/PCTLExpression.java

@@ -61,6 +61,24 @@ public class PCTLExpression extends PCTLFormula
 		return expr;
 	}
 	
+	// find all formulas (i.e. locate idents which are formulas)
+	
+	public PCTLFormula findAllFormulas(FormulaList formulaList) throws PrismException
+	{
+		expr = expr.findAllFormulas(formulaList);
+		
+		return this;
+	}
+	
+	// expand any formulas
+	
+	public PCTLFormula expandFormulas(FormulaList formulaList) throws PrismException
+	{
+		expr = expr.expandFormulas(formulaList);
+		
+		return this;
+	}
+		
 	// find all constants (i.e. locate idents which are constants)
 	
 	public PCTLFormula findAllConstants(ConstantList constantList) throws PrismException

prism/src/parser/PCTLFormula.java

@@ -65,6 +65,14 @@ public abstract class PCTLFormula
 		// default is ok - do nothing
 	}
 	
+	// find all formulas (i.e. locate idents which are formulas)
+	
+	public abstract PCTLFormula findAllFormulas(FormulaList formulaList) throws PrismException;
+	
+	// expand any formulas
+	
+	public abstract PCTLFormula expandFormulas(FormulaList formulaList) throws PrismException;
+	
 	// find all constants (i.e. locate idents which are constants)
 	
 	public abstract PCTLFormula findAllConstants(ConstantList constantList) throws PrismException;

prism/src/parser/PCTLFormulaBinary.java

@@ -81,6 +81,26 @@ public abstract class PCTLFormulaBinary extends PCTLFormula
 		operand2.checkLabelIdents(labelList);
 	}
 
+	// find all formulas (i.e. locate idents which are formulas)
+	
+	public PCTLFormula findAllFormulas(FormulaList formulaList) throws PrismException
+	{
+		operand1 = operand1.findAllFormulas(formulaList);
+		operand2 = operand2.findAllFormulas(formulaList);
+		
+		return this;
+	}
+	
+	// expand any formulas
+	
+	public PCTLFormula expandFormulas(FormulaList formulaList) throws PrismException
+	{
+		operand1 = operand1.expandFormulas(formulaList);
+		operand2 = operand2.expandFormulas(formulaList);
+		
+		return this;
+	}
+		
 	// find all constants (i.e. locate idents which are constants)
 	
 	public PCTLFormula findAllConstants(ConstantList constantList) throws PrismException

prism/src/parser/PCTLFormulaNary.java

@@ -79,6 +79,34 @@ public abstract class PCTLFormulaNary extends PCTLFormula
 		}
 	}
 
+	// find all formulas (i.e. locate idents which are formulas)
+	
+	public PCTLFormula findAllFormulas(FormulaList formulaList) throws PrismException
+	{
+		int i, n;
+		
+		n = getNumOperands();
+		for (i = 0; i < n; i++) {
+			setOperand(i, getOperand(i).findAllFormulas(formulaList));
+		}
+		
+		return this;
+	}
+	
+	// expand any formulas
+	
+	public PCTLFormula expandFormulas(FormulaList formulaList) throws PrismException
+	{
+		int i, n;
+		
+		n = getNumOperands();
+		for (i = 0; i < n; i++) {
+			setOperand(i, getOperand(i).expandFormulas(formulaList));
+		}
+		
+		return this;
+	}
+		
 	// find all constants (i.e. locate idents which are constants)
 	
 	public PCTLFormula findAllConstants(ConstantList constantList) throws PrismException

prism/src/parser/PCTLFormulaUnary.java

@@ -68,6 +68,24 @@ public abstract class PCTLFormulaUnary extends PCTLFormula
 		operand.checkLabelIdents(labelList);
 	}
 
+	// find all formulas (i.e. locate idents which are formulas)
+	
+	public PCTLFormula findAllFormulas(FormulaList formulaList) throws PrismException
+	{
+		operand = operand.findAllFormulas(formulaList);
+		
+		return this;
+	}
+	
+	// expand any formulas
+	
+	public PCTLFormula expandFormulas(FormulaList formulaList) throws PrismException
+	{
+		operand = operand.expandFormulas(formulaList);
+		
+		return this;
+	}
+		
 	// find all constants (i.e. locate idents which are constants)
 	
 	public PCTLFormula findAllConstants(ConstantList constantList) throws PrismException

prism/src/parser/PCTLInit.java

@@ -42,6 +42,20 @@ public class PCTLInit extends PCTLFormula
 		setType(Expression.BOOLEAN);
 	}
 
+	// find all formulas (i.e. locate idents which are formulas)
+	
+	public PCTLFormula findAllFormulas(FormulaList formulaList) throws PrismException
+	{
+		return this;
+	}
+	
+	// expand any formulas
+	
+	public PCTLFormula expandFormulas(FormulaList formulaList) throws PrismException
+	{
+		return this;
+	}
+		
 	// find all constants (i.e. locate idents which are constants)
 	
 	public PCTLFormula findAllConstants(ConstantList constantList) throws PrismException

prism/src/parser/PCTLLabel.java

@@ -62,6 +62,20 @@ public class PCTLLabel extends PCTLFormula
 		}
 	}
 
+	// find all formulas (i.e. locate idents which are formulas)
+	
+	public PCTLFormula findAllFormulas(FormulaList formulaList) throws PrismException
+	{
+		return this;
+	}
+	
+	// expand any formulas
+	
+	public PCTLFormula expandFormulas(FormulaList formulaList) throws PrismException
+	{
+		return this;
+	}
+		
 	// find all constants (i.e. locate idents which are constants)
 	
 	public PCTLFormula findAllConstants(ConstantList constantList) throws PrismException
@@ -87,7 +101,7 @@ public class PCTLLabel extends PCTLFormula
 	/**
 	 *	Convert and build simulator data structures
 	 */
-	public long toSimulator(SimulatorEngine sim ) throws SimulatorException
+	public long toSimulator(SimulatorEngine sim) throws SimulatorException
 	{
 		LabelList ll;
 		Expression expr;
@@ -95,9 +109,7 @@ public class PCTLLabel extends PCTLFormula
 		int i;
 		
 		// get expression associated with label
-		
 		ll = sim.getLabelList();
-		
 		i = ll.getLabelIndex(getName());
 		if (i == -1) throw new SimulatorException("Unknown label \"" + getName() + "\" in PCTL formula");
 		expr = ll.getLabel(i);

prism/src/parser/PCTLProb.java

@@ -115,6 +115,34 @@ public class PCTLProb extends PCTLFormulaUnary
 		if (filter != null) filter.checkLabelIdents(labelList);
 	}
 
+	// find all formulas (i.e. locate idents which are formulas)
+	
+	public PCTLFormula findAllFormulas(FormulaList formulaList) throws PrismException
+	{
+		// call superclass (unary)
+		super.findAllFormulas(formulaList);
+		// also do prob expression
+		if (prob != null) prob = prob.findAllFormulas(formulaList);
+		// also do filter
+		if (filter != null) filter = filter.findAllFormulas(formulaList);
+		
+		return this;
+	}
+	
+	// expand any formulas
+	
+	public PCTLFormula expandFormulas(FormulaList formulaList) throws PrismException
+	{
+		// call superclass (unary)
+		super.expandFormulas(formulaList);
+		// also do prob expression
+		if (prob != null) prob = prob.expandFormulas(formulaList);
+		// also do filter
+		if (filter != null) filter = filter.expandFormulas(formulaList);
+		
+		return this;
+	}
+		
 	// find all constants (i.e. locate idents which are constants)
 	
 	public PCTLFormula findAllConstants(ConstantList constantList) throws PrismException

prism/src/parser/PCTLProbBoundedFuture.java

@@ -55,6 +55,32 @@ public class PCTLProbBoundedFuture extends PCTLFormulaUnary
 		return uBound;
 	}
 
+	// find all formulas (i.e. locate idents which are formulas)
+	
+	public PCTLFormula findAllFormulas(FormulaList formulaList) throws PrismException
+	{
+		// call superclass (binary)
+		super.findAllFormulas(formulaList);
+		// also do bound expressions
+		if (lBound != null) lBound = lBound.findAllFormulas(formulaList);
+		if (uBound != null) uBound = uBound.findAllFormulas(formulaList);
+		
+		return this;
+	}
+	
+	// expand any formulas
+	
+	public PCTLFormula expandFormulas(FormulaList formulaList) throws PrismException
+	{
+		// call superclass (binary)
+		super.expandFormulas(formulaList);
+		// also do bound expressions
+		if (lBound != null) lBound = lBound.expandFormulas(formulaList);
+		if (uBound != null) uBound = uBound.expandFormulas(formulaList);
+		
+		return this;
+	}
+		
 	// find all constants (i.e. locate idents which are constants)
 	
 	public PCTLFormula findAllConstants(ConstantList constantList) throws PrismException

prism/src/parser/PCTLProbBoundedGlobal.java

@@ -55,6 +55,32 @@ public class PCTLProbBoundedGlobal extends PCTLFormulaUnary
 		return uBound;
 	}
 
+	// find all formulas (i.e. locate idents which are formulas)
+	
+	public PCTLFormula findAllFormulas(FormulaList formulaList) throws PrismException
+	{
+		// call superclass (binary)
+		super.findAllFormulas(formulaList);
+		// also do bound expressions
+		if (lBound != null) lBound = lBound.findAllFormulas(formulaList);
+		if (uBound != null) uBound = uBound.findAllFormulas(formulaList);
+		
+		return this;
+	}
+	
+	// expand any formulas
+	
+	public PCTLFormula expandFormulas(FormulaList formulaList) throws PrismException
+	{
+		// call superclass (binary)
+		super.expandFormulas(formulaList);
+		// also do bound expressions
+		if (lBound != null) lBound = lBound.expandFormulas(formulaList);
+		if (uBound != null) uBound = uBound.expandFormulas(formulaList);
+		
+		return this;
+	}
+		
 	// find all constants (i.e. locate idents which are constants)
 	
 	public PCTLFormula findAllConstants(ConstantList constantList) throws PrismException

prism/src/parser/PCTLProbBoundedUntil.java

@@ -56,6 +56,32 @@ public class PCTLProbBoundedUntil extends PCTLFormulaBinary
 		return uBound;
 	}
 
+	// find all formulas (i.e. locate idents which are formulas)
+	
+	public PCTLFormula findAllFormulas(FormulaList formulaList) throws PrismException
+	{
+		// call superclass (binary)
+		super.findAllFormulas(formulaList);
+		// also do bound expressions
+		if (lBound != null) lBound = lBound.findAllFormulas(formulaList);
+		if (uBound != null) uBound = uBound.findAllFormulas(formulaList);
+		
+		return this;
+	}
+	
+	// expand any formulas
+	
+	public PCTLFormula expandFormulas(FormulaList formulaList) throws PrismException
+	{
+		// call superclass (binary)
+		super.expandFormulas(formulaList);
+		// also do bound expressions
+		if (lBound != null) lBound = lBound.expandFormulas(formulaList);
+		if (uBound != null) uBound = uBound.expandFormulas(formulaList);
+		
+		return this;
+	}
+		
 	// find all constants (i.e. locate idents which are constants)
 	
 	public PCTLFormula findAllConstants(ConstantList constantList) throws PrismException

prism/src/parser/PCTLReward.java

@@ -135,6 +135,38 @@ public class PCTLReward extends PCTLFormulaUnary
 		if (filter != null) filter.checkLabelIdents(labelList);
 	}
 
+	// find all formulas (i.e. locate idents which are formulas)
+	
+	public PCTLFormula findAllFormulas(FormulaList formulaList) throws PrismException
+	{
+		// call superclass (unary)
+		super.findAllFormulas(formulaList);
+		// also do reward expression
+		if (reward != null) reward = reward.findAllFormulas(formulaList);
+		// also do reward struct index
+		if (rewardStructIndex != null) if (rewardStructIndex instanceof Expression) rewardStructIndex = ((Expression)rewardStructIndex).findAllFormulas(formulaList);
+		// also do filter
+		if (filter != null) filter = filter.findAllFormulas(formulaList);
+		
+		return this;
+	}
+	
+	// expand any formulas
+	
+	public PCTLFormula expandFormulas(FormulaList formulaList) throws PrismException
+	{
+		// call superclass (unary)
+		super.expandFormulas(formulaList);
+		// also do reward expression
+		if (reward != null) reward = reward.expandFormulas(formulaList);
+		// also do reward struct index
+		if (rewardStructIndex != null) if (rewardStructIndex instanceof Expression) rewardStructIndex = ((Expression)rewardStructIndex).expandFormulas(formulaList);
+		// also do filter
+		if (filter != null) filter = filter.expandFormulas(formulaList);
+		
+		return this;
+	}
+		
 	// find all constants (i.e. locate idents which are constants)
 	
 	public PCTLFormula findAllConstants(ConstantList constantList) throws PrismException

prism/src/parser/PCTLRewardCumul.java

@@ -48,6 +48,26 @@ public class PCTLRewardCumul extends PCTLFormula
 		return bound;
 	}
 
+	// find all formulas (i.e. locate idents which are formulas)
+	
+	public PCTLFormula findAllFormulas(FormulaList formulaList) throws PrismException
+	{
+		// do bound
+		if (bound != null) bound = bound.findAllFormulas(formulaList);
+		
+		return this;
+	}
+	
+	// expand any formulas
+	
+	public PCTLFormula expandFormulas(FormulaList formulaList) throws PrismException
+	{
+		// do bound
+		if (bound != null) bound = bound.expandFormulas(formulaList);
+		
+		return this;
+	}
+		
 	// find all constants (i.e. locate idents which are constants)
 	
 	public PCTLFormula findAllConstants(ConstantList constantList) throws PrismException

prism/src/parser/PCTLRewardInst.java

@@ -48,6 +48,26 @@ public class PCTLRewardInst extends PCTLFormula
 		return time;
 	}
 
+	// find all formulas (i.e. locate idents which are formulas)
+	
+	public PCTLFormula findAllFormulas(FormulaList formulaList) throws PrismException
+	{
+		// do time
+		if (time != null) time = time.findAllFormulas(formulaList);
+		
+		return this;
+	}
+	
+	// expand any formulas
+	
+	public PCTLFormula expandFormulas(FormulaList formulaList) throws PrismException
+	{
+		// do time
+		if (time != null) time = time.expandFormulas(formulaList);
+		
+		return this;
+	}
+		
 	// find all constants (i.e. locate idents which are constants)
 	
 	public PCTLFormula findAllConstants(ConstantList constantList) throws PrismException

prism/src/parser/PCTLRewardSS.java

@@ -40,6 +40,20 @@ public class PCTLRewardSS extends PCTLFormula
 	{
 	}
 
+	// find all formulas (i.e. locate idents which are formulas)
+	
+	public PCTLFormula findAllFormulas(FormulaList formulaList) throws PrismException
+	{
+		return this;
+	}
+	
+	// expand any formulas
+	
+	public PCTLFormula expandFormulas(FormulaList formulaList) throws PrismException
+	{
+		return this;
+	}
+		
 	// find all constants (i.e. locate idents which are constants)
 	
 	public PCTLFormula findAllConstants(ConstantList constantList) throws PrismException

prism/src/parser/PCTLSS.java

@@ -78,6 +78,34 @@ public class PCTLSS extends PCTLFormulaUnary
 		if (filter != null) filter.checkLabelIdents(labelList);
 	}
 
+	// find all formulas (i.e. locate idents which are formulas)
+	
+	public PCTLFormula findAllFormulas(FormulaList formulaList) throws PrismException
+	{
+		// call superclass (unary)
+		super.findAllFormulas(formulaList);
+		// also do prob expression
+		if (prob != null) prob = prob.findAllFormulas(formulaList);
+		// also do filter
+		if (filter != null) filter = filter.findAllFormulas(formulaList);
+		
+		return this;
+	}
+	
+	// expand any formulas
+	
+	public PCTLFormula expandFormulas(FormulaList formulaList) throws PrismException
+	{
+		// call superclass (unary)
+		super.expandFormulas(formulaList);
+		// also do prob expression
+		if (prob != null) prob = prob.expandFormulas(formulaList);
+		// also do filter
+		if (filter != null) filter = filter.expandFormulas(formulaList);
+		
+		return this;
+	}
+		
 	// find all constants (i.e. locate idents which are constants)
 	
 	public PCTLFormula findAllConstants(ConstantList constantList) throws PrismException

prism/src/parser/PrismParser.jj

@@ -177,6 +177,7 @@ public class PrismParser
 		
 		// clear all vectors/stacks
 		formulaList = new FormulaList();
+		labelList = new LabelList();
 		constantList = new ConstantList();
 		stack.clear();
 		reverseStack.clear();
@@ -208,6 +209,7 @@ public class PrismParser
 		ReInit(str);
 		
 		// clear all vectors/stacks
+		formulaList = new FormulaList();
 		labelList = new LabelList();
 		constantList = new ConstantList();
 		stack.clear();
@@ -466,7 +468,7 @@ ModulesFile ModulesFile() :
 }
 {
 	(
-	( ( type=ModulesFileType() {typeSpecs++;} ) | FormulaDef() | ConstantDef() | GlobalDecl() | Module() | RenamedModule() | SystemComp() | RewardStruct() | Init() )*
+	( ( type=ModulesFileType() {typeSpecs++;} ) | FormulaDef() | LabelDef() | ConstantDef() | GlobalDecl() | Module() | RenamedModule() | SystemComp() | RewardStruct() | Init() )*
 	<EOF>
 	)
 	{
@@ -475,8 +477,9 @@ ModulesFile ModulesFile() :
 		// create new ModulesFile object
 		ModulesFile modulesFile = new ModulesFile();
 		
-		// pass lists of formulas, constants to ModulesFile
+		// pass lists of formulas, labels, constants to ModulesFile
 		modulesFile.setFormulaList(formulaList);
+		modulesFile.setLabelList(labelList);
 		modulesFile.setConstantList(constantList);
 		
 		// set type (default is nondeterministic)
@@ -543,13 +546,14 @@ PropertiesFile PropertiesFile() :
 {
 }
 {
-	( ( LabelDef() | ConstantDef() | SinglePCTLFormula() )* <EOF> ) // possibly several pctl formulas then eof
+	( ( /*FormulaDef() |*/ LabelDef() | ConstantDef() | SinglePCTLFormula() )* <EOF> ) // possibly several pctl formulas then eof
 	{
 		// create new PropertiesFile object
 		// (pass in associated ModulesFile)
 		PropertiesFile propertiesFile = new PropertiesFile(modulesFile);
 		
-		// pass lists of labels, constants to PropertiesFile
+		// pass lists of formulas, labels, constants to PropertiesFile
+		propertiesFile.setFormulaList(formulaList);
 		propertiesFile.setLabelList(labelList);
 		propertiesFile.setConstantList(constantList);
 

prism/src/parser/PropertiesFile.java

@@ -37,8 +37,12 @@ public class PropertiesFile
 	// associated ModulesFile (for constants, ...)
 	private ModulesFile modulesFile;
 	
+	// formulas (macros)
+	private FormulaList formulaList;
+	
 	// labels (atomic propositions)
 	private LabelList labelList;
+	private LabelList combinedLabelList;
 	
 	// constants
 	private ConstantList constantList;
@@ -49,6 +53,7 @@ public class PropertiesFile
 	private Vector comments;
 	
 	// list of all identifiers used
+	private Vector modulesFileIdents;
 	private Vector allIdentsUsed;
 	
 	// actual values of constants
@@ -60,8 +65,11 @@ public class PropertiesFile
 	{
 		// initialise
 		modulesFile = mf;
-		labelList = null;
-		constantList = null;
+		modulesFileIdents = modulesFile.getAllIdentsUsed();
+		formulaList = new FormulaList(); // empty - will be overwritten
+		labelList = new LabelList(); // empty - will be overwritten
+		combinedLabelList = new LabelList();
+		constantList = new ConstantList(); // empty - will be overwritten
 		properties = new Vector();
 		comments = new Vector();
 		allIdentsUsed = new Vector();
@@ -70,6 +78,8 @@ public class PropertiesFile
 	
 	// set up methods - these are called by the parser to create a PropertiesFile object
 	
+	public void setFormulaList(FormulaList fl) { formulaList = fl; }
+	
 	public void setLabelList(LabelList ll) { labelList = ll; }
 	
 	public void setConstantList(ConstantList cl) { constantList = cl; }
@@ -84,8 +94,12 @@ public class PropertiesFile
 	
 	// accessor methods
 
+	public FormulaList getFormulaList() { return formulaList; }
+	
 	public LabelList getLabelList() { return labelList; }
 	
+	public LabelList getCombinedLabelList() { return combinedLabelList; }
+	
 	public ConstantList getConstantList() { return constantList; }
 	
 	public int getNumProperties() { return properties.size(); }
@@ -98,6 +112,16 @@ public class PropertiesFile
 	
 	public void tidyUp() throws PrismException
 	{
+		// check formula identifiers
+		checkFormulaIdents();
+		// find all instances of formulas
+		// (i.e. locate idents which are formulas)
+		findAllFormulas();
+		// check formulas for cyclic dependencies
+		formulaList.findCycles();
+		// expand any formulas
+		expandFormulas();
+		
 		// check label identifiers
 		checkLabelIdents();
 		
@@ -118,6 +142,82 @@ public class PropertiesFile
 		check();
 	}
 
+	// check formula identifiers
+	
+	private void checkFormulaIdents() throws PrismException
+	{
+		int i, n;
+		String s;
+
+		n = formulaList.size();
+		for (i = 0; i < n; i++) {
+			s = formulaList.getFormulaName(i);
+			// see if ident has been used elsewhere
+			if (modulesFileIdents.contains(s)) {
+				throw new PrismException("Identifier \"" + s + "\" already used in model file");
+			}
+			else if (allIdentsUsed.contains(s)) {
+				throw new PrismException("Duplicated identifier \"" + s + "\"");
+			}
+			else {
+				allIdentsUsed.addElement(s);
+			}
+		}
+	}
+
+	// find all formulas (i.e. locate idents which are formulas)
+	
+	private void findAllFormulas() throws PrismException
+	{
+		int i, n;
+		
+		// note: we have to look for both formulas defined here
+		//       and those defined in the modules file
+		
+		// look in formula list
+		formulaList.findAllFormulas(modulesFile.getFormulaList());
+		formulaList.findAllFormulas();
+		// look in labels
+		labelList.findAllFormulas(modulesFile.getFormulaList());
+		labelList.findAllFormulas(formulaList);
+		// look in constants
+		constantList.findAllFormulas(modulesFile.getFormulaList());
+		constantList.findAllFormulas(formulaList);
+		// look in properties
+		n = properties.size();
+		for (i = 0; i < n; i++) {
+			setProperty(i, getProperty(i).findAllFormulas(modulesFile.getFormulaList()));
+			setProperty(i, getProperty(i).findAllFormulas(formulaList));
+		}
+	}
+
+	// expand any formulas
+	
+	private void expandFormulas() throws PrismException
+	{
+		int i, n;
+		
+		// note: we have to look for both formulas defined here
+		//       and those defined in the modules file
+		
+		// look in formula list
+		// (best to do this first - sorts out any linked formulas)
+		formulaList.expandFormulas(modulesFile.getFormulaList());
+		formulaList.expandFormulas();
+		// look in labels
+		labelList.expandFormulas(modulesFile.getFormulaList());
+		labelList.expandFormulas(formulaList);
+		// look in constants
+		constantList.expandFormulas(modulesFile.getFormulaList());
+		constantList.expandFormulas(formulaList);
+		// look in properties
+		n = properties.size();
+		for (i = 0; i < n; i++) {
+			setProperty(i, getProperty(i).expandFormulas(modulesFile.getFormulaList()));
+			setProperty(i, getProperty(i).expandFormulas(formulaList));
+		}
+	}
+	
 	// check label identifiers
 	// also check reference to these identifiers in properties
 	
@@ -126,25 +226,41 @@ public class PropertiesFile
 		int i, n;
 		String s;
 		Vector labelIdents;
+		LabelList mfLabels;
 		
+		// get label list from model file
+		mfLabels = modulesFile.getLabelList();
+		// add model file lables to combined label list
+		n = mfLabels.size();
+		for (i = 0; i < n; i++) {
+			// do we need to clone these Expressions? hopefully not - they shouldn't be modified again
+			combinedLabelList.addLabel(mfLabels.getLabelName(i), mfLabels.getLabel(i));
+		}
 		// go thru labels
 		n = labelList.size();
 		labelIdents = new Vector();
 		for (i = 0; i < n; i++) {
 			s = labelList.getLabelName(i);
+			// see if ident has been used already for a label in model file
+			if (mfLabels.getLabelIndex(s) != -1) {
+				throw new PrismException("Label \"" + s + "\" already defined in model file");
+			}
 			// see if ident has been used already for a label
 			if (labelIdents.contains(s)) {
 				throw new PrismException("Duplicated label name \"" + s + "\"");
 			}
+			// store identifier
+			// and add label to combined list
 			else {
 				labelIdents.addElement(s);
+				combinedLabelList.addLabel(s, labelList.getLabel(i));
 			}
 		}
 		
 		// now go thru properties and check that any PCTLLabel objects refer only to existing labels
 		n = properties.size();
 		for (i = 0; i < n; i++) {
-			getProperty(i).checkLabelIdents(labelList);
+			getProperty(i).checkLabelIdents(combinedLabelList);
 		}
 	}
 
@@ -154,26 +270,20 @@ public class PropertiesFile
 	{
 		int i, n;
 		String s;
-		Vector mfIdents, constIdents;
-		
-		// get idents used in modules file
-		mfIdents = modulesFile.getAllIdentsUsed();
-		// create vector to store new idents
-		constIdents = new Vector();
 		
 		// go thru constants
 		n = constantList.size();
 		for (i = 0; i < n; i++) {
 			s = constantList.getConstantName(i);
 			// see if ident has been used elsewhere
-			if (mfIdents.contains(s)) {
+			if (modulesFileIdents.contains(s)) {
 				throw new PrismException("Identifier \"" + s + "\" already used in model file");
 			}
-			else if (constIdents.contains(s)) {
+			else if (allIdentsUsed.contains(s)) {
 				throw new PrismException("Duplicated identifier \"" + s + "\"");
 			}
 			else {
-				constIdents.addElement(s);
+				allIdentsUsed.addElement(s);
 			}
 		}
 	}
@@ -278,6 +388,10 @@ public class PropertiesFile
 		String s = "", tmp, tmp2;
 		int i, j, n;
 		
+		tmp = "" + formulaList;
+		if (tmp.length() > 0) tmp += "\n";
+		s += tmp;
+		
 		tmp = "" + labelList;
 		if (tmp.length() > 0) tmp += "\n";
 		s += tmp;
@@ -309,6 +423,10 @@ public class PropertiesFile
 		String s = "", tmp;
 		int i, n;
 		
+		tmp = "" + formulaList;
+		if (tmp.length() > 0) tmp += "\n";
+		s += tmp;
+		
 		tmp = "" + labelList.toTreeString();
 		if (tmp.length() > 0) tmp += "\n";
 		s += tmp;

prism/src/prism/NondetModelChecker.java

@@ -1110,7 +1110,7 @@ public class NondetModelChecker implements ModelChecker
 			return dd;
 		}
 		// get expression associated with label
-		ll = propertiesFile.getLabelList();
+		ll = propertiesFile.getCombinedLabelList();
 		i = ll.getLabelIndex(pctl.getName());
 		if (i == -1) throw new PrismException("Unknown label \"" + pctl.getName() + "\" in PCTL formula");
 		expr = ll.getLabel(i);

prism/src/prism/Prism.java

@@ -1073,7 +1073,7 @@ public class Prism implements PrismSettingsListener
 			ll = null;
 			n = 0;
 		} else {
-			ll = propertiesFile.getLabelList();
+			ll = propertiesFile.getCombinedLabelList();
 			n = ll.size();
 		}
 		

prism/src/prism/ProbModelChecker.java

@@ -1113,7 +1113,7 @@ public class ProbModelChecker implements ModelChecker
 			return dd;
 		}
 		// get expression associated with label
-		ll = propertiesFile.getLabelList();
+		ll = propertiesFile.getCombinedLabelList();
 		i = ll.getLabelIndex(pctl.getName());
 		if (i == -1) throw new PrismException("Unknown label \"" + pctl.getName() + "\" in PCTL formula");
 		expr = ll.getLabel(i);

prism/src/prism/StochModelChecker.java

@@ -1855,7 +1855,7 @@ public class StochModelChecker implements ModelChecker
 			return dd;
 		}
 		// get expression associated with label
-		ll = propertiesFile.getLabelList();
+		ll = propertiesFile.getCombinedLabelList();
 		i = ll.getLabelIndex(pctl.getName());
 		if (i == -1) throw new PrismException("Unknown label \"" + pctl.getName() + "\" in CSL formula");
 		expr = ll.getLabel(i);

prism/src/simulator/SimulatorEngine.java

@@ -2320,7 +2320,7 @@ public class SimulatorEngine
 	 */
 	public LabelList getLabelList()
 	{
-		return propertiesFile.getLabelList();
+		return propertiesFile.getCombinedLabelList();
 	}
 	
 	// Methods to compute parameters for simulation