Skip to content
Permalink
Browse files

CLI Trace Explorer, Stage 4 - #393

. Providing a REPL-bis command line functionality ala the Jupyter notebook example.

[Feature][Tools]
  • Loading branch information
quaeler committed Jan 14, 2020
1 parent b62ee8d commit 171727696ec7bd6446e636e0bf119ba3a424c63e
Showing with 241 additions and 49 deletions.
  1. +89 −0 tlatools/src/tlc2/REPLSpecWriter.java
  2. +40 −4 tlatools/src/tlc2/TLCRunner.java
  3. +112 −45 tlatools/src/tlc2/TraceExplorer.java
@@ -0,0 +1,89 @@
package tlc2;

import java.io.ByteArrayOutputStream;
import java.util.List;

import tlc2.output.AbstractSpecWriter;
import tlc2.output.SpecWriterUtilities;

class REPLSpecWriter extends AbstractSpecWriter {
private static final String EXPRESSION_OPEN = "\"EXPR_TLATE_BEGIN\"";
private static final String EXPRESSION_CLOSE = "\"EXPR_TLATE_END\"";
private static final String ASSUME_PREFIX = "ASSUME PrintT(" + EXPRESSION_OPEN + ") /\\ PrintT(\n";
private static final String ASSUME_SUFFIX = "\n) /\\ PrintT(" + EXPRESSION_CLOSE + ")\n";

REPLSpecWriter(final String specName, final List<String> expressions) {
super(true);

tlaBuffer.append(SpecWriterUtilities.getExtendingModuleContent(specName,
"Naturals", "Reals", "Sequences", "Bags",
"FiniteSets", "TLC"));
tlaBuffer.append(ASSUME_PREFIX);
tlaBuffer.append(String.join("\n", expressions));
tlaBuffer.append(ASSUME_SUFFIX);
}


static class REPLLogConsumerStream extends ByteArrayOutputStream {
private boolean inResponse;
private boolean haveCollected;
private StringBuilder currentLine;

private String collectedContent;

REPLLogConsumerStream() {
inResponse = false;
haveCollected = false;
currentLine = new StringBuilder();
}

String getCollectedContent() {
return collectedContent;
}

// Being wrapped in a Buffer invokes this method, we sub-optimally pass it off to our real digestion below
@Override
public void write(final byte b[], final int off, final int len) {
for (int i = off; i < (off + len); i++) {
write(b[i]);
}
}

@Override
public void write(final int b) {
if (haveCollected) {
return;
} else if (inResponse) {
if (b == '\n') {
if (EXPRESSION_CLOSE.equals(currentLine.toString())) {
haveCollected = true;

final String allCollectedContent = toString();
final int length = allCollectedContent.length();
collectedContent = allCollectedContent.substring(0, (length - (EXPRESSION_CLOSE.length() + 1)));
} else {
super.write(b);
}

currentLine = new StringBuilder();
} else {
super.write(b);

// casting to char is probably not the best thing - suffices for the majority of the presumed cases
currentLine.append((char)b);
}
} else {
if (b == '\n') {
if (EXPRESSION_OPEN.equals(currentLine.toString())) {
inResponse = true;
}

currentLine = new StringBuilder();
} else {
// casting to char is probably not the best thing - suffices for the majority of the presumed cases
currentLine.append((char)b);
}
}
}
}
}
@@ -43,11 +43,32 @@


private final File outputLogfile;
private final OutputStream outputOutputStream;
private final List<String> arguments;

private boolean silenceStdOut;

TLCRunner(final List<String> tlcArguments, final File logfileDestination) {
outputLogfile = logfileDestination;
outputOutputStream = null;
arguments = tlcArguments;

silenceStdOut = false;
}

TLCRunner(final List<String> tlcArguments, final OutputStream logfileOutputStream) {
outputLogfile = null;
outputOutputStream = logfileOutputStream;
arguments = tlcArguments;

silenceStdOut = false;
}

/**
* @param flag if true, no output from the TLC process will be sent to System.out
*/
void setSilenceStdOut(final boolean flag) {
silenceStdOut = flag;
}

/**
@@ -60,9 +81,24 @@ int run() throws IOException {
final Process p = processBuilder.start();
final BufferedInputStream stdOutReader = new BufferedInputStream(p.getInputStream());
final BufferedInputStream stdErrReader = new BufferedInputStream(p.getErrorStream());
final FileOutputStream fos = new FileOutputStream(outputLogfile);
final TeeOutputStream tos = new TeeOutputStream(System.out, new BufferedOutputStream(fos));
final StreamPump stdOutPump = new StreamPump(stdOutReader, tos);
final BufferedOutputStream logfileOutputStream;
if (outputOutputStream != null) {
if (outputOutputStream instanceof BufferedOutputStream) {
logfileOutputStream = (BufferedOutputStream)outputOutputStream;
} else {
logfileOutputStream = new BufferedOutputStream(outputOutputStream);
}
} else {
final FileOutputStream fos = new FileOutputStream(outputLogfile);
logfileOutputStream = new BufferedOutputStream(fos);
}
final OutputStream stdOutPumpOutput;
if (silenceStdOut) {
stdOutPumpOutput = logfileOutputStream;
} else {
stdOutPumpOutput = new TeeOutputStream(System.out, logfileOutputStream);
}
final StreamPump stdOutPump = new StreamPump(stdOutReader, stdOutPumpOutput);
final StreamPump stdErrPump = new StreamPump(stdErrReader, null);

try {
@@ -80,7 +116,7 @@ int run() throws IOException {
stdErrPump.stop();

try {
fos.close();
logfileOutputStream.close();
} catch (final Exception e) { }
}

0 comments on commit 1717276

Please sign in to comment.
You can’t perform that action at this time.