Rewards (and labels) attach-able to explicit.Model

prism/src/explicit/DTMCSparse.java

@@ -72,21 +72,7 @@ public class DTMCSparse extends DTMCExplicit<Double>
 	public DTMCSparse(final DTMC<Double> dtmc)
 	{
 		initialise(dtmc.getNumStates());
-		if (dtmc instanceof ActionListOwner) {
-			actionList.copyFrom(((ActionListOwner) dtmc).getActionList());
-		}
-		for (Integer state : dtmc.getDeadlockStates()) {
-			deadlocks.add(state);
-		}
-		for (Integer state : dtmc.getInitialStates()) {
-			initialStates.add(state);
-		}
-		constantValues = dtmc.getConstantValues();
-		varList = dtmc.getVarList();
-		statesList = dtmc.getStatesList();
-		for (String label : dtmc.getLabels()) {
-			labels.put(label, dtmc.getLabelStates(label));
-		}
+		copyFrom(dtmc);
 
 		// Copy transition function
 		final int numTransitions = dtmc.getNumTransitions();

prism/src/explicit/LTLModelChecker.java

@@ -40,6 +40,7 @@
 import java.util.Vector;
 
 import common.Interval;
+import explicit.rewards.MDPRewards;
 import parser.State;
 import parser.VarList;
 import parser.ast.Declaration;
@@ -754,11 +755,13 @@ protected <Value, M extends Model<Value>> LTLProduct<M> doConstructProductModel(
 		// generate acceptance for the product model by lifting
 		product.setAcceptance(liftAcceptance(product, da.getAcceptance()));
 
-		// lift the labels
+		// lift any labels
 		for (String label : model.getLabels()) {
 			BitSet liftedLabel = product.liftFromModel(model.getLabelStates(label));
 			prodModel.addLabel(label, liftedLabel);
 		}
+		// lift any rewards
+		((ModelSimple<Value>) prodModel).copyRewardsMapped(model, rews -> rews.liftFromModel(product));
 
 		return product;
 	}

prism/src/explicit/MDPSparse.java

@@ -98,14 +98,7 @@ public MDPSparse(final MDP<Double> mdp)
 	public MDPSparse(final MDP<Double> mdp, boolean sort)
 	{
 		initialise(mdp.getNumStates());
-		if (mdp instanceof ActionListOwner) {
-			actionList.copyFrom(((ActionListOwner) mdp).getActionList());
-		}
-		setStatesList(mdp.getStatesList());
-		setConstantValues(mdp.getConstantValues());
-		for (String label : mdp.getLabels()) {
-			addLabel(label, mdp.getLabelStates(label));
-		}
+		copyFrom(mdp);
 
 		// Copy stats
 		numDistrs = mdp.getNumChoices();
@@ -122,13 +115,6 @@ public MDPSparse(final MDP<Double> mdp, boolean sort)
 		final TreeMap<Integer, Double> sorted = sort ? new TreeMap<Integer, Double>() : null;
 		int rowIndex = 0, choiceIndex = 0;
 		for (int state = 0; state < numStates; state++) {
-			if (mdp.isInitialState(state)) {
-				addInitialState(state);
-			}
-			if (mdp.isDeadlockState(state)) {
-				deadlocks.add(state);
-			}
-
 			rowStarts[state] = rowIndex;
 			if (actions != null) {
 				for (int choice = 0, numChoices = mdp.getNumChoices(state); choice < numChoices; choice++) {

prism/src/explicit/Model.java

@@ -39,9 +39,8 @@
 
 import common.IterableStateSet;
 import common.IteratorTools;
-import io.DotExporter;
-import io.ModelExportOptions;
-import io.PrismExplicitExporter;
+import explicit.rewards.Rewards;
+import io.*;
 import parser.State;
 import parser.Values;
 import parser.VarList;
@@ -153,7 +152,43 @@ default Map<String, BitSet> getLabelToStatesMap()
 		}
 		return labels;
 	}
-
+
+	/**
+	 * Get an attached reward structure, by its (optional) name.
+	 * Returns null if it does not exist.
+	 */
+	Rewards<Value> getRewardsByName(String name);
+
+	/**
+	 * Get an attached reward structure, by its (optional) position.
+	 * By convention, positions are assumed to be indexed from 0.
+	 * Returns null if it does not exist.
+	 */
+	Rewards<Value> getRewardsByPosition(int r);
+
+	/**
+	 * Get the number of reward structures that are attached to the model.
+	 */
+	int getNumRewards();
+
+	/**
+	 * Get the {@code i}th stored reward structure.
+	 */
+	Rewards<Value> getRewards(int i);
+
+	/**
+	 * Get the name of the {@code i}th stored reward structure.
+	 * This is optionally stored and "" if absent.
+	 */
+	String getRewardName(int i);
+
+	/**
+	 * Get the position of the {@code i}th stored reward structure.
+	 * This is optionally stored, and refers to the order within its original source,
+	 * e.g., a properties file. By convention, positions are 0-indexed. Null if absent.
+	 */
+	Integer getRewardPosition(int i);
+
 	@Override
 	default int getNumTransitions()
 	{
@@ -389,6 +424,31 @@ default void prob1step(BitSet subset, BitSet u, BitSet v, BitSet result)
 	 */
 	void checkForDeadlocks(BitSet except) throws PrismException;
 
+	/**
+	 * Export to the specified model format.
+	 */
+	default void export(PrismLog out, ModelExportFormat exportFormat) throws PrismException
+	{
+		export(out, new ModelExportOptions(exportFormat));
+	}
+
+	/**
+	 * Export using the specified export options.
+	 */
+	default void export(PrismLog out, ModelExportOptions exportOptions) throws PrismException
+	{
+		// Create a model checker with {@code out} as the log and export to that
+		StateModelChecker mcExport = StateModelChecker.createModelChecker(getModelType());
+		mcExport.setLog(out);
+		// If {@code out} is backed by a real file (as opposed to stdout/the main log),
+		// pass that file through too, since some (e.g. binary) export formats need it
+		File file = null;
+		if (out instanceof PrismFileLog && !((PrismFileLog) out).isStdout()) {
+			file = new File(((PrismFileLog) out).getFileName());
+		}
+		mcExport.exportModel(this, ModelExportTask.fromOptions(file, exportOptions));
+	}
+
 	// Export methods (explicit files)
 
 	/**

prism/src/explicit/ModelExplicit.java

@@ -27,14 +27,10 @@
 package explicit;
 
 import java.io.File;
-import java.util.ArrayList;
-import java.util.BitSet;
-import java.util.List;
-import java.util.Map;
-import java.util.Set;
-import java.util.TreeMap;
-import java.util.TreeSet;
+import java.util.*;
+import java.util.function.Function;
 
+import explicit.rewards.Rewards;
 import io.ExplicitModelImporter;
 import io.PrismExplicitImporter;
 import parser.State;
@@ -96,7 +92,24 @@ public abstract class ModelExplicit<Value> implements Model<Value>, ActionListOw
 	 * (Optionally) some labels (atomic propositions) associated with the model,
 	 * represented as a String->BitSet mapping from their names to the states that satisfy them.
 	 */
-	protected Map<String, BitSet> labels = new TreeMap<String, BitSet>();
+	protected Map<String, BitSet> labels = new LinkedHashMap<>();
+
+	/**
+	 * (Optionally) some attached reward structures.
+	 * Each can have a name (set to "" if it is unnamed).
+	 * Each can have a position, referring to the order within its original source,
+	 * e.g., a properties file (null if undefined).
+	 * By convention, positions are assumed to be indexed from 0.
+	 * Both names and positions must be unique if defined.
+	 */
+	protected List<IndexedRewards<Value>> rewards = new ArrayList<>();
+
+	static protected class IndexedRewards<Value>
+	{
+		String name = "";
+		Integer position = null;
+		Rewards<Value> rews;
+	}
 
 	/**
 	 * (Optionally) the stored predecessor relation. Becomes inaccurate after the model is changed!
@@ -117,6 +130,7 @@ public void setEvaluator(Evaluator<Value> eval)
 	 * Copy data from another Model (used by superclass copy constructors).
 	 * Assumes that this has already been initialise()ed.
 	 */
+	@SuppressWarnings("unchecked")
 	public void copyFrom(Model<?> model)
 	{
 		setEvaluator((Evaluator<Value>) model.getEvaluator());
@@ -134,6 +148,7 @@ public void copyFrom(Model<?> model)
 		statesList = model.getStatesList();
 		constantValues = model.getConstantValues();
 		labels = model.getLabelToStatesMap();
+		copyRewards((Model<Value>) model);
 		varList = model.getVarList();
 	}
 
@@ -162,6 +177,7 @@ public void copyFrom(Model<Value> model, int permut[])
 		statesList = null;
 		constantValues = model.getConstantValues();
 		labels.clear();
+		rewards.clear();
 		varList = model.getVarList();
 	}
 
@@ -176,7 +192,8 @@ public void initialise(int numStates)
 		statesList = null;
 		constantValues = null;
 		varList = null;
-		labels = new TreeMap<String, BitSet>();
+		labels = new LinkedHashMap<>();
+		rewards = new ArrayList<>();
 	}
 
 	/**
@@ -313,6 +330,87 @@ public String addUniqueLabel(String prefix, BitSet labelStates, Set<String> defi
 		return label;
 	}
 
+	/**
+	 * Attach a reward structure with optional name and position.
+	 * If a reward structure already exists with the same (non-empty) name or the same
+	 * (non-null) position, it is overwritten. If both name and position are provided,
+	 * and they do not identify the same existing reward structure (or lack thereof),
+	 * this is an error.
+	 * @param name Name of reward structure ("" for unnamed; null also accepted)
+	 * @param position Position of reward structure (0-indexed; null if not stored)
+	 * @param rews The rewards
+	 * @return The index of the attached reward
+	 */
+	public int addRewards(String name, Integer position, Rewards<Value> rews)
+	{
+		String rewName = name == null ? "" : name;
+		int i = findRewardsIndex(rewName, position);
+		if (i == -1) {
+			i = rewards.size();
+			rewards.add(new IndexedRewards<>());
+		}
+		IndexedRewards<Value> ir = rewards.get(i);
+		ir.name = rewName;
+		ir.position = position;
+		ir.rews = rews;
+		return i;
+	}
+
+	/**
+	 * Find the index of a stored reward structure matching a (non-empty) name
+	 * or a (non-null) position, if any. Returns -1 if there is no match.
+	 * If both name and position are provided, but match different existing reward
+	 * structures, this is an error (they should either both be absent or agree).
+	 */
+	private int findRewardsIndex(String name, Integer position)
+	{
+		int nameMatch = -1;
+		int positionMatch = -1;
+		for (int i = 0; i < rewards.size(); i++) {
+			IndexedRewards<Value> ir = rewards.get(i);
+			if (!name.isEmpty() && name.equals(ir.name)) {
+				nameMatch = i;
+			}
+			if (position != null && position.equals(ir.position)) {
+				positionMatch = i;
+			}
+		}
+		if (nameMatch != -1 && positionMatch != -1 && nameMatch != positionMatch) {
+			throw new RuntimeException("Reward structure name \"" + name + "\" and position " + position + " refer to different existing reward structures");
+		}
+		return nameMatch != -1 ? nameMatch : positionMatch;
+	}
+
+	/**
+	 * Attach a reward structure with optional name.
+	 * @param name Name of reward structure ("" for unnamed; null also accepted)
+	 * @param rews The rewards
+	 * @return The index of the attached reward
+	 */
+	public int addRewards(String name, Rewards<Value> rews)
+	{
+		return addRewards(name, null, rews);
+	}
+
+	/**
+	 * Copy the rewards from an existing model.
+	 */
+	public void copyRewards(Model<Value> model)
+	{
+		copyRewardsMapped(model, rews -> rews);
+	}
+
+	/**
+	 * Copy the rewards from an existing model after first applying a function to them.
+	 */
+	public void copyRewardsMapped(Model<Value> model, Function<Rewards<Value>, Rewards<Value>> map)
+	{
+		int numRewards = model.getNumRewards();
+		for (int i = 0; i < numRewards; i++) {
+			addRewards(model.getRewardName(i), model.getRewardPosition(i), map.apply(model.getRewards(i)));
+		}
+	}
+
 	// Accessors (for Model interface)
 
 	@Override
@@ -450,6 +548,55 @@ public Map<String, BitSet> getLabelToStatesMap()
 		return labels;
 	}
 
+	@Override
+	public Rewards<Value> getRewardsByName(String name)
+	{
+		if (name == null || name.isEmpty()) {
+			return null;
+		}
+		for (IndexedRewards<Value> ir : rewards) {
+			if (name.equals(ir.name)) {
+				return ir.rews;
+			}
+		}
+		return null;
+	}
+
+	@Override
+	public Rewards<Value> getRewardsByPosition(int r)
+	{
+		for (IndexedRewards<Value> ir : rewards) {
+			if (ir.position != null && ir.position == r) {
+				return ir.rews;
+			}
+		}
+		return null;
+	}
+
+	@Override
+	public int getNumRewards()
+	{
+		return rewards.size();
+	}
+
+	@Override
+	public Rewards<Value> getRewards(int i)
+	{
+		return rewards.get(i).rews;
+	}
+
+	@Override
+	public String getRewardName(int i)
+	{
+		return rewards.get(i).name;
+	}
+
+	@Override
+	public Integer getRewardPosition(int i)
+	{
+		return rewards.get(i).position;
+	}
+
 	@Override
 	public void checkForDeadlocks() throws PrismException
 	{