<NME> MC02.tla
<BEF> ---- MODULE MC02 ----
EXTENDS EWD840, TLC, Sequences

const_143073460396411000 == 
	2

spec_143073460397412000 ==
	Spec

StateConstraint ==
	\* For the tests to be interesting, this triggers the evaluation 
    \* of a Java module override in one of TLC's standard modules that
    \* accesses a variable (the state) and involves EvalControl.
    \* Since we don't care about constraining the state space, this is
    \* a tautology.
    SelectSeq([i \in 1..N+1 |-> i - 1], LAMBDA node: node = tpos ) = <<tpos>>

ActionConstraint ==
    LET foo == SelectSeq([i \in 1..N+1 |-> i - 1], LAMBDA node: node = tpos )
    IN \/ foo = <<tpos>>'
       \/ foo # <<tpos'>>

-----------------------------------------------------------------------------

Stop == TLCGet("distinct") < 38

Alias ==
    [
         active |-> active,
         color |-> color,
         tpos |-> tpos,
         tcolor |-> tpos,
         enbld |-> ENABLED <<InitiateProbe>>_vars
    ]
    
=============================================================================

<MSG> Debugger crashes when checking liveness: Exception
'util.WrongInvocationException: TLCStateFun.deepCopy'

Fix Github issue #
https://github.com/tlaplus/tlaplus/issues/565

[Bug][TLC][Debugger]

<DFF> @@ -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 

