Closes #490: look up for modules in the directories that are defined in the environment variable TLA_PATH

[konnov]

This PR closes issue #490. The paths defined in the environment variable TLA_PATH are joined with the paths defined in the Java system variable TLA-Library. The latter is having priority over the former.

As it is not clear, how to test this behavior with unit tests, I only did rudimentary testing:

$ pwd
/Users/igor/tmp/tlapath
$ export TLA_PATH=`pwd`/a:`pwd`/b
$ echo $TLA_PATH 
/Users/igor/tmp/tlapath/a:/Users/igor/tmp/tlapath/b
$ cat a/A.tla
--------- MODULE A -----------
EXTENDS Integers
DO_A(x) == x + x
=======================
$ cat b/B.tla                 
--------- MODULE B -----------
EXTENDS A
DO_B(x) == DO_A(x) + 1
=======================
$ cat c/C.tla                                           
---------- MODULE C ---------
EXTENDS B
DO_C(x) == DO_B(4)
=======================
$ cd c
$ java -cp $HOME/tmp/tla2tools.jar tla2sany.SANY C.tla

****** SANY2 Version 2.2 created 08 July 2020

Parsing file /Users/igor/tmp/tlapath/c/C.tla
Parsing file /Users/igor/tmp/tlapath/b/B.tla
Parsing file /Users/igor/tmp/tlapath/a/A.tla
Parsing file /private/var/folders/42/77j16l715bd5k68fffptzgvw0000gn/T/Integers.tla
Parsing file /private/var/folders/42/77j16l715bd5k68fffptzgvw0000gn/T/Naturals.tla
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module A
Semantic processing of module B
Semantic processing of module C

[lemmy]

A few ad-hoc questions/comments:.

What takes precedence (env var or -D property)?

I believe that the changes have to be ported to RCPFilename... for the env var to be supported by the Toolbox

[konnov]

-DTLA-Library has priority over TLA_PATH. I will have a look at RCPFilename.

[konnov]

It looks like RCPNameToFileIStream does not respect -DTLA-Library either. Is that true?

[konnov]

I just googled a bit. Perhaps, environment variables do not fit in the eclipse ideology. They seem to be using URIs everywhere.

[lemmy]

The Toolbox has a preference to configure Toolbox-wide includes, but I personally would like to also have a system-wide include configured (via TLA_PATH) for e.g. the community modules. I supposed we just have to define a meaningful precedence order to not create a footgun.

[lemmy]

Btw. the test suite is executed with ant -f tlatools/org.lamport.tlatools/customBuild.xml test assuming the classes have been compiled.

[konnov]

Right. The problem is not in running the unit tests, but in writing a unit test that would test the new code using the environment variable. I even don't know how to do it JUnit.

[lemmy]

1. Derive a new JUnit test from ModelCheckerTestCase (see other subclasses for examples)
2. New test case checks a spec in test-module that extends a module in TLA_PATH
3. Add a new batchtest or junit block to test target in customBuild.xml to set TLA_PATH

[lemmy]

@konnov I'll be back from vacation tomorrow. How much of a blocker is this for you (I see that you have a workaround in apalache)? If this gets merged, are you going to wait until the next release anyway or will you consume a nightly build?

[konnov]

This is not a blocker for us at all. We will use the workaround until tla2tools gets released.

[lemmy]

This feature will also need proper documentation. I suggest

tlaplus/tlatools/org.lamport.tlatools/src/tlc2/TLC.java

