From 6569e885b64c395dd0cbea1aecabf78262ffc605 Mon Sep 17 00:00:00 2001
From: loki der quaeler <quaeler@gmail.com>
Date: Thu, 13 Feb 2020 11:04:43 -0800
Subject: [PATCH] Improving TLC error message for temporal existential
quantifier in spec - #304
. Upon encountering the usage of a temporal existential quantifier in the specification, a better fail message is displayed:
"TLC does not support temporal existential quantification over state variables."
[Enhancement][Tools]
---
tlatools/src/tlc2/output/EC.java | 1 +
tlatools/src/tlc2/output/MP.java | 12 +++++++++++-
tlatools/src/tlc2/tool/impl/SpecProcessor.java | 4 ++++
3 files changed, 16 insertions(+), 1 deletion(-)
diff --git a/tlatools/src/tlc2/output/EC.java b/tlatools/src/tlc2/output/EC.java
index e0fcaa243..e15213bec 100644
--- a/tlatools/src/tlc2/output/EC.java
+++ b/tlatools/src/tlc2/output/EC.java
@@ -166,6 +166,7 @@ public interface EC
public static final int TLC_MODULE_APPLY_EMPTY_SEQ = 2184;
public static final int TLC_SYMMETRY_SET_TOO_SMALL = 2300;
+ public static final int TLC_SPECIFICATION_FEATURES_TEMPORAL_EXISTS = 2301;
public static final int TLC_STARTING = 2185;
public static final int TLC_FINISHED = 2186;
diff --git a/tlatools/src/tlc2/output/MP.java b/tlatools/src/tlc2/output/MP.java
index c5159f966..83a6fb199 100644
--- a/tlatools/src/tlc2/output/MP.java
+++ b/tlatools/src/tlc2/output/MP.java
@@ -723,6 +723,10 @@ public class MP
case EC.TLC_SYMMETRY_SET_TOO_SMALL:
b.append("The set%1% %2% %3% been defined to be a symmetry set but only contain%4% a single element.");
break;
+
+ case EC.TLC_SPECIFICATION_FEATURES_TEMPORAL_EXISTS:
+ b.append("TLC does not support temporal existential quantification over state variables.");
+ break;
/* ************************************************************************ */
case EC.TLC_MODULE_TLCGET_UNDEFINED:
b.append("TLCGet(%1%) was undefined.");
@@ -1171,7 +1175,13 @@ public class MP
break;
case EC.TLC_CONFIG_MISSING_INIT:
b.append("The configuration file did not specify the initial state predicate." +
- // Following part of error message added by LL on 15 Nov 2012
+ // The below part of the error message was added by LL on 15 Nov 2012
+ //
+ // ldq, 13 Feb 2020: I don't think this is semantically correct; I receive
+ // no errors when defining a specification that references
+ // a formula which is a parameterized INSTANCE. I *do* receive
+ // such an error when that formula is being constrained via
+ // the temporal existential qualifier.
"\nCan also be caused by trying to run TLC on a specification from" +
"\na module imported with a parameterized INSTANCE statement.");
break;
diff --git a/tlatools/src/tlc2/tool/impl/SpecProcessor.java b/tlatools/src/tlc2/tool/impl/SpecProcessor.java
index dfc59ffa1..5249ba9f5 100644
--- a/tlatools/src/tlc2/tool/impl/SpecProcessor.java
+++ b/tlatools/src/tlc2/tool/impl/SpecProcessor.java
@@ -1051,6 +1051,10 @@ public class SpecProcessor implements ValueConstants, ToolGlobals {
}
int opcode = BuiltInOPs.getOpCode(pred1.getOperator().getName());
+ if (opcode == OPCODE_te)
+ {
+ Assert.fail(EC.TLC_SPECIFICATION_FEATURES_TEMPORAL_EXISTS);
+ }
if (opcode == OPCODE_cl || opcode == OPCODE_land)
{
for (int i = 0; i < args.length; i++)
--
GitLab