Addition of F (future) and G (global) operators to property specification language.

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

prism/include/simpctl.h

@@ -80,7 +80,8 @@ const int FORMULA_INSTANTANEOUS = 5;
 class CPathFormula
 {
 	protected:
-		bool answer;
+		bool answer; // the answer (true or false)
+		bool negate; // true if the actual result is the negation of "answer"
 
 	public:
 		bool answer_known;
@@ -96,6 +97,11 @@ class CPathFormula
 		{
 		}
 
+		/*
+		 *	Set whether or not the value of this formula should be negated
+		 */
+		void Set_Negate(bool b);
+
 		/*
 		 *	Access to the calculated answer for this CPathFormula object.
 		 */

prism/src/parser/PCTLProbBoundedFuture.java

@@ -0,0 +1,167 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-2004, Dave Parker
+//	
+//	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;
+
+import java.util.Vector;
+
+import prism.PrismException;
+import simulator.*;
+
+public class PCTLProbBoundedFuture extends PCTLFormulaUnary
+{
+	Expression lBound = null; // none if null, i.e. zero
+	Expression uBound = null; // none if null, i.e. infinity
+	
+	// constructor
+	
+	public PCTLProbBoundedFuture(PCTLFormula f, Expression l, Expression u)
+	{
+		super(f);
+		lBound = l;
+		uBound = u;
+	}
+
+	public Expression getLowerBound()
+	{
+		return lBound;
+	}
+
+	public Expression getUpperBound()
+	{
+		return uBound;
+	}
+
+	// find all constants (i.e. locate idents which are constants)
+	
+	public PCTLFormula findAllConstants(ConstantList constantList) throws PrismException
+	{
+		// call superclass (binary)
+		super.findAllConstants(constantList);
+		// also do bound expressions
+		if (lBound != null) lBound = lBound.findAllConstants(constantList);
+		if (uBound != null) uBound = uBound.findAllConstants(constantList);
+		
+		return this;
+	}
+	
+	// find all variables (i.e. locate idents which are variables)
+	
+	public PCTLFormula findAllVars(Vector varIdents, Vector varTypes) throws PrismException
+	{
+		// call superclass (binary)
+		super.findAllVars(varIdents, varTypes);
+		// also do bound expressions
+		if (lBound != null) lBound = lBound.findAllVars(varIdents, varTypes);
+		if (uBound != null) uBound = uBound.findAllVars(varIdents, varTypes);
+		
+		return this;
+	}
+	
+	// type check
+	
+	public void typeCheck() throws PrismException
+	{
+		// call superclass (binary)
+		super.typeCheck();
+		// check any time bounds are of type int/double
+		if (lBound != null) if (!(lBound.getType() == Expression.INT || lBound.getType() == Expression.DOUBLE)) {
+			throw new PrismException("Time bound \"" + lBound + "\" is the wrong type");
+		}
+		if (uBound != null) if (!(uBound.getType() == Expression.INT || uBound.getType() == Expression.DOUBLE)) {
+			throw new PrismException("Time bound \"" + uBound + "\" is the wrong type");
+		}
+	}
+
+	// check everything is ok
+	
+	public void check() throws PrismException
+	{
+		// call superclass (binary)
+		super.check();
+		// check any time bounds are ok and constant
+		if (lBound != null) {
+			lBound.check();
+			if (!lBound.isConstant()) {
+				throw new PrismException("Time bound \"" + lBound + "\" is not constant");
+			}
+		}
+		if (uBound != null) {
+			uBound.check();
+			if (!uBound.isConstant()) {
+				throw new PrismException("Time bound \"" + uBound + "\" is not constant");
+			}
+		}
+	}
+
+	// check if formula is valid pctl
+	
+	public void checkValidPCTL() throws PrismException
+	{
+		// must have upper bound only
+		if (lBound != null) throw new PrismException("PCTL bounded future formulas must have bounds of the form \"<=k\"");
+		// and it must be an integer
+		if (uBound.getType() != Expression.INT) throw new PrismException("Bounds in PCTL bounded future formulas must be of type integer");
+	}
+
+	// check if formula is valid csl
+	
+	public void checkValidCSL() throws PrismException
+	{
+		// ok
+	}
+
+	/**
+	 *	Convert and build simulator data structures
+	 *	Note: Although the simulator supports ProbBoundedFuture operators, they are 
+	 *	only supported if they belong to a top-most Prob formulae, and so are not 
+	 *	handled by a toSimulator method.  Therefore, this method will only be called 
+	 *	in error and hence throws an exception.
+	 */
+	public int toSimulator(SimulatorEngine sim ) throws SimulatorException
+	{
+		throw new SimulatorException("Unexpected Error when loading PCTL Formula into Simulator - BoundedFuture toSimulator should never be called");
+	}
+
+	// convert to string
+	
+	public String toString()
+	{
+		String s = "";
+		
+		s += "F";
+		if (lBound == null) {
+			s += "<=" + uBound;
+		}
+		else if (uBound == null) {
+			s += ">=" + lBound;
+		}
+		else {
+			s += "[" + lBound + "," + uBound + "]";
+		}
+		s += " " + operand;
+		
+		return s;
+	}
+}
+
+//------------------------------------------------------------------------------

prism/src/parser/PCTLProbBoundedGlobal.java

@@ -0,0 +1,167 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-2004, Dave Parker
+//	
+//	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;
+
+import java.util.Vector;
+
+import prism.PrismException;
+import simulator.*;
+
+public class PCTLProbBoundedGlobal extends PCTLFormulaUnary
+{
+	Expression lBound = null; // none if null, i.e. zero
+	Expression uBound = null; // none if null, i.e. infinity
+	
+	// constructor
+	
+	public PCTLProbBoundedGlobal(PCTLFormula f, Expression l, Expression u)
+	{
+		super(f);
+		lBound = l;
+		uBound = u;
+	}
+
+	public Expression getLowerBound()
+	{
+		return lBound;
+	}
+
+	public Expression getUpperBound()
+	{
+		return uBound;
+	}
+
+	// find all constants (i.e. locate idents which are constants)
+	
+	public PCTLFormula findAllConstants(ConstantList constantList) throws PrismException
+	{
+		// call superclass (binary)
+		super.findAllConstants(constantList);
+		// also do bound expressions
+		if (lBound != null) lBound = lBound.findAllConstants(constantList);
+		if (uBound != null) uBound = uBound.findAllConstants(constantList);
+		
+		return this;
+	}
+	
+	// find all variables (i.e. locate idents which are variables)
+	
+	public PCTLFormula findAllVars(Vector varIdents, Vector varTypes) throws PrismException
+	{
+		// call superclass (binary)
+		super.findAllVars(varIdents, varTypes);
+		// also do bound expressions
+		if (lBound != null) lBound = lBound.findAllVars(varIdents, varTypes);
+		if (uBound != null) uBound = uBound.findAllVars(varIdents, varTypes);
+		
+		return this;
+	}
+	
+	// type check
+	
+	public void typeCheck() throws PrismException
+	{
+		// call superclass (binary)
+		super.typeCheck();
+		// check any time bounds are of type int/double
+		if (lBound != null) if (!(lBound.getType() == Expression.INT || lBound.getType() == Expression.DOUBLE)) {
+			throw new PrismException("Time bound \"" + lBound + "\" is the wrong type");
+		}
+		if (uBound != null) if (!(uBound.getType() == Expression.INT || uBound.getType() == Expression.DOUBLE)) {
+			throw new PrismException("Time bound \"" + uBound + "\" is the wrong type");
+		}
+	}
+
+	// check everything is ok
+	
+	public void check() throws PrismException
+	{
+		// call superclass (binary)
+		super.check();
+		// check any time bounds are ok and constant
+		if (lBound != null) {
+			lBound.check();
+			if (!lBound.isConstant()) {
+				throw new PrismException("Time bound \"" + lBound + "\" is not constant");
+			}
+		}
+		if (uBound != null) {
+			uBound.check();
+			if (!uBound.isConstant()) {
+				throw new PrismException("Time bound \"" + uBound + "\" is not constant");
+			}
+		}
+	}
+
+	// check if formula is valid pctl
+	
+	public void checkValidPCTL() throws PrismException
+	{
+		// must have upper bound only
+		if (lBound != null) throw new PrismException("PCTL bounded global formulas must have bounds of the form \"<=k\"");
+		// and it must be an integer
+		if (uBound.getType() != Expression.INT) throw new PrismException("Bounds in PCTL bounded global formulas must be of type integer");
+	}
+
+	// check if formula is valid csl
+	
+	public void checkValidCSL() throws PrismException
+	{
+		// ok
+	}
+
+	/**
+	 *	Convert and build simulator data structures
+	 *	Note: Although the simulator supports ProbBoundedGlobal operators, they are 
+	 *	only supported if they belong to a top-most Prob formulae, and so are not 
+	 *	handled by a toSimulator method.  Therefore, this method will only be called 
+	 *	in error and hence throws an exception.
+	 */
+	public int toSimulator(SimulatorEngine sim ) throws SimulatorException
+	{
+		throw new SimulatorException("Unexpected Error when loading PCTL Formula into Simulator - BoundedGlobal toSimulator should never be called");
+	}
+
+	// convert to string
+	
+	public String toString()
+	{
+		String s = "";
+		
+		s += "G";
+		if (lBound == null) {
+			s += "<=" + uBound;
+		}
+		else if (uBound == null) {
+			s += ">=" + lBound;
+		}
+		else {
+			s += "[" + lBound + "," + uBound + "]";
+		}
+		s += " " + operand;
+		
+		return s;
+	}
+}
+
+//------------------------------------------------------------------------------

prism/src/parser/PCTLProbFuture.java

@@ -0,0 +1,57 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-2004, Dave Parker
+//	
+//	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;
+
+import java.util.Vector;
+
+import prism.PrismException;
+import simulator.*;
+
+public class PCTLProbFuture extends PCTLFormulaUnary
+{
+	// constructor
+	
+	public PCTLProbFuture(PCTLFormula f)
+	{
+		super(f);
+	}
+
+	/**
+	 *	Convert and build simulator data structures
+	 *	Note: Although the simulator supports ProbFuture operators, they are 
+	 *	only supported if they belong to a top-most Prob formulae, and so are not 
+	 *	handled by a toSimulator method.  Therefore, this method will only be called 
+	 *	in error and hence throws an exception.
+	 */
+	public int toSimulator(SimulatorEngine sim ) throws SimulatorException
+	{
+		throw new SimulatorException("Unexpected error when loading PCTL formula into simulator - Future toSimulator should never be called");
+	}
+
+	// convert to string
+	
+	public String toString()
+	{
+		return "F " + operand;
+	}
+}

prism/src/parser/PCTLProbGlobal.java

@@ -0,0 +1,57 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-2004, Dave Parker
+//	
+//	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;
+
+import java.util.Vector;
+
+import prism.PrismException;
+import simulator.*;
+
+public class PCTLProbGlobal extends PCTLFormulaUnary
+{
+	// constructor
+	
+	public PCTLProbGlobal(PCTLFormula f)
+	{
+		super(f);
+	}
+
+	/**
+	 *	Convert and build simulator data structures
+	 *	Note: Although the simulator supports ProbGlobal operators, they are 
+	 *	only supported if they belong to a top-most Prob formulae, and so are not 
+	 *	handled by a toSimulator method.  Therefore, this method will only be called 
+	 *	in error and hence throws an exception.
+	 */
+	public int toSimulator(SimulatorEngine sim ) throws SimulatorException
+	{
+		throw new SimulatorException("Unexpected error when loading PCTL formula into simulator - Global toSimulator should never be called");
+	}
+
+	// convert to string
+	
+	public String toString()
+	{
+		return "G " + operand;
+	}
+}

prism/src/parser/PrismParser.jj

@@ -1418,7 +1418,7 @@ void PCTLProb() :
 	( <PMAX> <EQ> <QMARK> {relOp="max=";} ) )
 	// path formula bit
 	<LBRACKET>
