From 3894e23144ab17efd285337cb6cabb30f9a1a3c0 Mon Sep 17 00:00:00 2001
From: loki der quaeler <quaeler@gmail.com>
Date: Tue, 18 Feb 2020 11:00:04 -0800
Subject: [PATCH] No-monolith option in TLC - #393
. Now providing an option to not include the module TLA+ code of all dependent modules in the generated SpecTE.tla file (-nomonolith)
[Enhancement][Tools]
---
tlatools/src/tlc2/TLC.java | 30 +++++--
.../src/tlc2/output/TLAMonolithCreator.java | 82 +++++++++++--------
tlatools/src/util/UsageGenerator.java | 24 ++++++
3 files changed, 99 insertions(+), 37 deletions(-)
diff --git a/tlatools/src/tlc2/TLC.java b/tlatools/src/tlc2/TLC.java
index 9a283bbfb..85257a293 100644
--- a/tlatools/src/tlc2/TLC.java
+++ b/tlatools/src/tlc2/TLC.java
@@ -136,6 +136,7 @@ public class TLC {
private File specTETLAFile;
private MCParserResults mcParserResults;
private MCOutputPipeConsumer mcOutputConsumer;
+ private boolean avoidMonolithSpecTECreation;
private final AtomicBoolean waitingOnGenerationCompletion;
/**
@@ -162,6 +163,7 @@ public class TLC {
fpSetConfiguration = new FPSetConfiguration();
+ avoidMonolithSpecTECreation = false;
waitingOnGenerationCompletion = new AtomicBoolean(false);
}
@@ -225,6 +227,8 @@ public class TLC {
* encountered during model checking; this will change
* to tool mode regardless of whether '-tool' was
* explicitly specified.
+ * o -nomonolith: if generating a SpecTE, do not generate the monolith
+ * version
* o -checkpoint num: interval for check pointing (in minutes)
* Defaults to 30
* o -fpmem num: a value between 0 and 1, exclusive, representing the ratio
@@ -410,6 +414,9 @@ public class TLC {
{
index++;
TLCGlobals.tool = true;
+ } else if (args[index].equals("-nomonolith")) {
+ index++;
+ avoidMonolithSpecTECreation = true;
} else if (args[index].equals("-generateSpecTE")) {
index++;
@@ -456,13 +463,22 @@ public class TLC {
mcOutFIS.close();
tempTLAFIS.close();
- final List<File> extendedModules = mcOutputConsumer.getExtendedModuleLocations();
- final TLAMonolithCreator monolithCreator
+ final TLAMonolithCreator monolithCreator;
+ if (avoidMonolithSpecTECreation) {
+ monolithCreator
+ = new TLAMonolithCreator(TLAConstants.TraceExplore.ERROR_STATES_MODULE_NAME,
+ mcOutputConsumer.getSourceDirectory(),
+ mcParserResults.getAllExtendedModules());
+ } else {
+ final List<File> extendedModules = mcOutputConsumer.getExtendedModuleLocations();
+ monolithCreator
= new TLAMonolithCreator(TLAConstants.TraceExplore.ERROR_STATES_MODULE_NAME,
mcOutputConsumer.getSourceDirectory(),
extendedModules,
mcParserResults.getAllExtendedModules(),
mcParserResults.getAllInstantiatedModules());
+ }
+
monolithCreator.copy();
}
@@ -1394,6 +1410,12 @@ public class TLC {
sharedArguments.add(new UsageGenerator.Argument("-metadir", "path",
"specify the directory in which to store metadata; defaults to\n"
+ "SPEC-directory/states if not specified", true));
+ sharedArguments.add(new UsageGenerator.Argument("-nomonolith",
+ "if -generateSpecTE was specified and a SpecTE is created due\n"
+ + "to errors encountered, this flag specifies not to create a\n"
+ + "monolithic SpecTE that embeds all non-Standard-Module\n"
+ + "dependent TLA modules - rather, include them via a\n"
+ + "complete EXTENDS list", true));
sharedArguments.add(new UsageGenerator.Argument("-nowarning",
"disable all warnings; defaults to reporting warnings", true));
sharedArguments.add(new UsageGenerator.Argument("-recover", "id",
@@ -1443,9 +1465,7 @@ public class TLC {
+ "model values to start with a non-numeral and rerun the model check to generate a new SpecTE.");
tips.add("If, while checking a SpecTE created via '-generateSpecTE', you get a warning concerning\n"
+ "duplicate operator definitions, this is likely due to the 'monolith' specification\n"
- + "creation. Until a 'disable monolith creation' flag is added to TLC, provide the tool\n"
- + "output of your model checking to tlc2.TraceExplorer to have it generate a non-monolithic\n"
- + "specification.");
+ + "creation. Try re-running TLC adding the -nomonolith flag.");
UsageGenerator.displayUsage(ToolIO.out, "TLC", TLCGlobals.versionOfTLC,
"provides model checking and simulation of TLA+ specifications",
diff --git a/tlatools/src/tlc2/output/TLAMonolithCreator.java b/tlatools/src/tlc2/output/TLAMonolithCreator.java
index b46f5407a..3ce15e66a 100644
--- a/tlatools/src/tlc2/output/TLAMonolithCreator.java
+++ b/tlatools/src/tlc2/output/TLAMonolithCreator.java
@@ -37,6 +37,17 @@ public class TLAMonolithCreator extends AbstractTLACopier {
// TODO this is insufficient for nestings beyond one level
private final List<File> modulesToNest;
+ /**
+ * This is the constructor for the version which embeds no dependent modules.
+ *
+ * @param entireExtendsList the modules which the root ModuleNode or one of its sub-ModuleNodes (or one or their
+ * sub-ModuleNodes and so on, turtles all the way down) has defined as EXTENDS-ing
+ * in their spec.
+ */
+ public TLAMonolithCreator(final String rootSpecName, final File sourceLocation, final Set<String> entireExtendsList) {
+ this(rootSpecName, sourceLocation, null, entireExtendsList, null);
+ }
+
/**
* @param rootSpecName
* @param sourceLocation
@@ -46,52 +57,59 @@ public class TLAMonolithCreator extends AbstractTLACopier {
* wrong order
* @param entireExtendsList the modules which the root ModuleNode or one of its sub-ModuleNodes (or one or their
* sub-ModuleNodes and so on, turtles all the way down) has defined as EXTENDS-ing
- * in their spec; this will get the Standard Modules filtered out of it prior to
- * usage in this class
+ * in their spec; this will get the non Standard Modules filtered out of it prior to
+ * usage in this class since those will get embedded as a dependent module.
* @param allInstantiatedModules
*/
public TLAMonolithCreator(final String rootSpecName, final File sourceLocation, final List<File> extendeds,
final Set<String> entireExtendsList, final Set<String> allInstantiatedModules) {
super(rootSpecName, ("tmp_" + System.currentTimeMillis() + "_monolith"), sourceLocation);
- final HashSet<String> instantiatedModules = new HashSet<>(allInstantiatedModules);
- final Stack<File> embedStack = new Stack<>();
+ final boolean willEmbedDependents = (extendeds != null);
+
moduleNamesBeingEmbedded = new HashSet<>();
- for (final File f : extendeds) {
- final String name = f.getName();
- final int index = name.toLowerCase().indexOf(TLAConstants.Files.TLA_EXTENSION);
- final boolean keep;
- final String moduleName;
- if (index == -1) {
- // this should never be the case
- keep = true;
- moduleName = name;
- } else {
- moduleName = name.substring(0, index);
-
- keep = !StandardModules.isDefinedInStandardModule(moduleName);
+ modulesToNest = new ArrayList<>();
+ modulesToEmbed = new ArrayList<>();
+ if (willEmbedDependents) {
+ final HashSet<String> instantiatedModules = new HashSet<>(allInstantiatedModules);
+ final Stack<File> embedStack = new Stack<>();
+ for (final File f : extendeds) {
+ final String name = f.getName();
+ final int index = name.toLowerCase().indexOf(TLAConstants.Files.TLA_EXTENSION);
+ final boolean keep;
+ final String moduleName;
+ if (index == -1) {
+ // this should never be the case
+ keep = true;
+ moduleName = name;
+ } else {
+ moduleName = name.substring(0, index);
+
+ keep = !StandardModules.isDefinedInStandardModule(moduleName);
+ }
+
+ if (keep) {
+ embedStack.push(f);
+ instantiatedModules.remove(moduleName);
+ moduleNamesBeingEmbedded.add(moduleName);
+ }
}
- if (keep) {
- embedStack.push(f);
- instantiatedModules.remove(moduleName);
- moduleNamesBeingEmbedded.add(moduleName);
+ while (!embedStack.isEmpty()) {
+ modulesToEmbed.add(embedStack.pop());
}
- }
- modulesToEmbed = new ArrayList<>();
- while (!embedStack.isEmpty()) {
- modulesToEmbed.add(embedStack.pop());
- }
-
- modulesToNest = new ArrayList<>();
- for (final String module : instantiatedModules) {
- if (!StandardModules.isDefinedInStandardModule(module)) {
- modulesToNest.add(new File(sourceLocation, (module + TLAConstants.Files.TLA_EXTENSION)));
+
+ for (final String module : instantiatedModules) {
+ if (!StandardModules.isDefinedInStandardModule(module)) {
+ modulesToNest.add(new File(sourceLocation, (module + TLAConstants.Files.TLA_EXTENSION)));
+ }
}
}
modulesToSpecifyInExtends = new HashSet<>(entireExtendsList);
- StandardModules.filterNonStandardModulesFromSet(modulesToSpecifyInExtends);
+ if (willEmbedDependents) {
+ StandardModules.filterNonStandardModulesFromSet(modulesToSpecifyInExtends);
+ }
// for TLC things
modulesToSpecifyInExtends.add(TLAConstants.BuiltInModules.TLC);
// for _TE things
diff --git a/tlatools/src/util/UsageGenerator.java b/tlatools/src/util/UsageGenerator.java
index cdc01d1af..aa4114dc0 100644
--- a/tlatools/src/util/UsageGenerator.java
+++ b/tlatools/src/util/UsageGenerator.java
@@ -6,6 +6,7 @@ import java.util.Collections;
import java.util.Comparator;
import java.util.HashSet;
import java.util.List;
+import java.util.Objects;
import java.util.regex.Matcher;
import java.util.regex.Pattern;
@@ -316,5 +317,28 @@ public class UsageGenerator {
public String getDescription() {
return description;
}
+
+ @Override
+ public int hashCode() {
+ return Objects.hash(argumentName);
+ }
+
+ @Override
+ public boolean equals(Object obj) {
+ if (this == obj) {
+ return true;
+ }
+
+ if (obj == null) {
+ return false;
+ }
+
+ if (getClass() != obj.getClass()) {
+ return false;
+ }
+
+ final Argument other = (Argument) obj;
+ return Objects.equals(argumentName, other.argumentName);
+ }
}
}
--
GitLab