diff --git a/tlatools/org.lamport.tlatools/src/org/eclipse/xtext/xbase/lib/Pure.java b/tlatools/org.lamport.tlatools/src/org/eclipse/xtext/xbase/lib/Pure.java
new file mode 100644
index 0000000000..48d75fddc0
--- /dev/null
+++ b/tlatools/org.lamport.tlatools/src/org/eclipse/xtext/xbase/lib/Pure.java
@@ -0,0 +1,16 @@
+package org.eclipse.xtext.xbase.lib;
+
+import static java.lang.annotation.ElementType.CONSTRUCTOR;
+import static java.lang.annotation.ElementType.METHOD;
+import static java.lang.annotation.RetentionPolicy.RUNTIME;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.Retention;
+import java.lang.annotation.Target;
+
+@Documented
+@Retention(RUNTIME)
+@Target({ METHOD, CONSTRUCTOR })
+public @interface Pure {
+
+}
diff --git a/tlatools/org.lamport.tlatools/src/org/eclipse/xtext/xbase/lib/util/ToStringBuilder.java b/tlatools/org.lamport.tlatools/src/org/eclipse/xtext/xbase/lib/util/ToStringBuilder.java
new file mode 100644
index 0000000000..07153f21f0
--- /dev/null
+++ b/tlatools/org.lamport.tlatools/src/org/eclipse/xtext/xbase/lib/util/ToStringBuilder.java
@@ -0,0 +1,15 @@
+package org.eclipse.xtext.xbase.lib.util;
+
+public class ToStringBuilder {
+	
+	public ToStringBuilder(Object instance) {
+	}
+	
+	public ToStringBuilder add(Object value) {
+		return this;
+	}
+
+	public ToStringBuilder add(String fieldName, Object value) {
+		return this;
+	}
+}
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/ITool.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/ITool.java
index 7f29635579..c3b32b3f9d 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/tool/ITool.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/tool/ITool.java
@@ -79,6 +79,10 @@ public interface ITool extends TraceApp {
 	
 	boolean getNextStates(final INextStateFunctor functor, final TLCState state);
 
+	IValue eval(SemanticNode expr);
+
+	IValue eval(SemanticNode expr, Context c);
+
 	IValue eval(SemanticNode expr, Context c, TLCState s0);
 
 	IValue eval(SemanticNode expr, Context c, TLCState s0, TLCState s1, int control);
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/DebugTool.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/DebugTool.java
index 444cb58019..d4895a6191 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/DebugTool.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/DebugTool.java
@@ -40,6 +40,7 @@
 import tlc2.tool.INextStateFunctor;
 import tlc2.tool.IStateFunctor;
 import tlc2.tool.TLCState;
+import tlc2.tool.TLCStateFun;
 import tlc2.tool.coverage.CostModel;
 import tlc2.util.Context;
 import tlc2.value.IValue;
@@ -66,15 +67,21 @@ public DebugTool(String mainFile, String configFile, FilenameToStream resolver,
 	}
 
 	// 88888888888888888888888888888888888888888888888888888888888888888888888888 //
+
+	@Override
+	public final IValue eval(SemanticNode expr, Context ctxt) {
+		mode = EvalMode.Const;
+		return this.evalImpl(expr, Context.Empty, TLCState.Empty, TLCState.Empty, EvalControl.Clear,
+				CostModel.DO_NOT_RECORD);
+	}
 	
 	@Override
 	public final IValue eval(SemanticNode expr, Context c, TLCState s0) {
-		mode = EvalMode.Const;
-		return this.evalImpl(expr, c, s0, TLCState.Empty, EvalControl.Clear, CostModel.DO_NOT_RECORD);
+		return this.eval(expr, c, s0, CostModel.DO_NOT_RECORD);
 	}
 
 	@Override
-	public IValue eval(SemanticNode expr, Context c, TLCState s0, CostModel cm) {
+	public final IValue eval(SemanticNode expr, Context c, TLCState s0, CostModel cm) {
 		mode = EvalMode.State;
 		return this.evalImpl(expr, c, s0, TLCState.Empty, EvalControl.Clear, cm);
 	}
@@ -100,13 +107,27 @@ public final Value eval(final SemanticNode expr, final Context c, final TLCState
 	}
 
 	@Override
-	protected Value evalImpl(final SemanticNode expr, final Context c, final TLCState s0, final TLCState s1,
+	protected final Value evalImpl(final SemanticNode expr, final Context c, final TLCState s0, final TLCState s1,
 			final int control, CostModel cm) {
 		if (target == null) {
 			// target is null during instantiation of super, ie. eager evaluation of
 			// operators in SpecProcessor.
 			return super.evalImpl(expr, c, s0, s1, control, cm);
 		}
+		if (EvalControl.isEnabled(control) || EvalControl.isPrimed(control)) {
+			// If EvalControl is set to primed or enabled, TLC is evaluating an ENABLED expr.
+			// TLCStateFun are passed in when enabled is evaluated. However, it is also
+			// possible for enabled to be replaced with primed. At any rate, there is no
+			// point evaluating ENABLED expr.
+			return super.evalImpl(expr, c, s0, s1, control, cm);
+		}
+		if (s0 instanceof TLCStateFun || s1 instanceof TLCStateFun) {
+			// If EvalControl is set to primed or enabled, TLC is evaluating an ENABLED expr.
+			// (see previous if branch).  However, if expr is built from an operator with a
+			// Java module override, control is cleared/reset and the only indicator that
+			// evaluation is in the scope of enabled, is TLCStateFunc.
+			return super.evalImpl(expr, c, s0, s1, control, cm);
+		}
 		if (KINDS.contains(expr.getKind())) {
 			// These nodes don't seem interesting to users. They are leaves and we don't
 			// care to see how TLC figures out that then token 1 evaluates to the IntValue 1.
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Tool.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Tool.java
index b8adfb9001..9a78c4b073 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Tool.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Tool.java
@@ -1426,8 +1426,14 @@ public IValue eval(SemanticNode expr, Context c, TLCState s0) {
 	    return this.eval(expr, c, s0, TLCState.Empty, EvalControl.Clear, CostModel.DO_NOT_RECORD);
 	  }
 
-  public final IValue eval(SemanticNode expr) {
-	    return this.eval(expr, Context.Empty, TLCState.Empty);
+  @Override
+  public IValue eval(SemanticNode expr, Context c) {
+	    return this.eval(expr, c, TLCState.Empty);
+	  }
+
+  @Override
+  public IValue eval(SemanticNode expr) {
+	    return this.eval(expr, Context.Empty);
 	  }
 
   @ExpectInlined
diff --git a/tlatools/org.lamport.tlatools/test-model/EWD840/EWD840.tla b/tlatools/org.lamport.tlatools/test-model/EWD840/EWD840.tla
index be06315c2b..0600b04c14 100644
--- a/tlatools/org.lamport.tlatools/test-model/EWD840/EWD840.tla
+++ b/tlatools/org.lamport.tlatools/test-model/EWD840/EWD840.tla
@@ -65,7 +65,7 @@ vars == <<active, color, tpos, tcolor>>
 
 Fairness == WF_vars(System)
 
-Spec == Init /\ [][Next]_vars (*/\ Fairness*)
+Spec == Init /\ [][Next]_vars /\ Fairness
 
 LInv == [][Next]_vars => WF_vars(System)
 
diff --git a/tlatools/org.lamport.tlatools/test-model/EWD840/MC02.cfg b/tlatools/org.lamport.tlatools/test-model/EWD840/MC02.cfg
index f79895237c..ce2009af36 100644
--- a/tlatools/org.lamport.tlatools/test-model/EWD840/MC02.cfg
+++ b/tlatools/org.lamport.tlatools/test-model/EWD840/MC02.cfg
@@ -8,3 +8,5 @@ CONSTRAINT
 StateConstraint
 ACTION_CONSTRAINT
 ActionConstraint
+PROPERTIES
+Liveness
diff --git a/tlatools/org.lamport.tlatools/test-model/EWD840/MC02.tla b/tlatools/org.lamport.tlatools/test-model/EWD840/MC02.tla
index e889d37750..c02f1d58f4 100644
--- a/tlatools/org.lamport.tlatools/test-model/EWD840/MC02.tla
+++ b/tlatools/org.lamport.tlatools/test-model/EWD840/MC02.tla
@@ -5,7 +5,7 @@ const_143073460396411000 ==
 	2
 
 spec_143073460397412000 ==
-	Spec
+	Spec /\ ENABLED Next /\ ENABLED (SelectSeq([i \in 1..N+1 |-> i - 1], LAMBDA node: node = tpos ) = <<tpos>>)
 
 StateConstraint ==
 	\* For the tests to be interesting, this triggers the evaluation