Adapt (explicit) LTLModelChecker to support generic acceptance types. [Joachim Klein]

Adapt product constructions (rename dra to da, generic lifting of acceptance)
Generic findAcceptingBSCCs() and findAcceptingECStates()



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

prism/src/explicit/DTMCModelChecker.java

@@ -31,6 +31,7 @@ import java.util.BitSet;
 import java.util.List;
 import java.util.Map;
 
+import acceptance.AcceptanceType;
 import parser.ast.Expression;
 import parser.type.TypeDouble;
 import prism.PrismComponent;
@@ -65,11 +66,12 @@ public class DTMCModelChecker extends ProbModelChecker
 		mcLtl = new LTLModelChecker(this);
 
 		// Build product of Markov chain and automaton
-		product = mcLtl.constructProductMC(this, (DTMC)model, expr, statesOfInterest);
+		AcceptanceType[] allowedAcceptance = {AcceptanceType.RABIN};
+		product = mcLtl.constructProductMC(this, (DTMC)model, expr, statesOfInterest, allowedAcceptance);
 
 		// Find accepting BSCCs + compute reachability probabilities
 		mainLog.println("\nFinding accepting BSCCs...");
-		BitSet acceptingBSCCs = mcLtl.findAcceptingBSCCsForRabin(product.getProductModel(), product.getAcceptance());
+		BitSet acceptingBSCCs = mcLtl.findAcceptingBSCCs(product.getProductModel(), product.getAcceptance());
 		mainLog.println("\nComputing reachability probabilities...");
 		mcProduct = new DTMCModelChecker(this);
 		mcProduct.inheritSettings(this);

prism/src/explicit/LTLModelChecker.java

@@ -38,7 +38,9 @@ import java.util.List;
 import java.util.Map;
 import java.util.Vector;
 
+import acceptance.AcceptanceOmega;
 import acceptance.AcceptanceRabin;
+import acceptance.AcceptanceType;
 import common.IterableStateSet;
 import parser.State;
 import parser.ast.Expression;
@@ -64,14 +66,14 @@ public class LTLModelChecker extends PrismComponent
 {
 	/** Make LTL product accessible as a Product */
 	public class LTLProduct<M extends Model> extends Product<M> {
-		private int draSize;
+		private int daSize;
 		private int invMap[];
-		private AcceptanceRabin acceptance;
+		private AcceptanceOmega acceptance;
 
-		public LTLProduct(M productModel, M originalModel, AcceptanceRabin acceptance, int draSize, int[] invMap)
+		public LTLProduct(M productModel, M originalModel, AcceptanceOmega acceptance, int daSize, int[] invMap)
 		{
 			super(productModel, originalModel);
-			this.draSize = draSize;
+			this.daSize = daSize;
 			this.invMap = invMap;
 			this.acceptance = acceptance;
 		}
@@ -79,18 +81,22 @@ public class LTLModelChecker extends PrismComponent
 		@Override
 		public int getModelState(int productState)
 		{
-			return invMap[productState] / draSize;
+			return invMap[productState] / daSize;
 		}
 
 		@Override
 		public int getAutomatonState(int productState)
 		{
-			return invMap[productState] % draSize;
+			return invMap[productState] % daSize;
 		}
 
-		public AcceptanceRabin getAcceptance() {
+		public AcceptanceOmega getAcceptance() {
 			return acceptance;
 		}
+
+		public void setAcceptance(AcceptanceOmega acceptance) {
+			this.acceptance = acceptance;
+		}
 	}
 
 
@@ -180,18 +186,19 @@ public class LTLModelChecker extends PrismComponent
 	}
 
 	/**
-	 * Generate the DRA for the given LTL expression and construct the product.
+	 * Generate a deterministic automaton for the given LTL expression and construct the product.
 	 *
 	 * @param mc a ProbModelChecker, used for checking maximal state formulas
 	 * @param dtmc the model
 	 * @param expr a path expression
  	 * @param statesOfInterest the set of states for which values should be calculated (null = all states)
-	 * @return the product with the DRA
+ 	 * @param allowedAcceptance the allowed acceptance types
+	 * @return the product with the DA
 	 */
-	public LTLProduct<DTMC> constructProductMC(ProbModelChecker mc, DTMC dtmc, Expression expr, BitSet statesOfInterest) throws PrismException
+	public LTLProduct<DTMC> constructProductMC(ProbModelChecker mc, DTMC dtmc, Expression expr, BitSet statesOfInterest, AcceptanceType... allowedAcceptance) throws PrismException
 	{
 		Expression ltl;
-		DA<BitSet,AcceptanceRabin> dra;
+		DA<BitSet,? extends AcceptanceOmega> da;
 		LTLProduct<DTMC> product;
 		long time;
 
@@ -218,26 +225,27 @@ public class LTLModelChecker extends PrismComponent
 		Vector<BitSet> labelBS = new Vector<BitSet>();
 		ltl = checkMaximalStateFormulas(mc, dtmc, expr.deepCopy(), labelBS);
 
-		// Convert LTL formula to deterministic Rabin automaton (DRA)
-		mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")...");
+		// Convert LTL formula to deterministic automaton
+		mainLog.println("\nBuilding deterministic automaton (for " + ltl + ")...");
 		time = System.currentTimeMillis();
 		LTL2DA ltl2da = new LTL2DA(this);
-		dra = ltl2da.convertLTLFormulaToDRA(ltl, mc.getConstantValues());
-		mainLog.println("DRA has " + dra.size() + " states, " + dra.getAcceptance().getSizeStatistics() + ".");
+		da = ltl2da.convertLTLFormulaToDA(ltl, mc.getConstantValues(), allowedAcceptance);
+		mainLog.println(da.getAutomataType()+" has " + da.size() + " states, " + da.getAcceptance().getSizeStatistics() + ".");
 		time = System.currentTimeMillis() - time;
-		mainLog.println("Time for Rabin translation: " + time / 1000.0 + " seconds.");
+		mainLog.println("Time for "+da.getAutomataType()+" translation: " + time / 1000.0 + " seconds.");
 		// If required, export DRA
 		if (settings.getExportPropAut()) {
 			mainLog.println("Exporting DRA to file \"" + settings.getExportPropAutFilename() + "\"...");
 			PrismLog out = new PrismFileLog(settings.getExportPropAutFilename());
-			out.println(dra);
+			out.println(da);
 			out.close();
 			//dra.printDot(new java.io.PrintStream("dra.dot"));
 		}
 
+
 		// Build product of Markov chain and automaton
-		mainLog.println("\nConstructing MC-DRA product...");
-		product = constructProductMC(dra, dtmc, labelBS, statesOfInterest);
+		mainLog.println("\nConstructing MC-"+da.getAutomataType()+" product...");
+		product = constructProductMC(da, dtmc, labelBS, statesOfInterest);
 
 		mainLog.print("\n" + product.getProductModel().infoStringTable());
 
@@ -245,30 +253,29 @@ public class LTLModelChecker extends PrismComponent
 	}
 
 	/**
-	 * Construct the product of a DRA and a DTMC.
-	 * @param dra The DRA
+	 * Construct the product of a DA and a DTMC.
+	 * @param dra The DA
 	 * @param dtmc The DTMC
-	 * @param labelBS BitSets giving the set of states for each AP in the DRA
+	 * @param labelBS BitSets giving the set of states for each AP in the DA
 	 * @param statesOfInterest the set of states for which values should be calculated (null = all states)
 	 * @return The product DTMC
 	 */
