diff --git a/prism-tests/functionality/language/labels-inside-guards.lab b/prism-tests/functionality/language/labels-inside-guards.lab
new file mode 100644
index 0000000000..56c23fc1d5
--- /dev/null
+++ b/prism-tests/functionality/language/labels-inside-guards.lab
@@ -0,0 +1,4 @@
+0="init" 1="deadlock" 2="foo"
+0: 0
+1: 2
+2: 2
diff --git a/prism-tests/functionality/language/labels-inside-guards.prism b/prism-tests/functionality/language/labels-inside-guards.prism
new file mode 100644
index 0000000000..b588cdbe72
--- /dev/null
+++ b/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;
diff --git a/prism-tests/functionality/language/labels-inside-guards.prism.props b/prism-tests/functionality/language/labels-inside-guards.prism.props
new file mode 100644
index 0000000000..9e8ae13014
--- /dev/null
+++ b/prism-tests/functionality/language/labels-inside-guards.prism.props
@@ -0,0 +1,3 @@
+// RESULT: 0
+P=? [ s1=true & s2=true ]
+
diff --git a/prism-tests/functionality/language/labels-inside-guards.prism.props.args b/prism-tests/functionality/language/labels-inside-guards.prism.props.args
new file mode 100644
index 0000000000..c46b784845
--- /dev/null
+++ b/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
diff --git a/prism-tests/functionality/language/labels-inside-guards.sta b/prism-tests/functionality/language/labels-inside-guards.sta
new file mode 100644
index 0000000000..ebdc013c3a
--- /dev/null
+++ b/prism-tests/functionality/language/labels-inside-guards.sta
@@ -0,0 +1,4 @@
+(s1,s2)
+0:(false,false)
+1:(false,true)
+2:(true,false)
diff --git a/prism-tests/functionality/language/labels-inside-guards.tra b/prism-tests/functionality/language/labels-inside-guards.tra
new file mode 100644
index 0000000000..651193bea4
--- /dev/null
+++ b/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
diff --git a/prism-tests/functionality/language/labels-inside-labels.lab b/prism-tests/functionality/language/labels-inside-labels.lab
new file mode 100644
index 0000000000..f984265305
--- /dev/null
+++ b/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
diff --git a/prism-tests/functionality/language/labels-inside-labels.prism b/prism-tests/functionality/language/labels-inside-labels.prism
new file mode 100644
index 0000000000..5c73486b91
--- /dev/null
+++ b/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;
diff --git a/prism-tests/functionality/language/labels-inside-labels.prism.props b/prism-tests/functionality/language/labels-inside-labels.prism.props
new file mode 100644
index 0000000000..a25a196ae3
--- /dev/null
+++ b/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" ]
diff --git a/prism-tests/functionality/language/labels-inside-labels.prism.props.args b/prism-tests/functionality/language/labels-inside-labels.prism.props.args
new file mode 100644
index 0000000000..cee1b246c9
--- /dev/null
+++ b/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
diff --git a/prism/src/explicit/ConstructModel.java b/prism/src/explicit/ConstructModel.java
index 22795ac98c..e3f928dd61 100644
--- a/prism/src/explicit/ConstructModel.java
+++ b/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.
diff --git a/prism/src/parser/EvaluateContext.java b/prism/src/parser/EvaluateContext.java
index 5eadbfe99a..83fab146c0 100644
--- a/prism/src/parser/EvaluateContext.java
+++ b/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.
 	 */
diff --git a/prism/src/parser/EvaluateContextState.java b/prism/src/parser/EvaluateContextState.java
index e9022d42dc..2149340613 100644
--- a/prism/src/parser/EvaluateContextState.java
+++ b/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);
+	}
 }
diff --git a/prism/src/parser/ParseException.java b/prism/src/parser/ParseException.java
index 839bcc2939..1d220a5f93 100644
--- a/prism/src/parser/ParseException.java
+++ b/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) */
diff --git a/prism/src/parser/PrismParser.java b/prism/src/parser/PrismParser.java
index 3caebbf460..be28778cb8 100644
--- a/prism/src/parser/PrismParser.java
+++ b/prism/src/parser/PrismParser.java
@@ -2626,6 +2626,10 @@ static class ExpressionPair { public Expression expr1 = null; public Expression
       ret = ExpressionParenth(prop, pathprop);
       break;
       }
+    case DQUOTE:{
+      ret = ExpressionLabel(prop, pathprop);
+      break;
+      }
     case PMAXMAX:
     case PMAXMIN:
     case PMAX:
@@ -2664,10 +2668,6 @@ static class ExpressionPair { public Expression expr1 = null; public Expression
       ret = ExpressionStrategy(prop, pathprop);
       break;
       }
-    case DQUOTE:{
-      ret = ExpressionLabel(prop, pathprop);
-      break;
-      }
     case FILTER:{
       ret = ExpressionFilter(prop, pathprop);
       break;
@@ -3837,8 +3837,8 @@ static class ExpressionPair { public Expression expr1 = null; public Expression
 Expression ExpressionLabel(boolean prop, boolean pathprop) throws ParseException {String s;
         ExpressionLabel ret = null;
         Token begin;
-if (!prop) {if (true) throw generateParseException();}
-    begin = jj_consume_token(DQUOTE);
+    // Label can be arbitary string or the "init" keyword
+            begin = jj_consume_token(DQUOTE);
     switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
     case REG_IDENT:{
       s = Identifier();
@@ -4215,7 +4215,7 @@ static private boolean jj_2_18(int xla)
     finally { jj_save(17, xla); }
   }
 
-  static private boolean jj_3R_ExpressionStrategy_1897_11_186()
+  static private boolean jj_3R_ExpressionStrategy_1897_11_188()
  {
     if (jj_3R_ExpressionParenth_1577_9_147()) return true;
     return false;
@@ -4224,9 +4224,9 @@ static private boolean jj_3R_ExpressionStrategy_1897_11_186()
   static private boolean jj_3R_SystemHideRename_1130_11_82()
  {
     if (jj_scan_token(LBRACE)) return true;
-    if (jj_3R_Identifier_1987_9_30()) return true;
+    if (jj_3R_Identifier_1985_9_30()) return true;
     if (jj_scan_token(RENAME)) return true;
-    if (jj_3R_Identifier_1987_9_30()) return true;
+    if (jj_3R_Identifier_1985_9_30()) return true;
     Token xsp;
     while (true) {
       xsp = jj_scanpos;
@@ -4266,7 +4266,7 @@ static private boolean jj_3R_ExpressionFuncOldStyle_1515_9_146()
 
   static private boolean jj_3R_ExpressionStrategy_1895_11_223()
  {
-    if (jj_3R_ExpressionProb_1618_9_148()) return true;
+    if (jj_3R_ExpressionProb_1618_9_149()) return true;
     return false;
   }
 
@@ -4276,7 +4276,7 @@ static private boolean jj_3_4()
     return false;
   }
 
-  static private boolean jj_3R_ExpressionStrategy_1895_9_185()
+  static private boolean jj_3R_ExpressionStrategy_1895_9_187()
  {
     Token xsp;
     xsp = jj_scanpos;
@@ -4287,7 +4287,7 @@ static private boolean jj_3R_ExpressionStrategy_1895_9_185()
     return false;
   }
 
-  static private boolean jj_3R_ExpressionStrategy_1892_11_184()
+  static private boolean jj_3R_ExpressionStrategy_1892_11_186()
  {
     if (jj_scan_token(DLBRACKET)) return true;
     if (jj_3R_ExpressionStrategyCoalition_1914_9_222()) return true;
@@ -4301,7 +4301,7 @@ static private boolean jj_3R_RewardIndex_1800_101_245()
     return false;
   }
 
-  static private boolean jj_3R_ExpressionStrategy_1891_10_183()
+  static private boolean jj_3R_ExpressionStrategy_1891_10_185()
  {
     if (jj_scan_token(DLT)) return true;
     if (jj_3R_ExpressionStrategyCoalition_1914_9_222()) return true;
@@ -4320,7 +4320,7 @@ static private boolean jj_3R_SystemHideRename_1124_9_81()
  {
     if (jj_scan_token(DIVIDE)) return true;
     if (jj_scan_token(LBRACE)) return true;
-    if (jj_3R_Identifier_1987_9_30()) return true;
+    if (jj_3R_Identifier_1985_9_30()) return true;
     Token xsp;
     while (true) {
       xsp = jj_scanpos;
@@ -4341,18 +4341,18 @@ static private boolean jj_3R_SystemHideRename_1124_9_70()
     return false;
   }
 
-  static private boolean jj_3R_ExpressionStrategy_1888_9_152()
+  static private boolean jj_3R_ExpressionStrategy_1888_9_153()
  {
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_ExpressionStrategy_1891_10_183()) {
+    if (jj_3R_ExpressionStrategy_1891_10_185()) {
     jj_scanpos = xsp;
-    if (jj_3R_ExpressionStrategy_1892_11_184()) return true;
+    if (jj_3R_ExpressionStrategy_1892_11_186()) return true;
     }
     xsp = jj_scanpos;
-    if (jj_3R_ExpressionStrategy_1895_9_185()) {
+    if (jj_3R_ExpressionStrategy_1895_9_187()) {
     jj_scanpos = xsp;
-    if (jj_3R_ExpressionStrategy_1897_11_186()) return true;
+    if (jj_3R_ExpressionStrategy_1897_11_188()) return true;
     }
     return false;
   }
@@ -4426,14 +4426,14 @@ static private boolean jj_3_10()
 
   static private boolean jj_3R_ExpressionFuncOrIdent_1486_9_144()
  {
-    if (jj_3R_Identifier_1987_9_30()) return true;
+    if (jj_3R_Identifier_1985_9_30()) return true;
     Token xsp;
     xsp = jj_scanpos;
     if (jj_3R_ExpressionFuncOrIdent_1488_11_159()) jj_scanpos = xsp;
     return false;
   }
 
-  static private boolean jj_3R_ExpressionForAll_1869_9_151()
+  static private boolean jj_3R_ExpressionForAll_1869_9_152()
  {
     if (jj_scan_token(A)) return true;
     if (jj_scan_token(LBRACKET)) return true;
@@ -4446,7 +4446,7 @@ static private boolean jj_3R_SystemParallel_1095_11_60()
  {
     if (jj_scan_token(OR)) return true;
     if (jj_scan_token(LBRACKET)) return true;
-    if (jj_3R_Identifier_1987_9_30()) return true;
+    if (jj_3R_Identifier_1985_9_30()) return true;
     Token xsp;
     while (true) {
       xsp = jj_scanpos;
@@ -4469,23 +4469,23 @@ static private boolean jj_3R_SystemParallel_1093_9_50()
 
   static private boolean jj_3R_ExpressionBasic_1464_17_142()
  {
-    if (jj_3R_ExpressionFilter_1960_9_154()) return true;
+    if (jj_3R_ExpressionFilter_1958_9_154()) return true;
     return false;
   }
 
   static private boolean jj_3R_ExpressionBasic_1462_17_141()
  {
-    if (jj_3R_ExpressionLabel_1942_9_153()) return true;
+    if (jj_3R_ExpressionStrategy_1888_9_153()) return true;
     return false;
   }
 
   static private boolean jj_3R_ExpressionBasic_1460_17_140()
  {
-    if (jj_3R_ExpressionStrategy_1888_9_152()) return true;
+    if (jj_3R_ExpressionForAll_1869_9_152()) return true;
     return false;
   }
 
-  static private boolean jj_3R_ExpressionExists_1850_9_150()
+  static private boolean jj_3R_ExpressionExists_1850_9_151()
  {
     if (jj_scan_token(E)) return true;
     if (jj_scan_token(LBRACKET)) return true;
@@ -4496,13 +4496,13 @@ static private boolean jj_3R_ExpressionExists_1850_9_150()
 
   static private boolean jj_3R_ExpressionBasic_1458_17_139()
  {
-    if (jj_3R_ExpressionForAll_1869_9_151()) return true;
+    if (jj_3R_ExpressionExists_1850_9_151()) return true;
     return false;
   }
 
   static private boolean jj_3R_ExpressionBasic_1456_17_138()
  {
-    if (jj_3R_ExpressionExists_1850_9_150()) return true;
+    if (jj_3R_ExpressionReward_1741_9_150()) return true;
     return false;
   }
 
@@ -4514,13 +4514,13 @@ static private boolean jj_3R_ExpressionTimesDivide_1408_64_128()
 
   static private boolean jj_3R_ExpressionBasic_1454_17_137()
  {
-    if (jj_3R_ExpressionReward_1741_9_149()) return true;
+    if (jj_3R_ExpressionSS_1697_9_34()) return true;
     return false;
   }
 
   static private boolean jj_3R_ExpressionBasic_1452_17_136()
  {
-    if (jj_3R_ExpressionSS_1697_9_34()) return true;
+    if (jj_3R_ExpressionProb_1618_9_149()) return true;
     return false;
   }
 
@@ -4531,9 +4531,9 @@ static private boolean jj_3_18()
     return false;
   }
 
-  static private boolean jj_3R_ExpressionBasic_1450_17_135()
+  static private boolean jj_3R_ExpressionBasic_1449_17_135()
  {
-    if (jj_3R_ExpressionProb_1618_9_148()) return true;
+    if (jj_3R_ExpressionLabel_1942_9_148()) return true;
     return false;
   }
 
@@ -4624,7 +4624,7 @@ static private boolean jj_3R_ExpressionRewardContents_1827_11_217()
     return false;
   }
 
-  static private boolean jj_3R_ExpressionReward_1769_69_182()
+  static private boolean jj_3R_ExpressionReward_1769_69_184()
  {
     if (jj_3R_Filter_1673_9_48()) return true;
     return false;
@@ -4645,7 +4645,7 @@ static private boolean jj_3R_ExpressionRewardContents_1826_9_216()
   static private boolean jj_3_2()
  {
     if (jj_scan_token(DQUOTE)) return true;
-    if (jj_3R_Identifier_1987_9_30()) return true;
+    if (jj_3R_Identifier_1985_9_30()) return true;
     if (jj_scan_token(DQUOTE)) return true;
     if (jj_scan_token(COLON)) return true;
     return false;
@@ -4654,12 +4654,12 @@ static private boolean jj_3_2()
   static private boolean jj_3R_RewardIndex_1800_33_244()
  {
     if (jj_scan_token(DQUOTE)) return true;
-    if (jj_3R_Identifier_1987_9_30()) return true;
+    if (jj_3R_Identifier_1985_9_30()) return true;
     if (jj_scan_token(DQUOTE)) return true;
     return false;
   }
 
-  static private boolean jj_3R_ExpressionRewardContents_1823_9_181()
+  static private boolean jj_3R_ExpressionRewardContents_1823_9_183()
  {
     Token xsp;
     xsp = jj_scanpos;
@@ -4696,7 +4696,7 @@ static private boolean jj_3R_ExpressionBasic_1438_9_129()
     jj_scanpos = xsp;
     if (jj_3R_ExpressionBasic_1447_17_134()) {
     jj_scanpos = xsp;
-    if (jj_3R_ExpressionBasic_1450_17_135()) {
+    if (jj_3R_ExpressionBasic_1449_17_135()) {
     jj_scanpos = xsp;
     if (jj_3R_ExpressionBasic_1452_17_136()) {
     jj_scanpos = xsp;
@@ -4759,7 +4759,7 @@ static private boolean jj_3R_SystemFullParallel_1046_9_36()
   static private boolean jj_3R_RewardIndex_1798_22_240()
  {
     if (jj_scan_token(DQUOTE)) return true;
-    if (jj_3R_Identifier_1987_9_30()) return true;
+    if (jj_3R_Identifier_1985_9_30()) return true;
     if (jj_scan_token(DQUOTE)) return true;
     return false;
   }
@@ -4831,7 +4831,7 @@ static private boolean jj_3R_RewardIndex_1798_9_231()
   static private boolean jj_3_7()
  {
     if (jj_scan_token(DQUOTE)) return true;
-    if (jj_3R_Identifier_1987_9_30()) return true;
+    if (jj_3R_Identifier_1985_9_30()) return true;
     if (jj_scan_token(DQUOTE)) return true;
     if (jj_3R_SystemDefn_1033_9_32()) return true;
     return false;
@@ -4900,7 +4900,7 @@ static private boolean jj_3R_ExpressionReward_1752_26_235()
     return false;
   }
 
-  static private boolean jj_3R_ExpressionReward_1767_10_180()
+  static private boolean jj_3R_ExpressionReward_1767_10_182()
  {
     if (jj_scan_token(RMAXMAX)) return true;
     if (jj_scan_token(EQ)) return true;
@@ -4924,7 +4924,7 @@ static private boolean jj_3R_ExpressionReward_1759_17_215()
     return false;
   }
 
-  static private boolean jj_3R_ExpressionReward_1766_10_179()
+  static private boolean jj_3R_ExpressionReward_1766_10_181()
  {
     if (jj_scan_token(RMAXMIN)) return true;
     if (jj_scan_token(EQ)) return true;
@@ -4948,7 +4948,7 @@ static private boolean jj_3R_ExpressionReward_1758_17_214()
     return false;
   }
 
-  static private boolean jj_3R_ExpressionReward_1765_10_178()
+  static private boolean jj_3R_ExpressionReward_1765_10_180()
  {
     if (jj_scan_token(RMINMAX)) return true;
     if (jj_scan_token(EQ)) return true;
@@ -4971,7 +4971,7 @@ static private boolean jj_3R_ExpressionReward_1757_17_213()
     return false;
   }
 
-  static private boolean jj_3R_ExpressionReward_1764_10_177()
+  static private boolean jj_3R_ExpressionReward_1764_10_179()
  {
     if (jj_scan_token(RMINMIN)) return true;
     if (jj_scan_token(EQ)) return true;
@@ -4987,7 +4987,7 @@ static private boolean jj_3R_ExpressionReward_1756_17_212()
     return false;
   }
 
-  static private boolean jj_3R_ExpressionReward_1763_10_176()
+  static private boolean jj_3R_ExpressionReward_1763_10_178()
  {
     if (jj_scan_token(RMAX)) return true;
     if (jj_scan_token(EQ)) return true;
@@ -4995,7 +4995,7 @@ static private boolean jj_3R_ExpressionReward_1763_10_176()
     return false;
   }
 
-  static private boolean jj_3R_ExpressionReward_1762_10_175()
+  static private boolean jj_3R_ExpressionReward_1762_10_177()
  {
     if (jj_scan_token(RMIN)) return true;
     if (jj_scan_token(EQ)) return true;
@@ -5042,7 +5042,7 @@ static private boolean jj_3R_ExpressionReward_1747_17_209()
 
   static private boolean jj_3R_ExpressionReward_1746_18_208()
  {
-    if (jj_3R_LtGt_2048_9_46()) return true;
+    if (jj_3R_LtGt_2046_9_46()) return true;
     if (jj_3R_Expression_1176_9_39()) return true;
     return false;
   }
@@ -5056,14 +5056,14 @@ static private boolean jj_3R_ExpressionReward_1745_18_207()
   static private boolean jj_3R_ExpressionReward_1744_19_206()
  {
     if (jj_scan_token(LPARENTH)) return true;
-    if (jj_3R_IdentifierExpression_1998_9_33()) return true;
+    if (jj_3R_IdentifierExpression_1996_9_33()) return true;
     if (jj_scan_token(RPARENTH)) return true;
     return false;
   }
 
   static private boolean jj_3R_ExpressionRelop_1369_11_115()
  {
-    if (jj_3R_LtGt_2048_9_46()) return true;
+    if (jj_3R_LtGt_2046_9_46()) return true;
     if (jj_3R_ExpressionPlusMinus_1389_9_114()) return true;
     return false;
   }
@@ -5085,7 +5085,7 @@ static private boolean jj_3R_ExpressionSS_1705_55_40()
     return false;
   }
 
-  static private boolean jj_3R_ExpressionReward_1743_10_174()
+  static private boolean jj_3R_ExpressionReward_1743_10_176()
  {
     if (jj_scan_token(R)) return true;
     Token xsp;
@@ -5119,23 +5119,23 @@ static private boolean jj_3R_ExpressionReward_1743_10_174()
     return false;
   }
 
-  static private boolean jj_3R_ExpressionReward_1741_9_149()
+  static private boolean jj_3R_ExpressionReward_1741_9_150()
  {
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_ExpressionReward_1743_10_174()) {
+    if (jj_3R_ExpressionReward_1743_10_176()) {
     jj_scanpos = xsp;
-    if (jj_3R_ExpressionReward_1762_10_175()) {
+    if (jj_3R_ExpressionReward_1762_10_177()) {
     jj_scanpos = xsp;
-    if (jj_3R_ExpressionReward_1763_10_176()) {
+    if (jj_3R_ExpressionReward_1763_10_178()) {
     jj_scanpos = xsp;
-    if (jj_3R_ExpressionReward_1764_10_177()) {
+    if (jj_3R_ExpressionReward_1764_10_179()) {
     jj_scanpos = xsp;
-    if (jj_3R_ExpressionReward_1765_10_178()) {
+    if (jj_3R_ExpressionReward_1765_10_180()) {
     jj_scanpos = xsp;
-    if (jj_3R_ExpressionReward_1766_10_179()) {
+    if (jj_3R_ExpressionReward_1766_10_181()) {
     jj_scanpos = xsp;
-    if (jj_3R_ExpressionReward_1767_10_180()) return true;
+    if (jj_3R_ExpressionReward_1767_10_182()) return true;
     }
     }
     }
@@ -5143,16 +5143,16 @@ static private boolean jj_3R_ExpressionReward_1741_9_149()
     }
     }
     if (jj_scan_token(LBRACKET)) return true;
-    if (jj_3R_ExpressionRewardContents_1823_9_181()) return true;
+    if (jj_3R_ExpressionRewardContents_1823_9_183()) return true;
     xsp = jj_scanpos;
-    if (jj_3R_ExpressionReward_1769_69_182()) jj_scanpos = xsp;
+    if (jj_3R_ExpressionReward_1769_69_184()) jj_scanpos = xsp;
     if (jj_scan_token(RBRACKET)) return true;
     return false;
   }
 
   static private boolean jj_3R_ExpressionEquality_1355_11_113()
  {
-    if (jj_3R_EqNeq_2038_9_116()) return true;
+    if (jj_3R_EqNeq_2036_9_116()) return true;
     if (jj_3R_ExpressionRelop_1368_9_112()) return true;
     return false;
   }
@@ -5171,7 +5171,7 @@ static private boolean jj_3R_ExpressionEquality_1354_9_111()
   static private boolean jj_3_1()
  {
     if (jj_scan_token(MODULE)) return true;
-    if (jj_3R_Identifier_1987_9_30()) return true;
+    if (jj_3R_Identifier_1985_9_30()) return true;
     if (jj_scan_token(EQ)) return true;
     return false;
   }
@@ -5240,7 +5240,7 @@ static private boolean jj_3R_ExpressionSS_1702_17_38()
   static private boolean jj_3R_ExpressionSS_1700_19_45()
  {
     if (jj_scan_token(LPARENTH)) return true;
-    if (jj_3R_IdentifierExpression_1998_9_33()) return true;
+    if (jj_3R_IdentifierExpression_1996_9_33()) return true;
     if (jj_scan_token(RPARENTH)) return true;
     return false;
   }
@@ -5257,7 +5257,7 @@ static private boolean jj_3R_ExpressionSS_1700_17_37()
     Token xsp;
     xsp = jj_scanpos;
     if (jj_3R_ExpressionSS_1700_19_45()) jj_scanpos = xsp;
-    if (jj_3R_LtGt_2048_9_46()) return true;
+    if (jj_3R_LtGt_2046_9_46()) return true;
     if (jj_3R_Expression_1176_9_39()) return true;
     return false;
   }
@@ -5315,7 +5315,7 @@ static private boolean jj_3R_Update_896_36_42()
     return false;
   }
 
-  static private boolean jj_3R_ExpressionProb_1644_51_173()
+  static private boolean jj_3R_ExpressionProb_1644_51_175()
  {
     if (jj_3R_Filter_1673_9_48()) return true;
     return false;
@@ -5367,7 +5367,7 @@ static private boolean jj_3R_Filter_1674_11_58()
   static private boolean jj_3R_UpdateElement_909_9_41()
  {
     if (jj_scan_token(LPARENTH)) return true;
-    if (jj_3R_IdentifierPrime_2020_9_49()) return true;
+    if (jj_3R_IdentifierPrime_2018_9_49()) return true;
     if (jj_scan_token(EQ)) return true;
     if (jj_3R_Expression_1176_9_39()) return true;
     if (jj_scan_token(RPARENTH)) return true;
@@ -5405,58 +5405,58 @@ static private boolean jj_3R_ExpressionImplies_1285_9_83()
     return false;
   }
 
-  static private boolean jj_3R_LtGt_2051_9_55()
+  static private boolean jj_3R_LtGt_2049_9_55()
  {
     if (jj_scan_token(LE)) return true;
     return false;
   }
 
-  static private boolean jj_3R_LtGt_2050_9_54()
+  static private boolean jj_3R_LtGt_2048_9_54()
  {
     if (jj_scan_token(GE)) return true;
     return false;
   }
 
-  static private boolean jj_3R_LtGt_2049_9_53()
+  static private boolean jj_3R_LtGt_2047_9_53()
  {
     if (jj_scan_token(LT)) return true;
     return false;
   }
 
-  static private boolean jj_3R_LtGt_2048_9_52()
+  static private boolean jj_3R_Update_896_10_35()
+ {
+    if (jj_3R_UpdateElement_909_9_41()) return true;
+    Token xsp;
+    while (true) {
+      xsp = jj_scanpos;
+      if (jj_3R_Update_896_36_42()) { jj_scanpos = xsp; break; }
+    }
+    return false;
+  }
+
+  static private boolean jj_3R_LtGt_2046_9_52()
  {
     if (jj_scan_token(GT)) return true;
     return false;
   }
 
-  static private boolean jj_3R_LtGt_2048_9_46()
+  static private boolean jj_3R_LtGt_2046_9_46()
  {
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_LtGt_2048_9_52()) {
+    if (jj_3R_LtGt_2046_9_52()) {
     jj_scanpos = xsp;
-    if (jj_3R_LtGt_2049_9_53()) {
+    if (jj_3R_LtGt_2047_9_53()) {
     jj_scanpos = xsp;
-    if (jj_3R_LtGt_2050_9_54()) {
+    if (jj_3R_LtGt_2048_9_54()) {
     jj_scanpos = xsp;
-    if (jj_3R_LtGt_2051_9_55()) return true;
+    if (jj_3R_LtGt_2049_9_55()) return true;
     }
     }
     }
     return false;
   }
 
-  static private boolean jj_3R_Update_896_10_35()
- {
-    if (jj_3R_UpdateElement_909_9_41()) return true;
-    Token xsp;
-    while (true) {
-      xsp = jj_scanpos;
-      if (jj_3R_Update_896_36_42()) { jj_scanpos = xsp; break; }
-    }
-    return false;
-  }
-
   static private boolean jj_3R_ExpressionITE_1271_17_84()
  {
     if (jj_scan_token(QMARK)) return true;
@@ -5479,61 +5479,61 @@ static private boolean jj_3R_Update_894_9_31()
 
   static private boolean jj_3_14()
  {
-    if (jj_3R_IdentifierExpression_1998_9_33()) return true;
+    if (jj_3R_IdentifierExpression_1996_9_33()) return true;
     if (jj_scan_token(LPARENTH)) return true;
     return false;
   }
 
   static private boolean jj_3_13()
  {
-    if (jj_3R_IdentifierExpression_1998_9_33()) return true;
+    if (jj_3R_IdentifierExpression_1996_9_33()) return true;
     if (jj_scan_token(LPARENTH)) return true;
     return false;
   }
 
   static private boolean jj_3_12()
  {
-    if (jj_3R_IdentifierExpression_1998_9_33()) return true;
+    if (jj_3R_IdentifierExpression_1996_9_33()) return true;
     if (jj_scan_token(LPARENTH)) return true;
     return false;
   }
 
   static private boolean jj_3_11()
  {
-    if (jj_3R_IdentifierExpression_1998_9_33()) return true;
+    if (jj_3R_IdentifierExpression_1996_9_33()) return true;
     if (jj_scan_token(LPARENTH)) return true;
     return false;
   }
 
-  static private boolean jj_3R_EqNeq_2039_9_120()
+  static private boolean jj_3R_EqNeq_2037_9_120()
  {
     if (jj_scan_token(NE)) return true;
     return false;
   }
 
-  static private boolean jj_3R_EqNeq_2038_9_116()
+  static private boolean jj_3_5()
+ {
+    if (jj_3R_Update_894_9_31()) return true;
+    return false;
+  }
+
+  static private boolean jj_3R_EqNeq_2036_9_116()
  {
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_EqNeq_2038_9_119()) {
+    if (jj_3R_EqNeq_2036_9_119()) {
     jj_scanpos = xsp;
-    if (jj_3R_EqNeq_2039_9_120()) return true;
+    if (jj_3R_EqNeq_2037_9_120()) return true;
     }
     return false;
   }
 
-  static private boolean jj_3R_EqNeq_2038_9_119()
+  static private boolean jj_3R_EqNeq_2036_9_119()
  {
     if (jj_scan_token(EQ)) return true;
     return false;
   }
 
-  static private boolean jj_3_5()
- {
-    if (jj_3R_Update_894_9_31()) return true;
-    return false;
-  }
-
   static private boolean jj_3R_ExpressionITE_1269_9_76()
  {
     if (jj_3R_ExpressionImplies_1285_9_83()) return true;
@@ -5545,19 +5545,19 @@ static private boolean jj_3R_ExpressionITE_1269_9_76()
 
   static private boolean jj_3R_TimeBound_1255_20_101()
  {
-    if (jj_3R_IdentifierExpression_1998_9_33()) return true;
+    if (jj_3R_IdentifierExpression_1996_9_33()) return true;
     return false;
   }
 
   static private boolean jj_3R_TimeBound_1254_20_99()
  {
-    if (jj_3R_IdentifierExpression_1998_9_33()) return true;
+    if (jj_3R_IdentifierExpression_1996_9_33()) return true;
     return false;
   }
 
   static private boolean jj_3R_TimeBound_1253_20_97()
  {
-    if (jj_3R_IdentifierExpression_1998_9_33()) return true;
+    if (jj_3R_IdentifierExpression_1996_9_33()) return true;
     return false;
   }
 
@@ -5571,7 +5571,7 @@ static private boolean jj_3R_ExpressionProb_1629_26_230()
 
   static private boolean jj_3R_TimeBound_1252_20_95()
  {
-    if (jj_3R_IdentifierExpression_1998_9_33()) return true;
+    if (jj_3R_IdentifierExpression_1996_9_33()) return true;
     return false;
   }
 
@@ -5590,7 +5590,7 @@ static private boolean jj_3R_ExpressionProb_1627_26_228()
     return false;
   }
 
-  static private boolean jj_3R_ExpressionProb_1642_10_172()
+  static private boolean jj_3R_ExpressionProb_1642_10_174()
  {
     if (jj_scan_token(PMAXMAX)) return true;
     if (jj_scan_token(EQ)) return true;
@@ -5614,7 +5614,7 @@ static private boolean jj_3R_ExpressionProb_1634_17_205()
     return false;
   }
 
-  static private boolean jj_3R_ExpressionProb_1641_10_171()
+  static private boolean jj_3R_ExpressionProb_1641_10_173()
  {
     if (jj_scan_token(PMAXMIN)) return true;
     if (jj_scan_token(EQ)) return true;
@@ -5645,7 +5645,7 @@ static private boolean jj_3R_ExpressionProb_1633_17_204()
     return false;
   }
 
-  static private boolean jj_3R_ExpressionProb_1640_10_170()
+  static private boolean jj_3R_ExpressionProb_1640_10_172()
  {
     if (jj_scan_token(PMINMAX)) return true;
     if (jj_scan_token(EQ)) return true;
@@ -5678,7 +5678,7 @@ static private boolean jj_3R_ExpressionProb_1632_17_203()
     return false;
   }
 
-  static private boolean jj_3R_ExpressionProb_1639_10_169()
+  static private boolean jj_3R_ExpressionProb_1639_10_171()
  {
     if (jj_scan_token(PMINMIN)) return true;
     if (jj_scan_token(EQ)) return true;
@@ -5706,7 +5706,7 @@ static private boolean jj_3R_ExpressionProb_1631_17_202()
     return false;
   }
 
-  static private boolean jj_3R_ExpressionProb_1638_10_168()
+  static private boolean jj_3R_ExpressionProb_1638_10_170()
  {
     if (jj_scan_token(PMAX)) return true;
     if (jj_scan_token(EQ)) return true;
@@ -5726,7 +5726,7 @@ static private boolean jj_3R_TimeBound_1254_11_87()
     return false;
   }
 
-  static private boolean jj_3R_ExpressionProb_1637_10_167()
+  static private boolean jj_3R_ExpressionProb_1637_10_169()
  {
     if (jj_scan_token(PMIN)) return true;
     if (jj_scan_token(EQ)) return true;
@@ -5748,7 +5748,7 @@ static private boolean jj_3R_TimeBound_1253_11_86()
 
   static private boolean jj_3R_ExpressionProb_1621_25_198()
  {
-    if (jj_3R_LtGt_2048_9_46()) return true;
+    if (jj_3R_LtGt_2046_9_46()) return true;
     if (jj_3R_Expression_1176_9_39()) return true;
     return false;
   }
@@ -5756,7 +5756,7 @@ static private boolean jj_3R_ExpressionProb_1621_25_198()
   static private boolean jj_3R_ExpressionProb_1620_26_197()
  {
     if (jj_scan_token(LPARENTH)) return true;
-    if (jj_3R_IdentifierExpression_1998_9_33()) return true;
+    if (jj_3R_IdentifierExpression_1996_9_33()) return true;
     if (jj_scan_token(RPARENTH)) return true;
     return false;
   }
@@ -5773,12 +5773,6 @@ static private boolean jj_3R_TimeBound_1252_11_85()
     return false;
   }
 
-  static private boolean jj_3R_IdentifierPrime_2020_9_49()
- {
-    if (jj_scan_token(REG_IDENTPRIME)) return true;
-    return false;
-  }
-
   static private boolean jj_3R_ExpressionProb_1627_17_201()
  {
     if (jj_scan_token(MAX)) return true;
@@ -5817,6 +5811,12 @@ static private boolean jj_3R_TimeBound_1252_9_77()
     return false;
   }
 
+  static private boolean jj_3R_IdentifierPrime_2018_9_49()
+ {
+    if (jj_scan_token(REG_IDENTPRIME)) return true;
+    return false;
+  }
+
   static private boolean jj_3R_ExpressionProb_1623_17_200()
  {
     if (jj_scan_token(MIN)) return true;
@@ -5839,15 +5839,15 @@ static private boolean jj_3R_ExpressionProb_1622_17_199()
     return false;
   }
 
-  static private boolean jj_3R_ExpressionFilter_1966_56_193()
+  static private boolean jj_3R_ExpressionTemporalUnary_1239_17_62()
  {
-    if (jj_scan_token(OR)) return true;
+    if (jj_3R_ExpressionITE_1269_9_76()) return true;
     return false;
   }
 
-  static private boolean jj_3R_ExpressionTemporalUnary_1239_17_62()
+  static private boolean jj_3R_ExpressionFilter_1964_56_193()
  {
-    if (jj_3R_ExpressionITE_1269_9_76()) return true;
+    if (jj_scan_token(OR)) return true;
     return false;
   }
 
@@ -5875,7 +5875,7 @@ static private boolean jj_3R_ExpressionTemporalUnary_1232_19_72()
     return false;
   }
 
-  static private boolean jj_3R_ExpressionProb_1620_10_166()
+  static private boolean jj_3R_ExpressionProb_1620_10_168()
  {
     if (jj_scan_token(P)) return true;
     Token xsp;
@@ -5924,23 +5924,23 @@ static private boolean jj_3R_ExpressionTemporalUnary_1230_17_61()
     return false;
   }
 
-  static private boolean jj_3R_ExpressionProb_1618_9_148()
+  static private boolean jj_3R_ExpressionProb_1618_9_149()
  {
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_ExpressionProb_1620_10_166()) {
+    if (jj_3R_ExpressionProb_1620_10_168()) {
     jj_scanpos = xsp;
-    if (jj_3R_ExpressionProb_1637_10_167()) {
+    if (jj_3R_ExpressionProb_1637_10_169()) {
     jj_scanpos = xsp;
-    if (jj_3R_ExpressionProb_1638_10_168()) {
+    if (jj_3R_ExpressionProb_1638_10_170()) {
     jj_scanpos = xsp;
-    if (jj_3R_ExpressionProb_1639_10_169()) {
+    if (jj_3R_ExpressionProb_1639_10_171()) {
     jj_scanpos = xsp;
-    if (jj_3R_ExpressionProb_1640_10_170()) {
+    if (jj_3R_ExpressionProb_1640_10_172()) {
     jj_scanpos = xsp;
-    if (jj_3R_ExpressionProb_1641_10_171()) {
+    if (jj_3R_ExpressionProb_1641_10_173()) {
     jj_scanpos = xsp;
-    if (jj_3R_ExpressionProb_1642_10_172()) return true;
+    if (jj_3R_ExpressionProb_1642_10_174()) return true;
     }
     }
     }
@@ -5950,14 +5950,14 @@ static private boolean jj_3R_ExpressionProb_1618_9_148()
     if (jj_scan_token(LBRACKET)) return true;
     if (jj_3R_Expression_1176_9_39()) return true;
     xsp = jj_scanpos;
-    if (jj_3R_ExpressionProb_1644_51_173()) jj_scanpos = xsp;
+    if (jj_3R_ExpressionProb_1644_51_175()) jj_scanpos = xsp;
     if (jj_scan_token(RBRACKET)) return true;
     return false;
   }
 
-  static private boolean jj_3R_IdentifierExpression_1998_9_33()
+  static private boolean jj_3R_IdentifierExpression_1996_9_33()
  {
-    if (jj_3R_Identifier_1987_9_30()) return true;
+    if (jj_3R_Identifier_1985_9_30()) return true;
     return false;
   }
 
@@ -5972,21 +5972,21 @@ static private boolean jj_3R_ExpressionTemporalUnary_1228_9_56()
     return false;
   }
 
-  static private boolean jj_3R_ExpressionFilter_1966_34_192()
+  static private boolean jj_3R_ExpressionTemporalBinary_1214_19_66()
  {
-    if (jj_scan_token(AND)) return true;
+    if (jj_3R_TimeBound_1252_9_77()) return true;
     return false;
   }
 
-  static private boolean jj_3R_ExpressionFilter_1965_35_190()
+  static private boolean jj_3R_ExpressionFilter_1964_34_192()
  {
-    if (jj_scan_token(MAX)) return true;
+    if (jj_scan_token(AND)) return true;
     return false;
   }
 
-  static private boolean jj_3R_ExpressionTemporalBinary_1214_19_66()
+  static private boolean jj_3R_ExpressionFilter_1963_35_190()
  {
-    if (jj_3R_TimeBound_1252_9_77()) return true;
+    if (jj_scan_token(MAX)) return true;
     return false;
   }
 
@@ -6008,7 +6008,7 @@ static private boolean jj_3R_ExpressionTemporalBinary_1211_19_63()
     return false;
   }
 
-  static private boolean jj_3R_Identifier_1987_9_30()
+  static private boolean jj_3R_Identifier_1985_9_30()
  {
     if (jj_scan_token(REG_IDENT)) return true;
     return false;
@@ -6031,7 +6031,7 @@ static private boolean jj_3R_ExpressionTemporalBinary_1209_17_57()
     return false;
   }
 
-  static private boolean jj_3R_ExpressionLabel_1944_47_188()
+  static private boolean jj_3R_ExpressionLabel_1942_45_167()
  {
     if (jj_scan_token(INIT)) return true;
     return false;
@@ -6044,16 +6044,9 @@ static private boolean jj_3R_ExpressionFuncArgs_1527_72_196()
     return false;
   }
 
-  static private boolean jj_3R_ExpressionFilter_1971_11_195()
- {
-    if (jj_scan_token(COMMA)) return true;
-    if (jj_3R_Expression_1176_9_39()) return true;
-    return false;
-  }
-
   static private boolean jj_3R_ExpressionFuncOldStyle_1515_83_165()
  {
-    if (jj_3R_Identifier_1987_9_30()) return true;
+    if (jj_3R_Identifier_1985_9_30()) return true;
     return false;
   }
 
@@ -6066,34 +6059,41 @@ static private boolean jj_3R_ExpressionTemporalBinary_1206_9_47()
     return false;
   }
 
-  static private boolean jj_3R_ExpressionFilter_1967_11_194()
+  static private boolean jj_3R_ExpressionFilter_1969_11_195()
  {
-    if (jj_3R_Identifier_1987_9_30()) return true;
+    if (jj_scan_token(COMMA)) return true;
+    if (jj_3R_Expression_1176_9_39()) return true;
     return false;
   }
 
-  static private boolean jj_3R_ExpressionFilter_1966_11_191()
+  static private boolean jj_3R_ExpressionFilter_1965_11_194()
  {
-    if (jj_scan_token(PLUS)) return true;
+    if (jj_3R_Identifier_1985_9_30()) return true;
     return false;
   }
 
-  static private boolean jj_3R_ExpressionFilter_1965_11_189()
+  static private boolean jj_3R_ExpressionFilter_1964_11_191()
  {
-    if (jj_scan_token(MIN)) return true;
+    if (jj_scan_token(PLUS)) return true;
     return false;
   }
 
-  static private boolean jj_3R_ExpressionLabel_1944_30_187()
+  static private boolean jj_3R_ExpressionFilter_1963_11_189()
  {
-    if (jj_3R_Identifier_1987_9_30()) return true;
+    if (jj_scan_token(MIN)) return true;
     return false;
   }
 
   static private boolean jj_3R_SystemHideRename_1126_81_91()
  {
     if (jj_scan_token(COMMA)) return true;
-    if (jj_3R_Identifier_1987_9_30()) return true;
+    if (jj_3R_Identifier_1985_9_30()) return true;
+    return false;
+  }
+
+  static private boolean jj_3R_ExpressionLabel_1942_28_166()
+ {
+    if (jj_3R_Identifier_1985_9_30()) return true;
     return false;
   }
 
@@ -6105,23 +6105,23 @@ static private boolean jj_3R_ExpressionParenth_1577_9_147()
     return false;
   }
 
-  static private boolean jj_3R_ExpressionFilter_1960_9_154()
+  static private boolean jj_3R_ExpressionFilter_1958_9_154()
  {
     if (jj_scan_token(FILTER)) return true;
     if (jj_scan_token(LPARENTH)) return true;
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_ExpressionFilter_1965_11_189()) {
+    if (jj_3R_ExpressionFilter_1963_11_189()) {
     jj_scanpos = xsp;
-    if (jj_3R_ExpressionFilter_1965_35_190()) {
+    if (jj_3R_ExpressionFilter_1963_35_190()) {
     jj_scanpos = xsp;
-    if (jj_3R_ExpressionFilter_1966_11_191()) {
+    if (jj_3R_ExpressionFilter_1964_11_191()) {
     jj_scanpos = xsp;
-    if (jj_3R_ExpressionFilter_1966_34_192()) {
+    if (jj_3R_ExpressionFilter_1964_34_192()) {
     jj_scanpos = xsp;
-    if (jj_3R_ExpressionFilter_1966_56_193()) {
+    if (jj_3R_ExpressionFilter_1964_56_193()) {
     jj_scanpos = xsp;
-    if (jj_3R_ExpressionFilter_1967_11_194()) return true;
+    if (jj_3R_ExpressionFilter_1965_11_194()) return true;
     }
     }
     }
@@ -6130,7 +6130,7 @@ static private boolean jj_3R_ExpressionFilter_1960_9_154()
     if (jj_scan_token(COMMA)) return true;
     if (jj_3R_Expression_1176_9_39()) return true;
     xsp = jj_scanpos;
-    if (jj_3R_ExpressionFilter_1971_11_195()) jj_scanpos = xsp;
+    if (jj_3R_ExpressionFilter_1969_11_195()) jj_scanpos = xsp;
     if (jj_scan_token(RPARENTH)) return true;
     return false;
   }
@@ -6159,14 +6159,14 @@ static private boolean jj_3R_Expression_1176_9_39()
     return false;
   }
 
-  static private boolean jj_3R_ExpressionLabel_1942_9_153()
+  static private boolean jj_3R_ExpressionLabel_1942_9_148()
  {
     if (jj_scan_token(DQUOTE)) return true;
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_ExpressionLabel_1944_30_187()) {
+    if (jj_3R_ExpressionLabel_1942_28_166()) {
     jj_scanpos = xsp;
-    if (jj_3R_ExpressionLabel_1944_47_188()) return true;
+    if (jj_3R_ExpressionLabel_1942_45_167()) return true;
     }
     if (jj_scan_token(DQUOTE)) return true;
     return false;
@@ -6174,7 +6174,7 @@ static private boolean jj_3R_ExpressionLabel_1942_9_153()
 
   static private boolean jj_3R_ExpressionStrategy_1895_51_224()
  {
-    if (jj_3R_ExpressionReward_1741_9_149()) return true;
+    if (jj_3R_ExpressionReward_1741_9_150()) return true;
     return false;
   }
 
@@ -6218,7 +6218,7 @@ static private boolean jj_3R_ExpressionLiteral_1538_9_155()
   static private boolean jj_3R_SystemAtomic_1154_10_79()
  {
     if (jj_scan_token(DQUOTE)) return true;
-    if (jj_3R_Identifier_1987_9_30()) return true;
+    if (jj_3R_Identifier_1985_9_30()) return true;
     if (jj_scan_token(DQUOTE)) return true;
     return false;
   }
@@ -6260,14 +6260,14 @@ static private boolean jj_3R_ExpressionStrategyCoalition_1916_11_243()
 
   static private boolean jj_3R_SystemAtomic_1152_9_78()
  {
-    if (jj_3R_Identifier_1987_9_30()) return true;
+    if (jj_3R_Identifier_1985_9_30()) return true;
     return false;
   }
 
   static private boolean jj_3R_SystemParallel_1096_65_71()
  {
     if (jj_scan_token(COMMA)) return true;
-    if (jj_3R_Identifier_1987_9_30()) return true;
+    if (jj_3R_Identifier_1985_9_30()) return true;
     return false;
   }
 
@@ -6330,9 +6330,9 @@ static private boolean jj_3R_ExpressionFuncArgs_1527_9_162()
   static private boolean jj_3R_SystemHideRename_1133_19_92()
  {
     if (jj_scan_token(COMMA)) return true;
-    if (jj_3R_Identifier_1987_9_30()) return true;
+    if (jj_3R_Identifier_1985_9_30()) return true;
     if (jj_scan_token(RENAME)) return true;
-    if (jj_3R_Identifier_1987_9_30()) return true;
+    if (jj_3R_Identifier_1985_9_30()) return true;
     return false;
   }
 
diff --git a/prism/src/parser/PrismParser.jj b/prism/src/parser/PrismParser.jj
index d80d828f0d..90e047cb70 100644
--- a/prism/src/parser/PrismParser.jj
+++ b/prism/src/parser/PrismParser.jj
@@ -1445,6 +1445,8 @@ Expression ExpressionBasic(boolean prop, boolean pathprop) :
 		ret = ExpressionFuncOldStyle(prop, pathprop)
 	|
 		ret = ExpressionParenth(prop, pathprop)
+	|
+		ret = ExpressionLabel(prop, pathprop)
 	|
 		// Remaining options are only applicable for properties
 		ret = ExpressionProb(prop, pathprop)
@@ -1458,8 +1460,6 @@ Expression ExpressionBasic(boolean prop, boolean pathprop) :
 		ret = ExpressionForAll(prop, pathprop)
 	|
 		ret = ExpressionStrategy(prop, pathprop)
-	|
-		ret = ExpressionLabel(prop, pathprop)
 	|
 		ret = ExpressionFilter(prop, pathprop)
 	)
@@ -1938,10 +1938,8 @@ Expression ExpressionLabel(boolean prop, boolean pathprop) :
 	Token begin;
 }
 {
-	// This production is only allowed in expressions if the "prop" parameter is true
-	{ if (!prop) throw generateParseException(); }
 	// Label can be arbitary string or the "init" keyword
-	( begin = <DQUOTE> ( s=Identifier() | <INIT> { s = "init"; } ) <DQUOTE> )
+	begin = <DQUOTE> ( s=Identifier() | <INIT> { s = "init"; } ) <DQUOTE>
 	{ ret = new ExpressionLabel(s); ret.setPosition(begin, getToken(0)); return ret; }
 }
 
diff --git a/prism/src/parser/ast/Expression.java b/prism/src/parser/ast/Expression.java
index 0f71f64789..c0330e86d3 100644
--- a/prism/src/parser/ast/Expression.java
+++ b/prism/src/parser/ast/Expression.java
@@ -50,6 +50,9 @@
 import prism.PrismException;
 import prism.PrismLangException;
 
+import java.util.Map;
+import java.util.function.Predicate;
+
 // Abstract class for PRISM language expressions
 
 public abstract class Expression extends ASTElement
@@ -103,6 +106,12 @@ public Object getConstantValue(String name)
 			{
 				return ec.getConstantValue(name);
 			}
+
+			@Override
+			public Boolean getLabelValue(String name)
+			{
+				return ec.getLabelValue(name);
+			}
 		}));
 	}
 
@@ -576,6 +585,19 @@ public boolean evaluateBoolean(Values constantValues, State state) throws PrismL
 		return evaluateBoolean(new EvaluateContextState(constantValues, state));
 	}
 
+	/**
+	 * Evaluate this expression as a boolean, based on values for labels/variables.
+	 * Any typing issues cause an exception.
+	 * Constant values are supplied as a Values object.
+	 * Label values are supplied as a Map.
+	 * 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, Predicate<String> labelValues, State state) throws PrismLangException
+	{
+		return evaluateBoolean(new EvaluateContextState(constantValues, labelValues, state));
+	}
+
 	/**
 	 * Evaluate this expression as a boolean, based on values for some variables (but not constants).
 	 * Basically casts the result to a boolean, checking for any type errors.
@@ -659,6 +681,19 @@ public BigRational evaluateExact(Values constantValues, State state) throws Pris
 		return evaluateExact(new EvaluateContextState(constantValues, state));
 	}
 
+	/**
+	 * Evaluate this expression exactly to a BigRational, based on values for constants, variables and labels.
+	 * This is regardless of the type (e.g. ints, booleans are also converted).
+	 * Constant values are supplied as a Values object.
+	 * Variable values are supplied as a State object, i.e. array of variable values.
+	 * Labels are supplied as a Map from label names to booleans.
+	 * Note: assumes that type checking has been done.
+	 */
+	public BigRational evaluateExact(Values constantValues, Predicate<String> labelValues, State state) throws PrismLangException
+	{
+		return evaluateExact(new EvaluateContextState(constantValues, labelValues, state));
+	}
+
 	/**
 	 * Evaluate this expression exactly to a BigRational, based on values for some variables (but not constants).
 	 * This is regardless of the type (e.g. ints, booleans are also converted).
diff --git a/prism/src/parser/ast/ExpressionLabel.java b/prism/src/parser/ast/ExpressionLabel.java
index b390d6ca41..644e5bd0e9 100644
--- a/prism/src/parser/ast/ExpressionLabel.java
+++ b/prism/src/parser/ast/ExpressionLabel.java
@@ -26,6 +26,7 @@
 
 package parser.ast;
 
+import param.BigRational;
 import parser.EvaluateContext;
 import parser.visitor.ASTVisitor;
 import parser.visitor.DeepCopy;
@@ -81,9 +82,21 @@ public boolean isProposition()
 	}
 	
 	@Override
-	public Object evaluate(EvaluateContext ec) throws PrismLangException
+	public Boolean evaluate(EvaluateContext ec) throws PrismLangException
 	{
-		throw new PrismLangException("Cannot evaluate labels", this);
+		Boolean value = ec.getLabelValue(this.name);
+		if (value == null)
+			throw new PrismLangException("Failed to evaluate label", this);
+		return value;
+	}
+
+	@Override
+	public BigRational evaluateExact(EvaluateContext ec) throws PrismLangException
+	{
+		Boolean value = ec.getLabelValue(this.name);
+		if (value == null)
+			throw new PrismLangException("Failed to evaluate label", this);
+		return BigRational.from(value);
 	}
 
 	@Override
diff --git a/prism/src/parser/ast/LabelList.java b/prism/src/parser/ast/LabelList.java
index b242192742..44fd139b0b 100644
--- a/prism/src/parser/ast/LabelList.java
+++ b/prism/src/parser/ast/LabelList.java
@@ -32,47 +32,89 @@
 import parser.visitor.ASTVisitor;
 import parser.visitor.DeepCopy;
 import prism.PrismLangException;
+import prism.PrismUtils;
 
 // class to store list of labels
 
 public class LabelList extends ASTElement
 {
 	// Name/expression pairs to define labels
-	private ArrayList<String> names;
-	private ArrayList<Expression> labels;
+	protected ArrayList<String> names;
+	protected ArrayList<Expression> labels;
 	// We also store an ExpressionIdent to match each name.
 	// This is to just to provide positional info.
-	private ArrayList<ExpressionIdent> nameIdents;
+	protected ArrayList<ExpressionIdent> nameIdents;
 	
 	// Constructor
-	
+
 	public LabelList()
 	{
 		names = new ArrayList<>();
 		labels = new ArrayList<>();
 		nameIdents = new ArrayList<>();
 	}
-	
+
+	/**
+	 * Checking all labels for cyclic dependencies. <br>
+	 * Note: This method does not take formulas into account. Therefore, to prevent
+	 * cycles completely, it is necessary to expand formulas beforehand.
+	 *
+	 * @throws PrismLangException In case a cyclic dependency was found.
+	 */
+	public void findCycles() throws PrismLangException
+	{
+		boolean[][] matrix = getLabelDependencies();
+		// Check for and report dependencies
+		int firstCycle = PrismUtils.findCycle(matrix);
+		if (firstCycle != -1) {
+			String s = "Cyclic dependency in definition of label \"" + names.get(firstCycle) + "\"";
+			throw new PrismLangException(s, labels.get(firstCycle));
+		}
+	}
+
+	/**
+	 * 	Create a boolean matrix of dependencies between labels.
+	 *
+	 * @return a matrix m such that label i depends on label j iff m[i][j]
+	 * @throws PrismLangException
+	 */
+	public boolean[][] getLabelDependencies() throws PrismLangException
+	{
+		// (matrix[i][j] is true if label i contains label j)
+		int n = size();
+		int j;
+		boolean[][] matrix = new boolean[n][n];
+		for (int i = 0; i < n; i++) {
+			List<String> iLabels = labels.get(i).getAllLabels();
+			for (j = 0; j < n; j++) {
+				if (iLabels.contains(names.get(j))) {
+					// label i contains j
+					matrix[i][j] = true;
+				}
+			}
+		}
+		return matrix;
+	}
+
 	// Set methods
-	
 	public void addLabel(ExpressionIdent n, Expression l)
 	{
 		names.add(n.getName());
 		labels.add(l);
 		nameIdents.add(n);
 	}
-	
+
 	public void setLabelName(int i , ExpressionIdent n)
 	{
 		names.set(i, n.getName());
 		nameIdents.set(i, n);
 	}
-	
+
 	public void setLabel(int i , Expression l)
 	{
 		labels.set(i, l);
 	}
-	
+
 	// Get methods
 
 	public int size()
@@ -84,17 +126,17 @@ public String getLabelName(int i)
 	{
 		return names.get(i);
 	}
-	
+
 	public List<String> getLabelNames()
 	{
 		return names;
 	}
-	
+
 	public Expression getLabel(int i)
 	{
 		return labels.get(i);
 	}
-	
+
 	public ExpressionIdent getLabelNameIdent(int i)
 	{
 		return nameIdents.get(i);
@@ -109,7 +151,7 @@ public int getLabelIndex(String s)
 	}
 
 	// Methods required for ASTElement:
-	
+
 	/**
 	 * Visitor method.
 	 */
@@ -117,7 +159,7 @@ public Object accept(ASTVisitor v) throws PrismLangException
 	{
 		return v.visit(this);
 	}
-	
+
 	/**
 	 * Convert to string.
 	 */
@@ -125,16 +167,16 @@ public String toString()
 	{
 		String s = "";
 		int i, n;
-		
+
 		n = size();
 		for (i = 0; i < n; i++) {
 			s += "label \"" + getLabelName(i);
 			s += "\" = " + getLabel(i) + ";\n";
 		}
-		
+
 		return s;
 	}
-	
+
 	@Override
 	public LabelList deepCopy(DeepCopy copier) throws PrismLangException
 	{
diff --git a/prism/src/parser/ast/ModulesFile.java b/prism/src/parser/ast/ModulesFile.java
index 147cdb538f..3f6944dc90 100644
--- a/prism/src/parser/ast/ModulesFile.java
+++ b/prism/src/parser/ast/ModulesFile.java
@@ -894,6 +894,10 @@ public void tidyUp() throws PrismLangException
 		// Check label identifiers
 		checkLabelIdents();
 
+		// Check labels for cyclic dependencies
+		// should be done after formulas were expanded
+		labelList.findCycles();
+
 		// Check module names
 		checkModuleNames();
 
diff --git a/prism/src/parser/ast/PropertiesFile.java b/prism/src/parser/ast/PropertiesFile.java
index 4cccaecb58..bf9b0184df 100644
--- a/prism/src/parser/ast/PropertiesFile.java
+++ b/prism/src/parser/ast/PropertiesFile.java
@@ -322,6 +322,10 @@ public void tidyUp() throws PrismLangException
 		// Check label identifiers
 		checkLabelIdents();
 
+		// Check label for cyclic dependencies
+		// should be done after formulas were expanded
+		combinedLabelList.findCycles();
+
 		// Check constant identifiers
 		checkConstantIdents();
 		// Find all instances of constants (i.e. locate idents which are constants).
diff --git a/prism/src/prism/ModelGenerator.java b/prism/src/prism/ModelGenerator.java
index 95cd919289..cf378e9452 100644
--- a/prism/src/prism/ModelGenerator.java
+++ b/prism/src/prism/ModelGenerator.java
@@ -29,6 +29,8 @@
 
 import java.util.Collections;
 import java.util.List;
+import java.util.BitSet;
+import java.util.function.Predicate;
 
 import common.Interval;
 import parser.State;
@@ -420,21 +422,6 @@ public default String getTransitionUpdateStringFull(int i, int offset) throws Pr
 	 */
 	public State computeTransitionTarget(int i, int offset) throws PrismException;
 	
-	/**
-	 * Is label {@code label} true in the state currently being explored?
-	 * @param label The name of the label to check 
-	 */
-	public default boolean isLabelTrue(String label) throws PrismException
-	{
-		// Default implementation: Look up label and then check by index
-		int i = getLabelIndex(label);
-		if (i == -1) {
-			throw new PrismException("Label \"" + label + "\" not defined");
-		} else {
-			return isLabelTrue(i);
-		}
-	}
-	
 	/**
 	 * For real-time models, get the clock invariant for the current state,
 	 * i.e., an expression over clock variables which must remain true.
@@ -448,16 +435,31 @@ public default Expression getClockInvariant() throws PrismException
 	}
 	
 	/**
-	 * Is the {@code i}th label of the model true in the state currently being explored?
-	 * @param i The index of the label to check 
+	 * Create a {@link Predicate} of all labels in the current state.
+	 *
+	 * @param state Context state for evaluation.
+	 * @throws PrismLangException If evaluation of a label fails.
 	 */
-	public default boolean isLabelTrue(int i) throws PrismException
+	default Predicate<String> getLabelValues(State state) throws PrismException
 	{
 		// No labels by default
-		throw new PrismException("Label number \"" + i + "\" not defined");
+		throw new PrismException("Labels not defined");
 	}
 	
 	/**
+	 * 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.
diff --git a/prism/src/prism/ModelGenerator2MTBDD.java b/prism/src/prism/ModelGenerator2MTBDD.java
index cc43316ffa..38ba6cb9d5 100644
--- a/prism/src/prism/ModelGenerator2MTBDD.java
+++ b/prism/src/prism/ModelGenerator2MTBDD.java
@@ -28,6 +28,7 @@
 
 import java.util.LinkedList;
 import java.util.Vector;
+import java.util.function.Predicate;
 
 import jdd.JDD;
 import jdd.JDDNode;
@@ -511,9 +512,10 @@ private void buildTransAndRewards() throws PrismException
 				// Print some progress info occasionally
 				// TODO progress.updateIfReady(src + 1);
 			}
-			
+
+			Predicate<String> labelValues = modelGen.getLabelValues(state);
 			for (int l = 0; l < numLabels; l++) {
-				if (modelGen.isLabelTrue(l)) {
+				if (labelValues.test(modelGen.getLabelName(l))) {
 					labelsArray[l] = JDD.Or(labelsArray[l], ddState.copy());
 				}
 			}
diff --git a/prism/src/prism/Modules2MTBDD.java b/prism/src/prism/Modules2MTBDD.java
index 9ecacb8d34..783e8c071d 100644
--- a/prism/src/prism/Modules2MTBDD.java
+++ b/prism/src/prism/Modules2MTBDD.java
@@ -272,7 +272,7 @@ public Model translate() throws PrismException
 			sortRanges();
 			
 			// create stripped-down StateModelChecker for expression to MTBDD conversions
-			expr2mtbdd = new StateModelChecker(prism, varList, allDDRowVars, varDDRowVars, constantValues);
+			expr2mtbdd = new StateModelChecker(prism, varList, modulesFile.getLabelList(), allDDRowVars, varDDRowVars, constantValues);
 			
 			// translate modules file into dd
 			translateModules();
diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java
index 531615a8b3..1f21ed5179 100644
--- a/prism/src/prism/StateModelChecker.java
+++ b/prism/src/prism/StateModelChecker.java
@@ -57,6 +57,9 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 	// Constant values
 	protected Values constantValues;
 
+	// Label list of Modules file
+	protected LabelList modulLabelList;
+
 	// Model info
 	protected Model model;
 	protected VarList varList;
@@ -135,7 +138,7 @@ public StateModelChecker(Prism prism, Model m, PropertiesFile pf) throws PrismEx
 	 * {@code clearDummyModel()} later.
 	 * <br>[ REFS: <i>none</i>, DEREFS: <i>none</i> ]
 	 */
-	public StateModelChecker(Prism prism, VarList varList, JDDVars allDDRowVars, JDDVars[] varDDRowVars, Values constantValues) throws PrismException
+	public StateModelChecker(Prism prism, VarList varList, LabelList modulLabelList, JDDVars allDDRowVars, JDDVars[] varDDRowVars, Values constantValues) throws PrismException
 	{
 		// Initialise PrismComponent
 		super(prism);
@@ -146,6 +149,7 @@ public StateModelChecker(Prism prism, VarList varList, JDDVars allDDRowVars, JDD
 		this.allDDRowVars = allDDRowVars;
 		this.varDDRowVars = varDDRowVars;
 		this.constantValues = constantValues;
+		this.modulLabelList = modulLabelList;
 		// Create dummy model
 		reach = null;
 		model = new ProbModel(JDD.Constant(0),  // trans
@@ -1614,7 +1618,7 @@ public LabelList getLabelList()
 		if (propertiesFile != null) {
 			return propertiesFile.getCombinedLabelList(); // combined list from properties and modules file
 		} else {
-			return null;
+			return modulLabelList; // (if available) labelList of modules file only
 		}
 	}
 
diff --git a/prism/src/prism/TestModelGenerator.java b/prism/src/prism/TestModelGenerator.java
index 3c65f63e00..83cf4285f6 100644
--- a/prism/src/prism/TestModelGenerator.java
+++ b/prism/src/prism/TestModelGenerator.java
@@ -134,16 +134,6 @@ public State computeTransitionTarget(int i, int offset) throws PrismException
 		}
 		return s;
 	}
-	
-	@Override
-	public boolean isLabelTrue(int i) throws PrismException
-	{
-		if (i == 0) {
-			return x == n;
-		} else {
-			throw new PrismException("Label number \"" + i + "\" not defined");
-		}
-	}
 
 	public static void main(String args[])
 	{
diff --git a/prism/src/simulator/LabelEvaluator.java b/prism/src/simulator/LabelEvaluator.java
new file mode 100644
index 0000000000..99b06adfc1
--- /dev/null
+++ b/prism/src/simulator/LabelEvaluator.java
@@ -0,0 +1,192 @@
+package simulator;
+
+
+import parser.State;
+import parser.ast.Expression;
+import parser.ast.LabelList;
+import prism.PrismException;
+import prism.PrismLangException;
+import prism.PrismUtils;
+
+import java.util.BitSet;
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+import java.util.NoSuchElementException;
+import java.util.function.Predicate;
+
+/**
+ * This class will evaluate labels. Therefore, it's wrapped around a {@link LabelList}.
+ * <br>
+ * It also caches the results.
+ */
+public class LabelEvaluator
+{
+	/** Map of each evaluated state and a bitset containing the label-values ordered as in labelList */
+	Map<State, BitSet> stateValues = new HashMap<>();
+	/** The labelList that will be evaluated */
+	LabelList labelList;
+	int[] evaluationOrder;
+
+	/**
+	 * Creates new object that will evaluate and cache the given {@link LabelList}.
+	 */
+	public LabelEvaluator(LabelList labelList) throws PrismLangException
+	{
+		this.labelList = labelList;
+		this.evaluationOrder = fixEvaluationOrder(labelList.getLabelDependencies());
+	}
+
+	/**
+	 * Fix an order on the labels such that l1 < l2 if l2 depends on l1.
+	 *
+	 * @param deps an adjacency matrix with adj[i][j] iff i->j
+	 * @return an int array of the label indices in ascending order
+	 */
+	public int[] fixEvaluationOrder(boolean[][] deps)
+	{
+		assert deps.length == 0 || deps.length == deps[0].length : "dependency matrix must be square";
+		assert PrismUtils.findCycle(deps) == -1 : "label dependencies must not contain a cycle";
+
+		int numLabels = deps.length;
+		BitSet done = new BitSet(numLabels);
+		int[] order = new int[numLabels];
+		for (int l = done.nextClearBit(0), last = -1; l < numLabels; l = done.nextClearBit(l)) {
+			last = traverseDfs(deps, l, order, last, done);
+		}
+		return order;
+	}
+
+	/**
+	 * Do a depth-first search in a graph given by an adjacency matrix starting at a given node.
+	 *
+	 * @param adj   an adjacency matrix with adj[i][j] iff i->j
+	 * @param start a start node
+	 * @param trace an int array to record the trace, will be modified
+	 * @param last  index of last element of the trace
+	 * @param done  a {@link BitSet} of already visited nodes, will be modified
+	 * @return the index of the last element of the extended trace, i.e., of the start node
+	 */
+	private int traverseDfs(boolean[][] adj, int start, int[] trace, int last, BitSet done)
+	{
+		if (!done.get(start)) {
+			boolean[] isSuccessor = adj[start];
+			for (int node = isSuccessor.length - 1; node >= 0; node--) {
+				if (isSuccessor[node]) {
+					last = traverseDfs(adj, node, trace, last, done);
+				}
+			}
+			trace[++last] = start;
+			done.set(start);
+		}
+		return last;
+	}
+
+	/**
+	 * Returns the value of a specific label in a specific state.
+	 *
+	 * @param state The state to evaluate in.
+	 * @param label The label that will be evaluated.
+	 * @return The value of the Label.
+	 * @throws PrismLangException In case a label couldn't be evaluated.
+	 */
+	public boolean getLabelValue(State state, String label) throws PrismLangException
+	{
+		return getStateValues(state).get(labelList.getLabelIndex(label));
+	}
+
+	/**
+	 * This method provides all label values concerning a given state. <br>
+	 * It will evaluate all the Labels if necessary.
+	 *
+	 * @param state The state to evaluate in.
+	 * @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 Predicate<String> getLabelValues(State state) throws PrismLangException
+	{
+		return asPredicate(getStateValues(state));
+	}
+
+	/**
+	 * This method provides all values of a certain label. They will be ordered by the given statesList. <br>
+	 * States will be evaluated if necessary.
+	 *
+	 * @param label      The name of the label.
+	 * @param statesList The states to evaluate against in correct order.
+	 * @return All values of the label.
+	 * @throws PrismException In case a label evaluation fails.
+	 */
+	public BitSet getLabel(String label, List<State> statesList) throws PrismException
+	{
+		int statesNum = statesList.size();
+		int labelIndex = labelList.getLabelIndex(label);
+		BitSet labelValues = new BitSet();
+		for (int i = statesNum - 1; i >= 0; i--) {
+			State state = statesList.get(i);
+			BitSet valuesOfState = getStateValues(state);
+			labelValues.set(i, valuesOfState.get(labelIndex));
+		}
+		return labelValues;
+	}
+
+	/**
+	 * This method provides all label values of a certain state as a {@link BitSet}.
+	 * The labels are indexed in the same order as inside the {@link LabelEvaluator#labelList}.
+	 *
+	 * @param state The state to evaluate in.
+	 * @return Always returns a BitSet with the label values.
+	 * @throws PrismLangException In case a label evaluation fails.
+	 */
+	protected BitSet getStateValues(State state) throws PrismLangException
+	{
+		BitSet values = stateValues.get(state);
+		if (values == null) {
+			values = evaluateState(state);
+			stateValues.put(state, values);
+		}
+		return values;
+	}
+
+	/**
+	 * Evaluates all label with the given state.
+	 *
+	 * @param state The state to evaluate the labels in.
+	 * @return A {@link BitSet} of all label values in this state.
+	 * @throws PrismLangException In case a label evaluation fails.
+	 */
+	private BitSet evaluateState(State state) throws PrismLangException
+	{
+		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);
+			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);
+			}
+		};
+	}
+}
diff --git a/prism/src/simulator/ModulesFileModelGenerator.java b/prism/src/simulator/ModulesFileModelGenerator.java
index 063eafda39..3f5c55967f 100644
--- a/prism/src/simulator/ModulesFileModelGenerator.java
+++ b/prism/src/simulator/ModulesFileModelGenerator.java
@@ -1,7 +1,9 @@
 package simulator;
 
 import java.util.ArrayList;
+import java.util.BitSet;
 import java.util.List;
+import java.util.function.Predicate;
 
 import common.Interval;
 import param.BigRational;
@@ -77,6 +79,8 @@ public class ModulesFileModelGenerator<Value> implements ModelGenerator<Value>,
 	
 	// Global clock invariant (conjunction of per-module invariants)
 	protected Expression invariant;
+	// label value cache
+	protected LabelEvaluator labelsCache;
 	
 	/**
 	 * Build a ModulesFileModelGenerator for a particular PRISM model, represented by a {@link ModulesFile} instance.
@@ -190,7 +194,7 @@ public ModulesFileModelGenerator(ModulesFile modulesFile, Evaluator<Value> eval,
 		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;
@@ -252,6 +256,9 @@ public Object visit(ExpressionConstant e) throws PrismLangException
 		labelList = modulesFile.getLabelList();
 		labelNames = labelList.getLabelNames();
 		
+		// create label-cache
+		labelsCache = new LabelEvaluator(labelList);
+
 		// Create data structures for exploring model
 		if (!modelType.uncertain()) {
 			updater = new Updater<Value>(modulesFile, varList, eval, parent);
@@ -603,12 +610,17 @@ public State computeTransitionTarget(int index, int offset) throws PrismExceptio
 	}
 
 	@Override
-	public boolean isLabelTrue(int i) throws PrismException
+	public Predicate<String> getLabelValues(State state) throws PrismLangException
 	{
-		Expression expr = labelList.getLabel(i);
-		return expr.evaluateBoolean(ec.setState(exploreState));
+		return labelsCache.getLabelValues(state);
 	}
-	
+
+	@Override
+	public BitSet getLabel(String name, List<State> statesList) throws PrismException
+	{
+		return labelsCache.getLabel(name, statesList);
+	}
+
 	@Override
 	public Expression getClockInvariant() throws PrismException
 	{
@@ -756,7 +768,7 @@ private TransitionList<Value> getTransitionListScalars() throws PrismException
 		}
 		// Compute the current transition list, if required
 		if (!transitionListBuilt) {
-			updater.calculateTransitions(exploreState, transitionList);
+			updater.calculateTransitions(exploreState, getLabelValues(exploreState) ,transitionList);
 			transitionListBuilt = true;
 		}
 		return transitionList;
@@ -772,7 +784,7 @@ private TransitionList<Interval<Value>> getTransitionListIntervals() throws Pris
 		}
 		// Compute the current transition list, if required
 		if (!transitionListBuilt) {
-			updaterInt.calculateTransitions(exploreState, transitionListInt);
+			updaterInt.calculateTransitions(exploreState, getLabelValues(exploreState),transitionListInt);
 			transitionListIntBuilt = true;
 		}
 		return transitionListInt;
diff --git a/prism/src/simulator/Updater.java b/prism/src/simulator/Updater.java
index f5ef9ef0b0..be41ad5a4b 100644
--- a/prism/src/simulator/Updater.java
+++ b/prism/src/simulator/Updater.java
@@ -32,6 +32,7 @@
 import java.util.HashSet;
 import java.util.List;
 import java.util.Map;
+import java.util.function.Predicate;
 
 import parser.EvaluateContextState;
 import parser.State;
@@ -165,7 +166,7 @@ public Updater(ModulesFile modulesFile, VarList varList, Evaluator<Value> eval,
 	 * @param state State from which to explore
 	 * @param transitionList TransitionList object in which to store result
 	 */
-	public void calculateTransitions(State state, TransitionList<Value> transitionList) throws PrismException
+	public void calculateTransitions(State state, Predicate<String> labelValues, TransitionList<Value> transitionList) throws PrismException
 	{
 		List<ChoiceListFlexi<Value>> chs;
 		int i, j, k, l, n, count;
@@ -186,7 +187,7 @@ public void calculateTransitions(State state, TransitionList<Value> transitionLi
 		// Calculate the available updates for each module/action
 		// (update information in updateLists, clockGuards, enabledSynchs and enabledModules)
 		for (i = 0; i < numModules; i++) {
-			calculateUpdatesForModule(i, state);
+			calculateUpdatesForModule(i, state, labelValues);
 		}
 		//System.out.println("updateLists: " + updateLists);
 
@@ -284,7 +285,7 @@ public void calculateTransitions(State state, TransitionList<Value> transitionLi
 	 * @param m The module index
 	 * @param state State from which to explore
 	 */
-	protected void calculateUpdatesForModule(int m, State state) throws PrismLangException
+	protected void calculateUpdatesForModule(int m, State state, Predicate<String> labelValues) throws PrismLangException
 	{
 		Module module = modulesFile.getModule(m);
 		int n = module.getNumCommands();
@@ -305,7 +306,7 @@ protected void calculateUpdatesForModule(int m, State state) throws PrismLangExc
 					guardSat = true;
 				}
 			} else {
-				guardSat = command.getGuard().evaluateBoolean(ec.setState(state));
+				guardSat = command.getGuard().evaluateBoolean(ec.setLabelValues(labelValues).setState(state));
 			}
 			// If the command is enabled, update stored info
 			if (guardSat) {
diff --git a/prism/unit-tests/parser/ast/LabelEvaluatorTest.java b/prism/unit-tests/parser/ast/LabelEvaluatorTest.java
new file mode 100644
index 0000000000..2748245cee
--- /dev/null
+++ b/prism/unit-tests/parser/ast/LabelEvaluatorTest.java
@@ -0,0 +1,133 @@
+package parser.ast;
+
+import org.junit.jupiter.api.Test;
+import parser.State;
+import prism.PrismLangException;
+import simulator.LabelEvaluator;
+
+import java.util.Arrays;
+import java.util.List;
+import java.util.function.Predicate;
+import java.util.stream.Collectors;
+
+import static org.junit.jupiter.api.Assertions.assertEquals;
+import static org.junit.jupiter.api.Assertions.assertTrue;
+import static parser.ast.LabelTest.createLabelListWithDependencyChain;
+import static parser.ast.LabelTest.createLabelListWithoutCycle;
+
+public class LabelEvaluatorTest
+{
+	@Test
+	public void testGetLabelValues() throws PrismLangException
+	{
+		/*
+		creating LabelList with
+
+		label "l2" = d<=3;
+		label "l1" = "l2" | d=5;
+
+		and checking for [0..5] of int d
+		 */
+		LabelList ll = createLabelListWithoutCycle();
+		LabelEvaluator labelEvaluator = new LabelEvaluator(ll);
+
+		// loop through all states and check label values
+		for (int i = 0; i <= 5; i++) {
+			// create the new state with 1 variable
+			State state = new State(1);
+			// set d to [0..5]
+			state.setValue(0, i); // index of d is 0
+
+			// expected labelValues
+			boolean l2 = i <= 3;
+			boolean l1 = l2 || i == 5;
+
+			// compare
+			Predicate<String> actualValues = labelEvaluator.getLabelValues(state);
+			assertEquals(l1, actualValues.test("l1"));
+			assertEquals(l2, actualValues.test("l2"));
+		}
+	}
+
+	@Test
+	public void testLabelChainEvaluation() throws PrismLangException
+	{
+		LabelList ll = createLabelListWithDependencyChain();
+		LabelEvaluator labelEvaluator = new LabelEvaluator(ll);
+
+		State state = new State(0);
+		assertTrue(labelEvaluator.getLabelValue(state, "l1"));
+		assertTrue(labelEvaluator.getLabelValue(state, "l2"));
+		assertTrue(labelEvaluator.getLabelValue(state, "l3"));
+	}
+
+	@Test
+	public void testLabelDFS_chain() throws PrismLangException
+	{
+		/*
+		 * label "l0" = "l2"
+		 * label "l2" = "l4"
+		 * label "l4" = "l3"
+		 * label "l3" = "l1"
+		 */
+		boolean[][] dependencies = new boolean[5][5];
+		dependencies[0][2] = true;
+		dependencies[2][4] = true;
+		dependencies[4][3] = true;
+		dependencies[3][1] = true;
+
+		List<Integer> order = getEvaluationOrder(dependencies);
+
+		assertTrue(order.indexOf(2) < order.indexOf(0));
+		assertTrue(order.indexOf(4) < order.indexOf(2));
+		assertTrue(order.indexOf(3) < order.indexOf(4));
+		assertTrue(order.indexOf(1) < order.indexOf(3));
+	}
+
+	@Test
+	public void testLabelDFS_unrelatedLabels() throws PrismLangException
+	{
+		// all false -- no dependencies
+		boolean[][] dependencies = new boolean[5][5];
+
+		List<Integer> order = getEvaluationOrder(dependencies);
+
+		assertEquals(5, order.size());
+	}
+
+	@Test
+	public void testLabelDFS_multipleCorrelationComponents() throws PrismLangException
+	{
+		/*
+		 * label "l0" = "l1" & "l3"
+		 * label "l3" = "l1"
+		 *
+		 * label "l4" = "l2" & "l5"
+		 * label "l2" = "l6"
+		 */
+		boolean[][] dependencies = new boolean[7][7];
+		dependencies[0][1] = dependencies[0][3] = true;
+		dependencies[3][1] = true;
+		dependencies[4][2] = dependencies[4][5] = true;
+		dependencies[2][6] = true;
+
+		List<Integer> order = getEvaluationOrder(dependencies);
+
+		assertTrue(order.indexOf(1) < order.indexOf(0));
+		assertTrue(order.indexOf(3) < order.indexOf(0));
+
+		assertTrue(order.indexOf(1) < order.indexOf(3));
+
+		assertTrue(order.indexOf(2) < order.indexOf(4));
+		assertTrue(order.indexOf(5) < order.indexOf(4));
+
+		assertTrue(order.indexOf(6) < order.indexOf(2));
+	}
+
+	private List<Integer> getEvaluationOrder(boolean[][] deps) throws PrismLangException
+	{
+		LabelEvaluator labelEvaluator = new LabelEvaluator(new LabelList());
+		return Arrays.stream(labelEvaluator.fixEvaluationOrder(deps)).boxed().collect(Collectors.toList());
+	}
+
+}
diff --git a/prism/unit-tests/parser/ast/LabelTest.java b/prism/unit-tests/parser/ast/LabelTest.java
new file mode 100644
index 0000000000..a00785cdb2
--- /dev/null
+++ b/prism/unit-tests/parser/ast/LabelTest.java
@@ -0,0 +1,121 @@
+package parser.ast;
+
+import org.junit.jupiter.api.Test;
+import parser.type.TypeBool;
+import parser.type.TypeInt;
+import prism.PrismLangException;
+
+import static org.junit.jupiter.api.Assertions.assertDoesNotThrow;
+import static org.junit.jupiter.api.Assertions.assertThrows;
+
+public class LabelTest
+{
+	@Test
+	public void testFindCycles_emptyList()
+	{
+		LabelList ll = new LabelList();
+		assertDoesNotThrow(ll::findCycles);
+	}
+
+	@Test
+	public void testFindCycles_1LabelCycle()
+	{
+		LabelList ll = createLabelListWith1LabelCycle();
+		assertThrows(PrismLangException.class, ll::findCycles);
+	}
+
+	@Test
+	public void testFindCycles_2LabelCycle()
+	{
+		LabelList ll = createLabelListWith2LabelCycle();
+		assertThrows(PrismLangException.class, ll::findCycles);
+	}
+
+	@Test
+	public void testFindCycles_noCycle()
+	{
+		LabelList ll = createLabelListWithoutCycle();
+		assertDoesNotThrow(ll::findCycles);
+	}
+
+	/**
+	 * <p>
+	 * Helper method that will create a {@link LabelList} with the following Labels:
+	 * </p>
+	 * <ul>
+	 *   <li>label "l2" = d<=3;</li>
+	 * 	 <li>label "l1" = "l2" | d=5;</li>
+	 * </ul>
+	 * </p>
+	 * Note: d is the only variable (index 0) and has {@link TypeInt}
+	 * <p>
+	 */
+	protected static LabelList createLabelListWithoutCycle()
+	{
+		LabelList ll = new LabelList();
+		ExpressionVar dVar = new ExpressionVar("d", TypeInt.getInstance());
+		dVar.setIndex(0); // index of d is 0
+		ll.addLabel(new ExpressionIdent("l1"), new ExpressionBinaryOp(ExpressionBinaryOp.OR,
+				new ExpressionLabel("l2"), new ExpressionBinaryOp(ExpressionBinaryOp.EQ,
+				dVar, new ExpressionLiteral(TypeInt.getInstance(), 5))));
+		ll.addLabel(new ExpressionIdent("l2"), new ExpressionBinaryOp(ExpressionBinaryOp.LE,
+				dVar, new ExpressionLiteral(TypeInt.getInstance(), 3)));
+		return ll;
+	}
+
+	/**
+	 * <p>
+	 * Helper method that will create a {@link LabelList} with the following Labels:
+	 * </p>
+	 * <ul>
+	 *   <li>label "l1" = "l1";</li>
+	 * </ul>
+	 */
+	protected static LabelList createLabelListWith1LabelCycle()
+	{
+		LabelList ll = new LabelList();
+		ll.addLabel(new ExpressionIdent("l1"), new ExpressionLabel("l1"));
+		return ll;
+	}
+
+	/**
+	 * <p>
+	 * Helper method that will create a {@link LabelList} with the following Labels:
+	 * </p>
+	 * <ul>
+	 *   <li>label "l1" = "l2";</li>
+	 *   <li>label "l2" = "l1" | d=5;</li>
+	 * </ul>
+	 * </p>
+	 * Note: d is the only variable (index 0) and has {@link TypeInt}
+	 * <p>
+	 */
+	protected static LabelList createLabelListWith2LabelCycle()
+	{
+		LabelList ll = new LabelList();
+		ll.addLabel(new ExpressionIdent("l1"), new ExpressionLabel("l2"));
+		ll.addLabel(new ExpressionIdent("l2"), new ExpressionBinaryOp(ExpressionBinaryOp.OR,
+				new ExpressionLabel("l1"), new ExpressionBinaryOp(ExpressionBinaryOp.EQ,
+				new ExpressionVar("d", TypeInt.getInstance()), new ExpressionLiteral(TypeInt.getInstance(), 5))));
+		return ll;
+	}
+
+	/**
+	 * <p>
+	 * Helper method that will create a {@link LabelList} with the following Labels:
+	 * </p>
+	 * <ul>
+	 *   <li>label "l1" = "l2";</li>
+	 *   <li>label "l2" = "l3";</li>
+	 *   <li>label "l3" = true;</li>
+	 * </ul>
+	 */
+	protected static LabelList createLabelListWithDependencyChain()
+	{
+		LabelList ll = new LabelList();
+		ll.addLabel(new ExpressionIdent("l1"), new ExpressionLabel("l2"));
+		ll.addLabel(new ExpressionIdent("l2"), new ExpressionLabel("l3"));
+		ll.addLabel(new ExpressionIdent("l3"), new ExpressionLiteral(TypeBool.getInstance(), true));
+		return ll;
+	}
+}