Skip to content
Snippets Groups Projects
Commit 6141aed0 authored by Markus Alexander Kuppe's avatar Markus Alexander Kuppe
Browse files

Supersede tlc2.Generator in favor of tlc2.TLC.

Where the command line for tlc2.Generator was:

tlc2.Generator -n 42 -d 23 -f /path/to/file ...

with tlc2.TLC it is:

tlc2.TLC -simulate num=42,file=/path/to/file -depth 23 ...

[Bug][TLC][Changelog]
parent 372d86b7
Branches
No related tags found
No related merge requests found
// Copyright (c) 2003 Compaq Corporation. All rights reserved.
// Portions Copyright (c) 2003 Microsoft Corporation. All rights reserved.
// Last modified on Mon 30 Apr 2007 at 16:11:13 PST by lamport
// modified on Fri Jun 1 15:26:01 PDT 2001 by yuanyu
package tlc2;
import tlc2.output.EC;
import tlc2.output.MP;
import tlc2.tool.Simulator;
import tlc2.util.RandomGenerator;
import util.ToolIO;
public class Generator {
/*
* This TLA trace generator generates random execution traces:
* srcjava tlc.Generator spec[.tla]
*
* The command line provides the following options:
* o -deadlock: do not check for deadlock.
* Defaults to checking deadlock if not specified
* o -f file: the file storing the traces. Defaults to spec_trace
* o -d num: the max length of the trace. Defaults to 10
* o -config file: the config file. Defaults to spec.cfg
* o -coverage seconds: collect coverage information on the spec,
* print out the information every seconds
* Defaults to no coverage if not specified
* o -n num: the max number of traces. Defaults to 10
* o -s: the seed for random simulation
* Defaults to a random seed if not specified
* o -aril num: Adjust the seed for random simulation
* Defaults to 0 if not specified
*/
public static void main(String[] args) {
System.out.println("TLC trace generator, " + TLCGlobals.versionOfTLC);
String mainFile = null;
String traceFile = null;
boolean deadlock = true;
String configFile = null;
int traceDepth = 10;
int traceNum = 10;
boolean noSeed = true;
long seed = 0;
long aril = 0;
int index = 0;
while (index < args.length) {
if (args[index].equals("-f")) {
index++;
if (index >= args.length) {
printErrorMsg("Error: no argument given for -f option.");
return;
}
traceFile = args[index++];
}
else if (args[index].equals("-deadlock")) {
index++;
deadlock = false;
}
else if (args[index].equals("-d")) {
index++;
if (index >= args.length) {
printErrorMsg("Error: no argument given for -d option.");
return;
}
traceDepth = Integer.parseInt(args[index]);
index++;
}
else if (args[index].equals("-n")) {
index++;
if (index >= args.length) {
printErrorMsg("Error: no argument given for -n option.");
return;
}
traceNum = Integer.parseInt(args[index]);
index++;
}
else if (args[index].equals("-coverage")) {
index++;
if (index < args.length) {
try {
TLCGlobals.coverageInterval = Integer.parseInt(args[index]) * 60 * 1000;
if (TLCGlobals.coverageInterval < 0) {
printErrorMsg("Error: expect a nonnegative integer for -coverage option.");
return;
}
index++;
}
catch (Exception e) {
printErrorMsg("Error: An integer for coverage report interval required." +
" But encountered " + args[index]);
return;
}
}
else {
printErrorMsg("Error: coverage report interval required.");
return;
}
}
else if (args[index].equals("-s")) {
index++;
if (index < args.length) {
seed = Long.parseLong(args[index++]);
noSeed = false;
}
else {
printErrorMsg("Error: seed required.");
return;
}
}
else if (args[index].equals("-aril")) {
index++;
if (index < args.length) {
aril = Long.parseLong(args[index++]);
}
else {
printErrorMsg("Error: aril required.");
return;
}
}
else if (args[index].equals("-config")) {
index++;
if (index < args.length) {
configFile = args[index];
int len = configFile.length();
if (configFile.startsWith(".cfg", len-4)) {
configFile = configFile.substring(0, len-4);
}
index++;
}
else {
printErrorMsg("Error: config file required.");
return;
}
}
else {
if (args[index].charAt(0) == '-') {
printErrorMsg("Error: unrecognized option: " + args[index]);
return;
}
if (mainFile != null) {
printErrorMsg("Error: more than one input files: " + mainFile
+ " and " + args[index]);
return;
}
mainFile = args[index++];
int len = mainFile.length();
if (mainFile.startsWith(".tla", len-4)) {
mainFile = mainFile.substring(0, len-4);
}
}
}
if (mainFile == null) {
printErrorMsg("Error: Missing input TLA+ module.");
return;
}
if (traceFile == null) traceFile = mainFile + "_trace";
if (configFile == null) configFile = mainFile;
// Start generating traces:
try {
RandomGenerator rng = new RandomGenerator();
if (noSeed) {
seed = rng.nextLong();
rng.setSeed(seed);
}
else {
rng.setSeed(seed, aril);
}
ToolIO.out.println("Generating random traces with seed " + seed + ".");
Simulator simulator = new Simulator(mainFile, configFile, traceFile,
deadlock, traceDepth, traceNum,
rng, seed, true, null, /* no spec obj */ null);
simulator.simulate();
}
catch (Exception e) {
// Assert.printStack(e);
MP.printError(EC.GENERAL, "generating traces", e); // LL changed call 7 April 2012
}
//System.exit(0); //SZ: no-op removed
}
// TODO replace
private static void printErrorMsg(String msg) {
MP.printError(EC.WRONG_COMMANDLINE_PARAMS_SIMULATOR, msg);
}
}
......@@ -93,6 +93,7 @@ public class TLC
* The number of traces/behaviors to generate in simulation mode
*/
public static long traceNum = Long.MAX_VALUE;
private String traceFile = null;
private int traceDepth;
private FilenameToStream resolver;
private SpecObj specObj;
......@@ -260,6 +261,26 @@ public class TLC
{
isSimulate = true;
index++;
// Simulation args can be:
// file=/path/to/file,num=4711 or num=4711,file=/path/to/file or num=4711 or
// file=/path/to/file
// "file=..." and "num=..." are only relevant for simulation which is why they
// are args to "-simulate".
if (index + 1 < args.length && (args[index].contains("file=") || args[index].contains("num="))) {
final String[] simArgs = args[index].split(",");
index++; // consume simulate args
for (String arg : simArgs) {
if (arg.startsWith("num=")) {
traceNum = Integer.parseInt(arg.replace("num=", ""));
} else if (arg.startsWith("file=")) {
traceFile = arg.replace("file=", "");
}
}
for (int i = 0; i < simArgs.length; i++) {
}
}
} else if (args[index].equals("-modelcheck"))
{
isSimulate = false;
......@@ -522,7 +543,7 @@ public class TLC
if (index < args.length)
{
try {
// Most problems will only show we TLC eventually tries
// Most problems will only show when TLC eventually tries
// to write to the file.
tlc2.module.TLC.OUTPUT = new BufferedWriter(new FileWriter(new File(args[index++])));
} catch (IOException e) {
......@@ -846,7 +867,7 @@ public class TLC
new String[] { String.valueOf(seed), String.valueOf(TLCGlobals.getNumWorkers()),
TLCGlobals.getNumWorkers() == 1 ? "" : "s", cores, osName, osVersion, osArch, vendor,
version, arch, Long.toString(heapMemory), Long.toString(offHeapMemory) });
Simulator simulator = new Simulator(mainFile, configFile, null, deadlock, traceDepth,
Simulator simulator = new Simulator(mainFile, configFile, traceFile, deadlock, traceDepth,
traceNum, rng, seed, true, resolver, specObj);
TLCGlobals.simulator = simulator;
// The following statement moved to Spec.processSpec by LL on 10 March 2011
......
......@@ -5,6 +5,7 @@ package tlc2.util;
import java.io.IOException;
import java.io.InputStream;
import java.util.Random;
/**
* A 64-bit fingerprint is stored in an instance of the type
......@@ -375,6 +376,21 @@ public class FP64 {
public static long getIrredPoly() { return IrredPoly; }
/**
* Initializes {@link FP64#IrredPoly} with a randomly chosen poly from
* {@link FP64#Polys}.
*/
public static void InitRnd() {
Init(new Random().nextInt(Polys.length));
}
/**
* Initializes {@link FP64#IrredPoly} the first poly in {@link FP64#Polys}.
*/
public static void Init() {
Init(0);
}
// Initialization code
public static void Init(int n) {
Init(Polys[n]);
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment