diff --git a/tlatools/src/tlc2/TLC.java b/tlatools/src/tlc2/TLC.java
index 4ebfd8e67de918593df8f2d6e285681d8dc9e69f..d3d9101212320ee4e55a349697b892d4238a372d 100644
--- a/tlatools/src/tlc2/TLC.java
+++ b/tlatools/src/tlc2/TLC.java
@@ -458,7 +458,9 @@ public class TLC {
final TLAMonolithCreator monolithCreator
= new TLAMonolithCreator(TLAConstants.TraceExplore.ERROR_STATES_MODULE_NAME,
mcOutputConsumer.getSourceDirectory(),
- extendedModules, mcParserResults.getAllExtendedModules());
+ extendedModules,
+ mcParserResults.getAllExtendedModules(),
+ mcParserResults.getAllInstantiatedModules());
monolithCreator.copy();
}
diff --git a/tlatools/src/tlc2/input/MCParser.java b/tlatools/src/tlc2/input/MCParser.java
index 518527ea63728901d338165f4a8fb2bbeaa8a216..b4fe53ebe4abaef18a20bbaaae2d5eae438e51be 100644
--- a/tlatools/src/tlc2/input/MCParser.java
+++ b/tlatools/src/tlc2/input/MCParser.java
@@ -8,6 +8,7 @@ import java.util.Comparator;
import java.util.HashSet;
import java.util.List;
+import tla2sany.semantic.InstanceNode;
import tla2sany.semantic.ModuleNode;
import tla2sany.semantic.OpDefNode;
import tla2sany.semantic.SymbolMatcher;
@@ -77,10 +78,26 @@ public class MCParser {
root.getExtendedModuleSet(true).stream().forEach(moduleNode -> allExtendees.add(moduleNode.getName().toString()));
rootModuleName = root.getName().toString();
+
+ final HashSet<String> instantiatedModules = new HashSet<>();
+ collectionInstantiatedModules(root, instantiatedModules, allExtendees);
- return new MCParserResults(rootModuleName, extendees, allExtendees, initNextLocationsToDelete,
- isInitNext, nextOrSpecName, modelConfig);
- }
+ return new MCParserResults(rootModuleName, extendees, allExtendees, instantiatedModules,
+ initNextLocationsToDelete, isInitNext, nextOrSpecName, modelConfig);
+ }
+
+ private static void collectionInstantiatedModules(final ModuleNode node, final HashSet<String> modulesList,
+ final HashSet<String> allExtendees) {
+ final InstanceNode[] instances = node.getInstances();
+ for (final InstanceNode instance : instances) {
+ final ModuleNode instanceModule = instance.getModule();
+ instanceModule.getExtendedModuleSet(true)
+ .stream().forEach(moduleNode -> allExtendees.add(moduleNode.getName().toString()));
+ modulesList.add(instanceModule.getName().toString());
+ collectionInstantiatedModules(instanceModule, modulesList, allExtendees);
+ }
+ }
+
private final ModelConfig configParser;
@@ -195,7 +212,7 @@ public class MCParser {
// we'll have a zero size if the output generated came from a TLC run that did not have the '-tool' flag
parserResults = new MCParserResults(null, ((outputParser != null) ? outputParser.getError() : null),
encounteredMessages, new ArrayList<>(), new HashSet<>(),
- new ArrayList<>(), true, null, configParser);
+ new HashSet<>(), new ArrayList<>(), true, null, configParser);
}
return parserResults;
diff --git a/tlatools/src/tlc2/input/MCParserResults.java b/tlatools/src/tlc2/input/MCParserResults.java
index 2545aab9a7df82f99ecde6bebc05117216247d69..b3f57e89acfc96ddf63dbb780e7c88098551954c 100644
--- a/tlatools/src/tlc2/input/MCParserResults.java
+++ b/tlatools/src/tlc2/input/MCParserResults.java
@@ -15,6 +15,7 @@ public class MCParserResults {
private final List<String> immediateExtendedModules;
private final Set<String> allExtendedModules;
+ private final Set<String> modulesInstantiated;
private final List<Location> initNextLocationsToDelete;
@@ -25,13 +26,15 @@ public class MCParserResults {
private final ModelConfig modelConfig;
MCParserResults(final String rootModuleName, final List<String> immediateExtendeds, final Set<String> allExtendeds,
- final List<Location> initNextLocations, final boolean wasInitNext, final String nextOrSpecName,
- final ModelConfig config) {
+ final Set<String> allInstantiated, final List<Location> initNextLocations,
+ final boolean wasInitNext, final String nextOrSpecName, final ModelConfig config) {
moduleName = rootModuleName;
immediateExtendedModules = immediateExtendeds;
allExtendedModules = allExtendeds;
+ modulesInstantiated = allInstantiated;
+
initNextLocationsToDelete = initNextLocations;
behaviorIsInitNext = wasInitNext;
@@ -43,9 +46,10 @@ public class MCParserResults {
MCParserResults(final String rootModuleName, final MCError mcError, final List<MCOutputMessage> messages,
final List<String> immediateExtendeds, final Set<String> allExtendeds,
- final List<Location> initNextLocations, final boolean wasInitNext, final String nextOrSpecName,
- final ModelConfig config) {
- this(rootModuleName, immediateExtendeds, allExtendeds, initNextLocations, wasInitNext, nextOrSpecName, config);
+ final Set<String> allInstantiated, final List<Location> initNextLocations,
+ final boolean wasInitNext, final String nextOrSpecName, final ModelConfig config) {
+ this(rootModuleName, immediateExtendeds, allExtendeds, allInstantiated, initNextLocations, wasInitNext,
+ nextOrSpecName, config);
error = mcError;
outputMessages = messages;
@@ -94,6 +98,16 @@ public class MCParserResults {
public Set<String> getAllExtendedModules() {
return allExtendedModules;
}
+
+ /**
+ * @return this returns a {@link Set} of all instantiated modules - in other words, all modules, X, found in any
+ * module of the entire module tree that is instantiated in TLA+ code like {@code ... = INSTANCE X}
+ * <b>Note:</b> the is the possibility of a non-null intersection between this set and the set of
+ * extended modules.
+ */
+ public Set<String> getAllInstantiatedModules() {
+ return modulesInstantiated;
+ }
/**
* @return ordered from location first in document to that which is last in document
diff --git a/tlatools/src/tlc2/output/TLAMonolithCreator.java b/tlatools/src/tlc2/output/TLAMonolithCreator.java
index 7ad35876246743f400853aaa2f0a59c42687ba27..cd5f0ea05a6957aed173603cabdd36858906807e 100644
--- a/tlatools/src/tlc2/output/TLAMonolithCreator.java
+++ b/tlatools/src/tlc2/output/TLAMonolithCreator.java
@@ -22,32 +22,48 @@ import tlc2.input.MCParserResults;
import util.TLAConstants;
public class TLAMonolithCreator extends AbstractTLACopier {
+ private static final String NESTED_MODULE_INDENT = " ";
+
+
// these are modules which SANY logs that it has parsed
- private final List<File> extendedModules;
+ private final List<File> modulesToEmbed;
// these are 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
private final Set<String> modulesToSpecifyInExtends;
+ // TODO this is insufficient for nestings beyond one level
+ private final List<File> modulesToNest;
public TLAMonolithCreator(final String rootSpecName, final File sourceLocation, final List<File> extendeds,
- final Set<String> entireExtendsList) {
+ final Set<String> entireExtendsList, final Set<String> allInstantiatedModules) {
super(rootSpecName, ("tmp_" + System.currentTimeMillis() + "_monolith"), sourceLocation);
- extendedModules = new ArrayList<File>();
+ final HashSet<String> instantiatedModules = new HashSet<>(allInstantiatedModules);
+ modulesToEmbed = new ArrayList<>();
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 {
- final String baseName = name.substring(0, index);
+ moduleName = name.substring(0, index);
- keep = !StandardModules.isDefinedInStandardModule(baseName);
+ keep = !StandardModules.isDefinedInStandardModule(moduleName);
}
if (keep) {
- extendedModules.add(f);
+ modulesToEmbed.add(f);
+ instantiatedModules.remove(moduleName);
+ }
+ }
+
+ modulesToNest = new ArrayList<>();
+ for (final String module : instantiatedModules) {
+ if (!StandardModules.isDefinedInStandardModule(module)) {
+ modulesToNest.add(new File(sourceLocation, (module + TLAConstants.Files.TLA_EXTENSION)));
}
}
@@ -72,8 +88,12 @@ public class TLAMonolithCreator extends AbstractTLACopier {
if (originalLine.trim().startsWith(TLAConstants.KeyWords.EXTENDS)) {
writer.write(TLAConstants.KeyWords.EXTENDS + " " + String.join(", ", modulesToSpecifyInExtends) + "\n");
- for (final File f : extendedModules) {
- insertModuleIntoMonolith(f, writer);
+ for (final File f : modulesToNest) {
+ insertModuleIntoMonolith(f, writer, true);
+ }
+
+ for (final File f : modulesToEmbed) {
+ insertModuleIntoMonolith(f, writer, false);
}
final StringBuilder commentLine = new StringBuilder(TLAConstants.CR);
@@ -98,7 +118,9 @@ public class TLAMonolithCreator extends AbstractTLACopier {
Files.move(monolithPath, originalPath, new CopyOption[0]);
}
- private void insertModuleIntoMonolith(final File module, final BufferedWriter monolithWriter) throws IOException {
+ private void insertModuleIntoMonolith(final File module, final BufferedWriter monolithWriter,
+ final boolean nestedModule)
+ throws IOException {
final StringBuilder commentLine = new StringBuilder(TLAConstants.CR);
final String moduleFilename = module.getName();
final int index = moduleFilename.indexOf(TLAConstants.Files.TLA_EXTENSION);
@@ -126,14 +148,23 @@ public class TLAMonolithCreator extends AbstractTLACopier {
final Matcher m = insertingModuleMatcher.matcher(line);
inModuleBody = m.find();
+ if (inModuleBody && nestedModule) {
+ monolithWriter.write(NESTED_MODULE_INDENT + line + '\n');
+ }
} else {
if (!line.trim().startsWith(TLAConstants.KeyWords.EXTENDS)) {
final Matcher m = CLOSING_BODY_PATTERN.matcher(line);
if (m.matches()) {
+ if (nestedModule) {
+ monolithWriter.write(NESTED_MODULE_INDENT + line + '\n');
+ }
break;
}
+ if (nestedModule) {
+ monolithWriter.write(NESTED_MODULE_INDENT);
+ }
monolithWriter.write(line + '\n');
}
}
@@ -188,7 +219,8 @@ public class TLAMonolithCreator extends AbstractTLACopier {
}
final TLAMonolithCreator creator = new TLAMonolithCreator(specName, sourceDirectory, extendeds,
- results.getAllExtendedModules());
+ results.getAllExtendedModules(),
+ results.getAllInstantiatedModules());
creator.copy();
System.out.println("The monolith file is now present at: " + originalTLA.getAbsolutePath());