Replace ExplicitFiles2ModulesFile with ExplicitFiles2ModelInfo.

prism/src/explicit/ExplicitFiles2Model.java

@@ -39,7 +39,7 @@ import java.util.Map.Entry;
 
 import common.IterableStateSet;
 import parser.State;
-import parser.ast.ModulesFile;
+import prism.ModelInfo;
 import prism.PrismComponent;
 import prism.PrismException;
 import prism.PrismNotSupportedException;
@@ -80,20 +80,20 @@ public class ExplicitFiles2Model extends PrismComponent
 	
 	/**
 	 * Build a Model corresponding to the passed in states/transitions/labels files.
-	 * Variable info and model type is taken from {@code modulesFile}.
+	 * Variable info and model type is taken from a {@code ModelInfo} object.
 	 * The number of states should also be passed in as {@code numStates}.
 	 *
 	 * @param statesFile .sta file (optional, may be {@code null})
 	 * @param transFile .tra file
 	 * @param labelsFile .lab file (optional, may be {@code null})
-	 * @param modulesFile modules file (normally created with ExplicitFiles2ModulesFile)
+	 * @param modelInfo model info (normally created with ExplicitFiles2ModelInfo)
 	 * @param numStates number of states
 	 * @return the constructed model
 	 */
-	public Model build(File statesFile, File transFile, File labelsFile, ModulesFile modulesFile, int numStates) throws PrismException
+	public Model build(File statesFile, File transFile, File labelsFile, ModelInfo modelInfo, int numStates) throws PrismException
 	{
 		ModelExplicit model = null;
-		switch (modulesFile.getModelType()) {
+		switch (modelInfo.getModelType()) {
 		case DTMC:
 			DTMCSimple dtmc = new DTMCSimple();
 			dtmc.buildFromPrismExplicit(transFile.getAbsolutePath());
@@ -114,10 +114,10 @@ public class ExplicitFiles2Model extends PrismComponent
 		case PTA:
 		case SMG:
 		case STPG:
-			throw new PrismNotSupportedException("Currently, importing " + modulesFile.getModelType() + " is not supported");
+			throw new PrismNotSupportedException("Currently, importing " + modelInfo.getModelType() + " is not supported");
 		}
 		if (model == null) {
-			throw new PrismException("Could not import " + modulesFile.getModelType());
+			throw new PrismException("Could not import " + modelInfo.getModelType());
 		}
 
 		if (model.getNumStates() == 0) {
@@ -139,7 +139,7 @@ public class ExplicitFiles2Model extends PrismComponent
 		model.findDeadlocks(fixdl);
 		
 		if (statesFile != null) {
-			loadStates(model, statesFile, modulesFile);
+			loadStates(model, statesFile, modelInfo);
 		} else {
 			// in absence of a statesFile, there is a single variable x
 			// in the model, with value corresponding to the state index
@@ -178,7 +178,7 @@ public class ExplicitFiles2Model extends PrismComponent
 	}
 
 	/** Load the state information, construct the statesList and attach to model */
-	private void loadStates(ModelExplicit model, File statesFile, ModulesFile mf) throws PrismException
+	private void loadStates(ModelExplicit model, File statesFile, ModelInfo modelInfo) throws PrismException
 	{
 		int numStates = model.getNumStates();
 		List<State> statesList = new ArrayList<State>(numStates);
@@ -189,7 +189,7 @@ public class ExplicitFiles2Model extends PrismComponent
 		String s, ss[];
 		int i, j, lineNum = 0;
 
-		int numVars = mf.getNumVars();
+		int numVars = modelInfo.getNumVars();
 
 		// open file for reading, automatic close when done
 		try (BufferedReader in = new BufferedReader(new FileReader(statesFile))) {

prism/src/parser/ast/ExpressionIdent.java

@@ -150,6 +150,13 @@ public class ExpressionIdent extends Expression
 			return false;
 		return true;
 	}
+	
+	// Static utility methods
+	
+	public static boolean isLegalIdentifierName(String name)
+	{
+		return name.matches("[_a-zA-z][_a-zA-z0-9]*");
+	}
 }
 
 //------------------------------------------------------------------------------

prism/src/prism/ExplicitFiles2MTBDD.java

@@ -42,7 +42,6 @@ import jdd.JDDNode;
 import jdd.JDDVars;
 import parser.Values;
 import parser.VarList;
-import parser.ast.ModulesFile;
 
 /**
  * Class to convert explicit-state file storage of a model to symbolic representation.
@@ -60,7 +59,7 @@ public class ExplicitFiles2MTBDD
 	private File stateRewardsFile;
 
 	// Model info
-	private ModulesFile modulesFile;
+	private ModelInfo modelInfo;
 	private ModelType modelType;
 	private VarList varList;
 	private int numVars;
@@ -117,18 +116,18 @@ public class ExplicitFiles2MTBDD
 
 	/**
 	 * Build a Model corresponding to the passed in states/transitions/labels files.
-	 * Variable info and model type is taken from {@code modulesFile}.
+	 * Variable info and model type is taken from a {@code ModelInfo} object.
 	 * The number of states should also be passed in as {@code numStates}.
 	 */
-	public Model build(File statesFile, File transFile, File labelsFile, File stateRewardsFile, ModulesFile modulesFile, int numStates) throws PrismException
+	public Model build(File statesFile, File transFile, File labelsFile, File stateRewardsFile, ModelInfo modelInfo, int numStates) throws PrismException
 	{
 		this.statesFile = statesFile;
 		this.transFile = transFile;
 		this.labelsFile = labelsFile;
 		this.stateRewardsFile = stateRewardsFile;
-		this.modulesFile = modulesFile;
-		modelType = modulesFile.getModelType();
-		varList = modulesFile.createVarList();
+		this.modelInfo = modelInfo;
+		modelType = modelInfo.getModelType();
+		varList = modelInfo.createVarList();
 		numVars = varList.getNumVars();
 		this.numStates = numStates;
 		modelVariables = new ModelVariablesDD();
@@ -248,8 +247,6 @@ public class ExplicitFiles2MTBDD
 		// compute state rewards
 		computeStateRewards();
 
-		int numModules = 1; // just one module
-		String moduleNames[] = modulesFile.getModuleNames(); // whose name is stored here
 		Values constantValues = new Values(); // no constants
 
 		JDDNode stateRewardsArray[] = new JDDNode[1];
@@ -260,6 +257,9 @@ public class ExplicitFiles2MTBDD
 		rewardStructNames[0] = "";
 
 		// create new Model object to be returned
+		// they need a module name list, so we fake that
+		int numModules = 1;
+		String moduleNames[] = new String[] { "M" };
 		if (modelType == ModelType.DTMC) {
 			model = new ProbModel(trans, start, stateRewardsArray, transRewardsArray, rewardStructNames, allDDRowVars, allDDColVars, modelVariables, numModules,
 					moduleNames, moduleDDRowVars, moduleDDColVars, numVars, varList, varDDRowVars, varDDColVars, constantValues);

prism/src/parser/ExplicitFiles2ModulesFile.java → prism/src/prism/ExplicitFiles2ModelInfo.java

@@ -1,8 +1,8 @@
 //==============================================================================
 //	
-//	Copyright (c) 2002-
+//	Copyright (c) 2019-
 //	Authors:
-//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
+//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham)
 //	
 //------------------------------------------------------------------------------
 //	
@@ -24,44 +24,48 @@
 //	
 //==============================================================================
 
-package parser;
+package prism;
 
 import java.io.BufferedReader;
 import java.io.File;
 import java.io.FileReader;
 import java.io.IOException;
+import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.Collections;
+import java.util.List;
 import java.util.regex.Matcher;
 import java.util.regex.Pattern;
 
+import parser.VarList;
 import parser.ast.Declaration;
 import parser.ast.DeclarationBool;
 import parser.ast.DeclarationInt;
 import parser.ast.DeclarationType;
 import parser.ast.Expression;
 import parser.ast.ExpressionIdent;
-import parser.ast.ExpressionLiteral;
-import parser.ast.LabelList;
-import parser.ast.Module;
-import parser.ast.ModulesFile;
-import parser.ast.RewardStruct;
 import parser.type.Type;
 import parser.type.TypeBool;
 import parser.type.TypeInt;
-import prism.ModelType;
-import prism.PrismComponent;
-import prism.PrismException;
 
 /**
- * Class to build a (partial) ModulesFile corresponding to imported explicit-state file storage of a model.
- * Basically, the ModulesFile just stores the model type and variable info.
+ * Class to build a ModelInfo object corresponding to imported explicit-state file storage of a model.
+ * Basically, just stores the model type and variable info.
  * The number of states in the model is also extracted.
  */
-public class ExplicitFiles2ModulesFile extends PrismComponent
+public class ExplicitFiles2ModelInfo extends PrismComponent
 {
+	// Info extracted from files for ModelInfo object
+	private int numVars;
+	private List<String> varNames;
+	private List<Type> varTypes;
+	private VarList varList;
+	private List<String> labelNames;
+	
 	// Num states
 	private int numStates = 0;
 
-	public ExplicitFiles2ModulesFile(PrismComponent parent)
+	public ExplicitFiles2ModelInfo(PrismComponent parent)
 	{
 		super(parent);
 	}
@@ -76,66 +80,109 @@ public class ExplicitFiles2ModulesFile extends PrismComponent
 	}
 
 	/**
-	 * Build a ModulesFile corresponding to the passed in states/transitions/labels files.
+	 * Build a ModelInfo object corresponding to the passed in states/transitions/labels files.
 	 * If {@code typeOverride} is null, we assume model is an MDP.
 	 *
 	 * @param statesFile states file (may be {@code null})
 	 * @param transFile transitions file
 	 * @param labelsFile labels file (may be {@code null})
 	 */
-	public ModulesFile buildModulesFile(File statesFile, File transFile, File labelsFile, File stateRewardsFile, ModelType typeOverride) throws PrismException
+	public ModelInfo buildModelInfo(File statesFile, File transFile, File labelsFile, ModelType typeOverride) throws PrismException
 	{
-		ModulesFile modulesFile;
-		ModelType modelType;
-
-		// Generate ModulesFile from states or transitions file, depending what is available
+		// Extract variable info from states or transitions file, depending on what is available
 		if (statesFile != null) {
-			modulesFile = createVarInfoFromStatesFile(statesFile);
+			extractVarInfoFromStatesFile(statesFile);
 		} else {
-			modulesFile = createVarInfoFromTransFile(transFile);
+			extractVarInfoFromTransFile(transFile);
 		}
 
-		// Generate and store a label list from the labelsFile, if available.
+		// Generate and store label names from the labels file, if available.
 		// This way, expressions can refer to the labels later on.
 		if (labelsFile != null) {
-			modulesFile.setLabelList(createLabelListFromLabelsFile(labelsFile));
+			extractLabelNamesFromLabelsFile(labelsFile);
 		}
 		
-		// Add a new (unnamed) reward structure if there is a state rewards file
-		if (stateRewardsFile != null) {
-			modulesFile.addRewardStruct(new RewardStruct());
-		}
-
 		// Set model type: if no preference stated, assume default of MDP
-		modelType = (typeOverride == null) ? ModelType.MDP : typeOverride;
-		modulesFile.setModelType(modelType);
+		ModelType modelType = (typeOverride == null) ? ModelType.MDP : typeOverride;
 
-		return modulesFile;
+		// Create and return ModelInfo object with above info 
+		ModelInfo modelInfo = new ModelInfo()
+		{
+			@Override
+			public ModelType getModelType()
+			{
+				return modelType;
+			}
+			
+			@Override
+			public List<String> getVarNames()
+			{
+				return varNames;
+			}
+			
+			@Override
+			public List<Type> getVarTypes()
+			{
+				return varTypes;
+			}
+			
+			@Override
+			public VarList createVarList() throws PrismException
+			{
+				return varList;
+			}
+			
+			@Override
+			public List<String> getLabelNames()
+			{
+				return labelNames;
+			}
+		};
+		
+		return modelInfo;
 	}
 
 	/**
-	 * Build a ModulesFile corresponding to a states file.
+	 * Build a "dummy" RewardGenerator object corresponding to the passed in rewards file.
+	 * Provides access to reward struct names, but not the rewards themselves.
+	 * @param stateRewardsFile state rewards file (may be {@code null})
 	 */
-	private ModulesFile createVarInfoFromStatesFile(File statesFile) throws PrismException
+	public RewardGenerator buildRewardInfo(File stateRewardsFile) throws PrismException
+	{
+		// Very simple for now: either 1 unnamed reward struct or none
+		if (stateRewardsFile != null) {
+			return new RewardGenerator()
+			{
+				@Override
+				public List<String> getRewardStructNames()
+				{
+					return Collections.singletonList("");
+				}
+			};
+		} else {
+			return new RewardGenerator()
+			{
+			};
+		}
+	}
+	
+	/**
+	 * Extract variable info from a states file.
+	 */
+	private void extractVarInfoFromStatesFile(File statesFile) throws PrismException
 	{
-		String s, ss[];
 		int i, j, lineNum = 0;
-		Module m;
 		Declaration d;
 		DeclarationType dt;
 		// Var info
-		int numVars;
-		String varNames[];
 		int varMins[];
 		int varMaxs[];
 		int varRanges[];
-		Type varTypes[];
-		ModulesFile modulesFile;
 
 		// open file for reading, automatic close when done
 		try (BufferedReader in = new BufferedReader(new FileReader(statesFile))) {
 			// read first line and extract var names
-			s = in.readLine();
+			String s = in.readLine();
 			lineNum = 1;
 			if (s == null)
 				throw new PrismException("empty states file");
@@ -143,13 +190,13 @@ public class ExplicitFiles2ModulesFile extends PrismComponent
 			if (s.charAt(0) != '(' || s.charAt(s.length() - 1) != ')')
 				throw new PrismException("badly formatted state");
 			s = s.substring(1, s.length() - 1);
-			varNames = s.split(",");
-			numVars = varNames.length;
+			varNames = new ArrayList<String>(Arrays.asList(s.split(",")));
+			numVars = varNames.size();
 			// create arrays to store info about vars
 			varMins = new int[numVars];
 			varMaxs = new int[numVars];
 			varRanges = new int[numVars];
-			varTypes = new Type[numVars];
+			varTypes = new ArrayList<Type>();
 			// read remaining lines
 			s = in.readLine();
 			lineNum++;
@@ -162,20 +209,21 @@ public class ExplicitFiles2ModulesFile extends PrismComponent
 					numStates++;
 					// split string
 					s = s.substring(s.indexOf('(') + 1, s.indexOf(')'));
-					ss = s.split(",");
+					String[] ss = s.split(",");
 					if (ss.length != numVars)
 						throw new PrismException("wrong number of variables");
 					// for each variable...
 					for (i = 0; i < numVars; i++) {
 						// if this is the first state, establish variable type
 						if (numStates == 1) {
-							if (ss[i].equals("true") || ss[i].equals("false"))
-								varTypes[i] = TypeBool.getInstance();
-							else
-								varTypes[i] = TypeInt.getInstance();
+							if (ss[i].equals("true") || ss[i].equals("false")) {
+								varTypes.add(TypeBool.getInstance());
+							} else {
+								varTypes.add(TypeInt.getInstance());
+							}
 						}
 						// check for new min/max values (ints only)
-						if (varTypes[i] instanceof TypeInt) {
+						if (varTypes.get(i) instanceof TypeInt) {
 							j = Integer.parseInt(ss[i]);
 							if (numStates == 1) {
 								varMins[i] = varMaxs[i] = j;
@@ -194,7 +242,7 @@ public class ExplicitFiles2ModulesFile extends PrismComponent
 			}
 			// compute variable ranges
 			for (i = 0; i < numVars; i++) {
-				if (varTypes[i] instanceof TypeInt) {
+				if (varTypes.get(i) instanceof TypeInt) {
 					varRanges[i] = varMaxs[i] - varMins[i];
 					// if range = 0, increment maximum - we don't allow zero-range variables
 					if (varRanges[i] == 0)
@@ -208,115 +256,83 @@ public class ExplicitFiles2ModulesFile extends PrismComponent
 		} catch (PrismException e) {
 			throw new PrismException("Error detected (" + e.getMessage() + ") at line " + lineNum + " of states file \"" + statesFile + "\"");
 		}
-		// create modules file
-		modulesFile = new ModulesFile();
-		m = new Module("M");
+		
+		varList = new VarList();
 		for (i = 0; i < numVars; i++) {
-			if (varTypes[i] instanceof TypeInt) {
+			if (varTypes.get(i) instanceof TypeInt) {
 				dt = new DeclarationInt(Expression.Int(varMins[i]), Expression.Int(varMaxs[i]));
-				d = new Declaration(varNames[i], dt);
+				d = new Declaration(varNames.get(i), dt);
 				d.setStart(Expression.Int(varMins[i]));
 			} else {
 				dt = new DeclarationBool();
-				d = new Declaration(varNames[i], dt);
+				d = new Declaration(varNames.get(i), dt);
 				d.setStart(Expression.False());
 			}
-			m.addDeclaration(d);
+			varList.addVar(d, -1, null);
 		}
-		modulesFile.addModule(m);
-		modulesFile.tidyUp();
-
-		return modulesFile;
 	}
 
 	/**
-	 * Build a ModulesFile corresponding to a transitions file.
+	 * Extract variable info from a transitions file.
 	 */
-	private ModulesFile createVarInfoFromTransFile(File transFile) throws PrismException
+	private void extractVarInfoFromTransFile(File transFile) throws PrismException
 	{
-		String s, ss[];
-		int lineNum = 0;
-		Module m;
-		Declaration d;
-		DeclarationType dt;
-		ModulesFile modulesFile;
-
-		// open file for reading, automatic close when done
+		// Open file for reading, automatic close when done
 		try (BufferedReader in = new BufferedReader(new FileReader(transFile))) {
-			// read first line and extract num states
-			s = in.readLine();
-			lineNum = 1;
+			// Read first line and extract num states
+			String s = in.readLine();
 			if (s == null)
 				throw new PrismException("empty transitions file");
 			s = s.trim();
-			ss = s.split(" ");
+			String[] ss = s.split(" ");
 			if (ss.length < 2)
 				throw new PrismException("");
 			numStates = Integer.parseInt(ss[0]);
 		} catch (IOException e) {
 			throw new PrismException("File I/O error reading from \"" + transFile + "\"");
 		} catch (NumberFormatException e) {
-			throw new PrismException("Error detected at line " + lineNum + " of transition matrix file \"" + transFile + "\"");
-		} catch (PrismException e) {
-			throw new PrismException("Error detected (" + e.getMessage() + ") at line " + lineNum + " of transition matrix file \"" + transFile + "\"");
+			throw new PrismException("Error detected at line 1 of transition matrix file \"" + transFile + "\"");
 		}
-		// create modules file
-		modulesFile = new ModulesFile();
-		m = new Module("M");
-		dt = new DeclarationInt(Expression.Int(0), Expression.Int(numStates - 1));
-		d = new Declaration("x", dt);
+		
+		varList = new VarList();
+		DeclarationType dt = new DeclarationInt(Expression.Int(0), Expression.Int(numStates - 1));
+		Declaration d = new Declaration("x", dt);
 		d.setStart(Expression.Int(0));
-		m.addDeclaration(d);
-		modulesFile.addModule(m);
-		modulesFile.tidyUp();
-
-		return modulesFile;
+		varList.addVar(d, -1, null);
 	}
 	
 
 	/**
-	 * Create a LabelList from a labels file, i.e., a label definition per
-	 * label that is encountered in the file.
-	 * <br>
-	 * In the label definitions, the label expression is set to "false",
-	 * the actual information about the states belonging to the label
-	 * is later on directly stored in the model.
-	 * <br>
+	 * Extract names of labels from the labels file.
 	 * The "init" and "deadlock" labels are skipped, as they have special
 	 * meaning and are implicitly defined for all models.
 	 */
-	private LabelList createLabelListFromLabelsFile(File labelsFile) throws PrismException
+	private void extractLabelNamesFromLabelsFile(File labelsFile) throws PrismException
 	{
-		LabelList list = new LabelList();
-
 		try (BufferedReader in = new BufferedReader(new FileReader(labelsFile))) {
-			// read first line (label names)
-			String labelNames = in.readLine();
-			// split
+			// Read/parse first line (label names)
+			// Looks like, e.g.: 0="init" 1="deadlock" 2="heads" 3="tails" 4="end"
+			String labelsString = in.readLine();
 			Pattern label = Pattern.compile("(\\d+)=\"([^\"]+)\"\\s*");
-			Matcher matcher = label.matcher(labelNames);
+			Matcher matcher = label.matcher(labelsString);
+			labelNames = new ArrayList<>();
 			while (matcher.find()) {
 				String labelName = matcher.group(2);
-
+				// Skip built-in labels
 				if (labelName.equals("init") || labelName.equals("deadlock")) {
-					// "init" and "deadlock" are special labels that exist
-					// in every model, so we don't need to add them to the ModulesFile
 					continue;
 				}
-
-				// TODO: Check that label name is valid identifier
-
-				if (list.getLabelIndex(labelName) != -1) {
-					throw new PrismException("duplicate label \"" + labelName + "\"");
+				// Check legal and non-dupe
+				if (!ExpressionIdent.isLegalIdentifierName(labelName)) {
+					throw new PrismException("Illegal label name \"" + labelName + "\"");
 				}
-
-				Expression falseExpression = new ExpressionLiteral(TypeBool.getInstance(), false);
-				list.addLabel(new ExpressionIdent(labelName), falseExpression);
+				if (labelNames.contains(labelName)) {
+					throw new PrismException("Duplicate label \"" + labelName + "\"");
+				}
+				labelNames.add(labelName);
 			}
 		} catch (IOException e) {
 			throw new PrismException("File I/O error reading from \"" + labelsFile + "\"");
 		}
-		return list;
 	}
-
 }

prism/src/prism/Prism.java

@@ -53,7 +53,6 @@ import param.ModelBuilder;
 import param.ParamModel;
 import param.ParamModelChecker;
 import param.ParamResult;
-import parser.ExplicitFiles2ModulesFile;
 import parser.PrismParser;
 import parser.State;
 import parser.Values;
@@ -1918,34 +1917,32 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 
 	/**
 	 * Load files containing an explicit list of transitions/etc. for subsequent model building.
-	 * A corresponding ModulesFile object is created and returned.
 	 * @param statesFile File containing a list of states (optional, can be null)
 	 * @param transFile File containing the list of transitions (required)
 	 * @param labelsFile File containing label definitions (optional, can be null)
 	 * @param stateRewardsFile File containing state reward definitions (optional, can be null)
 	 * @param typeOverride Type of model to be built (optional, use null if not required)
 	 */
-	public ModulesFile loadModelFromExplicitFiles(File statesFile, File transFile, File labelsFile, File stateRewardsFile, ModelType typeOverride) throws PrismException
+	public void loadModelFromExplicitFiles(File statesFile, File transFile, File labelsFile, File stateRewardsFile, ModelType typeOverride) throws PrismException
 	{
 		currentModelSource = ModelSource.EXPLICIT_FILES;
 		// Clear any existing built model(s)
 		clearBuiltModel();
-		// Construct ModulesFile
-		ExplicitFiles2ModulesFile ef2mf = new ExplicitFiles2ModulesFile(this);
-		currentModulesFile = ef2mf.buildModulesFile(statesFile, transFile, labelsFile, stateRewardsFile, typeOverride);
-		currentRewardGenerator = currentModulesFile;
+		// Construct ModelInfo
+		ExplicitFiles2ModelInfo ef2mi = new ExplicitFiles2ModelInfo(this);
+		currentModelInfo = ef2mi.buildModelInfo(statesFile, transFile, labelsFile, typeOverride);
+		currentModulesFile = null;
+		// Construct reward generator 
+		currentRewardGenerator = ef2mi.buildRewardInfo(stateRewardsFile);
 		// Store explicit files info for later
 		explicitFilesStatesFile = statesFile;
 		explicitFilesTransFile = transFile;
 		explicitFilesLabelsFile = labelsFile;
 		explicitFilesStateRewardsFile = stateRewardsFile;
-		explicitFilesNumStates = ef2mf.getNumStates();
+		explicitFilesNumStates = ef2mi.getNumStates();
 		// Reset dependent info
-		currentModelType = currentModulesFile == null ? null : currentModulesFile.getModelType();
-		currentModelInfo = currentModulesFile;
+		currentModelType = currentModelInfo == null ? null : currentModelInfo.getModelType();
 		currentDefinedMFConstants = null;
-
-		return currentModulesFile;
 	}
 
 	/**
@@ -2086,9 +2083,9 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 				if (!getExplicit()) {
 					expf2mtbdd = new ExplicitFiles2MTBDD(this);
 					currentModel = expf2mtbdd.build(explicitFilesStatesFile, explicitFilesTransFile, explicitFilesLabelsFile, explicitFilesStateRewardsFile,
-							currentModulesFile, explicitFilesNumStates);
+							currentModelInfo, explicitFilesNumStates);
 				} else {
-					currentModelExpl = new ExplicitFiles2Model(this).build(explicitFilesStatesFile, explicitFilesTransFile, explicitFilesLabelsFile, currentModulesFile, explicitFilesNumStates);
+					currentModelExpl = new ExplicitFiles2Model(this).build(explicitFilesStatesFile, explicitFilesTransFile, explicitFilesLabelsFile, currentModelInfo, explicitFilesNumStates);
 				}
 				break;
 			default:

prism/src/prism/PrismCL.java

@@ -618,7 +618,7 @@ public class PrismCL implements PrismModelListener
 					srf = new File(importStateRewardsFilename);
 				}
 				mainLog.println("...");
-				modulesFile = prism.loadModelFromExplicitFiles(sf, new File(modelFilename), lf, srf, typeOverride);
+				prism.loadModelFromExplicitFiles(sf, new File(modelFilename), lf, srf, typeOverride);
 			} else {
 				mainLog.print("\nParsing model file \"" + modelFilename + "\"...\n");
 				modulesFile = prism.parseModelFile(new File(modelFilename), typeOverride);