-	( PCTLProbNext() | PCTLProbBoundedUntil() | PCTLProbUntil() )
+	( PCTLProbNext() | PCTLProbBoundedUntil() | PCTLProbUntil() | PCTLProbBoundedFutureGlobal() | PCTLProbFutureGlobal() )
 	( tf=<LBRACE> PCTLFormula() <RBRACE>
 	(( tfmin=<LBRACE> <MIN> <RBRACE> ) | ( tfmax=<LBRACE> <MAX> <RBRACE> ))*
 	)? <RBRACKET> )
@@ -1527,6 +1527,71 @@ void PCTLProbUntil() :
 	}
 }
 
+// pctl bounded future (eventually) or global
+
+void PCTLProbBoundedFutureGlobal() :
+{
+	Token tfuture = null; // detects if a future formula is used
+	Token tglobal = null; // detects if a global formula is used
+	Token tle = null; // detects if a <= time bound is used
+	Token tge = null; // detects if a >= time bound is used
+	Token tr = null; // detects if a range time bound is used
+}
+{
+	( (tfuture=<FUTURE>|tglobal=<GLOB>) ((tle=<LE> Expression()) | (tge=<GE> Expression()) | (tr=<LBRACKET> Expression() <COMMA> Expression() <RBRACKET>)) PCTLFormula() )
+	{
+		PCTLFormula f = null;
+		Expression lb, ub;
+		PCTLFormula u;
+		
+		// pop operand off stack
+		f = (PCTLFormula)stack.pop();
+		// U<=ub
+		if (tle != null) {
+			ub = (Expression)stack.pop();
+			if (tfuture != null) u = new PCTLProbBoundedFuture(f, null, ub);
+			else u = new PCTLProbBoundedGlobal(f, null, ub);
+		}
+		// U>=lb
+		else if (tge != null) {
+			lb = (Expression)stack.pop();
+			if (tfuture != null) u = new PCTLProbBoundedFuture(f, lb, null);
+			else u = new PCTLProbBoundedGlobal(f, lb, null);
+		}
+		// U[lb,ub]
+		else {
+			ub = (Expression)stack.pop();
+			lb = (Expression)stack.pop();
+			if (tfuture != null) u = new PCTLProbBoundedFuture(f, lb, ub);
+			else u = new PCTLProbBoundedGlobal(f, lb, ub);
+		}
+		// push result onto stack
+		stack.push(u);
+	}
+}
+
+// pctl future (eventually) or globally
+
+void PCTLProbFutureGlobal() :
+{
+	Token tfuture = null; // detects if a future formula is used
+	Token tglobal = null; // detects if a global formula is used
+}
+{
+	( (tfuture=<FUTURE>|tglobal=<GLOB>) PCTLFormula() )
+	{
+		PCTLFormula f;
+		PCTLFormula u;
+		
+		// create PCTLProbFuture/PCTLProbGlobal object
+		f = (PCTLFormula)stack.pop();
+		if (tfuture != null) u = new PCTLProbFuture(f);
+		else u = new PCTLProbGlobal(f);
+		// push result onto stack
+		stack.push(u);
+	}
+}
+
 // pctl steady state (actually only csl - not pctl at all)
 
 void PCTLSS() :

