Skip to content
Snippets Groups Projects
Commit 3894e231 authored by loki der quaeler's avatar loki der quaeler Committed by loki der quaeler
Browse files

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]
parent 12e81733
No related merge requests found
...@@ -136,6 +136,7 @@ public class TLC { ...@@ -136,6 +136,7 @@ public class TLC {
private File specTETLAFile; private File specTETLAFile;
private MCParserResults mcParserResults; private MCParserResults mcParserResults;
private MCOutputPipeConsumer mcOutputConsumer; private MCOutputPipeConsumer mcOutputConsumer;
private boolean avoidMonolithSpecTECreation;
private final AtomicBoolean waitingOnGenerationCompletion; private final AtomicBoolean waitingOnGenerationCompletion;
/** /**
...@@ -162,6 +163,7 @@ public class TLC { ...@@ -162,6 +163,7 @@ public class TLC {
fpSetConfiguration = new FPSetConfiguration(); fpSetConfiguration = new FPSetConfiguration();
avoidMonolithSpecTECreation = false;
waitingOnGenerationCompletion = new AtomicBoolean(false); waitingOnGenerationCompletion = new AtomicBoolean(false);
} }
...@@ -225,6 +227,8 @@ public class TLC { ...@@ -225,6 +227,8 @@ public class TLC {
* encountered during model checking; this will change * encountered during model checking; this will change
* to tool mode regardless of whether '-tool' was * to tool mode regardless of whether '-tool' was
* explicitly specified. * explicitly specified.
* o -nomonolith: if generating a SpecTE, do not generate the monolith
* version
* o -checkpoint num: interval for check pointing (in minutes) * o -checkpoint num: interval for check pointing (in minutes)
* Defaults to 30 * Defaults to 30
* o -fpmem num: a value between 0 and 1, exclusive, representing the ratio * o -fpmem num: a value between 0 and 1, exclusive, representing the ratio
...@@ -410,6 +414,9 @@ public class TLC { ...@@ -410,6 +414,9 @@ public class TLC {
{ {
index++; index++;
TLCGlobals.tool = true; TLCGlobals.tool = true;
} else if (args[index].equals("-nomonolith")) {
index++;
avoidMonolithSpecTECreation = true;
} else if (args[index].equals("-generateSpecTE")) { } else if (args[index].equals("-generateSpecTE")) {
index++; index++;
...@@ -456,13 +463,22 @@ public class TLC { ...@@ -456,13 +463,22 @@ public class TLC {
mcOutFIS.close(); mcOutFIS.close();
tempTLAFIS.close(); tempTLAFIS.close();
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(); final List<File> extendedModules = mcOutputConsumer.getExtendedModuleLocations();
final TLAMonolithCreator monolithCreator monolithCreator
= new TLAMonolithCreator(TLAConstants.TraceExplore.ERROR_STATES_MODULE_NAME, = new TLAMonolithCreator(TLAConstants.TraceExplore.ERROR_STATES_MODULE_NAME,
mcOutputConsumer.getSourceDirectory(), mcOutputConsumer.getSourceDirectory(),
extendedModules, extendedModules,
mcParserResults.getAllExtendedModules(), mcParserResults.getAllExtendedModules(),
mcParserResults.getAllInstantiatedModules()); mcParserResults.getAllInstantiatedModules());
}
monolithCreator.copy(); monolithCreator.copy();
} }
...@@ -1394,6 +1410,12 @@ public class TLC { ...@@ -1394,6 +1410,12 @@ public class TLC {
sharedArguments.add(new UsageGenerator.Argument("-metadir", "path", sharedArguments.add(new UsageGenerator.Argument("-metadir", "path",
"specify the directory in which to store metadata; defaults to\n" "specify the directory in which to store metadata; defaults to\n"
+ "SPEC-directory/states if not specified", true)); + "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", sharedArguments.add(new UsageGenerator.Argument("-nowarning",
"disable all warnings; defaults to reporting warnings", true)); "disable all warnings; defaults to reporting warnings", true));
sharedArguments.add(new UsageGenerator.Argument("-recover", "id", sharedArguments.add(new UsageGenerator.Argument("-recover", "id",
...@@ -1443,9 +1465,7 @@ public class TLC { ...@@ -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."); + "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" 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" + "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" + "creation. Try re-running TLC adding the -nomonolith flag.");
+ "output of your model checking to tlc2.TraceExplorer to have it generate a non-monolithic\n"
+ "specification.");
UsageGenerator.displayUsage(ToolIO.out, "TLC", TLCGlobals.versionOfTLC, UsageGenerator.displayUsage(ToolIO.out, "TLC", TLCGlobals.versionOfTLC,
"provides model checking and simulation of TLA+ specifications", "provides model checking and simulation of TLA+ specifications",
......
...@@ -37,6 +37,17 @@ public class TLAMonolithCreator extends AbstractTLACopier { ...@@ -37,6 +37,17 @@ public class TLAMonolithCreator extends AbstractTLACopier {
// TODO this is insufficient for nestings beyond one level // TODO this is insufficient for nestings beyond one level
private final List<File> modulesToNest; 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 rootSpecName
* @param sourceLocation * @param sourceLocation
...@@ -46,17 +57,22 @@ public class TLAMonolithCreator extends AbstractTLACopier { ...@@ -46,17 +57,22 @@ public class TLAMonolithCreator extends AbstractTLACopier {
* wrong order * wrong order
* @param entireExtendsList the modules which the root ModuleNode or one of its sub-ModuleNodes (or one or their * @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 * 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 * in their spec; this will get the non Standard Modules filtered out of it prior to
* usage in this class * usage in this class since those will get embedded as a dependent module.
* @param allInstantiatedModules * @param allInstantiatedModules
*/ */
public TLAMonolithCreator(final String rootSpecName, final File sourceLocation, final List<File> extendeds, public TLAMonolithCreator(final String rootSpecName, final File sourceLocation, final List<File> extendeds,
final Set<String> entireExtendsList, final Set<String> allInstantiatedModules) { final Set<String> entireExtendsList, final Set<String> allInstantiatedModules) {
super(rootSpecName, ("tmp_" + System.currentTimeMillis() + "_monolith"), sourceLocation); super(rootSpecName, ("tmp_" + System.currentTimeMillis() + "_monolith"), sourceLocation);
final boolean willEmbedDependents = (extendeds != null);
moduleNamesBeingEmbedded = new HashSet<>();
modulesToNest = new ArrayList<>();
modulesToEmbed = new ArrayList<>();
if (willEmbedDependents) {
final HashSet<String> instantiatedModules = new HashSet<>(allInstantiatedModules); final HashSet<String> instantiatedModules = new HashSet<>(allInstantiatedModules);
final Stack<File> embedStack = new Stack<>(); final Stack<File> embedStack = new Stack<>();
moduleNamesBeingEmbedded = new HashSet<>();
for (final File f : extendeds) { for (final File f : extendeds) {
final String name = f.getName(); final String name = f.getName();
final int index = name.toLowerCase().indexOf(TLAConstants.Files.TLA_EXTENSION); final int index = name.toLowerCase().indexOf(TLAConstants.Files.TLA_EXTENSION);
...@@ -78,20 +94,22 @@ public class TLAMonolithCreator extends AbstractTLACopier { ...@@ -78,20 +94,22 @@ public class TLAMonolithCreator extends AbstractTLACopier {
moduleNamesBeingEmbedded.add(moduleName); moduleNamesBeingEmbedded.add(moduleName);
} }
} }
modulesToEmbed = new ArrayList<>();
while (!embedStack.isEmpty()) { while (!embedStack.isEmpty()) {
modulesToEmbed.add(embedStack.pop()); modulesToEmbed.add(embedStack.pop());
} }
modulesToNest = new ArrayList<>();
for (final String module : instantiatedModules) { for (final String module : instantiatedModules) {
if (!StandardModules.isDefinedInStandardModule(module)) { if (!StandardModules.isDefinedInStandardModule(module)) {
modulesToNest.add(new File(sourceLocation, (module + TLAConstants.Files.TLA_EXTENSION))); modulesToNest.add(new File(sourceLocation, (module + TLAConstants.Files.TLA_EXTENSION)));
} }
} }
}
modulesToSpecifyInExtends = new HashSet<>(entireExtendsList); modulesToSpecifyInExtends = new HashSet<>(entireExtendsList);
if (willEmbedDependents) {
StandardModules.filterNonStandardModulesFromSet(modulesToSpecifyInExtends); StandardModules.filterNonStandardModulesFromSet(modulesToSpecifyInExtends);
}
// for TLC things // for TLC things
modulesToSpecifyInExtends.add(TLAConstants.BuiltInModules.TLC); modulesToSpecifyInExtends.add(TLAConstants.BuiltInModules.TLC);
// for _TE things // for _TE things
......
...@@ -6,6 +6,7 @@ import java.util.Collections; ...@@ -6,6 +6,7 @@ import java.util.Collections;
import java.util.Comparator; import java.util.Comparator;
import java.util.HashSet; import java.util.HashSet;
import java.util.List; import java.util.List;
import java.util.Objects;
import java.util.regex.Matcher; import java.util.regex.Matcher;
import java.util.regex.Pattern; import java.util.regex.Pattern;
...@@ -316,5 +317,28 @@ public class UsageGenerator { ...@@ -316,5 +317,28 @@ public class UsageGenerator {
public String getDescription() { public String getDescription() {
return description; 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);
}
} }
} }
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment