Adapt (symbolic) adapt LTLModelChecker to support generic acceptance types for DTMC. [Joachim Klein]

Adapt product construction (rename dra to da)
Switch from findAcceptingBSCCsForRabin() to generic findAcceptingBSCCs()



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

prism/src/prism/LTLModelChecker.java

@@ -32,6 +32,8 @@ import java.util.BitSet;
 import java.util.List;
 import java.util.Vector;
 
+import acceptance.AcceptanceOmega;
+import acceptance.AcceptanceOmegaDD;
 import acceptance.AcceptanceRabin;
 import jdd.JDD;
 import jdd.JDDNode;
@@ -139,41 +141,41 @@ public class LTLModelChecker extends PrismComponent
 	}
 
 	/**
-	 * Construct the product of a DRA and a DTMC/CTMC.
-	 * @param dra The DRA
-	 * @param model The  DTMC/CTMC
+	 * Construct the product of a DA and a DTMC/CTMC.
+	 * @param da The DA
+	 * @param model The DTMC/CTMC
 	 * @param labelDDs BDDs giving the set of states for each AP in the DRA
 	 */
-	public ProbModel constructProductMC(DA<BitSet,AcceptanceRabin> dra, ProbModel model, Vector<JDDNode> labelDDs) throws PrismException
+	public ProbModel constructProductMC(DA<BitSet, ? extends AcceptanceOmega> da, ProbModel model, Vector<JDDNode> labelDDs) throws PrismException
 	{
-		return constructProductMC(dra, model, labelDDs, null, null, true);
+		return constructProductMC(da, model, labelDDs, null, null, true);
 	}
 
 	/**
-	 * Construct the product of a DRA and a DTMC/CTMC.
-	 * @param dra The DRA
+	 * Construct the product of a DA and a DTMC/CTMC.
+	 * @param dra The DA
 	 * @param model The  DTMC/CTMC
-	 * @param labelDDs BDDs giving the set of states for each AP in the DRA
-	 * @param draDDRowVarsCopy (Optionally) empty JDDVars object to obtain copy of DD row vars for DRA
-	 * @param draDDColVarsCopy (Optionally) empty JDDVars object to obtain copy of DD col vars for DRA
+	 * @param labelDDs BDDs giving the set of states for each AP in the DA
+	 * @param daDDRowVarsCopy (Optionally) empty JDDVars object to obtain copy of DD row vars for DA
+	 * @param daDDColVarsCopy (Optionally) empty JDDVars object to obtain copy of DD col vars for DA
 	 */
-	public ProbModel constructProductMC(DA<BitSet,AcceptanceRabin> dra, ProbModel model, Vector<JDDNode> labelDDs, JDDVars draDDRowVarsCopy, JDDVars draDDColVarsCopy)
+	public ProbModel constructProductMC(DA<BitSet, ? extends AcceptanceOmega> da, ProbModel model, Vector<JDDNode> labelDDs, JDDVars daDDRowVarsCopy, JDDVars daDDColVarsCopy)
 			throws PrismException
 	{
-		return constructProductMC(dra, model, labelDDs, draDDRowVarsCopy, draDDColVarsCopy, true);
+		return constructProductMC(da, model, labelDDs, daDDRowVarsCopy, daDDColVarsCopy, true);
 	}
 
 	/**
-	 * Construct the product of a DRA and a DTMC/CTMC.
-	 * @param dra The DRA
+	 * Construct the product of a DA and a DTMC/CTMC.
+	 * @param da The DA
 	 * @param model The  DTMC/CTMC
-	 * @param labelDDs BDDs giving the set of states for each AP in the DRA
-	 * @param draDDRowVarsCopy (Optionally) empty JDDVars object to obtain copy of DD row vars for DRA
-	 * @param draDDColVarsCopy (Optionally) empty JDDVars object to obtain copy of DD col vars for DRA
+	 * @param labelDDs BDDs giving the set of states for each AP in the DA
+	 * @param daDDRowVarsCopy (Optionally) empty JDDVars object to obtain copy of DD row vars for DA
+	 * @param daDDColVarsCopy (Optionally) empty JDDVars object to obtain copy of DD col vars for DA
 	 * @param allInit Do we assume that all states of the original model are initial states?
 	 *        (just for the purposes of reachability)
 	 */
-	public ProbModel constructProductMC(DA<BitSet,AcceptanceRabin> dra, ProbModel model, Vector<JDDNode> labelDDs, JDDVars draDDRowVarsCopy, JDDVars draDDColVarsCopy,
+	public ProbModel constructProductMC(DA<BitSet, ? extends AcceptanceOmega> da, ProbModel model, Vector<JDDNode> labelDDs, JDDVars daDDRowVarsCopy, JDDVars daDDColVarsCopy,
 			boolean allInit) throws PrismException
 	{
 		// Existing model - dds, vars, etc.
@@ -189,9 +191,9 @@ public class LTLModelChecker extends PrismComponent
 		JDDVars newAllDDRowVars, newAllDDColVars;
 		Vector<String> newDDVarNames;
 		VarList newVarList;
-		String draVar;
-		// DRA stuff
-		JDDVars draDDRowVars, draDDColVars;
+		String daVar;
+		// DA stuff
+		JDDVars daDDRowVars, daDDColVars;
 		// Misc
 		int i, j, n;
 		boolean before;
@@ -204,16 +206,16 @@ public class LTLModelChecker extends PrismComponent
 		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;
+		// Create a (new, unique) name for the variable that will represent DA states
+		daVar = "_da";
+		while (varList.getIndex(daVar) != -1) {
+			daVar = "_" + daVar;
 		}
 
-		// See how many new dd vars will be needed for DRA
+		// See how many new dd vars will be needed for DA
 		// and whether there is room to put them before rather than after the existing vars
-		// (if DRA only has one state, we add an extra dummy state)
-		n = (int) Math.ceil(PrismUtils.log2(dra.size()));
+		// (if DA only has one state, we add an extra dummy state)
+		n = (int) Math.ceil(PrismUtils.log2(da.size()));
 		n = Math.max(n, 1);
 		before = true;
 		if (allDDRowVars.getMinVarIndex() - 1 < 2 * n) {
@@ -222,28 +224,28 @@ public class LTLModelChecker extends PrismComponent
 
 		// If passed in var lists are null, create new lists
 		// (which won't be accessible later in this case)
-		draDDRowVars = (draDDRowVarsCopy == null) ? new JDDVars() : draDDRowVarsCopy;
-		draDDColVars = (draDDColVarsCopy == null) ? new JDDVars() : draDDColVarsCopy;
+		daDDRowVars = (daDDRowVarsCopy == null) ? new JDDVars() : daDDRowVarsCopy;
+		daDDColVars = (daDDColVarsCopy == null) ? new JDDVars() : daDDColVarsCopy;
 		// Create the new dd variables
 		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++));
+			daDDRowVars.addVar(JDD.Var(j++));
+			daDDColVars.addVar(JDD.Var(j++));
 			if (!before) {
 				newDDVarNames.add("");
 				newDDVarNames.add("");
 			}
-			newDDVarNames.set(j - 2, draVar + "." + i);
-			newDDVarNames.set(j - 1, draVar + "'." + i);
+			newDDVarNames.set(j - 2, daVar + "." + i);
+			newDDVarNames.set(j - 1, daVar + "'." + 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;
+		newVarDDRowVars[before ? 0 : varDDRowVars.length] = daDDRowVars;
+		newVarDDColVars[before ? 0 : varDDColVars.length] = daDDColVars;
 		for (i = 0; i < varDDRowVars.length; i++) {
 			newVarDDRowVars[before ? i + 1 : i] = new JDDVars();
 			newVarDDColVars[before ? i + 1 : i] = new JDDVars();
@@ -253,19 +255,19 @@ public class LTLModelChecker extends PrismComponent
 		newAllDDRowVars = new JDDVars();
 		newAllDDColVars = new JDDVars();
 		if (before) {
-			newAllDDRowVars.addVars(draDDRowVars);
-			newAllDDColVars.addVars(draDDColVars);
+			newAllDDRowVars.addVars(daDDRowVars);
+			newAllDDColVars.addVars(daDDColVars);
 			newAllDDRowVars.addVars(allDDRowVars);
 			newAllDDColVars.addVars(allDDColVars);
 		} else {
 			newAllDDRowVars.addVars(allDDRowVars);
 			newAllDDColVars.addVars(allDDColVars);
-			newAllDDRowVars.addVars(draDDRowVars);
-			newAllDDColVars.addVars(draDDColVars);
+			newAllDDRowVars.addVars(daDDRowVars);
+			newAllDDColVars.addVars(daDDColVars);
 		}
 		newVarList = (VarList) varList.clone();
-		// NB: if DRA only has one state, we add an extra dummy state
-		Declaration decl = new Declaration(draVar, new DeclarationInt(Expression.Int(0), Expression.Int(Math.max(dra.size() - 1, 1))));
+		// NB: if DA only has one state, we add an extra dummy state
+		Declaration decl = new Declaration(daVar, new DeclarationInt(Expression.Int(0), Expression.Int(Math.max(da.size() - 1, 1))));
 		newVarList.addVar(before ? 0 : varList.getNumVars(), decl, 1, model.getConstantValues());
 
 		// Extra references (because will get derefed when new model is done with)
@@ -277,11 +279,11 @@ public class LTLModelChecker extends PrismComponent
 			model.getModuleDDRowVars(i).refAll();
 			model.getModuleDDColVars(i).refAll();
 		}
-		draDDRowVars.refAll();
-		draDDColVars.refAll();
+		daDDRowVars.refAll();
+		daDDColVars.refAll();
 
 		// Build transition matrix for product
-		newTrans = buildTransMask(dra, labelDDs, allDDRowVars, allDDColVars, draDDRowVars, draDDColVars);
+		newTrans = buildTransMask(da, labelDDs, allDDRowVars, allDDColVars, daDDRowVars, daDDColVars);
 		JDD.Ref(model.getTrans());
 		newTrans = JDD.Apply(JDD.TIMES, model.getTrans(), newTrans);
 
@@ -293,7 +295,7 @@ public class LTLModelChecker extends PrismComponent
 		// but some of these may not be reachable from the initial state of the product model.
 		// Optionally (if allInit is false), we don't do this - maybe because we only care about result for the initial state
 		// Note that we reset the initial states after reachability, corresponding to just the initial states of the original model.  
-		newStart = buildStartMask(dra, labelDDs, draDDRowVars);
+		newStart = buildStartMask(da, labelDDs, daDDRowVars);
 		JDD.Ref(allInit ? model.getReach() : model.getStart());
 		newStart = JDD.And(allInit ? model.getReach() : model.getStart(), newStart);
 
@@ -320,20 +322,20 @@ public class LTLModelChecker extends PrismComponent
 		modelProd.findDeadlocks(false);
 		if (modelProd.getDeadlockStates().size() > 0) {
 			// Assuming original model has no deadlocks, neither should product
-			throw new PrismException("Model-DRA product has deadlock states");
+			throw new PrismException("Model-"+da.getAutomataType()+" product has deadlock states");
 		}
 
 		// Reset initial state
-		newStart = buildStartMask(dra, labelDDs, draDDRowVars);
+		newStart = buildStartMask(da, labelDDs, daDDRowVars);
 		JDD.Ref(model.getStart());
 		newStart = JDD.And(model.getStart(), newStart);
 		modelProd.setStart(newStart);
 
-		// Reference DRA DD vars (if being returned)
-		if (draDDRowVarsCopy != null)
-			draDDRowVarsCopy.refAll();
-		if (draDDColVarsCopy != null)
-			draDDColVarsCopy.refAll();
+		// Reference DA DD vars (if being returned)
+		if (daDDRowVarsCopy != null)
+			daDDRowVarsCopy.refAll();
+		if (daDDColVarsCopy != null)
+			daDDColVarsCopy.refAll();
 
 		return modelProd;
 	}
@@ -562,30 +564,30 @@ public class LTLModelChecker extends PrismComponent
 
 	/**
 	 * Builds a (referenced) mask BDD representing all possible transitions in a product built with
-	 * DRA {@code dra}, i.e. all the transitions ((s,q),(s',q')) where q' = delta(q, label(s')) in the DRA.
+	 * DA {@code da}, i.e. all the transitions ((s,q),(s',q')) where q' = delta(q, label(s')) in the DA.
 	 * So the BDD is over column variables for model states (permuted from those found in the BDDs in
-	 * {@code labelDDs}) and row/col variables for the DRA (from {@code draDDRowVars}, {@code draDDColVars}).
+	 * {@code labelDDs}) and row/col variables for the DA (from {@code daDDRowVars}, {@code daDDColVars}).
 	 */
-	public JDDNode buildTransMask(DA<BitSet,AcceptanceRabin> dra, Vector<JDDNode> labelDDs, JDDVars allDDRowVars, JDDVars allDDColVars, JDDVars draDDRowVars,
-			JDDVars draDDColVars)
+	public JDDNode buildTransMask(DA<BitSet, ? extends AcceptanceOmega> da, Vector<JDDNode> labelDDs, JDDVars allDDRowVars, JDDVars allDDColVars, JDDVars daDDRowVars,
+			JDDVars daDDColVars)
 	{
-		JDDNode draMask, label, exprBDD, transition;
+		JDDNode daMask, label, exprBDD, transition;
 		int i, j, k, numAPs, numStates, numEdges;
 
-		numAPs = dra.getAPList().size();
-		draMask = JDD.Constant(0);
-		// Iterate through all (states and) transitions of DRA
-		numStates = dra.size();
+		numAPs = da.getAPList().size();
+		daMask = JDD.Constant(0);
+		// Iterate through all (states and) transitions of DA
+		numStates = da.size();
 		for (i = 0; i < numStates; i++) {
-			numEdges = dra.getNumEdges(i);
+			numEdges = da.getNumEdges(i);
 			for (j = 0; j < numEdges; j++) {
 				// Build a transition label BDD for each edge
 				label = JDD.Constant(1);
 				for (k = 0; k < numAPs; k++) {
 					// Get the expression BDD for AP k (via label "Lk")
-					exprBDD = labelDDs.get(Integer.parseInt(dra.getAPList().get(k).substring(1)));
+					exprBDD = labelDDs.get(Integer.parseInt(da.getAPList().get(k).substring(1)));
 					JDD.Ref(exprBDD);
-					if (!dra.getEdgeLabel(i, j).get(k)) {
+					if (!da.getEdgeLabel(i, j).get(k)) {
 						exprBDD = JDD.Not(exprBDD);
 					}
 					label = JDD.And(label, exprBDD);
@@ -593,48 +595,48 @@ public class LTLModelChecker extends PrismComponent
 				// 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, i, dra.getEdgeDest(i, j), 1);
+				transition = JDD.SetMatrixElement(JDD.Constant(0), daDDRowVars, daDDColVars, i, da.getEdgeDest(i, j), 1);
 				// Now get the conjunction of the two
 				transition = JDD.And(transition, label);
-				// Add edge BDD to the DRA transition mask
-				draMask = JDD.Or(draMask, transition);
+				// Add edge BDD to the DA transition mask
+				daMask = JDD.Or(daMask, transition);
 			}
 		}
 
-		return draMask;
+		return daMask;
 	}
 
 	/**
 	 * Builds a (referenced) mask BDD representing all possible "start" states for a product built with
-	 * DRA {@code dra}, i.e. all the states (s,q) where q = delta(q_init, label(s)) in the DRA.
+	 * DA {@code da}, i.e. all the states (s,q) where q = delta(q_init, label(s)) in the DA.
 	 * So the BDD is over row variables for model states (as found in the BDDs in {@code labelDDs})
-	 * and row variables for the DRA (from {@code draDDRowVars}).
+	 * and row variables for the DA (from {@code daDDRowVars}).
 	 */
-	public JDDNode buildStartMask(DA<BitSet,AcceptanceRabin> dra, Vector<JDDNode> labelDDs, JDDVars draDDRowVars)
+	public JDDNode buildStartMask(DA<BitSet,? extends AcceptanceOmega> da, Vector<JDDNode> labelDDs, JDDVars daDDRowVars)
 	{
 		JDDNode startMask, label, exprBDD, dest, tmp;
 		int i, j, k, numAPs, numEdges;
 
-		numAPs = dra.getAPList().size();
+		numAPs = da.getAPList().size();
 		startMask = JDD.Constant(0);
-		// Iterate through all transitions of start state of DRA
-		i = dra.getStartState();
-		numEdges = dra.getNumEdges(i);
+		// Iterate through all transitions of start state of DA
+		i = da.getStartState();
+		numEdges = da.getNumEdges(i);
 		for (j = 0; j < numEdges; j++) {
 			// Build a transition label BDD for each edge
 			label = JDD.Constant(1);
 			for (k = 0; k < numAPs; k++) {
 				// Get the expression BDD for AP k (via label "Lk")
-				exprBDD = labelDDs.get(Integer.parseInt(dra.getAPList().get(k).substring(1)));
+				exprBDD = labelDDs.get(Integer.parseInt(da.getAPList().get(k).substring(1)));
 				JDD.Ref(exprBDD);
-				if (!dra.getEdgeLabel(i, j).get(k)) {
+				if (!da.getEdgeLabel(i, j).get(k)) {
 					exprBDD = JDD.Not(exprBDD);
 				}
 				label = JDD.And(label, exprBDD);
 			}
-			// Build a BDD for the DRA destination state
+			// Build a BDD for the DA destination state
 			dest = JDD.Constant(0);
-			dest = JDD.SetVectorElement(dest, draDDRowVars, dra.getEdgeDest(i, j), 1);
+			dest = JDD.SetVectorElement(dest, daDDRowVars, da.getEdgeDest(i, j), 1);
 
 			// Now get the conjunction of the two
 			tmp = JDD.And(dest, label);
@@ -681,17 +683,15 @@ public class LTLModelChecker extends PrismComponent
 
 	/**
 	 * Find the set of accepting BSCCs in a model wrt a Rabin acceptance condition.
-	 * @param dra The DRA storing the Rabin acceptance condition
-	 * @param draDDRowVars BDD row variables for the DRA part of the model
-	 * @param draDDColVars BDD column variables for the DRA part of the model
+	 * Find the set of accepting BSCCs in a model wrt an acceptance condition.
+	 * @param acceptance the acceptance condition, with BDD based storage
 	 * @param model The model
 	 * @return A referenced BDD for the union of all states in accepting BSCCs
 	 */
-	public JDDNode findAcceptingBSCCsForRabin(DA<BitSet,AcceptanceRabin> dra, ProbModel model, JDDVars draDDRowVars, JDDVars draDDColVars) throws PrismException
+	public JDDNode findAcceptingBSCCs(AcceptanceOmegaDD acceptance, ProbModel model) throws PrismException
 	{
 		JDDNode allAcceptingStates;
 		List<JDDNode> vectBSCCs;
-		int i;
 
 		allAcceptingStates = JDD.Constant(0);
 		// Compute all BSCCs for model
@@ -700,34 +700,16 @@ public class LTLModelChecker extends PrismComponent
 		vectBSCCs = sccComputer.getBSCCs();
 		JDD.Deref(sccComputer.getNotInBSCCs());
 
-		// Build BDDs for !L_i and K_i
-		ArrayList<JDDNode> statesL_not = new ArrayList<JDDNode>();
-		ArrayList<JDDNode> statesK = new ArrayList<JDDNode>();
-		for (i = 0; i < dra.getAcceptance().size(); i++) {
-			statesL_not.add(buildLStatesForRabinPair(draDDRowVars, dra, i, true));
-			statesK.add(buildKStatesForRabinPair(draDDRowVars, dra, i));
-		}
-		
-		// Go through the BSCCs
+		// Go through the BSCC
 		for (JDDNode bscc : vectBSCCs) {
-			// Go through the DRA acceptance pairs (L_i, K_i)
-			for (i = 0; i < dra.getAcceptance().size(); i++) {
-				// Check each BSCC for inclusion in !L_i and intersection with K_i
-				if (JDD.IsContainedIn(bscc, statesL_not.get(i)) && JDD.AreInterecting(bscc, statesK.get(i))) {
-					// This BSCC is accepting: add and move on onto next one
-					JDD.Ref(bscc);
-					allAcceptingStates = JDD.Or(allAcceptingStates, bscc);
-					break;
-				}
+			// Check for acceptance
+			if (acceptance.isBSCCAccepting(bscc)) {
+				// This BSCC is accepting: add to allAcceptingStates
+				JDD.Ref(bscc);
+				allAcceptingStates = JDD.Or(allAcceptingStates, bscc);
 			}
 			JDD.Deref(bscc);
 		}
-		
-		// Dereference BDDs for !L_i and K_i
-		for (i = 0; i < statesK.size(); i++) {
-			JDD.Deref(statesL_not.get(i));
-			JDD.Deref(statesK.get(i));
-		}
 
 		return allAcceptingStates;
 	}

prism/src/prism/ProbModelChecker.java

@@ -34,7 +34,9 @@ import java.util.BitSet;
 import java.util.List;
 import java.util.Vector;
 
-import acceptance.AcceptanceRabin;
+import acceptance.AcceptanceOmega;
+import acceptance.AcceptanceOmegaDD;
+import acceptance.AcceptanceType;
 import jdd.JDD;
 import jdd.JDDNode;
 import jdd.JDDVars;
@@ -498,17 +500,17 @@ public class ProbModelChecker extends NonProbModelChecker
 		StateValues probsProduct = null, probs = null;
 		Expression ltl;
 		Vector<JDDNode> labelDDs;
-		DA<BitSet,AcceptanceRabin> dra;
+		DA<BitSet, ? extends AcceptanceOmega> da;
 		ProbModel modelProduct;
 		ProbModelChecker mcProduct;
 		JDDNode startMask;
-		JDDVars draDDRowVars, draDDColVars;
+		JDDVars daDDRowVars, daDDColVars;
 		int i;
 		long l;
 
 		if (Expression.containsTemporalTimeBounds(expr)) {
 			if (model.getModelType().continuousTime()) {
-				throw new PrismException("DRA construction for time-bounded operators not supported for " + model.getModelType()+".");
+				throw new PrismException("DA construction for time-bounded operators not supported for " + model.getModelType()+".");
 			}
 
 			if (expr.isSimplePathFormula()) {
@@ -532,29 +534,30 @@ public class ProbModelChecker extends NonProbModelChecker
 		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 + ")...");
+		// Convert LTL formula to deterministic automaton (DA)
+		mainLog.println("\nBuilding deterministic automaton (for " + ltl + ")...");
 		l = System.currentTimeMillis();
 		LTL2DA ltl2da = new LTL2DA(prism);
-		dra = ltl2da.convertLTLFormulaToDRA(ltl, constantValues);
-		mainLog.println("DRA has " + dra.size() + " states, " + dra.getAcceptance().getSizeStatistics()+".");
+		AcceptanceType[] allowedAcceptance = {AcceptanceType.RABIN};
+		da = ltl2da.convertLTLFormulaToDA(ltl, constantValues, allowedAcceptance);
+		mainLog.println(da.getAutomataType()+" has " + da.size() + " states, " + da.getAcceptance().getSizeStatistics() + ".");
 		l = System.currentTimeMillis() - l;
-		mainLog.println("Time for Rabin translation: " + l / 1000.0 + " seconds.");
-		// If required, export DRA 
+		mainLog.println("Time for deterministic automaton translation: " + l / 1000.0 + " seconds.");
+		// If required, export DA
 		if (prism.getSettings().getExportPropAut()) {
-			mainLog.println("Exporting DRA to file \"" + prism.getSettings().getExportPropAutFilename() + "\"...");
+			mainLog.println("Exporting DA to file \"" + prism.getSettings().getExportPropAutFilename() + "\"...");
 			PrismLog out = new PrismFileLog(prism.getSettings().getExportPropAutFilename());
-			out.println(dra);
+			out.println(da);
 			out.close();
 			//dra.printDot(new java.io.PrintStream("dra.dot"));
 		}
 
 		// Build product of Markov chain and automaton
 		// (note: might be a CTMC - StochModelChecker extends this class)
-		mainLog.println("\nConstructing MC-DRA product...");
-		draDDRowVars = new JDDVars();
-		draDDColVars = new JDDVars();
-		modelProduct = mcLtl.constructProductMC(dra, model, labelDDs, draDDRowVars, draDDColVars);
+		mainLog.println("\nConstructing MC-"+da.getAutomataType()+" product...");
+		daDDRowVars = new JDDVars();
+		daDDColVars = new JDDVars();
+		modelProduct = mcLtl.constructProductMC(da, model, labelDDs, daDDRowVars, daDDColVars);
 		mainLog.println();
 		modelProduct.printTransInfo(mainLog, prism.getExtraDDInfo());
 		// Output product, if required
@@ -575,20 +578,22 @@ public class ProbModelChecker extends NonProbModelChecker
 
 		// Find accepting BSCCs + compute reachability probabilities
 		mainLog.println("\nFinding accepting BSCCs...");
-		JDDNode acc = mcLtl.findAcceptingBSCCsForRabin(dra, modelProduct, draDDRowVars, draDDColVars);
+		AcceptanceOmegaDD acceptance = da.getAcceptance().toAcceptanceDD(daDDRowVars);
+		JDDNode acc = mcLtl.findAcceptingBSCCs(acceptance, modelProduct);
+		acceptance.clear();
 		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
-		startMask = mcLtl.buildStartMask(dra, labelDDs, draDDRowVars);
+		startMask = mcLtl.buildStartMask(da, labelDDs, daDDRowVars);
 		JDD.Ref(model.getReach());
 		startMask = JDD.And(model.getReach(), startMask);
 		probsProduct.filter(startMask);
-		// Then sum over DD vars for the DRA state (could also have used,
-		// e.g. max, since there is just one state for each valuation of draDDRowVars) 
-		probs = probsProduct.sumOverDDVars(draDDRowVars, model);
+		// Then sum over DD vars for the DA state (could also have used,
+		// e.g. max, since there is just one state for each valuation of daDDRowVars) 
+		probs = probsProduct.sumOverDDVars(daDDRowVars, model);
 
 		// Deref, clean up
 		probsProduct.clear();
@@ -598,8 +603,8 @@ public class ProbModelChecker extends NonProbModelChecker
 		}
 		JDD.Deref(acc);
 		JDD.Deref(startMask);
-		draDDRowVars.derefAll();
-		draDDColVars.derefAll();
+		daDDRowVars.derefAll();
+		daDDColVars.derefAll();
 
 		return probs;
 	}