-	public LTLProduct<DTMC> constructProductMC(DA<BitSet,AcceptanceRabin> dra, DTMC dtmc, Vector<BitSet> labelBS, BitSet statesOfInterest) throws PrismException
+	public LTLProduct<DTMC> constructProductMC(DA<BitSet,? extends AcceptanceOmega> da, DTMC dtmc, Vector<BitSet> labelBS, BitSet statesOfInterest) throws PrismException
 	{
 		DTMCSimple prodModel = new DTMCSimple();
 
-		int draSize = dra.size();
-		int numAPs = dra.getAPList().size();
+		int daSize = da.size();
+		int numAPs = da.getAPList().size();
 		int modelNumStates = dtmc.getNumStates();
-		int prodNumStates = modelNumStates * draSize;
+		int prodNumStates = modelNumStates * daSize;
 		int s_1, s_2, q_1, q_2;
 		BitSet s_labels = new BitSet(numAPs);
-		AcceptanceRabin prodAcceptance;
 		List<State> prodStatesList = null;
 
 		// Encoding: 
-		// each state s' = <s, q> = s * draSize + q
-		// s(s') = s' / draSize
-		// q(s') = s' % draSize
+		// each state s' = <s, q> = s * daSize + q
+		// s(s') = s' / daSize
+		// q(s') = s' % daSize
 
 		LinkedList<Point> queue = new LinkedList<Point>();
 		int map[] = new int[prodNumStates];
@@ -287,15 +294,15 @@ public class LTLModelChecker extends PrismComponent
 		for (int s_0 : new IterableStateSet(statesOfInterest, dtmc.getNumStates())) {
 			// Get BitSet representing APs (labels) satisfied by state s_0
 			for (int k = 0; k < numAPs; k++) {
-				s_labels.set(k, labelBS.get(Integer.parseInt(dra.getAPList().get(k).substring(1))).get(s_0));
+				s_labels.set(k, labelBS.get(Integer.parseInt(da.getAPList().get(k).substring(1))).get(s_0));
 			}
-			// Find corresponding initial state in DRA
-			int q_0 = dra.getEdgeDestByLabel(dra.getStartState(), s_labels);
+			// Find corresponding initial state in DA
+			int q_0 = da.getEdgeDestByLabel(da.getStartState(), s_labels);
 			// Add (initial) state to product
 			queue.add(new Point(s_0, q_0));
 			prodModel.addState();
 			prodModel.addInitialState(prodModel.getNumStates() - 1);
-			map[s_0 * draSize + q_0] = prodModel.getNumStates() - 1;
+			map[s_0 * daSize + q_0] = prodModel.getNumStates() - 1;
 			if (prodStatesList != null) {
 				// store DTMC state information for the product state
 				prodStatesList.add(dtmc.getStatesList().get(s_0));
@@ -308,7 +315,7 @@ public class LTLModelChecker extends PrismComponent
 			Point p = queue.pop();
 			s_1 = p.x;
 			q_1 = p.y;
-			visited.set(s_1 * draSize + q_1);
+			visited.set(s_1 * daSize + q_1);
 
 			// Go through transitions from state s_1 in original DTMC
 			Iterator<Map.Entry<Integer, Double>> iter = dtmc.getTransitionsIterator(s_1);
@@ -318,21 +325,21 @@ public class LTLModelChecker extends PrismComponent
 				double prob = e.getValue();
 				// Get BitSet representing APs (labels) satisfied by successor state s_2
 				for (int k = 0; k < numAPs; k++) {
-					s_labels.set(k, labelBS.get(Integer.parseInt(dra.getAPList().get(k).substring(1))).get(s_2));
+					s_labels.set(k, labelBS.get(Integer.parseInt(da.getAPList().get(k).substring(1))).get(s_2));
 				}
 				// Find corresponding successor in DRA
-				q_2 = dra.getEdgeDestByLabel(q_1, s_labels);
+				q_2 = da.getEdgeDestByLabel(q_1, s_labels);
 				// Add state/transition to model
-				if (!visited.get(s_2 * draSize + q_2) && map[s_2 * draSize + q_2] == -1) {
+				if (!visited.get(s_2 * daSize + q_2) && map[s_2 * daSize + q_2] == -1) {
 					queue.add(new Point(s_2, q_2));
 					prodModel.addState();
-					map[s_2 * draSize + q_2] = prodModel.getNumStates() - 1;
+					map[s_2 * daSize + q_2] = prodModel.getNumStates() - 1;
 					if (prodStatesList != null) {
 						// store DTMC state information for the product state
 						prodStatesList.add(dtmc.getStatesList().get(s_2));
 					}
 				}
-				prodModel.setProbability(map[s_1 * draSize + q_1], map[s_2 * draSize + q_2], prob);
+				prodModel.setProbability(map[s_1 * daSize + q_1], map[s_2 * daSize + q_2], prob);
 			}
 		}
 
@@ -350,15 +357,10 @@ public class LTLModelChecker extends PrismComponent
 			prodModel.setStatesList(prodStatesList);
 		}
 
-		prodAcceptance = new AcceptanceRabin();
-		LTLProduct<DTMC> product = new LTLProduct<DTMC>(prodModel, dtmc, prodAcceptance, draSize, invMap);
+		LTLProduct<DTMC> product = new LTLProduct<DTMC>(prodModel, dtmc, null, daSize, invMap);
 
 		// generate acceptance for the product model by lifting
-		for (AcceptanceRabin.RabinPair pair : dra.getAcceptance()) {
-			BitSet Lprod = product.liftFromAutomaton(pair.getL());
-			BitSet Kprod = product.liftFromAutomaton(pair.getK());
-			prodAcceptance.add(new AcceptanceRabin.RabinPair(Lprod, Kprod));
-		}
+		product.setAcceptance(liftAcceptance(product, da.getAcceptance()));
 
 		// lift the labels
 		for (String label : dtmc.getLabels()) {
@@ -369,18 +371,20 @@ public class LTLModelChecker extends PrismComponent
 		return product;
 	}
 	/**
-	 * Generate the DRA for the given LTL expression and construct the product.
+	 * Generate the DA for the given LTL expression and construct the product.
 	 *
 	 * @param mc a ProbModelChecker, used for checking maximal state formulas
 	 * @param model the model
 	 * @param expr a path expression
- 	 * @param statesOfInterest the set of states for which values should be calculated (null = all states)
-	 * @return the product with the DRA
+	 * @param statesOfInterest the set of states for which values should be calculated (null = all states)
+	 * @param allowedAcceptance the allowed acceptance conditions
+	 * @return the product with the DA
+	 * @throws PrismException
 	 */
-	public LTLProduct<MDP> constructProductMDP(ProbModelChecker mc, MDP model, Expression expr, BitSet statesOfInterest) throws PrismException
+	public LTLProduct<MDP> constructProductMDP(ProbModelChecker mc, MDP model, Expression expr, BitSet statesOfInterest, AcceptanceType... allowedAcceptance) throws PrismException
 	{
 		Expression ltl;
-		DA<BitSet,AcceptanceRabin> dra;
+		DA<BitSet, ? extends AcceptanceOmega> da;
 		LTLProduct<MDP> product;
 		long time;
 
@@ -407,26 +411,26 @@ public class LTLModelChecker extends PrismComponent
 		Vector<BitSet> labelBS = new Vector<BitSet>();
 		ltl = checkMaximalStateFormulas(mc, model, expr.deepCopy(), labelBS);
 
-		// Convert LTL formula to deterministic Rabin automaton (DRA)
-		mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")...");
+		// Convert LTL formula to deterministic automaton
+		mainLog.println("\nBuilding deterministic automaton (for " + ltl + ")...");
 		time = System.currentTimeMillis();
 		LTL2DA ltl2da = new LTL2DA(this);
-		dra = ltl2da.convertLTLFormulaToDRA(ltl, mc.getConstantValues());
-		mainLog.println("DRA has " + dra.size() + " states, " + dra.getAcceptance().getSizeStatistics() + ".");
+		da = ltl2da.convertLTLFormulaToDA(ltl, mc.getConstantValues(), allowedAcceptance);
+		mainLog.println(da.getAutomataType()+" has " + da.size() + " states, " + da.getAcceptance().getSizeStatistics() + ".");
 		time = System.currentTimeMillis() - time;
-		mainLog.println("Time for Rabin translation: " + time / 1000.0 + " seconds.");
-		// If required, export DRA
+		mainLog.println("Time for "+da.getAutomataType()+" translation: " + time / 1000.0 + " seconds.");
+		// If required, export DA
 		if (settings.getExportPropAut()) {
-			mainLog.println("Exporting DRA to file \"" + settings.getExportPropAutFilename() + "\"...");
+			mainLog.println("Exporting "+da.getAutomataType()+" to file \"" + settings.getExportPropAutFilename() + "\"...");
 			PrismLog out = new PrismFileLog(settings.getExportPropAutFilename());
-			out.println(dra);
+			out.println(da);
 			out.close();
-			//dra.printDot(new java.io.PrintStream("dra.dot"));
+			//da.printDot(new java.io.PrintStream("da.dot"));
 		}
 
 		// Build product of MDP and automaton
-		mainLog.println("\nConstructing MDP-DRA product...");
-		product = constructProductMDP(dra, (MDP) model, labelBS, statesOfInterest);
+		mainLog.println("\nConstructing MDP-"+da.getAutomataType()+" product...");
+		product = constructProductMDP(da, model, labelBS, statesOfInterest);
 
 		mainLog.print("\n" + product.getProductModel().infoStringTable());
 
@@ -434,24 +438,23 @@ public class LTLModelChecker extends PrismComponent
 	}
 
 	/**
-	 * Construct the product of a DRA and an MDP.
-	 * @param dra The DRA
+	 * Construct the product of a DA and an MDP.
+	 * @param da The DA
 	 * @param mdp The MDP
-	 * @param labelBS BitSets giving the set of states for each AP in the DRA
+	 * @param labelBS BitSets giving the set of states for each AP in the DA
 	 * @param statesOfInterest the set of states for which values should be calculated (null = all states)
 	 * @return The product MDP
 	 */
