CLI Trace Explorer, Stage 4 - #393

. The monolith creator now nests modules that are instantiated (via INSTANCE) but not directly imported by other modules in the tree (via EXTENDS)

[Feature][Tools]

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();
 							}
 							

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;
@@ -78,9 +79,25 @@ public class MCParser {
 		
 		rootModuleName = root.getName().toString();
 		
-		return new MCParserResults(rootModuleName, extendees, allExtendees, initNextLocationsToDelete,
-								   isInitNext, nextOrSpecName, modelConfig);
+		final HashSet<String> instantiatedModules = new HashSet<>();
+		collectionInstantiatedModules(root, instantiatedModules, allExtendees);
+
+		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;

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;
@@ -95,6 +99,16 @@ public class MCParserResults {
 		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
 	 */

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());