From cee3bfcf0d79669ad58e91e881de8721ae28deb6 Mon Sep 17 00:00:00 2001
From: loki der quaeler <quaeler@gmail.com>
Date: Wed, 26 Feb 2020 10:38:11 -0800
Subject: [PATCH] Problems with SYMMETRY constraint on unions of mixed
cardinality sets - #432
. Allowing cardinality-zero sets.
. Instead of err-ing out model checking for zero and one element symmtery sets, we now only emit a Warning level MP message
. Still pending the addition of a number of unit tests
[Bug][Tools]
---
tlatools/src/tlc2/output/MP.java | 2 +-
tlatools/src/tlc2/tool/impl/Tool.java | 16 ++++++++--------
2 files changed, 9 insertions(+), 9 deletions(-)
diff --git a/tlatools/src/tlc2/output/MP.java b/tlatools/src/tlc2/output/MP.java
index 0f44b383a..bb814d4d6 100644
--- a/tlatools/src/tlc2/output/MP.java
+++ b/tlatools/src/tlc2/output/MP.java
@@ -718,7 +718,7 @@ public class MP
break;
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.");
+ b.append("The set%1% %2% %3% been defined to be a symmetry set but contain%4% less than two elements.");
break;
case EC.TLC_SPECIFICATION_FEATURES_TEMPORAL_QUANTIFIER:
diff --git a/tlatools/src/tlc2/tool/impl/Tool.java b/tlatools/src/tlc2/tool/impl/Tool.java
index f4f8f0376..91e136dcd 100644
--- a/tlatools/src/tlc2/tool/impl/Tool.java
+++ b/tlatools/src/tlc2/tool/impl/Tool.java
@@ -3221,11 +3221,11 @@ public abstract class Tool
// enumerable size() check even if they are single element sets
final StringBuilder cardinalityOneSetList = new StringBuilder();
int offenderCount = 0;
- if (argNodes.length == values.size()) {
- // We have as many values as we have permuted sets => we have all 1-element sets
- // else, we may still have one or more 1-element sets which we will catch below.
+ if (argNodes.length >= values.size()) {
+ // If equal, we have as many values as we have permuted sets => we have all 1-element sets;
+ // if greater than, then we have a heterogenous cardinality of sets, including 0 element sets.
for (final ExprOrOpArgNode node : argNodes) {
- addToOneSizedSymmetrySetList(node, cardinalityOneSetList);
+ addToSubTwoSizedSymmetrySetList(node, cardinalityOneSetList);
offenderCount++;
}
}
@@ -3255,7 +3255,7 @@ public abstract class Tool
}
if (!found) {
- addToOneSizedSymmetrySetList(node, cardinalityOneSetList);
+ addToSubTwoSizedSymmetrySetList(node, cardinalityOneSetList);
offenderCount++;
}
}
@@ -3269,8 +3269,8 @@ public abstract class Tool
final String antiPlurality = (offenderCount > 1) ? "" : "s";
final String toHaveConjugation = (offenderCount > 1) ? "have" : "has";
- Assert.fail(EC.TLC_SYMMETRY_SET_TOO_SMALL,
- new String[] { plurality, cardinalityOneSetList.toString(), toHaveConjugation, antiPlurality });
+ MP.printWarning(EC.TLC_SYMMETRY_SET_TOO_SMALL,
+ new String[] { plurality, cardinalityOneSetList.toString(), toHaveConjugation, antiPlurality });
}
return subgroup;
@@ -3279,7 +3279,7 @@ public abstract class Tool
/**
* Teases the original spec name for the set out of node and appends it to the {@code StringBuilder} instance.
*/
- private void addToOneSizedSymmetrySetList(final ExprOrOpArgNode node, final StringBuilder cardinalityOneSetList) {
+ private void addToSubTwoSizedSymmetrySetList(final ExprOrOpArgNode node, final StringBuilder cardinalityOneSetList) {
final SyntaxTreeNode tn = (SyntaxTreeNode)node.getTreeNode();
final String image = tn.getHumanReadableImage();
final String alias;
--
GitLab