Lines 1335 to 1471 in e434e13

	private void printUsage()
	{
	final List<List<UsageGenerator.Argument>> commandVariants = new ArrayList<>();
	final List<UsageGenerator.Argument> sharedArguments = new ArrayList<>();
	// N.B. alphabetical ordering is not required by the UsageGenerator, but introduced here to more easily
	// find options when reading the code
	sharedArguments.add(new UsageGenerator.Argument("-checkpoint", "minutes",
	"interval between check point; defaults to 30",
	true));
	sharedArguments.add(new UsageGenerator.Argument("-cleanup", "clean up the states directory", true));
	sharedArguments.add(new UsageGenerator.Argument("-config", "file",
	"provide the configuration file; defaults to SPEC.cfg", true));
	sharedArguments.add(new UsageGenerator.Argument("-continue",
	"continue running even when an invariant is violated; default\n"
	+ "behavior is to halt on first violation", true));
	sharedArguments.add(new UsageGenerator.Argument("-coverage", "minutes",
	"interval between the collection of coverage information;\n"
	+ "if not specified, no coverage will be collected", true));
	sharedArguments.add(new UsageGenerator.Argument("-deadlock",
	"if specified DO NOT CHECK FOR DEADLOCK. Setting the flag is\n"
	+ "the same as setting CHECK_DEADLOCK to FALSE in config\n"
	+ "file. When -deadlock is specified, config entry is\n"
	+ "ignored; default behavior is to check for deadlocks",
	true));
	sharedArguments.add(new UsageGenerator.Argument("-difftrace",
	"show only the differences between successive states when\n"
	+ "printing trace information; defaults to printing\n"
	+ "full state descriptions", true));
	sharedArguments.add(new UsageGenerator.Argument("-debug",
	"print various debugging information - not for production use\n",
	true));
	sharedArguments.add(new UsageGenerator.Argument("-dump", "file",
	"dump all states into the specified file; this parameter takes\n"
	+ "optional parameters for dot graph generation. Specifying\n"
	+ "'dot' allows further options, comma delimited, of zero\n"
	+ "or more of 'actionlabels', 'colorize', 'snapshot' to be\n"
	+ "specified before the '.dot'-suffixed filename", true,
	"dot actionlabels,colorize,snapshot"));
	sharedArguments.add(new UsageGenerator.Argument("-fp", "N",
	"use the Nth irreducible polynomial from the list stored\n"
	+ "in the class FP64", true));
	sharedArguments.add(new UsageGenerator.Argument("-fpbits", "num",
	"the number of MSB used by MultiFPSet to create nested\n"
	+ "FPSets; defaults to 1", true));
	sharedArguments.add(new UsageGenerator.Argument("-fpmem", "num",
	"a value in (0.0,1.0) representing the ratio of total\n"
	+ "physical memory to devote to storing the fingerprints\n"
	+ "of found states; defaults to 0.25", true));
	sharedArguments.add(new UsageGenerator.Argument("-generateSpecTE", null,
	"if errors are encountered during model checking, generate\n"
	+ "a SpecTE tla/cfg file pair which encapsulates Init-Next\n"
	+ "definitions to specify the state conditions of the error\n"
	+ "state; this enables 'tool' mode. The generated SpecTE\n"
	+ "will include tool output as well as all non-Standard-\n"
	+ "Modules dependencies embeded in the module. To prevent\n"
	+ "the embedding of dependencies, add the parameter\n"
	+ "'nomonolith' to this declaration", true,
	"nomonolith"));
	sharedArguments.add(new UsageGenerator.Argument("-gzip",
	"control if gzip is applied to value input/output streams;\n"
	+ "defaults to 'off'", true));
	sharedArguments.add(new UsageGenerator.Argument("-h", "display these help instructions", true));
	sharedArguments.add(new UsageGenerator.Argument("-maxSetSize", "num",
	"the size of the largest set which TLC will enumerate; defaults\n"
	+ "to 1000000 (10^6)", true));
	sharedArguments.add(new UsageGenerator.Argument("-metadir", "path",
	"specify the directory in which to store metadata; defaults to\n"
	+ "SPEC-directory/states if not specified", true));
	sharedArguments.add(new UsageGenerator.Argument("-nowarning",
	"disable all warnings; defaults to reporting warnings", true));
	sharedArguments.add(new UsageGenerator.Argument("-recover", "id",
	"recover from the checkpoint with the specified id", true));
	sharedArguments.add(new UsageGenerator.Argument("-terse",
	"do not expand values in Print statements; defaults to\n"
	+ "expanding values", true));
	sharedArguments.add(new UsageGenerator.Argument("-tool",
	"run in 'tool' mode, surrounding output with message codes;\n"
	+ "if '-generateSpecTE' is specified, this is enabled\n"
	+ "automatically", true));
	sharedArguments.add(new UsageGenerator.Argument("-userFile", "file",
	"an absolute path to a file in which to log user output (for\n"
	+ "example, that which is produced by Print)", true));
	sharedArguments.add(new UsageGenerator.Argument("-workers", "num",
	"the number of TLC worker threads; defaults to 1. Use 'auto'\n"
	+ "to automatically select the number of threads based on the\n"
	+ "number of available cores.", true));
	sharedArguments.add(new UsageGenerator.Argument("SPEC", null));
	final List<UsageGenerator.Argument> modelCheckVariant = new ArrayList<>(sharedArguments);
	modelCheckVariant.add(new UsageGenerator.Argument("-dfid", "num",
	"run the model check in depth-first iterative deepening\n"
	+ "starting with an initial depth of 'num'", true));
	modelCheckVariant.add(new UsageGenerator.Argument("-view",
	"apply VIEW (if provided) when printing out states", true));
	commandVariants.add(modelCheckVariant);
	final List<UsageGenerator.Argument> simulateVariant = new ArrayList<>(sharedArguments);
	simulateVariant.add(new UsageGenerator.Argument("-depth", "num",
	"specifies the depth of random simulation; defaults to 100",
	true));
	simulateVariant.add(new UsageGenerator.Argument("-seed", "num",
	"provide the seed for random simulation; defaults to a\n"
	+ "random long pulled from a pseudo-RNG", true));
	simulateVariant.add(new UsageGenerator.Argument("-aril", "num",
	"adjust the seed for random simulation; defaults to 0", true));
	simulateVariant.add(new UsageGenerator.Argument("-simulate", null,
	"run in simulation mode; optional parameters may be specified\n"
	+ "comma delimited: 'num=X' where X is the maximum number of\n"
	+ "total traces to generate and/or 'file=Y' where Y is the\n"
	+ "absolute-pathed prefix for trace file modules to be written\n"
	+ "by the simulation workers; for example Y='/a/b/c/tr' would\n"
	+ "produce, e.g, '/a/b/c/tr_1_15'", false,
	"file=X,num=Y"));
	commandVariants.add(simulateVariant);
	final List<String> tips = new ArrayList<String>();
	tips.add("When using the '-generateSpecTE' you can version the generated specification by doing:\n\t"
	+ "./tla2tools.jar -generateSpecTE MySpec.tla && NAME=\"SpecTE-$(date +%s)\" && sed -e \"s/MODULE"
	+ " SpecTE/MODULE $NAME/g\" SpecTE.tla > $NAME.tla");
	tips.add("If, while checking a SpecTE created via '-generateSpecTE', you get an error message concerning\n"
	+ "CONSTANT declaration and you've previous used 'integers' as model values, rename your\n"
	+ "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"
	+ "duplicate operator definitions, this is likely due to the 'monolith' specification\n"
	+ "creation. Try re-running TLC adding the 'nomonolith' option to the '-generateSpecTE'\n"
	+ "parameter.");
	UsageGenerator.displayUsage(ToolIO.out, "TLC", TLCGlobals.versionOfTLC,
	"provides model checking and simulation of TLA+ specifications",
	Messages.getString("TLCDescription"),
	commandVariants, tips, ' ');
	}

