Adding support for labels inside labels

prism-tests/functionality/language/labels-inside-guards.lab

@@ -0,0 +1,4 @@
+0="init" 1="deadlock" 2="foo"
+0: 0
+1: 2
+2: 2

prism-tests/functionality/language/labels-inside-guards.prism

@@ -0,0 +1,16 @@
+dtmc
+
+// 1. labels should not be expanded like formulas
+// 2. label should be evaluated correctly so that
+// (s1 = true & s2 = true) is unreachable
+
+module m1
+	s1: bool init false;
+
+	[] !"foo" -> (s1'=true);
+	[] true -> (s1'=false);
+endmodule
+
+module m2=m1[s1=s2] endmodule
+
+label "foo" = s1 | s2;

prism-tests/functionality/language/labels-inside-guards.prism.props

@@ -0,0 +1,3 @@
+// RESULT: 0
+P=? [ s1=true & s2=true ]
+

prism-tests/functionality/language/labels-inside-guards.prism.props.args

@@ -0,0 +1,5 @@
+-explicit -exportmodel labels-inside-guards.tra,sta,lab
+-mtbdd -exportmodel labels-inside-guards.tra,sta,lab
+-hybrid -exportmodel labels-inside-guards.tra,sta,lab
+-sparse -exportmodel labels-inside-guards.tra,sta,lab
+-exact

prism-tests/functionality/language/labels-inside-guards.sta

@@ -0,0 +1,4 @@
+(s1,s2)
+0:(false,false)
+1:(false,true)
+2:(true,false)

prism-tests/functionality/language/labels-inside-guards.tra

@@ -0,0 +1,8 @@
+3 7
+0 0 0.5
+0 1 0.25
+0 2 0.25
+1 0 0.5
+1 1 0.5
+2 0 0.5
+2 2 0.5

prism-tests/functionality/language/labels-inside-labels.lab

@@ -0,0 +1,13 @@
+0="init" 1="deadlock" 2="l1" 3="l2" 4="l3" 5="l4" 6="l5"
+0: 0 3 5 6
+1: 3 5 6
+2: 3 5 6
+3: 3 5 6
+4: 3 5 6
+5: 3 5 6
+6: 3 5 6
+7: 3 5 6
+8: 2 3 5 6
+9: 3 4 5 6
+10: 3 4 5 6
+11: 3 4 5 6

prism-tests/functionality/language/labels-inside-labels.prism

@@ -0,0 +1,33 @@
+dtmc
+
+module die
+
+	// local state
+	s : [0..7] init 0;
+	// value of the die
+	d : [0..6] init 0;
+
+	[] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2);
+	[] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4);
+	[] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6);
+	[] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1);
+	[] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3);
+	[] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5);
+	[] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6);
+	[] s=7 -> (s'=7);
+
+endmodule
+
+// l1 = ((d>=3 & d<=5) | d<=5) & d=2
+label "l1" = "l2" & d=2;
+// l2 = (d>=3 & d<=5) | d<=5
+label "l2" = "l3" | "l4";
+// l3 = d>=3 & d<=5
+label "l3" = f2 & "l4";
+// l4 = d<=5
+label "l4" = f1;
+// l5 = d<=5
+label "l5" = d<=5;
+
+formula f1 = "l5";
+formula f2 = d>=3;

prism-tests/functionality/language/labels-inside-labels.prism.props

@@ -0,0 +1,10 @@
+// RESULT: 1/6
+P=? [ F s=7 & "l1" ]
+// RESULT: 5/6
+P=? [ F s=7 & "l2" ]
+// RESULT: 3/6
+P=? [ F s=7 & "l3" ]
+// RESULT: 5/6
+P=? [ F s=7 & "l4" ]
+// RESULT: 5/6
+P=? [ F s=7 & "l5" ]

prism-tests/functionality/language/labels-inside-labels.prism.props.args

@@ -0,0 +1,5 @@
+-explicit -exportlabels labels-inside-labels.lab
+-mtbdd -exportlabels labels-inside-labels.lab
+-hybrid -exportlabels labels-inside-labels.lab
+-sparse -exportlabels labels-inside-labels.lab
+-exact

prism/src/explicit/ConstructModel.java

@@ -32,6 +32,7 @@
 import java.util.BitSet;
 import java.util.LinkedList;
 import java.util.List;
+import java.util.Map;
 
 import common.Interval;
 import parser.State;
@@ -456,9 +457,14 @@ public <Value> Model<Value> constructModel(ModelGenerator<Value> modelGen, boole
 		// Discard permutation
 		permut = null;
 
-		if (!justReach && attachLabels)
-			attachLabels(modelGen, model);
-
+		if (!justReach && attachLabels) {
+			// Attach labels/bitsets
+			List <State> statesList = model.getStatesList();
+			for (String label : model.getLabels()){
+				model.addLabel(label, modelGen.getLabel(label, statesList));
+			}
+		}
+
 		return model;
 	}
 
@@ -482,35 +488,6 @@ private <Value> void setStateObservation(ModelGenerator<Value> modelGen, POMDPSi
 		// Set observation/unobservation
 		pomdp.setObservation(s, sObs, sUnobs, modelGen.getObservableNames());
 	}
-
-	private <Value> void attachLabels(ModelGenerator<Value> modelGen, ModelExplicit<Value> model) throws PrismException
-	{
-		// Get state info
-		List <State> statesList = model.getStatesList();
-		int numStates = statesList.size();
-		// 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 (int j = 0; j < numLabels; j++) {
-			bitsets[j] = new BitSet();
-		}
-		// Construct bitsets for labels
-		for (int i = 0; i < numStates; i++) {
-			State state = statesList.get(i);
-			modelGen.exploreState(state);
-			for (int j = 0; j < numLabels; j++) {
-				if (modelGen.isLabelTrue(j)) {
-					bitsets[j].set(i);
-				}
-			}
-		}
-		// Attach labels/bitsets
-		for (int j = 0; j < numLabels; j++) {
-			model.addLabel(modelGen.getLabelName(j), bitsets[j]);
-		}
-	}
 
 	/**
 	 * Test method.

prism/src/parser/EvaluateContext.java

@@ -128,6 +128,15 @@ public Object getConstantValue(String name)
 	 */
 	public abstract Object getVarValue(String name, int index);
 
