LTL for DTMCs/CTMCs (and a bit of a tidy-up of LTL stuff).

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

prism/src/prism/LTLModelChecker.java

@@ -42,30 +42,29 @@ public class LTLModelChecker
 {
 	protected Prism prism;
 	protected PrismLog mainLog;
-	protected ModelChecker parent;
 	// DRA/product stuff
 	protected JDDVars draDDRowVars;
 	protected JDDVars draDDColVars;
 
-	public LTLModelChecker(Prism prism, ModelChecker parent) throws PrismException
+	public LTLModelChecker(Prism prism) throws PrismException
 	{
 		this.prism = prism;
 		mainLog = prism.getMainLog();
-		this.parent = parent;
 	}
 
-	/* Extract maximal state formula from an LTL path formula, model check them (with
-	 * parent model checker) and replace them with ExpressionLabel objects L0, L1, etc.
-	 * As an optimisation, model checking that results in true/false for all states is
-	 * converted to an actual true/false, and duplicate results are given the same label.
+	/**
+	 * Extract maximal state formula from an LTL path formula, model check them (with passed in model checker) and
+	 * replace them with ExpressionLabel objects L0, L1, etc. Expression passed in is modified directly, but the result
+	 * is also returned. As an optimisation, model checking that results in true/false for all states is converted to an
+	 * actual true/false, and duplicate results are given the same label.
 	 */
-	public Expression checkMaximalStateFormulas(Model model, Expression expr, Vector<JDDNode> labelDDs)
+	public Expression checkMaximalStateFormulas(ModelChecker mc, Model model, Expression expr, Vector<JDDNode> labelDDs)
 			throws PrismException
 	{
 		// A state formula
 		if (expr.getType() == Expression.BOOLEAN) {
 			// Model check
-			JDDNode dd = parent.checkExpressionDD(expr);
+			JDDNode dd = mc.checkExpressionDD(expr);
 			// Detect special cases (true, false) for optimisation
 			if (dd.equals(JDD.ZERO)) {
 				JDD.Deref(dd);
@@ -82,7 +81,7 @@ public class LTLModelChecker
 				JDD.Deref(dd);
 				return new ExpressionLabel("L" + i);
 			}
-			// Otherwise, add result to list, return new label 
+			// Otherwise, add result to list, return new label
 			labelDDs.add(dd);
 			return new ExpressionLabel("L" + (labelDDs.size() - 1));
 		}
@@ -90,25 +89,28 @@ public class LTLModelChecker
 		else if (expr.getType() == Expression.PATH_BOOLEAN) {
 			if (expr instanceof ExpressionBinaryOp) {
 				ExpressionBinaryOp exprBinOp = (ExpressionBinaryOp) expr;
-				exprBinOp.setOperand1(checkMaximalStateFormulas(model, exprBinOp.getOperand1(), labelDDs));
-				exprBinOp.setOperand2(checkMaximalStateFormulas(model, exprBinOp.getOperand2(), labelDDs));
+				exprBinOp.setOperand1(checkMaximalStateFormulas(mc, model, exprBinOp.getOperand1(), labelDDs));
+				exprBinOp.setOperand2(checkMaximalStateFormulas(mc, model, exprBinOp.getOperand2(), labelDDs));
 			} else if (expr instanceof ExpressionUnaryOp) {
 				ExpressionUnaryOp exprUnOp = (ExpressionUnaryOp) expr;
-				exprUnOp.setOperand(checkMaximalStateFormulas(model, exprUnOp.getOperand(), labelDDs));
+				exprUnOp.setOperand(checkMaximalStateFormulas(mc, model, exprUnOp.getOperand(), labelDDs));
 			} else if (expr instanceof ExpressionTemporal) {
 				ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
 				if (exprTemp.getOperand1() != null) {
-					exprTemp.setOperand1(checkMaximalStateFormulas(model, exprTemp.getOperand1(), labelDDs));
+					exprTemp.setOperand1(checkMaximalStateFormulas(mc, model, exprTemp.getOperand1(), labelDDs));
 				}
 				if (exprTemp.getOperand2() != null) {
-					exprTemp.setOperand2(checkMaximalStateFormulas(model, exprTemp.getOperand2(), labelDDs));
+					exprTemp.setOperand2(checkMaximalStateFormulas(mc, model, exprTemp.getOperand2(), labelDDs));
 				}
 			}
 		}
 		return expr;
 	}
 
-	public NondetModel constructProductModel(DRA dra, Model model, Vector<JDDNode> labelDDs) throws PrismException
+	/**
+	 * Construct product of DRA and DTMC/CTMC.
+	 */
+	public ProbModel constructProductMC(DRA dra,ProbModel model, Vector<JDDNode> labelDDs) throws PrismException
 	{
 		// Existing model - dds, vars, etc.
 		JDDVars varDDRowVars[];
@@ -143,10 +145,10 @@ public class LTLModelChecker
 		}
 
 		// See how many new dd vars will be needed for DRA
-		// and whether there is room to put them before rather than after the existing vars  
+		// and whether there is room to put them before rather than after the existing vars
 		n = (int) Math.ceil(PrismUtils.log2(dra.size()));
 		before = true;
-		if ((allDDRowVars.getMinVarIndex() - ((NondetModel) model).getAllDDNondetVars().getMaxVarIndex()) - 1 < 2 * n) {
+		if (allDDRowVars.getMinVarIndex() - 1 < 2 * n) {
 			before = false;
 		}
 
@@ -195,7 +197,6 @@ public class LTLModelChecker
 		newVarList.addVar(before ? 0 : varList.getNumVars(), draVar, 0, dra.size() - 1, 0, 1, Expression.INT);
 
 		// Extra references (because will get derefed when new model is done with)
-		// TODO: tidy this up, make it corresond to model.clear()
 		allDDRowVars.refAll();
 		allDDRowVars.refAll();
 		allDDColVars.refAll();
@@ -206,17 +207,167 @@ public class LTLModelChecker
 		}
 		draDDRowVars.refAll();
 		draDDColVars.refAll();
-		((NondetModel) model).getAllDDSchedVars().refAll();
-		((NondetModel) model).getAllDDSynchVars().refAll();
-		((NondetModel) model).getAllDDChoiceVars().refAll();
-		((NondetModel) model).getAllDDNondetVars().refAll();
 
+		// Build transition matrix for product
 		newTrans = buildTransMask(dra, labelDDs, allDDRowVars, allDDColVars, draDDRowVars, draDDColVars);
 		JDD.Ref(model.getTrans());
 		newTrans = JDD.Apply(JDD.TIMES, model.getTrans(), newTrans);
-		
-		// Note: ... TODO
-		newStart = buildStartMask(dra, labelDDs);
+
+		// Build set of initial states for product
+		// Note that we take product of *all* states of the original MDP, not just its initial states.
+		// Initial states are only used for reachability in this instance.
+		// We need to ensure that the product model includes states corresponding to all
+		// states of the original MDP (because we compute probabilities for all of them)
+		// but some of these may not be reachable from the initial state of the product model.
+		newStart = buildStartMask(dra, labelDDs, draDDRowVars);
+		JDD.Ref(model.getReach());
+		newStart = JDD.And(model.getReach(), newStart);
+
+		// Create a new model model object to store the product model
+		ProbModel modelProd = new ProbModel(
+				// New transition matrix/start state
+				newTrans, newStart,
+				// Don't pass in any rewards info
+				new JDDNode[0], new JDDNode[0], new String[0],
+				// New list of all row/col vars
+				newAllDDRowVars, newAllDDColVars,
+				// New list of var names
+				newDDVarNames,
+				// Module info (unchanged)
+				model.getNumModules(), model.getModuleNames(), model.getModuleDDRowVars(), model.getModuleDDColVars(),
+				// New var info
+				model.getNumVars() + 1, newVarList, newVarDDRowVars, newVarDDColVars,
+				// Constants (no change)
+				model.getConstantValues());
+
+		// Do reachability/etc. for the new model
+		modelProd.doReachability(prism.getExtraReachInfo());
+		modelProd.filterReachableStates();
+		modelProd.findDeadlocks();
+		if (modelProd.getDeadlockStates().size() > 0) {
+			throw new PrismException("Model-DRA product has deadlock states");
+		}
+
+		return modelProd;
+	}
+
+	/**
+	 * Construct product of DRA and MDP.
+	 */
+	public NondetModel constructProductMDP(DRA dra, NondetModel model, Vector<JDDNode> labelDDs) throws PrismException
+	{
+		// Existing model - dds, vars, etc.
+		JDDVars varDDRowVars[];
+		JDDVars varDDColVars[];
+		JDDVars allDDRowVars;
+		JDDVars allDDColVars;
+		Vector<String> ddVarNames;
+		VarList varList;
+		// New (product) model - dds, vars, etc.
+		JDDNode newTrans, newStart;
+		JDDVars newVarDDRowVars[], newVarDDColVars[];
+		JDDVars newAllDDRowVars, newAllDDColVars;
+		Vector<String> newDDVarNames;
+		VarList newVarList;
+		String draVar;
+		// Misc
+		int i, j, n;
+		boolean before;
+
+		// Get details of old model
+		varDDRowVars = model.getVarDDRowVars();
+		varDDColVars = model.getVarDDColVars();
+		allDDRowVars = model.getAllDDRowVars();
+		allDDColVars = model.getAllDDColVars();
+		ddVarNames = model.getDDVarNames();
+		varList = model.getVarList();
+
+		// Create a (new, unique) name for the variable that will represent DRA states
+		draVar = "_dra";
+		while (varList.getIndex(draVar) != -1) {
+			draVar = "_" + draVar;
+		}
+
+		// See how many new dd vars will be needed for DRA
+		// and whether there is room to put them before rather than after the existing vars
+		n = (int) Math.ceil(PrismUtils.log2(dra.size()));
+		before = true;
+		if ((allDDRowVars.getMinVarIndex() - model.getAllDDNondetVars().getMaxVarIndex()) - 1 < 2 * n) {
+			before = false;
+		}
+
+		// Create the new dd variables
+		draDDRowVars = new JDDVars();
+		draDDColVars = new JDDVars();
+		newDDVarNames = new Vector<String>();
+		newDDVarNames.addAll(ddVarNames);
+		j = before ? allDDRowVars.getMinVarIndex() - 2 * n : model.getAllDDColVars().getMaxVarIndex() + 1;
+		for (i = 0; i < n; i++) {
+			draDDRowVars.addVar(JDD.Var(j++));
+			draDDColVars.addVar(JDD.Var(j++));
+			if (!before) {
+				newDDVarNames.add("");
+				newDDVarNames.add("");
+			}
+			newDDVarNames.set(j - 2, draVar + "." + i);
+			newDDVarNames.set(j - 1, draVar + "'." + i);
+		}
+
+		// Create/populate new lists
+		newVarDDRowVars = new JDDVars[varDDRowVars.length + 1];
+		newVarDDColVars = new JDDVars[varDDRowVars.length + 1];
+		newVarDDRowVars[before ? 0 : varDDRowVars.length] = draDDRowVars;
+		newVarDDColVars[before ? 0 : varDDColVars.length] = draDDColVars;
+		for (i = 0; i < varDDRowVars.length; i++) {
+			newVarDDRowVars[before ? i + 1 : i] = new JDDVars();
+			newVarDDColVars[before ? i + 1 : i] = new JDDVars();
+			newVarDDRowVars[before ? i + 1 : i].addVars(varDDRowVars[i]);
+			newVarDDColVars[before ? i + 1 : i].addVars(varDDColVars[i]);
+		}
+		newAllDDRowVars = new JDDVars();
+		newAllDDColVars = new JDDVars();
+		if (before) {
+			newAllDDRowVars.addVars(draDDRowVars);
+			newAllDDColVars.addVars(draDDColVars);
+			newAllDDRowVars.addVars(allDDRowVars);
+			newAllDDColVars.addVars(allDDColVars);
+		} else {
+			newAllDDRowVars.addVars(allDDRowVars);
+			newAllDDColVars.addVars(allDDColVars);
+			newAllDDRowVars.addVars(draDDRowVars);
+			newAllDDColVars.addVars(draDDColVars);
+		}
+		newVarList = (VarList) varList.clone();
+		newVarList.addVar(before ? 0 : varList.getNumVars(), draVar, 0, dra.size() - 1, 0, 1, Expression.INT);
+
+		// Extra references (because will get derefed when new model is done with)
+		allDDRowVars.refAll();
+		allDDRowVars.refAll();
+		allDDColVars.refAll();
+		allDDColVars.refAll();
+		for (i = 0; i < model.getNumModules(); i++) {
+			model.getModuleDDRowVars(i).refAll();
+			model.getModuleDDColVars(i).refAll();
+		}
+		draDDRowVars.refAll();
+		draDDColVars.refAll();
+		model.getAllDDSchedVars().refAll();
+		model.getAllDDSynchVars().refAll();
+		model.getAllDDChoiceVars().refAll();
+		model.getAllDDNondetVars().refAll();
+
+		// Build transition matrix for product
+		newTrans = buildTransMask(dra, labelDDs, allDDRowVars, allDDColVars, draDDRowVars, draDDColVars);
+		JDD.Ref(model.getTrans());
+		newTrans = JDD.Apply(JDD.TIMES, model.getTrans(), newTrans);
+
+		// Build set of initial states for product
+		// Note that we take product of *all* states of the original MDP, not just its initial states.
+		// Initial states are only used for reachability in this instance.
+		// We need to ensure that the product model includes states corresponding to all
+		// states of the original MDP (because we compute probabilities for all of them)
+		// but some of these may not be reachable from the initial state of the product model.
+		newStart = buildStartMask(dra, labelDDs, draDDRowVars);
 		JDD.Ref(model.getReach());
 		newStart = JDD.And(model.getReach(), newStart);
 
@@ -229,8 +380,7 @@ public class LTLModelChecker
 				// New list of all row/col vars
 				newAllDDRowVars, newAllDDColVars,
 				// Nondet variables (unchanged)
-				((NondetModel) model).getAllDDSchedVars(), ((NondetModel) model).getAllDDSynchVars(),
-				((NondetModel) model).getAllDDChoiceVars(), ((NondetModel) model).getAllDDNondetVars(),
+				model.getAllDDSchedVars(), model.getAllDDSynchVars(), model.getAllDDChoiceVars(), model.getAllDDNondetVars(),
 				// New list of var names
 				newDDVarNames,
 				// Module info (unchanged)
@@ -251,14 +401,14 @@ public class LTLModelChecker
 		return modelProd;
 	}
 
-	/** 
-	 * Builds a mask BDD for trans (which contains transitions between every
-	 * DRA state after adding draRow/Colvars) that includes only the transitions
-	 * that exist in the DRA.
-	 * @return		a referenced mask BDD over trans
+	/**
+	 * Builds a mask BDD for trans (which contains transitions between every DRA state after adding draRow/ColVars) that
+	 * includes only the transitions that exist in the DRA.
+	 * 
+	 * @return a referenced mask BDD over trans
 	 */
-	public JDDNode buildTransMask(DRA dra, Vector<JDDNode> labelDDs, JDDVars allDDRowVars, JDDVars allDDColVars,
-			JDDVars draDDRowVars, JDDVars draDDColVars)
+	public JDDNode buildTransMask(DRA dra, Vector<JDDNode> labelDDs, JDDVars allDDRowVars, JDDVars allDDColVars, JDDVars draDDRowVars,
+			JDDVars draDDColVars)
 	{
 		Iterator<DA_State> it;
 		DA_State state;
@@ -271,7 +421,8 @@ public class LTLModelChecker
 			state = it.next();
 			for (Map.Entry<APElement, DA_State> edge : state.edges().entrySet()) {
 				// Build a transition label BDD for each edge
-				//System.out.println(state.getName() + " to " + edge.getValue().getName() + " through " + edge.getKey().toString(dra.getAPSet(), false));
+				// System.out.println(state.getName() + " to " + edge.getValue().getName() + " through " +
+				// edge.getKey().toString(dra.getAPSet(), false));
 				label = JDD.Constant(1);
 				n = dra.getAPSize();
 				for (i = 0; i < n; i++) {
@@ -286,8 +437,8 @@ public class LTLModelChecker
 				// Switch label BDD to col vars
 				label = JDD.PermuteVariables(label, allDDRowVars, allDDColVars);
 				// Build a BDD for the edge
-				transition = JDD.SetMatrixElement(JDD.Constant(0), draDDRowVars, draDDColVars, state.getName(), edge
-						.getValue().getName(), 1);
+				transition = JDD.SetMatrixElement(JDD.Constant(0), draDDRowVars, draDDColVars, state.getName(), edge.getValue().getName(),
+						1);
 				// Now get the conjunction of the two
 				transition = JDD.And(transition, label);
 				// Add edge BDD to the DRA transition mask
@@ -298,20 +449,21 @@ public class LTLModelChecker
 		return draMask;
 	}
 
-	/** 
-	 * Builds a mask BDD for start (which contains start nodes for every
-	 * DRA state after adding draRow/ColVars) that includes only the start states
-	 * (s, q) such that q = delta(q_in, label(s)) in the DRA.
-	 * @return		a referenced mask BDD over start
+	/**
+	 * Builds a mask BDD for start (which contains start nodes for every DRA state after adding draRowVars) that
+	 * includes only the start states (s, q) such that q = delta(q_in, label(s)) in the DRA.
+	 * 
+	 * @return a referenced mask BDD over start
 	 */
-	public JDDNode buildStartMask(DRA dra, Vector<JDDNode> labelDDs)
+	public JDDNode buildStartMask(DRA dra, Vector<JDDNode> labelDDs, JDDVars draDDRowVars)
 	{
 		JDDNode startMask, label, exprBDD, dest, tmp;
 
 		startMask = JDD.Constant(0);
 		for (Map.Entry<APElement, DA_State> edge : dra.getStartState().edges().entrySet()) {
 			// Build a transition label BDD for each edge
-			//System.out.println("To " + edge.getValue().getName() + " through " + edge.getKey().toString(dra.getAPSet(), false));
+			// System.out.println("To " + edge.getValue().getName() + " through " +
+			// edge.getKey().toString(dra.getAPSet(), false));
 			label = JDD.Constant(1);
 			for (int i = 0; i < dra.getAPSize(); i++) {
 				exprBDD = labelDDs.get(Integer.parseInt(dra.getAPSet().getAP(i).substring(1)));
@@ -334,31 +486,105 @@ public class LTLModelChecker
 
 		return startMask;
 	}
-	
+
 	/**
-	 * computes sets of accepting states for each Rabin acceptance pair
+	 * Computes sets of accepting states in a DTMC/CTMC for each Rabin acceptance pair
 	 * 
 	 * @returns a referenced BDD of the union of all the accepting sets
-	 */ 
-	public JDDNode findAcceptingStates(DRA dra, NondetModel model, boolean fairness) throws PrismException {
+	 */
+	public JDDNode findAcceptingBSCCs(DRA dra, ProbModel model) throws PrismException
+	{
+		SCCComputer sccComputer ;
+		JDDNode acceptingStates, allAcceptingStates;
+		Vector<JDDNode> vectBSCCs, newVectBSCCs;
+		JDDNode tmp;
+		int i, j, n;
+		
+		// Compute BSCCs for model
+		sccComputer = prism.getSCCComputer(model);
+		sccComputer.computeBSCCs();
+		vectBSCCs = sccComputer.getVectBSCCs();
+		JDD.Deref(sccComputer.getNotInBSCCs());
+		
+		allAcceptingStates = JDD.Constant(0);
+
+		// for each acceptance pair (H_i, L_i) in the DRA, build H'_i = S x H_i
+		// and compute the BSCCs in H'_i
+		for (i = 0; i < dra.acceptance().size(); i++) {
 
-		JDDNode allAcceptingStates = JDD.Constant(0);
+			// build the acceptance vectors H_i and L_i
+			JDDNode acceptanceVector_H = JDD.Constant(0);
+			JDDNode acceptanceVector_L = JDD.Constant(0);
+			for (j = 0; j < dra.size(); j++) {
+				/*
+				 * [dA97] uses Rabin acceptance pairs (H_i, L_i) such that H_i contains Inf(ρ) The intersection of
+				 * Inf(ρ) and L_i is non-empty
+				 * 
+				 * OTOH ltl2dstar (and our port to java) uses pairs (L_i, U_i) such that The intersection of U_i and
+				 * Inf(ρ) is empty (H_i = S - U_i) The intersection of L_i and Inf(ρ) is non-empty
+				 */
+				if (!dra.acceptance().isStateInAcceptance_U(i, j)) {
+					acceptanceVector_H = JDD.SetVectorElement(acceptanceVector_H, draDDRowVars, j, 1.0);
+				}
+				if (dra.acceptance().isStateInAcceptance_L(i, j)) {
+					acceptanceVector_L = JDD.SetVectorElement(acceptanceVector_L, draDDRowVars, j, 1.0);
+				}
+			}
+			
+			// Restrict each BSCC to H_i states
+			n = vectBSCCs.size();
+			newVectBSCCs = new Vector<JDDNode>();
+			for (j = 0; j < n; j++) {
+				tmp = vectBSCCs.get(j);
+				JDD.Ref(tmp);
+				JDD.Ref(acceptanceVector_H);
+				tmp = JDD.And(tmp, acceptanceVector_H);
+				newVectBSCCs.add(tmp);
+			}
+			JDD.Deref(acceptanceVector_H);
+			
+			// Compute union of BSCCs which overlap with acceptanceVector_L
+			acceptingStates = filteredUnion(newVectBSCCs, acceptanceVector_L);
+			
+			// Add states to our destination BDD
+			allAcceptingStates = JDD.Or(allAcceptingStates, acceptingStates);
+		}
+		
+		// Deref BSCCs 
+		n = vectBSCCs.size();
+		for (j = 0; j < n; j++) {
+			JDD.Deref(vectBSCCs.get(j));
+		}
+		
+		return allAcceptingStates;
+	}
+
+	/**
+	 * Computes sets of accepting states in an MDP for each Rabin acceptance pair
+	 * 
+	 * @returns a referenced BDD of the union of all the accepting sets
+	 */
+	public JDDNode findAcceptingStates(DRA dra, NondetModel model, boolean fairness) throws PrismException
+	{
+		JDDNode acceptingStates, allAcceptingStates;
+		int i, j;
+		
+		allAcceptingStates = JDD.Constant(0);
 
 		// for each acceptance pair (H_i, L_i) in the DRA, build H'_i = S x H_i
 		// and compute the maximal ECs in H'_i
-		for (int i = 0; i < dra.acceptance().size(); i++) {
+		for (i = 0; i < dra.acceptance().size(); i++) {
 
 			// build the acceptance vectors H_i and L_i
 			JDDNode acceptanceVector_H = JDD.Constant(0);
 			JDDNode acceptanceVector_L = JDD.Constant(0);
-			for (int j = 0; j < dra.size(); j++) {
-				/* [dA97] uses Rabin acceptance pairs (H_i, L_i) such that
-				 * H_i contains Inf(ρ)
-				 * The intersection of Inf(ρ) and L_i is non-empty
-				 *
-				 * OTOH ltl2dstar (and our port to java) uses pairs (L_i, U_i) such that
-				 * The intersection of U_i and Inf(ρ) is empty (H_i = S - U_i)
-				 * The intersection of L_i and Inf(ρ) is non-empty
+			for (j = 0; j < dra.size(); j++) {
+				/*
+				 * [dA97] uses Rabin acceptance pairs (H_i, L_i) such that H_i contains Inf(ρ) The intersection of
+				 * Inf(ρ) and L_i is non-empty
+				 * 
+				 * OTOH ltl2dstar (and our port to java) uses pairs (L_i, U_i) such that The intersection of U_i and
+				 * Inf(ρ) is empty (H_i = S - U_i) The intersection of L_i and Inf(ρ) is non-empty
 				 */
 				if (!dra.acceptance().isStateInAcceptance_U(i, j)) {
 					acceptanceVector_H = JDD.SetVectorElement(acceptanceVector_H, draDDRowVars, j, 1.0);
@@ -367,7 +593,7 @@ public class LTLModelChecker
 					acceptanceVector_L = JDD.SetVectorElement(acceptanceVector_L, draDDRowVars, j, 1.0);
 				}
 			}
-			
+
 			// build bdd of accepting states (under H_i) in the product model
 			JDD.Ref(model.getTrans01());
 			JDD.Ref(acceptanceVector_H);
@@ -376,8 +602,7 @@ public class LTLModelChecker
 			candidateStates = JDD.Apply(JDD.TIMES, candidateStates, acceptanceVector_H);
 			candidateStates = JDD.ThereExists(candidateStates, model.getAllDDColVars());
 			candidateStates = JDD.ThereExists(candidateStates, model.getAllDDNondetVars());
-		
-			JDDNode acceptingStates;
+
 			if (fairness) {
 				// compute the backward set of S x L_i
 				JDD.Ref(candidateStates);
@@ -385,40 +610,42 @@ public class LTLModelChecker
 				JDD.Ref(model.getTrans01());
 				JDDNode edges = JDD.ThereExists(model.getTrans01(), model.getAllDDNondetVars());
 				JDDNode filterStates = backwardSet(model, tmp, edges);
-								
+
 				// Filter out states that can't reach a state in L'_i
 				candidateStates = JDD.And(candidateStates, filterStates);
-				
+
 				// Find accepting states in S x H_i
-				acceptingStates = findFairECs(model, candidateStates);	
-			}
-			else {
+				acceptingStates = findFairECs(model, candidateStates);
+			} else {
 				// find ECs in acceptingStates that are accepting under L_i
 				acceptingStates = filteredUnion(findEndComponents(model, candidateStates), acceptanceVector_L);
 			}
-			
+
 			// Add states to our destination BDD
 			allAcceptingStates = JDD.Or(allAcceptingStates, acceptingStates);
 		}
+		
 		return allAcceptingStates;
 	}
-	
-	/** 
+
+	/**
 	 * Returns all end components in candidateStates under fairness assumptions
-	 * @param candidateStates		set of candidate states S x H_i 
-	 * 								(dereferenced after calling this function)
-	 * @return		a referenced BDD with the maximal stable set in c
+	 * 
+	 * @param candidateStates
+	 *            set of candidate states S x H_i (dereferenced after calling this function)
+	 * @return a referenced BDD with the maximal stable set in c
 	 */
-	private JDDNode findFairECs(NondetModel model, JDDNode candidateStates) {
-		
+	private JDDNode findFairECs(NondetModel model, JDDNode candidateStates)
+	{
+
 		JDDNode old = JDD.Constant(0);
 		JDDNode current = candidateStates;
-		
+
 		while (!current.equals(old)) {
 			JDD.Deref(old);
 			JDD.Ref(current);
 			old = current;
-						
+
 			JDD.Ref(current);
 			JDD.Ref(model.getTrans01());
 			// Select transitions starting in current
@@ -436,11 +663,9 @@ public class LTLModelChecker
 		JDD.Deref(old);
 		return current;
 	}
-	
-	/** 
-	 * Return the set of states that reach nodes through edges
-	 * Refs: result
-	 * Derefs: nodes, edges
+
+	/**
+	 * Return the set of states that reach nodes through edges Refs: result Derefs: nodes, edges
 	 */
 	private JDDNode backwardSet(NondetModel model, JDDNode nodes, JDDNode edges)
 	{
@@ -458,11 +683,9 @@ public class LTLModelChecker
 		JDD.Deref(old);
 		return current;
 	}
-	
-	/** 
-	 * Return the preimage of nodes in edges
-	 * Refs: result
-	 * Derefs: edges, nodes
+
+	/**
+	 * Return the preimage of nodes in edges Refs: result Derefs: edges, nodes
 	 */
 	// FIXME: Refactor this out (duplicated in SCCComputers)
 	private JDDNode preimage(NondetModel model, JDDNode nodes, JDDNode edges)
@@ -476,34 +699,37 @@ public class LTLModelChecker
 		tmp = JDD.ThereExists(tmp, model.getAllDDColVars());
 		return tmp;
 	}
-	
+
 	/**
 	 * Computes maximal accepting end components in states
-	 * @param states	BDD of a set of states (dereferenced after calling this function)
-	 * @return			a vector of referenced BDDs containing all the ECs in states
+	 * 
+	 * @param states
+	 *            BDD of a set of states (dereferenced after calling this function)
+	 * @return a vector of referenced BDDs containing all the ECs in states
 	 */
-	private Vector<JDDNode> findEndComponents(NondetModel model, JDDNode states) throws PrismException {
-		
+	private Vector<JDDNode> findEndComponents(NondetModel model, JDDNode states) throws PrismException
+	{
+
 		boolean initialCandidate = true;
 		Stack<JDDNode> candidates = new Stack<JDDNode>();
 		candidates.push(states);
 		Vector<JDDNode> ecs = new Vector<JDDNode>();
 		SCCComputer sccComputer;
-		
+
 		while (!candidates.isEmpty()) {
 			JDDNode candidate = candidates.pop();
-			
+
 			// Compute the stable set
 			JDD.Ref(candidate);
 			JDDNode stableSet = findMaximalStableSet(model, candidate);
-			
+
 			// Drop empty sets
 			if (stableSet.equals(JDD.ZERO)) {
 				JDD.Deref(stableSet);
 				JDD.Deref(candidate);
 				continue;
 			}
-			
+
 			if (!initialCandidate) {
 				// candidate is an SCC, check if it's stable
 				if (stableSet.equals(candidate)) {
@@ -511,45 +737,46 @@ public class LTLModelChecker
 					JDD.Deref(stableSet);
 					continue;
 				}
-			}
-			else {
+			} else {
 				initialCandidate = false;
 			}
 			JDD.Deref(candidate);
-			
+
 			// Filter bad transitions
 			JDD.Ref(stableSet);
 			JDDNode stableSetTrans = maxStableSetTrans(model, stableSet);
-			
+
 			// now find the maximal SCCs in (stableSet, stableSetTrans)
 			Vector<JDDNode> sccs;
 			sccComputer = prism.getSCCComputer(stableSet, stableSetTrans, model.getAllDDRowVars(), model.getAllDDColVars());
-			sccComputer.computeBSCCs();
+			sccComputer.computeSCCs();
 			JDD.Deref(stableSet);
 			JDD.Deref(stableSetTrans);
-			sccs = sccComputer.getVectBSCCs();
-			JDD.Deref(sccComputer.getNotInBSCCs());
+			sccs = sccComputer.getVectSCCs();
+			JDD.Deref(sccComputer.getNotInSCCs());
 			candidates.addAll(sccs);
 		}
 		return ecs;
 	}
-	
-	/** 
+
+	/**
 	 * Returns a stable set of states contained in candidateStates
-	 * @param candidateStates		set of candidate states S x H_i 
-	 * 								(dereferenced after calling this function)
-	 * @return		a referenced BDD with the maximal stable set in c
+	 * 
+	 * @param candidateStates
+	 *            set of candidate states S x H_i (dereferenced after calling this function)
+	 * @return a referenced BDD with the maximal stable set in c
 	 */
-	private JDDNode findMaximalStableSet(NondetModel model, JDDNode candidateStates) {
-		
+	private JDDNode findMaximalStableSet(NondetModel model, JDDNode candidateStates)
+	{
+
 		JDDNode old = JDD.Constant(0);
 		JDDNode current = candidateStates;
-		
+
 		while (!current.equals(old)) {
 			JDD.Deref(old);
 			JDD.Ref(current);
 			old = current;
-						
+
 			JDD.Ref(current);
 			JDD.Ref(model.getTrans());
 			// Select transitions starting in current
@@ -568,13 +795,16 @@ public class LTLModelChecker
 		JDD.Deref(old);
 		return current;
 	}
-	
+
 	/**
 	 * Returns the transition relation of a stable set
-	 * @param b		BDD of a stable set (dereferenced after calling this function)
-	 * @return		referenced BDD of the transition relation restricted to the stable set
+	 * 
+	 * @param b
+	 *            BDD of a stable set (dereferenced after calling this function)
+	 * @return referenced BDD of the transition relation restricted to the stable set
 	 */
-	private JDDNode maxStableSetTrans(NondetModel model, JDDNode b) {
+	private JDDNode maxStableSetTrans(NondetModel model, JDDNode b)
+	{
 
 		JDD.Ref(b);
 		JDD.Ref(model.getTrans());
@@ -596,12 +826,14 @@ public class LTLModelChecker
 	}
 
 	/**
-	 * Returns the union of each set in the vector that has nonempty intersection
-	 * with the filter BDD.
-	 * @param sets		Vector with sets which are dereferenced after calling this function
-	 * @param filter	filter BDD against which each set is checked for nonempty intersection
-	 * 					also dereferenced after calling this function
-	 * @return		Referenced BDD with the filtered union
+	 * Returns the union of each set in the vector that has nonempty intersection with the filter BDD.
+	 * 
+	 * @param sets
+	 *            Vector with sets which are dereferenced after calling this function
+	 * @param filter
+	 *            filter BDD against which each set is checked for nonempty intersection also dereferenced after calling
+	 *            this function
+	 * @return Referenced BDD with the filtered union
 	 */
 	private JDDNode filteredUnion(Vector<JDDNode> sets, JDDNode filter)
 	{

prism/src/prism/NondetModelChecker.java

@@ -400,13 +400,15 @@ public class NondetModelChecker extends NonProbModelChecker
 		}
 
 		// For LTL model checking routines
-		mcLtl = new LTLModelChecker(prism, this);
+		mcLtl = new LTLModelChecker(prism);
 
 		// Model check maximal state formulas
 		labelDDs = new Vector<JDDNode>();
-		ltl = mcLtl.checkMaximalStateFormulas(model, expr.deepCopy(), labelDDs);
+		ltl = mcLtl.checkMaximalStateFormulas(this, model, expr.deepCopy(), labelDDs);
 
 		// Convert LTL formula to deterministic Rabin automaton (DRA)
+		// For min probabilities, need to negate the formula
+		// (But check fairness setting since this may affect min/max)
 		mainLog.println("\nBuilding deterministic Rabin automaton (for " + (min && !fairness ? "!" : "") + ltl + ")...");
 		l = System.currentTimeMillis();
 		if (min && !fairness) {
@@ -414,22 +416,24 @@ public class NondetModelChecker extends NonProbModelChecker
 		} else {
 			dra = LTL2Rabin.ltl2rabin(ltl.convertForJltl2ba());
 		}
-		mainLog.println("\nDRA has " + dra.size() + " states.");
+		mainLog.println("\nDRA has " + dra.size() + " states, " + dra.acceptance().size() + " pairs.");
 		// dra.print(System.out);
 		l = System.currentTimeMillis() - l;
 		mainLog.println("\nTime for Rabin translation: " + l / 1000.0 + " seconds.");
 
 		// Build product of MDP and automaton
-		mainLog.println("\nConstructing Model-DRA product...");
-		modelProduct = mcLtl.constructProductModel(dra, model, labelDDs);
+		mainLog.println("\nConstructing MDP-DRA product...");
+		modelProduct = mcLtl.constructProductMDP(dra, model, labelDDs);
 		mainLog.println();
 		modelProduct.printTransInfo(mainLog, prism.getExtraDDInfo());
 		// prism.exportStatesToFile(modelProduct, Prism.EXPORT_PLAIN, null);
 		// prism.exportTransToFile(modelProduct, true, Prism.EXPORT_PLAIN, null);
 
+		// Find accepting maximum end components
 		mainLog.println("\nFinding accepting end components...");
 		JDDNode acc = mcLtl.findAcceptingStates(dra, modelProduct, fairness);
 
+		// Compute reachability probabilities
 		mainLog.println("\nComputing reachability probabilities...");
 		mcProduct = new NondetModelChecker(prism, modelProduct, null);
 		probsProduct = mcProduct.checkProbUntil(modelProduct.getReach(), acc, qual, min && fairness);
@@ -441,9 +445,10 @@ public class NondetModelChecker extends NonProbModelChecker
 
 		// Convert probability vector to original model
 		// First, filter over DRA start states
-		startMask = mcLtl.buildStartMask(dra, labelDDs);
+		// (which we can get from initial states of product model,
+		// because of the way it is constructed)
+		startMask = modelProduct.getStart();
 		probsProduct.filter(startMask);
-		JDD.Deref(startMask);
 		// Then sum over DD vars for the DRA state
 		draDDRowVars = new JDDVars();
 		draDDRowVars.addVars(modelProduct.getAllDDRowVars());

prism/src/prism/ProbModelChecker.java

@@ -29,19 +29,22 @@ package prism;
 import java.util.Vector;
 
 import jdd.*;
+import jltl2dstar.DRA;
+import jltl2dstar.LTL2Rabin;
 import dv.*;
 import mtbdd.*;
 import sparse.*;
 import hybrid.*;
 import parser.ast.*;
+import parser.visitor.ASTTraverse;
 
 /*
  * Model checker for DTMCs.
  */
 public class ProbModelChecker extends NonProbModelChecker
 {
-	// SCC computer
-	protected SCCComputer sccComputer;
+	// Model (DTMC or CTMC)
+	protected ProbModel model;
 
 	// Options (in addition to those inherited from StateModelChecker):
 
@@ -56,9 +59,10 @@ public class ProbModelChecker extends NonProbModelChecker
 	{
 		// Initialise
 		super(prism, m, pf);
-
-		// Create SCCComputer object
-		sccComputer = prism.getSCCComputer(m);
+		if (!(m instanceof ProbModel)) {
+			throw new PrismException("Wrong model type passed to ProbModelChecker.");
+		}
+		model = (ProbModel) m;
 
 		// Inherit some options from parent Prism object.
 		// Store locally and/or pass onto engines.
@@ -96,6 +100,13 @@ public class ProbModelChecker extends NonProbModelChecker
 		}
 	}
 
+	// Override-able "Constructor"
+
+	public ProbModelChecker createNewModelChecker(Prism prism, Model m, PropertiesFile pf) throws PrismException
+	{
+		return new ProbModelChecker(prism, m, pf);
+	}
+
 	// -----------------------------------------------------------------------------------
 	// Check a property, i.e. an expression
 	// -----------------------------------------------------------------------------------
@@ -350,6 +361,7 @@ public class ProbModelChecker extends NonProbModelChecker
 
 		// compute bottom strongly connected components (bsccs)
 		if (bsccComp) {
+			SCCComputer sccComputer = prism.getSCCComputer(model);
 			sccComputer.computeBSCCs();
 			vectBSCCs = sccComputer.getVectBSCCs();
 			notInBSCCs = sccComputer.getNotInBSCCs();
@@ -512,7 +524,8 @@ public class ProbModelChecker extends NonProbModelChecker
 		if (expr.isSimplePathFormula()) {
 			return checkProbPathFormulaSimple(expr, qual);
 		} else {
-			throw new PrismException("LTL-style path formulas are not yet supported");
+			return checkProbPathFormulaLTL(expr, qual);
+			//throw new PrismException("LTL-style path formulas are not yet supported");
 		}
 	}
 
@@ -562,6 +575,97 @@ public class ProbModelChecker extends NonProbModelChecker
 		return probs;
 	}
 
+	// LTL-like path formula for P operator
+
+	protected StateProbs checkProbPathFormulaLTL(Expression expr, boolean qual) throws PrismException
+	{
+		LTLModelChecker mcLtl;
+		StateProbs probsProduct = null, probs = null;
+		Expression ltl;
+		Vector<JDDNode> labelDDs;
+		DRA dra;
+		ProbModel modelProduct;
+		ProbModelChecker mcProduct;
+		JDDNode startMask;
+		JDDVars draDDRowVars;
+		int i;
+		long l;
+
+		// Can't do LTL with time-bounded variants of the temporal operators
+		try {
+			expr.accept(new ASTTraverse()
+			{
+				public void visitPre(ExpressionTemporal e) throws PrismLangException
+				{
+					if (e.getLowerBound() != null)
+						throw new PrismLangException(e.getOperatorSymbol());
+					if (e.getUpperBound() != null)
+						throw new PrismLangException(e.getOperatorSymbol());
+				}
+			});
+		} catch (PrismLangException e) {
+			String s = "Temporal operators (like " + e.getMessage() + ")";
+			s += " cannot have time bounds for LTL properties";
+			throw new PrismException(s);
+		}
+
+		// For LTL model checking routines
+		mcLtl = new LTLModelChecker(prism);
+
+		// Model check maximal state formulas
+		labelDDs = new Vector<JDDNode>();
+		ltl = mcLtl.checkMaximalStateFormulas(this, model, expr.deepCopy(), labelDDs);
+
+		// Convert LTL formula to deterministic Rabin automaton (DRA)
+		mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")...");
+		l = System.currentTimeMillis();
+		dra = LTL2Rabin.ltl2rabin(ltl.convertForJltl2ba());
+		mainLog.println("\nDRA has " + dra.size() + " states, " + dra.acceptance().size() + " pairs.");
+		// dra.print(System.out);
+		l = System.currentTimeMillis() - l;
+		mainLog.println("\nTime for Rabin translation: " + l / 1000.0 + " seconds.");
+
+		// Build product of Markov chain and automaton
+		// (note: might be a CTMC - StochModelChecker extends this class)
+		mainLog.println("\nConstructing MC-DRA product...");
+		modelProduct = mcLtl.constructProductMC(dra, model, labelDDs);
+		mainLog.println();
+		modelProduct.printTransInfo(mainLog, prism.getExtraDDInfo());
+		// prism.exportStatesToFile(modelProduct, Prism.EXPORT_PLAIN, null);
+		// prism.exportTransToFile(modelProduct, true, Prism.EXPORT_PLAIN, null);
+		
+		// Find accepting maximum end BSCC
+		mainLog.println("\nFinding accepting BSCCs...");
+		JDDNode acc = mcLtl.findAcceptingBSCCs(dra, modelProduct);
+
+		// Compute reachability probabilities
+		mainLog.println("\nComputing reachability probabilities...");
+		mcProduct = createNewModelChecker(prism, modelProduct, null);
+		probsProduct = mcProduct.checkProbUntil(modelProduct.getReach(), acc, qual);
+		
+		// Convert probability vector to original model
+		// First, filter over DRA start states
+		// (which we can get from initial states of product model,
+		// because of the way it is constructed)
+		startMask = modelProduct.getStart();
+		probsProduct.filter(startMask);
+		// Then sum over DD vars for the DRA state
+		draDDRowVars = new JDDVars();
+		draDDRowVars.addVars(modelProduct.getAllDDRowVars());
+		draDDRowVars.removeVars(allDDRowVars);
+		probs = probsProduct.sumOverDDVars(draDDRowVars, model);
+
+		// Deref, clean up
+		probsProduct.clear();
+		modelProduct.clear();
+		for (i = 0; i < labelDDs.size(); i++) {
+			JDD.Deref(labelDDs.get(i));
+		}
+		JDD.Deref(acc);
+
+		return probs;
+	}
+
 	// next
 
 	protected StateProbs checkProbNext(ExpressionTemporal expr) throws PrismException
@@ -640,6 +744,8 @@ public class ProbModelChecker extends NonProbModelChecker
 
 	// until (unbounded)
 
+	// this method is split into two steps so that the LTL model checker can use the second part directly
+
 	protected StateProbs checkProbUntil(ExpressionTemporal expr, boolean qual) throws PrismException
 	{
 		JDDNode b1, b2;
@@ -660,6 +766,27 @@ public class ProbModelChecker extends NonProbModelChecker
 		// mainLog.print(" states, b2 = " + JDD.GetNumMintermsString(b2,
 		// allDDRowVars.n()) + " states\n");
 
+		try {
+			probs = checkProbUntil(b1, b2, qual);
+		} catch (PrismException e) {
+			JDD.Deref(b1);
+			JDD.Deref(b2);
+			throw e;
+		}
+
+		// derefs
+		JDD.Deref(b1);
+		JDD.Deref(b2);
+
+		return probs;
+	}
+
+	// until (unbounded): b1/b2 are bdds for until operands
+
+	protected StateProbs checkProbUntil(JDDNode b1, JDDNode b2, boolean qual) throws PrismException
+	{
+		StateProbs probs = null;
+
 		// compute probabilities
 
 		// if requested (i.e. when prob bound is 0 or 1 and precomputation algorithms are enabled),
@@ -671,19 +798,9 @@ public class ProbModelChecker extends NonProbModelChecker
 		}
 		// otherwise actually compute probabilities
 		else {
-			try {
-				probs = computeUntilProbs(trans, trans01, b1, b2);
-			} catch (PrismException e) {
-				JDD.Deref(b1);
-				JDD.Deref(b2);
-				throw e;
-			}
+			probs = computeUntilProbs(trans, trans01, b1, b2);
 		}
 
-		// derefs
-		JDD.Deref(b1);
-		JDD.Deref(b2);
-
 		return probs;
 	}
 
@@ -795,6 +912,7 @@ public class ProbModelChecker extends NonProbModelChecker
 
 		// compute bottom strongly connected components (bsccs)
 		if (bsccComp) {
+			SCCComputer sccComputer = prism.getSCCComputer(model);
 			sccComputer.computeBSCCs();
 			vectBSCCs = sccComputer.getVectBSCCs();
 			notInBSCCs = sccComputer.getNotInBSCCs();
@@ -940,6 +1058,7 @@ public class ProbModelChecker extends NonProbModelChecker
 
 		// compute bottom strongly connected components (bsccs)
 		if (bsccComp) {
+			SCCComputer sccComputer = prism.getSCCComputer(model);
 			sccComputer.computeBSCCs();
 			vectBSCCs = sccComputer.getVectBSCCs();
 			notInBSCCs = sccComputer.getNotInBSCCs();

prism/src/prism/StochModelChecker.java

@@ -63,6 +63,13 @@ public class StochModelChecker extends ProbModelChecker
 		super(prism, m, pf);
 	}
 
+	// Override-able "Constructor"
+
+	public ProbModelChecker createNewModelChecker(Prism prism, Model m, PropertiesFile pf) throws PrismException
+	{
+		return new StochModelChecker(prism, m, pf);
+	}
+
 	// -----------------------------------------------------------------------------------
 	// Check method for each operator
 	// -----------------------------------------------------------------------------------