{'commit': "diff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/ITool.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/ITool.java\nindex 7f2963557..c3b32b3f9 100644\n--- a/tlatools/org.lamport.tlatools/src/tlc2/tool/ITool.java\n+++ b/tlatools/org.lamport.tlatools/src/tlc2/tool/ITool.java\n@@ -79,6 +79,10 @@ public interface ITool extends TraceApp {\n \t\n \tboolean getNextStates(final INextStateFunctor functor, final TLCState state);\n \n+\tIValue eval(SemanticNode expr);\n+\n+\tIValue eval(SemanticNode expr, Context c);\n+\n \tIValue eval(SemanticNode expr, Context c, TLCState s0);\n \n \tIValue eval(SemanticNode expr, Context c, TLCState s0, TLCState s1, int control);\ndiff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/DebugTool.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/DebugTool.java\nindex 444cb5801..d4895a619 100644\n--- a/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/DebugTool.java\n+++ b/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/DebugTool.java\n@@ -40,6 +40,7 @@ import tlc2.tool.IActionItemList;\n import tlc2.tool.INextStateFunctor;\n import tlc2.tool.IStateFunctor;\n import tlc2.tool.TLCState;\n+import tlc2.tool.TLCStateFun;\n import tlc2.tool.coverage.CostModel;\n import tlc2.util.Context;\n import tlc2.value.IValue;\n@@ -66,15 +67,21 @@ public class DebugTool extends Tool {\n \t}\n \n \t// 88888888888888888888888888888888888888888888888888888888888888888888888888 //\n+\n+\t@Override\n+\tpublic final IValue eval(SemanticNode expr, Context ctxt) {\n+\t\tmode = EvalMode.Const;\n+\t\treturn this.evalImpl(expr, Context.Empty, TLCState.Empty, TLCState.Empty, EvalControl.Clear,\n+\t\t\t\tCostModel.DO_NOT_RECORD);\n+\t}\n \t\n \t@Override\n \tpublic final IValue eval(SemanticNode expr, Context c, TLCState s0) {\n-\t\tmode = EvalMode.Const;\n-\t\treturn this.evalImpl(expr, c, s0, TLCState.Empty, EvalControl.Clear, CostModel.DO_NOT_RECORD);\n+\t\treturn this.eval(expr, c, s0, CostModel.DO_NOT_RECORD);\n \t}\n \n \t@Override\n-\tpublic IValue eval(SemanticNode expr, Context c, TLCState s0, CostModel cm) {\n+\tpublic final IValue eval(SemanticNode expr, Context c, TLCState s0, CostModel cm) {\n \t\tmode = EvalMode.State;\n \t\treturn this.evalImpl(expr, c, s0, TLCState.Empty, EvalControl.Clear, cm);\n \t}\n@@ -100,13 +107,27 @@ public class DebugTool extends Tool {\n \t}\n \n \t@Override\n-\tprotected Value evalImpl(final SemanticNode expr, final Context c, final TLCState s0, final TLCState s1,\n+\tprotected final Value evalImpl(final SemanticNode expr, final Context c, final TLCState s0, final TLCState s1,\n \t\t\tfinal int control, CostModel cm) {\n \t\tif (target == null) {\n \t\t\t// target is null during instantiation of super, ie. eager evaluation of\n \t\t\t// operators in SpecProcessor.\n \t\t\treturn super.evalImpl(expr, c, s0, s1, control, cm);\n \t\t}\n+\t\tif (EvalControl.isEnabled(control) || EvalControl.isPrimed(control)) {\n+\t\t\t// If EvalControl is set to primed or enabled, TLC is evaluating an ENABLED expr.\n+\t\t\t// TLCStateFun are passed in when enabled is evaluated. However, it is also\n+\t\t\t// possible for enabled to be replaced with primed. At any rate, there is no\n+\t\t\t// point evaluating ENABLED expr.\n+\t\t\treturn super.evalImpl(expr, c, s0, s1, control, cm);\n+\t\t}\n+\t\tif (s0 instanceof TLCStateFun || s1 instanceof TLCStateFun) {\n+\t\t\t// If EvalControl is set to primed or enabled, TLC is evaluating an ENABLED expr.\n+\t\t\t// (see previous if branch).  However, if expr is built from an operator with a\n+\t\t\t// Java module override, control is cleared/reset and the only indicator that\n+\t\t\t// evaluation is in the scope of enabled, is TLCStateFunc.\n+\t\t\treturn super.evalImpl(expr, c, s0, s1, control, cm);\n+\t\t}\n \t\tif (KINDS.contains(expr.getKind())) {\n \t\t\t// These nodes don't seem interesting to users. They are leaves and we don't\n \t\t\t// care to see how TLC figures out that then token 1 evaluates to the IntValue 1.\ndiff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Tool.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Tool.java\nindex 916e2de25..f3ad60751 100644\n--- a/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Tool.java\n+++ b/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Tool.java\n@@ -1427,8 +1427,14 @@ public abstract class Tool\n \t    return this.eval(expr, c, s0, TLCState.Empty, EvalControl.Clear, CostModel.DO_NOT_RECORD);\n \t  }\n \n-  public final IValue eval(SemanticNode expr) {\n-\t    return this.eval(expr, Context.Empty, TLCState.Empty);\n+  @Override\n+  public IValue eval(SemanticNode expr, Context c) {\n+\t    return this.eval(expr, c, TLCState.Empty);\n+\t  }\n+\n+  @Override\n+  public IValue eval(SemanticNode expr) {\n+\t    return this.eval(expr, Context.Empty);\n \t  }\n \n   @ExpectInlined\ndiff --git a/tlatools/org.lamport.tlatools/test-model/EWD840/EWD840.tla b/tlatools/org.lamport.tlatools/test-model/EWD840/EWD840.tla\nindex be06315c2..0600b04c1 100644\n--- a/tlatools/org.lamport.tlatools/test-model/EWD840/EWD840.tla\n+++ b/tlatools/org.lamport.tlatools/test-model/EWD840/EWD840.tla\n@@ -65,7 +65,7 @@ vars == <<active, color, tpos, tcolor>>\n \n Fairness == WF_vars(System)\n \n-Spec == Init /\\ [][Next]_vars (*/\\ Fairness*)\n+Spec == Init /\\ [][Next]_vars /\\ Fairness\n \n LInv == [][Next]_vars => WF_vars(System)\n \ndiff --git a/tlatools/org.lamport.tlatools/test-model/EWD840/MC02.cfg b/tlatools/org.lamport.tlatools/test-model/EWD840/MC02.cfg\nindex f79895237..ce2009af3 100644\n--- a/tlatools/org.lamport.tlatools/test-model/EWD840/MC02.cfg\n+++ b/tlatools/org.lamport.tlatools/test-model/EWD840/MC02.cfg\n@@ -8,3 +8,5 @@ CONSTRAINT\n StateConstraint\n ACTION_CONSTRAINT\n ActionConstraint\n+PROPERTIES\n+Liveness\ndiff --git a/tlatools/org.lamport.tlatools/test-model/EWD840/MC02.tla b/tlatools/org.lamport.tlatools/test-model/EWD840/MC02.tla\nindex e889d3775..c02f1d58f 100644\n--- a/tlatools/org.lamport.tlatools/test-model/EWD840/MC02.tla\n+++ b/tlatools/org.lamport.tlatools/test-model/EWD840/MC02.tla\n@@ -5,7 +5,7 @@ const_143073460396411000 ==\n \t2\n \n spec_143073460397412000 ==\n-\tSpec\n+\tSpec /\\ ENABLED Next /\\ ENABLED (SelectSeq([i \\in 1..N+1 |-> i - 1], LAMBDA node: node = tpos ) = <<tpos>>)\n \n StateConstraint ==\n \t\\* For the tests to be interesting, this triggers the evaluation \n", 'commit_subject': "Debugger crashes when checking liveness: Exception 'util.WrongInvocationException: TLCStateFun.deepCopy'", 'repo_name': 'tlaplus/tlaplus', 'committer': {'name': 'Markus Alexander Kuppe', 'email': '82b77c4221e60124667659f5857eb35e1ec57936@lemmster.de', 'time_sec': '1617337228', 'tz_offset': '-420', 'date': {'seconds': '1617337228'}}, 'commit_tree': 'cca8cbb37789b05780fd38272e64fd50fdb1bbf1', 'commit_message': "Debugger crashes when checking liveness: Exception\n'util.WrongInvocationException: TLCStateFun.deepCopy'\n\nFix Github issue #\nhttps://github.com/tlaplus/tlaplus/issues/565\n\n[Bug][TLC][Debugger]\n", 'language_name': 'Shell', 'license': 'mit', 'hunks': '@@ -5,7 +5,7 @@ const_143073460396411000 ==\n \t2\n \n spec_143073460397412000 ==\n-\tSpec\n+\tSpec /\\ ENABLED Next /\\ ENABLED (SelectSeq([i \\in 1..N+1 |-> i - 1], LAMBDA node: node = tpos ) = <<tpos>>)\n \n StateConstraint ==\n \t\\* For the tests to be interesting, this triggers the evaluation \n', 'addition_count': 1, 'deletion_count': 1, 'src_file': 'a/tlatools/org.lamport.tlatools/test-model/EWD840/MC02.tla', 'tgt_file': 'b/tlatools/org.lamport.tlatools/test-model/EWD840/MC02.tla', 'file_extension': '.tla', 'before_file': '---- MODULE MC02 ----\nEXTENDS EWD840, TLC, Sequences\n\nconst_143073460396411000 == \n\t2\n\nspec_143073460397412000 ==\n\tSpec\n\nStateConstraint ==\n\t\\* For the tests to be interesting, this triggers the evaluation \n    \\* of a Java module override in one of TLC\'s standard modules that\n    \\* accesses a variable (the state) and involves EvalControl.\n    \\* Since we don\'t care about constraining the state space, this is\n    \\* a tautology.\n    SelectSeq([i \\in 1..N+1 |-> i - 1], LAMBDA node: node = tpos ) = <<tpos>>\n\nActionConstraint ==\n    LET foo == SelectSeq([i \\in 1..N+1 |-> i - 1], LAMBDA node: node = tpos )\n    IN \\/ foo = <<tpos>>\'\n       \\/ foo # <<tpos\'>>\n\n-----------------------------------------------------------------------------\n\nStop == TLCGet("distinct") < 38\n\nAlias ==\n    [\n         active |-> active,\n         color |-> color,\n         tpos |-> tpos,\n         tcolor |-> tpos,\n         enbld |-> ENABLED <<InitiateProbe>>_vars\n    ]\n    \n=============================================================================\n', 'message': "Debugger crashes when checking liveness: Exception\n'util.WrongInvocationException: TLCStateFun.deepCopy'\n\nFix Github issue #\nhttps://github.com/tlaplus/tlaplus/issues/565\n\n[Bug][TLC][Debugger]\n", 'author_name': 'Markus Alexander Kuppe', 'lang': 'lamport'}