prism/src/prism/NondetModelChecker.java

@@ -494,6 +494,14 @@ public class NondetModelChecker implements ModelChecker
 				probs = checkPCTLProbBoundedUntil((PCTLProbBoundedUntil)f, min);
 			else if (f instanceof PCTLProbUntil)
 				probs = checkPCTLProbUntil((PCTLProbUntil)f, pe, p, min);
+			else if (f instanceof PCTLProbBoundedFuture)
+				probs = checkPCTLProbBoundedFuture((PCTLProbBoundedFuture)f, min);
+			else if (f instanceof PCTLProbFuture)
+				probs = checkPCTLProbFuture((PCTLProbFuture)f, pe, p, min);
+			else if (f instanceof PCTLProbBoundedGlobal)
+				probs = checkPCTLProbBoundedGlobal((PCTLProbBoundedGlobal)f, min);
+			else if (f instanceof PCTLProbGlobal)
+				probs = checkPCTLProbGlobal((PCTLProbGlobal)f, pe, p, min);
 			else
 				throw new PrismException("Unrecognised path operator in P[] formula");
 		}
@@ -964,9 +972,10 @@ public class NondetModelChecker implements ModelChecker
 		}
 		
 		// if p is 0 or 1 and precomputation algorithms are enabled, compute probabilities qualitatively
