Add dummy classes for xtext @pure and ToStringBuilder to prevent

ClassNotFoundExceptions while debugging.  See
eclipse-lsp4j/lsp4j#494 for context.

[Bug]

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 {
+
+}

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;
+	}
+}

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);

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.

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

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)
 

tlatools/org.lamport.tlatools/test-model/EWD840/MC02.cfg

@@ -8,3 +8,5 @@ CONSTRAINT
 StateConstraint
 ACTION_CONSTRAINT
 ActionConstraint
+PROPERTIES
+Liveness

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