caching labels inside modelgenerator

Author: maxkurze1

prism/src/explicit/ConstructModel.java

@@ -410,7 +410,11 @@ public Model constructModel(ModelGenerator modelGen, boolean justReach) throws P
 		permut = null;
 
 		if (!justReach && attachLabels) {
-			attachLabels(modelGen, model);
+			// Attach labels/bitsets
+			List <State> statesList = model.getStatesList();
+			for (String label : model.getLabels()){
+				model.addLabel(label, modelGen.getLabel(label, statesList));
+			}
 		}
 
 		return model;
@@ -436,38 +440,6 @@ private void setStateObservation(ModelGenerator modelGen, POMDPSimple pomdp, int
 		// Set observation/unobservation
 		pomdp.setObservation(s, sObs, sUnobs, modelGen.getObservableNames());
 	}
-	
-	private void attachLabels(ModelGenerator modelGen, ModelExplicit model) throws PrismException
-	{
-		int i,j;
-		// Create storage for labels
-		int numLabels = modelGen.getNumLabels();
-		// No need to continue unless this ModelGenerator uses labels
-		if (numLabels == 0) return;
-		BitSet[] bitsets = new BitSet[numLabels];
-		for (j = 0; j < numLabels; j++) {
-			bitsets[j] = new BitSet();
-		}
-
-		// Get state info
-		List <State> statesList = model.getStatesList();
-		int numStates = statesList.size();
-
-		// Construct bitsets for labels
-		for (i = 0; i < numStates; i++) {
-			State state = statesList.get(i);
-			Map<String, Boolean> labelValues = modelGen.getLabelValues(state);
-			for (j = 0; j < numLabels; j++) {
-				if (labelValues.get(modelGen.getLabelName(j))) {
-					bitsets[j].set(i);
-				}
-			}
-		}
-		// Attach labels/bitsets
-		for (j = 0; j < numLabels; j++) {
-			model.addLabel(modelGen.getLabelName(j), bitsets[j]);
-		}
-	}
 
 	/**
 	 * Test method.

prism/src/prism/ModelGenerator.java

@@ -28,8 +28,8 @@
 package prism;
 
 import parser.State;
-import parser.Values;
 
+import java.util.BitSet;
 import java.util.Collections;
 import java.util.List;
 import java.util.Map;
@@ -311,7 +311,7 @@ public default String getTransitionUpdateStringFull(int i, int offset) throws Pr
 	public State computeTransitionTarget(int i, int offset) throws PrismException;
 
 	/**
-	 * Creates a {@link Values} map for all labels in the current state.
+	 * Creates a {@link Map} of (label-name -> label-value) for all labels in the current state.
 	 */
 	default Map<String, Boolean> getLabelValues(State state) throws PrismException
 	{
@@ -320,6 +320,19 @@ default Map<String, Boolean> getLabelValues(State state) throws PrismException
 	}
 
 	/**
+	 * This method creates a BitSet for the given label-name containing all values in the
+	 * order of the given statesList.
+	 * @param name The name of the Label.
+	 * @param statesList The List of states in right order.
+	 * @return a {@link BitSet} of all values from the given label.
+	 * @throws PrismException If the label values aren't cached or not all states have been evaluated
+	 */
+	default BitSet getLabel(String name, List<State> statesList) throws PrismException
+	{
+		throw new PrismException("Labels are not cached");
+	}
+
+    /**
 	 * Get the observation when entering state {@code state}.
 	 * This is represented as a {@link parser.State} object, with one value per observable.
 	 * For models that are not partially observable, null can be returned.

prism/src/simulator/LabelsCache.java

@@ -0,0 +1,73 @@
+package simulator;
+
+
+import common.iterable.Range;
+import parser.State;
+import parser.ast.LabelList;
+import prism.PrismException;
+import prism.PrismLangException;
+
+import java.util.BitSet;
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+
+public class LabelsCache
+{
+    // cache internal order of states
+    Map<State, Integer> stateIndices = new HashMap<>();
+    Map<String, BitSet> labelValues = new HashMap<>();
+    LabelList labelList;
+
+    LabelsCache(LabelList ll)
+    {
+        this.labelList = ll;
+        for (String label : ll.getLabelNames()) {
+            labelValues.put(label, new BitSet());
+        }
+    }
+
+    public boolean getLabelValue(State state, String label)
+    {
+        return labelValues.get(label).get(stateIndices.get(state));
+    }
+
+    public Map<String, Boolean> getLabelValues(State state) throws PrismLangException
+    {
+        int index;
+        Map<String, Boolean> stateLabelValues;
+
+        if (stateIndices.containsKey(state)) {
+            index = stateIndices.get(state);
+            stateLabelValues = new HashMap<>();
+            labelValues.forEach((name, bitset) -> stateLabelValues.put(name, bitset.get(index)));
+        } else {
+            index = addState(state);
+            stateLabelValues = labelList.getLabelValues(state);
+            labelValues.forEach((name, bitset) -> bitset.set(index, stateLabelValues.get(name)));
+        }
+        return stateLabelValues;
+    }
+
+    private int addState(State state)
+    {
+        int nextIndex = stateIndices.size();
+        stateIndices.put(state, nextIndex);
+        return nextIndex;
+    }
+
+    public BitSet getLabel(String name, List<State> statesList) throws PrismException
+    {
+        // check if all states have been evaluated
+        for (State state : statesList) {
+            if (!stateIndices.containsKey(state)) {
+                throw new PrismException("Labels not evaluated for state: " + state);
+            }
+        }
+        // assuming statesList has efficient indexed access, e.g., ArrayList
+        BitSet values = labelValues.get(name);
+
+        Range indices = new Range(statesList.size()).reversed(); // iterate in revese order to avoid multiple resizing of BitSet
+        return indices.filter((int i) -> values.get(stateIndices.get(statesList.get(i)))).collect(new BitSet());
+    }
+}

prism/src/simulator/ModulesFileModelGenerator.java

@@ -1,10 +1,5 @@
 package simulator;
 
-import java.util.ArrayList;
-import java.util.HashMap;
-import java.util.List;
-import java.util.Map;
-
 import parser.State;
 import parser.Values;
 import parser.VarList;
@@ -21,6 +16,11 @@
 import prism.PrismLangException;
 import prism.RewardGenerator;
 
+import java.util.ArrayList;
+import java.util.BitSet;
+import java.util.List;
+import java.util.Map;
+
 public class ModulesFileModelGenerator implements ModelGenerator, RewardGenerator
 {
 	// Parent PrismComponent (logs, settings etc.)
@@ -47,6 +47,9 @@ public class ModulesFileModelGenerator implements ModelGenerator, RewardGenerato
 	protected TransitionList transitionList;
 	// Has the transition list been built? 
 	protected boolean transitionListBuilt;
+
+	// label value cache
+	protected LabelsCache labelsCache;
 
 	/**
 	 * Build a ModulesFileModelGenerator for a particular PRISM model, represented by a ModuleFile instance.
@@ -75,7 +78,7 @@ public ModulesFileModelGenerator(ModulesFile modulesFile, PrismComponent parent)
 		if (modulesFile.getSystemDefn() != null) {
 			throw new PrismException("The system...endsystem construct is not currently supported");
 		}
-		
+
 		// Store basic model info
 		this.modulesFile = modulesFile;
 		this.originalModulesFile = modulesFile;
@@ -103,6 +106,9 @@ private void initialise() throws PrismException
 		labelList = modulesFile.getLabelList();
 		labelNames = labelList.getLabelNames();
 
+		// create label-cache
+		labelsCache = new LabelsCache(labelList);
+
 		// Create data structures for exploring model
 		updater = new Updater(modulesFile, varList, parent);
 		transitionList = new TransitionList();
@@ -413,9 +419,15 @@ public State computeTransitionTarget(int index, int offset) throws PrismExceptio
 	@Override
 	public Map<String, Boolean> getLabelValues(State state) throws PrismLangException
 	{
-		return labelList.getLabelValues(state);
+		return labelsCache.getLabelValues(state);
 	}
-	
+
+	@Override
+	public BitSet getLabel(String name, List<State> statesList) throws PrismException
+	{
+		return labelsCache.getLabel(name, statesList);
+	}
+
 	@Override
 	public State getObservation(State state) throws PrismException
 	{