-		if (pe != null && ((p==0) || (p==1)) & precomp) {
+		if (pe != null && ((p==0) || (p==1)) && precomp) {
 			mainLog.print("\nWarning: probability bound in formula is " + p + " so exact probabilities may not be computed\n");
-			probs = computeUntilProbsQual(trans01, b1, b2, p, min);
+			// for fairness, we compute max here
+			probs = computeUntilProbsQual(trans01, b1, b2, min&&!fairness);
 		}
 		// otherwise actually compute probabilities
 		else {
@@ -994,6 +1003,56 @@ public class NondetModelChecker implements ModelChecker
 		
 		return probs;
 	}
+	
+	// bounded future (eventually)
+	// F<=k phi == true U<=k phi
+	
+	private StateProbs checkPCTLProbBoundedFuture(PCTLProbBoundedFuture pctl, boolean min) throws PrismException
+	{
+		PCTLProbBoundedUntil pctlBUntil;
+		pctlBUntil = new PCTLProbBoundedUntil(new PCTLExpression(new ExpressionTrue()), pctl.getOperand(), pctl.getLowerBound(), pctl.getUpperBound());
+		return checkPCTLProbBoundedUntil(pctlBUntil, min);
+	}
+	
+	// future (eventually)
+	// F phi == true U phi
+	
+	private StateProbs checkPCTLProbFuture(PCTLProbFuture pctl, Expression pe, double p, boolean min) throws PrismException
+	{
+		PCTLProbUntil pctlUntil;
+		pctlUntil = new PCTLProbUntil(new PCTLExpression(new ExpressionTrue()), pctl.getOperand());
+		return checkPCTLProbUntil(pctlUntil, pe, p, min);
+	}
+	
+	// bounded global (always)
+	// F<=k phi == true U<=k phi
+	// P(G<=k phi) == 1-P(true U<=k !phi)
+	// Pmin(G<=k phi) == 1-Pmax(true U<=k !phi)
+	
+	private StateProbs checkPCTLProbBoundedGlobal(PCTLProbBoundedGlobal pctl, boolean min) throws PrismException
+	{
+		PCTLProbBoundedUntil pctlBUntil;
+		StateProbs probs;
+		pctlBUntil = new PCTLProbBoundedUntil(new PCTLExpression(new ExpressionTrue()), new PCTLNot(pctl.getOperand()), pctl.getLowerBound(), pctl.getUpperBound());
+		probs = checkPCTLProbBoundedUntil(pctlBUntil, !min);
+		probs.subtractFromOne();
+		return probs;
+	}
+	
+	// global (always)
+	// G phi == !(true U !phi)
+	// P(G phi) == 1-P(true U !phi)
+	// Pmin(G phi) == 1-Pmax(true U !phi)
+	
+	private StateProbs checkPCTLProbGlobal(PCTLProbGlobal pctl, Expression pe, double p, boolean min) throws PrismException
+	{
+		PCTLProbUntil pctlUntil;
+		StateProbs probs;
+		pctlUntil = new PCTLProbUntil(new PCTLExpression(new ExpressionTrue()), new PCTLNot(pctl.getOperand()));
+		probs = checkPCTLProbUntil(pctlUntil, pe, p, !min);
+		probs.subtractFromOne();
+		return probs;
+	}
 
 	// reach reward
 	
@@ -1187,9 +1246,11 @@ public class NondetModelChecker implements ModelChecker
 	}
 
 	// compute probabilities for until (for qualitative properties)
-	// note: this func needs to know 'min', 'fairness' and 'p'
 	