because standalone SANY doesn't have a help page.

[konnov]

@lemmy I have found out that I've created this PR right off the master branch in my fork. Do you know how to retarget it against https://github.com/konnov/tlaplus/tree/igor/tlapath? I would like to advance master in my fork.

[lemmy]

@konnov I would try to cherry-pick the commits related to this PR from your master into your tlapath branch, followed by a reset of master.

[Calvin-L]

This PR has sat idle for a while. I want to chime in and say that I would use this feature if it were merged. (In fact, I already do: I have a bash wrapper for TLC that does exactly what Apalache does to fake support for $TLA_PATH).

It sounds like these are the remaining tasks:

1. Document the environment variable and how it relates to the existing system property
2. Add a unit test to check that the environment variable functions correctly
3. A mystery amount of work to ensure that the toolbox also picks up $TLA_PATH

I am happy to help with some or all of these if we are still interested in getting this merged.

[lemmy]

I'm a bit cautious because everything around reading resources from disk is extremely messy in TLC and in the Toolbox (see RCPFilenameToStream vs. SimpleFilenameToStream.java), and adding support for env vars would just add to the complexity. That said, having the functionality would be convenient, especially if users could add CommunityModules-deps.jar to a system-wide TLA_PATH to globally include it.

[lemmy]

Also, are we sure that TLAPS supports TLA_PATH?

[Calvin-L]

If I had to guess, I would guess TLAPS does not honor TLA_PATH. I believe it has its own logic for locating modules on the filesystem.

[lemmy]

If I had to guess, I would guess TLAPS does not honor TLA_PATH. I believe it has its own logic for locating modules on the filesystem.

You can pass it multiple input paths with tlapm -I /path/to/TLA/modules -I ..., which is at least consistent with TLC in the sense that they both only support parameters and not env vars.