-	public LTLProduct<MDP> constructProductMDP(DA<BitSet,AcceptanceRabin> dra, MDP mdp, Vector<BitSet> labelBS, BitSet statesOfInterest) throws PrismException
+	public LTLProduct<MDP> constructProductMDP(DA<BitSet,? extends AcceptanceOmega> da, MDP mdp, Vector<BitSet> labelBS, BitSet statesOfInterest) throws PrismException
 	{
 		MDPSimple prodModel = new MDPSimple();
 
-		int draSize = dra.size();
-		int numAPs = dra.getAPList().size();
+		int daSize = da.size();
+		int numAPs = da.getAPList().size();
 		int modelNumStates = mdp.getNumStates();
-		int prodNumStates = modelNumStates * draSize;
+		int prodNumStates = modelNumStates * daSize;
 		int s_1, s_2, q_1, q_2;
 		BitSet s_labels = new BitSet(numAPs);
-		AcceptanceRabin prodAcceptance;
 		List<State> prodStatesList = null;
 
 
@@ -477,15 +480,15 @@ public class LTLModelChecker extends PrismComponent
 		for (int s_0 : new IterableStateSet(statesOfInterest, mdp.getNumStates())) {
 			// Get BitSet representing APs (labels) satisfied by state s_0
 			for (int k = 0; k < numAPs; k++) {
-				s_labels.set(k, labelBS.get(Integer.parseInt(dra.getAPList().get(k).substring(1))).get(s_0));
+				s_labels.set(k, labelBS.get(Integer.parseInt(da.getAPList().get(k).substring(1))).get(s_0));
 			}
 			// Find corresponding initial state in DRA
-			int q_0 = dra.getEdgeDestByLabel(dra.getStartState(), s_labels);
+			int q_0 = da.getEdgeDestByLabel(da.getStartState(), s_labels);
 			// Add (initial) state to product
 			queue.add(new Point(s_0, q_0));
 			prodModel.addState();
 			prodModel.addInitialState(prodModel.getNumStates() - 1);
-			map[s_0 * draSize + q_0] = prodModel.getNumStates() - 1;
+			map[s_0 * daSize + q_0] = prodModel.getNumStates() - 1;
 			if (prodStatesList != null) {
 				// store MDP state information for the product state
 				prodStatesList.add(mdp.getStatesList().get(s_0));
@@ -498,7 +501,7 @@ public class LTLModelChecker extends PrismComponent
 			Point p = queue.pop();
 			s_1 = p.x;
 			q_1 = p.y;
-			visited.set(s_1 * draSize + q_1);
+			visited.set(s_1 * daSize + q_1);
 
 			// Go through transitions from state s_1 in original DTMC
 			int numChoices = mdp.getNumChoices(s_1);
@@ -511,23 +514,23 @@ public class LTLModelChecker extends PrismComponent
 					double prob = e.getValue();
 					// Get BitSet representing APs (labels) satisfied by successor state s_2
 					for (int k = 0; k < numAPs; k++) {
-						s_labels.set(k, labelBS.get(Integer.parseInt(dra.getAPList().get(k).substring(1))).get(s_2));
+						s_labels.set(k, labelBS.get(Integer.parseInt(da.getAPList().get(k).substring(1))).get(s_2));
 					}
 					// Find corresponding successor in DRA
-					q_2 = dra.getEdgeDestByLabel(q_1, s_labels);
+					q_2 = da.getEdgeDestByLabel(q_1, s_labels);
 					// Add state/transition to model
-					if (!visited.get(s_2 * draSize + q_2) && map[s_2 * draSize + q_2] == -1) {
+					if (!visited.get(s_2 * daSize + q_2) && map[s_2 * daSize + q_2] == -1) {
 						queue.add(new Point(s_2, q_2));
 						prodModel.addState();
-						map[s_2 * draSize + q_2] = prodModel.getNumStates() - 1;
+						map[s_2 * daSize + q_2] = prodModel.getNumStates() - 1;
 						if (prodStatesList != null) {
 							// store MDP state information for the product state
 							prodStatesList.add(mdp.getStatesList().get(s_2));
 						}
 					}
-					prodDistr.set(map[s_2 * draSize + q_2], prob);
+					prodDistr.set(map[s_2 * daSize + q_2], prob);
 				}
-				prodModel.addActionLabelledChoice(map[s_1 * draSize + q_1], prodDistr, mdp.getAction(s_1, j));
+				prodModel.addActionLabelledChoice(map[s_1 * daSize + q_1], prodDistr, mdp.getAction(s_1, j));
 			}
 		}
 
@@ -545,15 +548,10 @@ public class LTLModelChecker extends PrismComponent
 			prodModel.setStatesList(prodStatesList);
 		}
 