-	private StateProbs computeUntilProbsQual(JDDNode tr01, JDDNode b1, JDDNode b2, double p, boolean min)
+	// note: this function doesn't need to know anything about fairness
+	//       it is just told whether to compute min or max probabilities
+	
+	private StateProbs computeUntilProbsQual(JDDNode tr01, JDDNode b1, JDDNode b2, boolean min)
 	{
 		JDDNode yes = null, no = null, maybe;
 		StateProbs probs = null;
@@ -1212,9 +1273,8 @@ public class NondetModelChecker implements ModelChecker
 			maybe = JDD.Constant(0);
 		}
 		else {
-			// note: if using fairness, we're always looking for the max probabilities
 			// min
-			if (min&&!fairness) {
+			if (min) {
 				// no: "min prob = 0" equates to "there exists an adversary prob equals 0"
 				no = PrismMTBDD.Prob0E(tr01, reach, nondetMask, allDDRowVars, allDDColVars, allDDNondetVars, b1, b2);
 				// yes: "min prob = 1" equates to "for all adversaries prob equals 1"
@@ -1260,41 +1320,15 @@ public class NondetModelChecker implements ModelChecker
 			JDD.Ref(yes);
 			probs = new StateProbsMTBDD(yes, model);
 		}
-		// p = 0
-		else if (p == 0) {
-			if (!(min && fairness)) {
-				// anything that's unknown but definitely > 0
-				// may as well be 1
-				JDD.Ref(yes);
-				JDD.Ref(maybe);
-				probs = new StateProbsMTBDD(JDD.Or(yes, maybe), model);
-			}
-			else {
-				// have to be careful here though because actually solving the dual problem
-				// solving min so must be checking for > 0
-				// for states in maybe, p is in (0,1) and 1-p > 0
-				// so just set them to 0 and will become 1 which is still > 0
-				JDD.Ref(yes);
-				probs = new StateProbsMTBDD(yes, model);
-			}
-		}
-		// p = 1
+		// otherwise we set the probabilities for maybe states to be 0.5
+		// (actual probabilities for these states are unknown but definitely >0 and <1)
+		// (this is safe because the results of this function will only be used to compare against 0/1 bounds)
+		// (this is not entirely elegant but is simpler and less error prone than
+		//  trying to work out whether to use 0/1 for all case of min/max, fairness, future/global, etc.)
 		else {
-			if (!(min && fairness)) {
-				// anything that's unknown but definitely < 1
-				// may as well be 0
-				JDD.Ref(yes);
-				probs = new StateProbsMTBDD(yes, model);
-			}
-			else {
-				// have to be careful here though because actually solving the dual problem
-				// solving min so must be checking for >= 1
-				// for states in maybe, p is in (0,1) and 1-p not >= 1
-				// so just set them to 1 and will become 0 which is still not >= 1
-				JDD.Ref(yes);
-				JDD.Ref(maybe);
-				probs = new StateProbsMTBDD(JDD.Or(yes, maybe), model);
-			}
+			JDD.Ref(yes);
+			JDD.Ref(maybe);
+			probs = new StateProbsMTBDD(JDD.Apply(JDD.PLUS, yes, JDD.Apply(JDD.TIMES, maybe, JDD.Constant(0.5))), model);
 		}
 		
 		// derefs

prism/src/prism/ProbModelChecker.java

@@ -507,6 +507,14 @@ public class ProbModelChecker implements ModelChecker
 				probs = checkPCTLProbBoundedUntil((PCTLProbBoundedUntil)f);
 			else if (f instanceof PCTLProbUntil)
 				probs = checkPCTLProbUntil((PCTLProbUntil)f, pe, p);
+			else if (f instanceof PCTLProbBoundedFuture)
+				probs = checkPCTLProbBoundedFuture((PCTLProbBoundedFuture)f);
+			else if (f instanceof PCTLProbFuture)
+				probs = checkPCTLProbFuture((PCTLProbFuture)f, pe, p);
+			else if (f instanceof PCTLProbBoundedGlobal)
+				probs = checkPCTLProbBoundedGlobal((PCTLProbBoundedGlobal)f);
+			else if (f instanceof PCTLProbGlobal)
+				probs = checkPCTLProbGlobal((PCTLProbGlobal)f, pe, p);
 			else
 				throw new PrismException("Unrecognised path operator in P[] formula");
 		}
@@ -937,7 +945,7 @@ public class ProbModelChecker implements ModelChecker
 		// compute probabilities
 		
 		// if prob bound is 0 or 1 and precomputation algorithms are enabled, compute probabilities qualitatively
-		if (pe != null && ((p==0) || (p==1)) & precomp) {
+		if (pe != null && ((p==0) || (p==1)) && precomp) {
 			mainLog.print("\nWarning: Probability bound in formula is " + p + " so exact probabilities may not be computed\n");
 			probs = computeUntilProbsQual(trans01, b1, b2, p);
 		}
@@ -959,6 +967,54 @@ public class ProbModelChecker implements ModelChecker
 		
 		return probs;
 	}
+	
+	// bounded future (eventually)
+	// F<=k phi == true U<=k phi
+	
+	private StateProbs checkPCTLProbBoundedFuture(PCTLProbBoundedFuture pctl) throws PrismException
+	{
+		PCTLProbBoundedUntil pctlBUntil;
+		pctlBUntil = new PCTLProbBoundedUntil(new PCTLExpression(new ExpressionTrue()), pctl.getOperand(), pctl.getLowerBound(), pctl.getUpperBound());
+		return checkPCTLProbBoundedUntil(pctlBUntil);
+	}
+	
+	// future (eventually)
+	// F phi == true U phi
+	
+	private StateProbs checkPCTLProbFuture(PCTLProbFuture pctl, Expression pe, double p) throws PrismException
+	{
+		PCTLProbUntil pctlUntil;
+		pctlUntil = new PCTLProbUntil(new PCTLExpression(new ExpressionTrue()), pctl.getOperand());
+		return checkPCTLProbUntil(pctlUntil, pe, p);
+	}
+	
+	// bounded global (always)
+	// F<=k phi == true U<=k phi
+	// P(G<=k phi) == 1-P(true U<=k !phi)
+	
+	private StateProbs checkPCTLProbBoundedGlobal(PCTLProbBoundedGlobal pctl) throws PrismException
+	{
+		PCTLProbBoundedUntil pctlBUntil;
+		StateProbs probs;
+		pctlBUntil = new PCTLProbBoundedUntil(new PCTLExpression(new ExpressionTrue()), new PCTLNot(pctl.getOperand()), pctl.getLowerBound(), pctl.getUpperBound());
+		probs = checkPCTLProbBoundedUntil(pctlBUntil);
+		probs.subtractFromOne();
+		return probs;
+	}
+	
+	// global (always)
+	// G phi == !(true U !phi)
+	// P(G phi) == 1-P(true U !phi)
+	
+	private StateProbs checkPCTLProbGlobal(PCTLProbGlobal pctl, Expression pe, double p) throws PrismException
+	{
+		PCTLProbUntil pctlUntil;
+		StateProbs probs;
+		pctlUntil = new PCTLProbUntil(new PCTLExpression(new ExpressionTrue()), new PCTLNot(pctl.getOperand()));
+		probs = checkPCTLProbUntil(pctlUntil, pe, p);
+		probs.subtractFromOne();
+		return probs;
+	}
 
 	// reach reward
 	

prism/src/prism/StochModelChecker.java

@@ -531,6 +531,14 @@ public class StochModelChecker implements ModelChecker
 				probs = checkPCTLProbBoundedUntil((PCTLProbBoundedUntil)f);
 			else if (f instanceof PCTLProbUntil)
 				probs = checkPCTLProbUntil((PCTLProbUntil)f, pe, p);
+			else if (f instanceof PCTLProbBoundedFuture)
+				probs = checkPCTLProbBoundedFuture((PCTLProbBoundedFuture)f);
+			else if (f instanceof PCTLProbFuture)
+				probs = checkPCTLProbFuture((PCTLProbFuture)f, pe, p);
+			else if (f instanceof PCTLProbBoundedGlobal)
+				probs = checkPCTLProbBoundedGlobal((PCTLProbBoundedGlobal)f);
+			else if (f instanceof PCTLProbGlobal)
+				probs = checkPCTLProbGlobal((PCTLProbGlobal)f, pe, p);
 			else
 				throw new PrismException("Unrecognised path operator in P[] formula");
 		}
