Skip to content
Permalink
Browse files

Improving TLC error message for temporal existential quantifier in sp…

…ec - #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]
  • Loading branch information
quaeler committed Feb 13, 2020
1 parent 3b254ac commit 6569e885b64c395dd0cbea1aecabf78262ffc605
@@ -166,6 +166,7 @@
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;
@@ -723,6 +723,10 @@ else if (parameters.length == 2) {
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 @@ else if (parameters.length == 2) {
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;
@@ -1051,6 +1051,10 @@ private final void processConfigSpec(ExprNode pred, Context c, List subs)
}

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

0 comments on commit 6569e88

Please sign in to comment.
You can’t perform that action at this time.