Use predicates for label evaluation instead of maps

Author: merkste

prism/src/param/SymbolicEngine.java

@@ -34,6 +34,7 @@
 import java.util.List;
 import java.util.Map;
 import java.util.Vector;
+import java.util.function.Predicate;
 
 import parser.State;
 import parser.ast.Command;
@@ -141,7 +142,7 @@ static boolean hasMoreThanOneVariable(Expression exp)
 		}
 	}
 
-	public TransitionList calculateTransitions(State state, Map<String, Boolean> labelValues, boolean noWarnings) throws PrismException
+	public TransitionList calculateTransitions(State state, Predicate<String> labelValues, boolean noWarnings) throws PrismException
 	{
 		List<ChoiceListFlexi> chs;
 		int i, j, k, l, n, count;
@@ -249,7 +250,7 @@ public TransitionList calculateTransitions(State state, Map<String, Boolean> lab
 	 * @param m The module index
 	 * @param state State from which to explore
 	 */
-	protected void calculateUpdatesForModule(int m, State state, Map<String, Boolean> labelValues) throws PrismLangException
+	protected void calculateUpdatesForModule(int m, State state, Predicate<String> labelValues) throws PrismLangException
 	{
 		Module module;
 		Command command;

prism/src/parser/EvaluateContextState.java

@@ -27,6 +27,7 @@
 package parser;
 
 import java.util.Map;
+import java.util.function.Predicate;
 
 /**
  * Information required to evaluate an expression: a State object.
@@ -37,7 +38,7 @@ public class EvaluateContextState implements EvaluateContext
 {
 	protected final Values constantValues;
 	protected final Object[] varValues;
-	protected final Map<String, Boolean> labelValues;
+	protected final Predicate<String> labelValues;
 
 	public EvaluateContextState(State state)
 	{
@@ -49,7 +50,7 @@ public EvaluateContextState(Values constantValues, State state)
 		this(constantValues, null, state);
 	}
 
-	public EvaluateContextState(Values constantValues, Map<String, Boolean> labelValues, State state)
+	public EvaluateContextState(Values constantValues, Predicate<String> labelValues, State state)
 	{
 		this.constantValues = constantValues;
 		this.labelValues = labelValues;
@@ -74,6 +75,6 @@ public Object getVarValue(String name, int index)
 
 	public Boolean getLabelValue(String name)
 	{
-		return labelValues.get(name);
+		return labelValues.test(name);
 	}
 }

prism/src/parser/ast/Expression.java

@@ -49,6 +49,7 @@
 import prism.PrismLangException;
 
 import java.util.Map;
+import java.util.function.Predicate;
 
 // Abstract class for PRISM language expressions
 
@@ -545,7 +546,7 @@ public boolean evaluateBoolean(Values constantValues, State state) throws PrismL
 	 * Variable values are supplied as a State object, i.e. array of variable values.
 	 * Note: assumes that type checking has been done.
 	 */
-	public boolean evaluateBoolean(Values constantValues, Map<String, Boolean> labelValues, State state) throws PrismLangException
+	public boolean evaluateBoolean(Values constantValues, Predicate<String> labelValues, State state) throws PrismLangException
 	{
 		return evaluateBoolean(new EvaluateContextState(constantValues, labelValues, state));
 	}
@@ -627,7 +628,7 @@ public BigRational evaluateExact(State state) throws PrismLangException
 	 * Variable values are supplied as a State object, i.e. array of variable values.
 	 * Note: assumes that type checking has been done.
 	 */
-	public BigRational evaluateExact(Values constantValues, Map<String, Boolean> labelValues, State state) throws PrismLangException
+	public BigRational evaluateExact(Values constantValues, Predicate<String> labelValues, State state) throws PrismLangException
 	{
 		return evaluateExact(new EvaluateContextState(constantValues, labelValues, state));
 	}

prism/src/parser/ast/ExpressionLabel.java

@@ -81,9 +81,9 @@ public boolean isProposition()
 	}
 
 	@Override
-	public Object evaluate(EvaluateContext ec) throws PrismLangException
+	public Boolean evaluate(EvaluateContext ec) throws PrismLangException
 	{
-		Object value = ec.getLabelValue(this.name);
+		Boolean value = ec.getLabelValue(this.name);
 		if (value == null)
 			throw new PrismLangException("Failed to evaluate label", this);
 		return value;

prism/src/prism/ModelGenerator.java

@@ -33,6 +33,7 @@
 import java.util.Collections;
 import java.util.List;
 import java.util.Map;
+import java.util.function.Predicate;
 
 /**
  * Interface for classes that generate a probabilistic model:
@@ -313,7 +314,7 @@ public default String getTransitionUpdateStringFull(int i, int offset) throws Pr
 	/**
 	 * 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
+	default Predicate<String> getLabelValues(State state) throws PrismException
 	{
 		// No labels by default
 		throw new PrismException("Labels not defined");

prism/src/prism/ModelGenerator2MTBDD.java

@@ -29,6 +29,7 @@
 import java.util.LinkedList;
 import java.util.Map;
 import java.util.Vector;
+import java.util.function.Predicate;
 
 import jdd.JDD;
 import jdd.JDDNode;
@@ -513,9 +514,9 @@ private void buildTransAndRewards() throws PrismException
 				// TODO progress.updateIfReady(src + 1);
 			}
 
-			Map<String, Boolean> labelValues = modelGen.getLabelValues(state);
+			Predicate<String> labelValues = modelGen.getLabelValues(state);
 			for (int l = 0; l < numLabels; l++) {
-				if (labelValues.get(modelGen.getLabelName(l))) {
+				if (labelValues.test(modelGen.getLabelName(l))) {
 					labelsArray[l] = JDD.Or(labelsArray[l], ddState.copy());
 				}
 			}

prism/src/simulator/LabelEvaluator.java

@@ -87,16 +87,10 @@ public boolean getLabelValue(State state, String label) throws PrismLangExceptio
      * @return Returns a {@link Map} containing all label-values for the given state, indexed by their name.
      * @throws PrismLangException In case a label couldn't be evaluated.
      */
-    public Map<String, Boolean> getLabelValues(State state) throws PrismLangException
+    public Predicate<String> getLabelValues(State state) throws PrismLangException
     {
-        // convert BitSet to Map to provide intuitiv interface
-        BitSet value = getStateValues(state);
-        Map<String, Boolean> labelValueMap = new HashMap<>();
-        for (int i = 0, numLabels = labelList.size(); i < numLabels; i++){
-            labelValueMap.put(labelList.getLabelName(i), value.get(i));
-        }
-        return labelValueMap;
-   }
+        return asPredicate(getStateValues(state));
+    }
 
     /**
      * This method provides all values of a certain label. They will be ordered by the given statesList. <br>
@@ -146,15 +140,35 @@ protected BitSet getStateValues(State state) throws PrismLangException
     private BitSet evaluateState(State state) throws PrismLangException
     {
         int numLabels = labelList.size();
-        Map<String, Boolean> labelValues = new HashMap<>(numLabels);
         BitSet values = new BitSet();
+        Predicate<String> labelValues = asPredicate(values);
         for (int i : evaluationOrder) {
             Expression label = labelList.getLabel(i);
             boolean labelValue = label.evaluateBoolean(null, labelValues, state);
-            labelValues.put(labelList.getLabelName(i), labelValue);
             values.set(i, labelValue);
         }
         stateValues.put(state, values);
         return values;
     }
+
+    /**
+     * Convert the label values for a state to a predicate on the label names.
+     *
+     * @param values the label values for some state
+     * @return a Predicate evaluating to {@code true} for a label name iff the Bit at the corresponding index in {@code values} is set
+     */
+    public Predicate<String> asPredicate(BitSet values)
+    {
+        return new Predicate<String>() {
+            @Override
+            public boolean test(String name)
+            {
+                int index = labelList.getLabelIndex(name);
+                if (index == -1) {
+                    throw new NoSuchElementException("Unknown label \"" + name + "\"");
+                }
+                return values.get(index);
+            }
+        };
+    }
 }

prism/src/simulator/ModulesFileModelGenerator.java

@@ -20,6 +20,7 @@
 import java.util.BitSet;
 import java.util.List;
 import java.util.Map;
+import java.util.function.Predicate;
 
 public class ModulesFileModelGenerator implements ModelGenerator, RewardGenerator
 {
@@ -417,7 +418,7 @@ public State computeTransitionTarget(int index, int offset) throws PrismExceptio
 	}
 
 	@Override
-	public Map<String, Boolean> getLabelValues(State state) throws PrismLangException
+	public Predicate<String> getLabelValues(State state) throws PrismLangException
 	{
 		return labelEvaluator.getLabelValues(state);
 	}

prism/src/simulator/ModulesFileModelGeneratorSymbolic.java

@@ -3,6 +3,7 @@
 import java.util.ArrayList;
 import java.util.List;
 import java.util.Map;
+import java.util.function.Predicate;
 
 import param.Function;
 import param.FunctionFactory;
@@ -449,7 +450,7 @@ public State computeTransitionTarget(int index, int offset) throws PrismExceptio
 	}
 
 	@Override