@@ -1404,7 +1412,7 @@ public class StochModelChecker implements ModelChecker
 		mainLog.print(" states, b2 = " + JDD.GetNumMintermsString(b2, allDDRowVars.n()) + " states\n");
 		
 		// if p is 0 or 1 and precomputation algorithms are enabled, compute probabilities qualitatively
-		if (pe != null && ((p==0) || (p==1)) & precomp) {
+		if (pe != null && ((p==0) || (p==1)) && precomp) {
 			mainLog.print("\nWarning: probability bound in formula is " + p + " so exact probabilities may not be computed\n");
 			probs = computeUntilProbsQual(trans01, b1, b2, p);
 		}
@@ -1446,6 +1454,54 @@ public class StochModelChecker implements ModelChecker
 		return probs;
 	}
 	
+	// bounded future (eventually)
+	// F[t1,t2] phi == true U[t1,t2] phi
+	
+	private StateProbs checkPCTLProbBoundedFuture(PCTLProbBoundedFuture pctl) throws PrismException
+	{
+		PCTLProbBoundedUntil pctlBUntil;
+		pctlBUntil = new PCTLProbBoundedUntil(new PCTLExpression(new ExpressionTrue()), pctl.getOperand(), pctl.getLowerBound(), pctl.getUpperBound());
+		return checkPCTLProbBoundedUntil(pctlBUntil);
+	}
+	
+	// future (eventually)
+	// F phi == true U phi
+	
+	private StateProbs checkPCTLProbFuture(PCTLProbFuture pctl, Expression pe, double p) throws PrismException
+	{
+		PCTLProbUntil pctlUntil;
+		pctlUntil = new PCTLProbUntil(new PCTLExpression(new ExpressionTrue()), pctl.getOperand());
+		return checkPCTLProbUntil(pctlUntil, pe, p);
+	}
+	
+	// bounded global (always)
+	// F<=k phi == true U<=k phi
+	// P(G<=k phi) == 1-P(true U<=k !phi)
+	
+	private StateProbs checkPCTLProbBoundedGlobal(PCTLProbBoundedGlobal pctl) throws PrismException
+	{
+		PCTLProbBoundedUntil pctlBUntil;
+		StateProbs probs;
+		pctlBUntil = new PCTLProbBoundedUntil(new PCTLExpression(new ExpressionTrue()), new PCTLNot(pctl.getOperand()), pctl.getLowerBound(), pctl.getUpperBound());
+		probs = checkPCTLProbBoundedUntil(pctlBUntil);
+		probs.subtractFromOne();
+		return probs;
+	}
+	
+	// global (always)
+	// G phi == !(true U !phi)
+	// P(G phi) == 1-P(true U !phi)
+	
+	private StateProbs checkPCTLProbGlobal(PCTLProbGlobal pctl, Expression pe, double p) throws PrismException
+	{
+		PCTLProbUntil pctlUntil;
+		StateProbs probs;
+		pctlUntil = new PCTLProbUntil(new PCTLExpression(new ExpressionTrue()), new PCTLNot(pctl.getOperand()));
+		probs = checkPCTLProbUntil(pctlUntil, pe, p);
+		probs.subtractFromOne();
+		return probs;
+	}
+
 	// cumulative reward
 	
 	private StateProbs checkPCTLRewardCumul(PCTLRewardCumul pctl, JDDNode stateRewards, JDDNode transRewards) throws PrismException

