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

Monolith and variable output improvements - #393 

. Correcting indenting on subaction variables' pretty print.
. Scrubbing out LOCAL INSTANCE declarations of modules which are being embedded in the monolith (this produced a warning but did not halt checking.)

[Bug][Enhancement][Tools]
parent 0958a599
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
tlatools/src/tlc2/model/MCVariable.java
+ 15
− 1
View file @ 7cde038b
......@@ -27,13 +27,27 @@ public class MCVariable {
public String getSingleLineDisplayName() {
final String s = isTraceExplorerExpression() ? traceExpression : name;
return s.replaceAll("\n", "").replaceAll("\r", "");
return s.replaceAll("\\n", "").replaceAll("\\r", "");
}
public String getValueAsString() {
return valueAsString;
}
public String getValueAsStringReIndentedAs(final String indent) {
final String[] split = valueAsString.split("(\\r\\n|\\r|\\n)");
final StringBuilder sb = new StringBuilder();
for (int i = 0; i < split.length; i++) {
sb.append(indent).append(split[i]);
if (i < (split.length - 1)) {
sb.append("\n");
}
}
return sb.toString();
}
public boolean isTraceExplorerExpression() {
return (traceExpression != null);
}
......
tlatools/src/tlc2/output/SpecTraceExpressionWriter.java
+ 12
− 10
View file @ 7cde038b
......@@ -19,6 +19,7 @@ import util.TLAConstants;
*/
public class SpecTraceExpressionWriter extends AbstractSpecWriter {
private static final String TRACE_EXPRESSION_VARIABLE = "TraceExp";
private static final String TRI_INDENT = TLAConstants.INDENT + TLAConstants.INDENT + TLAConstants.INDENT;
/**
* This will generate three identifiers equal to the initial and next state
......@@ -244,8 +245,7 @@ public class SpecTraceExpressionWriter extends AbstractSpecWriter {
initAndNext.append(var.getName()).append(TLAConstants.EQ).append(TLAConstants.L_PAREN);
initAndNext.append(TLAConstants.CR);
initAndNext.append(TLAConstants.INDENT).append(TLAConstants.INDENT).append(TLAConstants.INDENT);
initAndNext.append(var.getValueAsString()).append(TLAConstants.CR);
initAndNext.append(var.getValueAsStringReIndentedAs(TRI_INDENT)).append(TLAConstants.CR);
initAndNext.append(TLAConstants.INDENT).append(TLAConstants.INDENT);
initAndNext.append(TLAConstants.R_PAREN).append(TLAConstants.CR);
......@@ -259,7 +259,7 @@ public class SpecTraceExpressionWriter extends AbstractSpecWriter {
initAndNext.append(expressionInfo.getVariableName()).append(TLAConstants.EQ);
initAndNext.append(TLAConstants.L_PAREN).append(TLAConstants.CR);
initAndNext.append(TLAConstants.INDENT).append(TLAConstants.INDENT).append(TLAConstants.INDENT);
initAndNext.append(TRI_INDENT);
if (expressionInfo.getLevel() == 2) {
// add "--" if the expression is temporal level
initAndNext.append(TLAConstants.TRACE_NA);
......@@ -397,8 +397,10 @@ public class SpecTraceExpressionWriter extends AbstractSpecWriter {
final MCVariable currentStateVar = currentStateVars[i];
subActionsAndConstraint.append(TLAConstants.INDENT).append(TLAConstants.INDENTED_CONJUNCTIVE);
subActionsAndConstraint.append(currentStateVar.getName()).append(TLAConstants.EQ);
subActionsAndConstraint.append(TLAConstants.L_PAREN).append(currentStateVar.getValueAsString());
subActionsAndConstraint.append(TLAConstants.R_PAREN).append(TLAConstants.CR);
subActionsAndConstraint.append(TLAConstants.L_PAREN).append(TLAConstants.CR);
subActionsAndConstraint.append(currentStateVar.getValueAsStringReIndentedAs(TRI_INDENT + TLAConstants.INDENT));
subActionsAndConstraint.append(TLAConstants.CR);
subActionsAndConstraint.append(TRI_INDENT).append(TLAConstants.R_PAREN).append(TLAConstants.CR);
}
/*
......@@ -427,9 +429,10 @@ public class SpecTraceExpressionWriter extends AbstractSpecWriter {
final MCVariable nextStateVar = nextStateVars[i];
subActionsAndConstraint.append(TLAConstants.INDENT).append(TLAConstants.INDENTED_CONJUNCTIVE);
subActionsAndConstraint.append(nextStateVar.getName()).append(TLAConstants.PRIME);
subActionsAndConstraint.append(TLAConstants.EQ).append(TLAConstants.L_PAREN);
subActionsAndConstraint.append(nextStateVar.getValueAsString()).append(TLAConstants.R_PAREN);
subActionsAndConstraint.append(TLAConstants.EQ).append(TLAConstants.L_PAREN).append(TLAConstants.CR);
subActionsAndConstraint.append(nextStateVar.getValueAsStringReIndentedAs(TRI_INDENT + TLAConstants.INDENT));
subActionsAndConstraint.append(TLAConstants.CR);
subActionsAndConstraint.append(TRI_INDENT).append(TLAConstants.R_PAREN).append(TLAConstants.CR);
}
/*
......@@ -449,10 +452,9 @@ public class SpecTraceExpressionWriter extends AbstractSpecWriter {
subActionsAndConstraint.append(TLAConstants.INDENT).append(TLAConstants.INDENTED_CONJUNCTIVE);
subActionsAndConstraint.append(expressionInfo.getVariableName()).append(TLAConstants.PRIME);
subActionsAndConstraint.append(TLAConstants.EQ).append(TLAConstants.L_PAREN).append(TLAConstants.CR);
subActionsAndConstraint.append(TLAConstants.INDENT).append(TLAConstants.INDENT).append(TLAConstants.INDENT);
subActionsAndConstraint.append(TRI_INDENT);
subActionsAndConstraint.append(expressionInfo.getExpression()).append(TLAConstants.CR);
subActionsAndConstraint.append(TLAConstants.INDENT).append(TLAConstants.INDENT).append(TLAConstants.INDENT);
subActionsAndConstraint.append(TLAConstants.R_PAREN);
subActionsAndConstraint.append(TRI_INDENT).append(TLAConstants.R_PAREN);
if (expressionInfo.getLevel() < 2) {
subActionsAndConstraint.append(TLAConstants.PRIME);
......
tlatools/src/tlc2/output/TLAMonolithCreator.java
+ 43
− 8
View file @ 7cde038b
......@@ -13,6 +13,7 @@ import java.util.ArrayList;
import java.util.HashSet;
import java.util.List;
import java.util.Set;
import java.util.Stack;
import java.util.regex.Matcher;
import java.util.regex.Pattern;
......@@ -23,22 +24,39 @@ import util.TLAConstants;
public class TLAMonolithCreator extends AbstractTLACopier {
private static final String NESTED_MODULE_INDENT = " ";
private static final String LOCAL_INSTANCE_REGEX = "^LOCAL INSTANCE ([^\\s]+)\\s*$";
private static final Pattern LOCAL_INSTANCE_PATTERN = Pattern.compile(LOCAL_INSTANCE_REGEX);
// these are modules which SANY logs that it has parsed
// these are modules which SANY logs that it has parsed, scrubbed of Standard Modules and in reverse order
private final List<File> modulesToEmbed;
private final Set<String> moduleNamesBeingEmbedded;
// 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;
/**
* @param rootSpecName
* @param sourceLocation
* @param extendeds these are modules which SANY logs that it has parsed; we expect to receive this in the order
* which SANY emits it in logging; if that order changes in the future, the monolith
* spec will potentially break due to dependent functions being declared in the
* 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
* @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);
modulesToEmbed = new ArrayList<>();
final Stack<File> embedStack = new Stack<>();
moduleNamesBeingEmbedded = new HashSet<>();
for (final File f : extendeds) {
final String name = f.getName();
final int index = name.toLowerCase().indexOf(TLAConstants.Files.TLA_EXTENSION);
......@@ -55,9 +73,14 @@ public class TLAMonolithCreator extends AbstractTLACopier {
}
if (keep) {
modulesToEmbed.add(f);
embedStack.push(f);
instantiatedModules.remove(moduleName);
moduleNamesBeingEmbedded.add(moduleName);
}
}
modulesToEmbed = new ArrayList<>();
while (!embedStack.isEmpty()) {
modulesToEmbed.add(embedStack.pop());
}
modulesToNest = new ArrayList<>();
......@@ -83,7 +106,9 @@ public class TLAMonolithCreator extends AbstractTLACopier {
inBody = m.find();
if (!vetoLocalInstanceLine(originalLine)) {
writer.write(originalLine + '\n');
}
} else {
if (originalLine.trim().startsWith(TLAConstants.KeyWords.EXTENDS)) {
writer.write(TLAConstants.KeyWords.EXTENDS + " " + String.join(", ", modulesToSpecifyInExtends) + "\n");
......@@ -162,6 +187,7 @@ public class TLAMonolithCreator extends AbstractTLACopier {
break;
}
if (!vetoLocalInstanceLine(line)) {
if (nestedModule) {
monolithWriter.write(NESTED_MODULE_INDENT);
}
......@@ -171,6 +197,15 @@ public class TLAMonolithCreator extends AbstractTLACopier {
}
}
}
}
private boolean vetoLocalInstanceLine(final String line) {
final Matcher m = LOCAL_INSTANCE_PATTERN.matcher(line);
if (m.matches()) {
return moduleNamesBeingEmbedded.contains(m.group(1));
}
return false;
}
public static void main(final String[] args) {
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment