explicit.LTLModelChecker: construct a VarList for the Model-DA product if the model had a varlist

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

prism/src/explicit/LTLModelChecker.java

@@ -40,6 +40,9 @@ import java.util.Stack;
 import java.util.Vector;
 
 import parser.State;
+import parser.VarList;
+import parser.ast.Declaration;
+import parser.ast.DeclarationInt;
 import parser.ast.Expression;
 import parser.ast.ExpressionBinaryOp;
 import parser.ast.ExpressionLabel;
@@ -385,18 +388,43 @@ public class LTLModelChecker extends PrismComponent
 		BitSet s_labels = new BitSet(numAPs);
 		List<State> prodStatesList = null, daStatesList = null;
 
+		VarList newVarList = null;
+
+		if (model.getVarList() != null) {
+			VarList varList = model.getVarList();
+			// Create a (new, unique) name for the variable that will represent DA states
+			String daVar = "_da";
+			while (varList.getIndex(daVar) != -1) {
+				daVar = "_" + daVar;
+			}
+
+			newVarList = (VarList) varList.clone();
+			// 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(0, decl, 1, model.getConstantValues());
+		}
+
 		// Create a (simple, mutable) model of the appropriate type
 		ModelSimple prodModel = null;
 		switch (modelType) {
-		case DTMC:
-			prodModel = new DTMCSimple();
+		case DTMC: {
+			DTMCSimple dtmcProd = new DTMCSimple();
+			dtmcProd.setVarList(newVarList);
+			prodModel = dtmcProd;
 			break;
-		case MDP:
-			prodModel = new MDPSimple();
+		}
+		case MDP: {
+			MDPSimple mdpProd = new MDPSimple();
+			mdpProd.setVarList(newVarList);
+			prodModel = mdpProd;
 			break;
-		case STPG:
-			prodModel = new STPGExplicit();
+		}
+		case STPG: {
+			STPGExplicit stpgProd = new STPGExplicit();
+			stpgProd.setVarList(newVarList);
+			prodModel = stpgProd;
 			break;
+		}
 		default:
 			throw new PrismNotSupportedException("Model construction not supported for " + modelType + "s");
 		}