prism/src/simulator/SimulatorEngine.java

@@ -2043,77 +2043,92 @@ public class SimulatorEngine
 		allConstants.addValues(getConstants());
 		allConstants.addValues(getPropertyConstants());
 		
-		if(operand instanceof PCTLProbBoundedUntil)
-		{
-			try
+		try {
+			
+			if (operand instanceof PCTLProbNext)
+			{
+				int expressionPointer = ((PCTLProbNext)operand).getOperand().toSimulator(this);
+				return loadPctlNext(expressionPointer);
+			}
+			else if (operand instanceof PCTLProbBoundedUntil)
 			{
 				int leftExpressionPointer = ((PCTLProbBoundedUntil)operand).getOperand1().toSimulator(this);
 				int rightExpressionPointer = ((PCTLProbBoundedUntil)operand).getOperand2().toSimulator(this);
-				
+				double lowerBound;
+				if (((PCTLProbBoundedUntil)operand).getLowerBound() != null)
+					lowerBound = ((PCTLProbBoundedUntil)operand).getLowerBound().evaluateDouble(allConstants, null);
+				else
+					lowerBound = 0.0;
 				double upperBound;
-				
-				if(((PCTLProbBoundedUntil)operand).getUpperBound() != null)
+				if (((PCTLProbBoundedUntil)operand).getUpperBound() != null)
 					upperBound = ((PCTLProbBoundedUntil)operand).getUpperBound().evaluateDouble(allConstants, null);
 				else
 					upperBound = Integer.MAX_VALUE;
-				
+				return loadPctlBoundedUntil(leftExpressionPointer, rightExpressionPointer, lowerBound, upperBound);
+			}
+			else if (operand instanceof PCTLProbUntil)
+			{
+				int leftExpressionPointer = ((PCTLProbUntil)operand).getOperand1().toSimulator(this);
+				int rightExpressionPointer = ((PCTLProbUntil)operand).getOperand2().toSimulator(this);
+				return loadPctlUntil(leftExpressionPointer, rightExpressionPointer);
+			}
+			else if (operand instanceof PCTLProbBoundedFuture)
+			{
+				int leftExpressionPointer = (new PCTLExpression(new ExpressionTrue())).toSimulator(this);
+				int rightExpressionPointer = ((PCTLProbFuture)operand).getOperand().toSimulator(this);
 				double lowerBound;
-				if(((PCTLProbBoundedUntil)operand).getLowerBound() != null)
-					lowerBound = ((PCTLProbBoundedUntil)operand).getLowerBound().evaluateDouble(allConstants, null);
+				if (((PCTLProbBoundedFuture)operand).getLowerBound() != null)
+					lowerBound = ((PCTLProbBoundedFuture)operand).getLowerBound().evaluateDouble(allConstants, null);
 				else
 					lowerBound = 0.0;
-				
-				return  loadPctlBoundedUntil(leftExpressionPointer, rightExpressionPointer, lowerBound, upperBound);
-				
+				double upperBound;
+				if (((PCTLProbBoundedFuture)operand).getUpperBound() != null)
+					upperBound = ((PCTLProbBoundedFuture)operand).getUpperBound().evaluateDouble(allConstants, null);
+				else
+					upperBound = Integer.MAX_VALUE;
+				return loadPctlBoundedUntil(leftExpressionPointer, rightExpressionPointer, lowerBound, upperBound);
 			}
-			catch(SimulatorException e)
+			else if (operand instanceof PCTLProbFuture)
 			{
-				System.err.println("Property: "+operand.toString()+" could not be used in the simulator because: \n"+ e.toString());
-				return -1;
+				int leftExpressionPointer = (new PCTLExpression(new ExpressionTrue())).toSimulator(this);
+				int rightExpressionPointer = ((PCTLProbFuture)operand).getOperand().toSimulator(this);
+				return loadPctlUntil(leftExpressionPointer, rightExpressionPointer);
 			}
-			catch(PrismException e)
+			else if (operand instanceof PCTLProbBoundedGlobal)
 			{
-				System.err.println("Property: "+operand.toString()+" could not be used in the simulator because: \n"+ e.toString());
-				return -1;
+				int leftExpressionPointer = (new PCTLExpression(new ExpressionTrue())).toSimulator(this);
+				int rightExpressionPointer = (new PCTLNot(((PCTLProbGlobal)operand).getOperand())).toSimulator(this);
+				double lowerBound;
+				if (((PCTLProbBoundedGlobal)operand).getLowerBound() != null)
+					lowerBound = ((PCTLProbBoundedGlobal)operand).getLowerBound().evaluateDouble(allConstants, null);
+				else
+					lowerBound = 0.0;
+				double upperBound;
+				if (((PCTLProbBoundedGlobal)operand).getUpperBound() != null)
+					upperBound = ((PCTLProbBoundedFuture)operand).getUpperBound().evaluateDouble(allConstants, null);
+				else
+					upperBound = Integer.MAX_VALUE;
+				return loadPctlBoundedUntilNegated(leftExpressionPointer, rightExpressionPointer, lowerBound, upperBound);
 			}
-			
-			
-		}
-		else if(operand instanceof PCTLProbNext)
-		{
-			try
+			else if (operand instanceof PCTLProbGlobal)
 			{
-				
-				int expressionPointer = ((PCTLProbNext)operand).getOperand().toSimulator(this);
-				
-				return loadPctlNext(expressionPointer);
+				int leftExpressionPointer = (new PCTLExpression(new ExpressionTrue())).toSimulator(this);
+				int rightExpressionPointer = (new PCTLNot(((PCTLProbGlobal)operand).getOperand())).toSimulator(this);
+				return loadPctlUntilNegated(leftExpressionPointer, rightExpressionPointer);
 			}
-			catch(SimulatorException e)
+			else
 			{
-				System.err.println("Property: "+operand.toString()+" could not be used in the simulator because: \n"+ e.toString());
 				return -1;
 			}
 		}
-		else if(operand instanceof PCTLProbUntil)
+		catch(SimulatorException e)
 		{
-			try
-			{
-				int leftExpressionPointer = ((PCTLProbUntil)operand).getOperand1().toSimulator(this);
-				int rightExpressionPointer = ((PCTLProbUntil)operand).getOperand2().toSimulator(this);
-				
-				return loadPctlUntil(leftExpressionPointer, rightExpressionPointer);
-				
-			}
-			catch(SimulatorException e)
-			{
-				System.err.println("Property: "+operand.toString()+" could not be used in the simulator because: \n"+ e.toString());
-				return -1;
-			}
+			System.err.println("Property: "+operand.toString()+" could not be used in the simulator because: \n"+ e.toString());
+			return -1;
 		}
-		else
+		catch(PrismException e)
 		{
-			//System.out.println("cannot be added");
-			//cannot be added
+			System.err.println("Property: "+operand.toString()+" could not be used in the simulator because: \n"+ e.toString());
 			return -1;
 		}
 	}