+	/**
+	 * Return the value for a label; null if unknown.
+	 */
+	public Boolean getLabelValue(String name)
+	{
+		// no labels defined by default
+		return null;
+	}
+
 	/**
 	 * Return the value for an observable (by name or index); null if unknown.
 	 */

prism/src/parser/EvaluateContextState.java

@@ -26,6 +26,8 @@
 
 package parser;
 
+import java.util.function.Predicate;
+
 /**
  * Information required to evaluate an expression,
  * where the values for variables are stored in a State object.
@@ -40,15 +42,24 @@ public class EvaluateContextState extends EvaluateContext
 	 */
 	private Object[] varValues;
 
+	/** values of all labels in this state */
+	protected Predicate<String> labelValues;
+
 	public EvaluateContextState(State state)
 	{
-		setState(state);
+		this(null, state);
 	}
 
 	public EvaluateContextState(Values constantValues, State state)
 	{
-		setConstantValues(constantValues);
+		this(constantValues, null, state);
+	}
+
+	public EvaluateContextState(Values constantValues, Predicate<String> labelValues, State state)
+	{
 		setState(state);
+		setConstantValues(constantValues);
+		setLabelValues(labelValues);
 	}
 
 	/**
@@ -68,4 +79,16 @@ public Object getVarValue(String name, int index)
 		// so use index if provided; otherwise unknown
 		return index == -1 ? null : varValues[index];
 	}
+
+	public EvaluateContextState setLabelValues(Predicate<String> labelValues)
+	{
+		this.labelValues = labelValues;
+		return this;
+	}
+
+	@Override
+	public Boolean getLabelValue(String name)
+	{
+		return labelValues.test(name);
+	}
 }

prism/src/parser/ParseException.java

@@ -122,9 +122,7 @@ private static String initialise(Token currentToken,
       retval += " \"";
       tok = tok.next;
     }
-    if (currentToken.next != null) {
-      retval += "\" at line " + currentToken.next.beginLine + ", column " + currentToken.next.beginColumn;
-    }
+    retval += "\" at line " + currentToken.next.beginLine + ", column " + currentToken.next.beginColumn;
     retval += "." + EOL;
 
 
@@ -192,4 +190,4 @@ static String add_escapes(String str) {
    }
 
 }
-/* JavaCC - OriginalChecksum=8dbcceed9d408427f9932dcf43e59aaa (do not edit this line) */
+/* JavaCC - OriginalChecksum=498e95145a190935df56665f42563744 (do not edit this line) */