-		prodAcceptance = new AcceptanceRabin();
-		LTLProduct<MDP> product = new LTLProduct<MDP>(prodModel, mdp, prodAcceptance, draSize, invMap);
+		LTLProduct<MDP> product = new LTLProduct<MDP>(prodModel, mdp, null, daSize, invMap);
 
 		// generate acceptance for the product model by lifting
-		for (AcceptanceRabin.RabinPair pair : dra.getAcceptance()) {
-			BitSet Lprod = product.liftFromAutomaton(pair.getL());
-			BitSet Kprod = product.liftFromAutomaton(pair.getK());
-			prodAcceptance.add(new AcceptanceRabin.RabinPair(Lprod, Kprod));
-		}
+		product.setAcceptance(liftAcceptance(product, da.getAcceptance()));
 
 		// lift the labels
 		for (String label : mdp.getLabels()) {
@@ -565,11 +563,11 @@ public class LTLModelChecker extends PrismComponent
 	}
 
 	/**
-	 * Find the set of states belong to accepting BSCCs in a model wrt a Rabin acceptance condition.
+	 * Find the set of states that belong to accepting BSCCs in a model wrt an acceptance condition.
 	 * @param model The model
-	 * @param acceptance The Rabin acceptance condition
+	 * @param acceptance The acceptance condition
 	 */
-	public BitSet findAcceptingBSCCsForRabin(Model model, AcceptanceRabin acceptance) throws PrismException
+	public BitSet findAcceptingBSCCs(Model model, AcceptanceOmega acceptance) throws PrismException
 	{
 		// Compute bottom strongly connected components (BSCCs)
 		SCCComputer sccComputer = SCCComputer.createSCCComputer(this, model);
@@ -588,10 +586,25 @@ public class LTLModelChecker extends PrismComponent
 		return result;
 	}
 
+	/**
+	 * Compute the set of states in end components of the model that are accepting
+	 * with regard to the acceptance condition.
+	 * @param model the model
+	 * @param acceptance the acceptance condition
+	 * @return BitSet with the set of states that are accepting
+	 */
+	public BitSet findAcceptingECStates(NondetModel model, AcceptanceOmega acceptance) throws PrismException
+	{
+		if (acceptance instanceof AcceptanceRabin) {
+			return findAcceptingECStatesForRabin(model, (AcceptanceRabin) acceptance);
+		}
+		throw new PrismException("Computing end components for acceptance type '"+acceptance.getTypeName()+"' currently not supported (explicit engine).");
+	}
+
 	/**
 	 * Find the set of states in accepting end components (ECs) in a nondeterministic model wrt a Rabin acceptance condition.
 	 * @param model The model
-	 * @param acceptance the acceptance condition
+	 * @param acceptance The acceptance condition
 	 */
 	public BitSet findAcceptingECStatesForRabin(NondetModel model, AcceptanceRabin acceptance) throws PrismException
 	{
@@ -626,4 +639,23 @@ public class LTLModelChecker extends PrismComponent
 
 		return allAcceptingStates;
 	}