@@ -2535,8 +2550,10 @@ public class SimulatorEngine
 	//location
 	
 	private static native int loadPctlBoundedUntil(int leftExprPointer, int rightExprPointer, double lowerBound, double upperBound);
+	private static native int loadPctlBoundedUntilNegated(int leftExprPointer, int rightExprPointer, double lowerBound, double upperBound);
 	
 	private static native int loadPctlUntil(int leftExprPointer, int rightExprPointer);
+	private static native int loadPctlUntilNegated(int leftExprPointer, int rightExprPointer);
 	
 	private static native int loadPctlNext(int exprPointer);
 	

prism/src/simulator/simpctl.cc

@@ -79,6 +79,16 @@ CPathFormula::CPathFormula()
 {
 	answer_known = false;
 	answer = false;
+	negate = false;
+}
+
+
+/*
+ *	Set whether or not the value of this formula should be negated
+ */
+void CPathFormula::Set_Negate(bool b)
+{
+	negate = b;
 }
 
 /*
@@ -86,7 +96,7 @@ CPathFormula::CPathFormula()
  */
 bool CPathFormula::Get_Answer()
 {
-	return answer;
+	return (negate)?(!answer):(answer);
 }
 
 /*

prism/src/simulator/simpctlbuilder.cc

@@ -78,6 +78,20 @@ JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_loadPctlBoundedUntil
 	return Formula_To_JInt(bu);
 }
 
+JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_loadPctlBoundedUntilNegated
+  (JNIEnv *env, jclass cls, jint exprPointer1, jint exprPointer2, jdouble lowerBound, jdouble upperBound, jboolean)
+{
+	CExpression* expr1 = To_Expr(exprPointer1);
+	CExpression* expr2 = To_Expr(exprPointer2);
+	
+	CBoundedUntil* bu = new CBoundedUntil(expr1, expr2, (double)lowerBound, (double)upperBound);
+	bu->Set_Negate(true);
+
+	Register_Path_Formula(bu);
+
+	return Formula_To_JInt(bu);
+}
+
 /*
  * Class:     simulator_SimulatorEngine
  * Method:    loadPctlUntil
@@ -96,6 +110,20 @@ JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_loadPctlUntil
 	return Formula_To_JInt(bu);
 }
 
+JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_loadPctlUntilNegated
+  (JNIEnv *env, jclass cls, jint exprPointer1, jint exprPointer2)
+{
+	CExpression* expr1 = To_Expr(exprPointer1);
+	CExpression* expr2 = To_Expr(exprPointer2);
+	
+	CUntil* bu = new CUntil(expr1, expr2);
+	bu->Set_Negate(true);
+
+	Register_Path_Formula(bu);
+
+	return Formula_To_JInt(bu);
+}
+
 /*
  * Class:     simulator_SimulatorEngine
  * Method:    loadPctlNext