-	public Map<String, Boolean> getLabelValues(State state) throws PrismLangException
+	public Predicate<String> getLabelValues(State state) throws PrismLangException
 	{
 		return labelsEvaluator.getLabelValues(state);
 	}

prism/src/simulator/Updater.java

@@ -32,6 +32,7 @@
 import java.util.List;
 import java.util.Vector;
 import java.util.Map;
+import java.util.function.Predicate;
 
 import parser.State;
 import parser.VarList;
@@ -151,7 +152,7 @@ public double getSumRoundOff()
 	 * @param state State from which to explore
 	 * @param transitionList TransitionList object in which to store result
 	 */
-	public void calculateTransitions(State state, Map<String, Boolean> labelValues, TransitionList transitionList) throws PrismException
+	public void calculateTransitions(State state, Predicate<String> labelValues, TransitionList transitionList) throws PrismException
 	{
 		List<ChoiceListFlexi> chs;
 		int i, j, k, l, n, count;
@@ -269,7 +270,7 @@ public void calculateTransitions(State state, Map<String, Boolean> labelValues,
 	 * @param m The module index
 	 * @param state State from which to explore
 	 */
-	protected void calculateUpdatesForModule(int m, State state, Map<String, Boolean> labelValues) throws PrismLangException
+	protected void calculateUpdatesForModule(int m, State state, Predicate<String> labelValues) throws PrismLangException
 	{
 		Module module;
 		Command command;