+
+	/** Lift the acceptance condition from the automaton to the product states. */
+	private AcceptanceOmega liftAcceptance(final LTLProduct<?> product, AcceptanceOmega acceptance)
+	{
+		// make a copy of the acceptance condition
+		AcceptanceOmega lifted = acceptance.clone();
+
+		// lift state sets
+		lifted.lift(new AcceptanceOmega.LiftBitSet() {
+			@Override
+			public BitSet lift(BitSet states)
+			{
+				return product.liftFromAutomaton(states);
+			}
+		});
+
+		return lifted;
+	}
+
 }

prism/src/explicit/MDPModelChecker.java

@@ -31,6 +31,7 @@ import java.util.Iterator;
 import java.util.List;
 import java.util.Map;
 
+import acceptance.AcceptanceType;
 import parser.ast.Expression;
 import prism.PrismComponent;
 import prism.PrismDevNullLog;
@@ -75,11 +76,12 @@ public class MDPModelChecker extends ProbModelChecker
 		// For LTL model checking routines
 		mcLtl = new LTLModelChecker(this);
 
-		product = mcLtl.constructProductMDP(this, (MDP)model, expr, statesOfInterest);
+		AcceptanceType[] allowedAcceptance = {AcceptanceType.RABIN};
+		product = mcLtl.constructProductMDP(this, (MDP)model, expr, statesOfInterest, allowedAcceptance);
 		
 		// Find accepting MECs + compute reachability probabilities
 		mainLog.println("\nFinding accepting MECs...");
-		BitSet acceptingMECs = mcLtl.findAcceptingECStatesForRabin(product.getProductModel(), product.getAcceptance());
+		BitSet acceptingMECs = mcLtl.findAcceptingECStates(product.getProductModel(), product.getAcceptance());
 		mainLog.println("\nComputing reachability probabilities...");
 		mcProduct = new MDPModelChecker(this);
 		mcProduct.inheritSettings(this);