Bug: test_tlc.py hangs

[ivan-gavran]

Great project, @danwt !

However, I was not able yet to get it fully working:
While I was setting up the framework and running commands provided in the CONTRIBUTING.md, I noticed that the test test_tlc.py hangs.
(Running poetry run pytest tests/tlc/test_tlc.py -s --log-cli-level=debug.)

I managed to narrow the problem down actual running of the TLC solver (in raw.py).
Specifically, the command that is run in a subprocess is java -cp /Users/ivan/Documents/codebase/modelator-py/large/tlc_2_18.jar tlc2.TLC -cleanup -config HelloWorld.cfg -workers auto HelloWorld.tla.

This command is run in a temp folder.
When adding a breakpoint in that folder and running it on my own, the TLC solver hangs with the following output:

Exception in thread "main" java.lang.NoSuchMethodError: java.util.Optional.isEmpty()Z
	at tlc2.TraceExplorationSpec.generate(TraceExplorationSpec.java:71)
	at tlc2.TLC.process(TLC.java:1244)
	at tlc2.TLC.main(TLC.java:352)

I am adding the relevant TLA+ files:
HelloWorld.tla.txt
HelloWorld.cfg.txt
My java version is 1.8.0_321

[rnbguy]

Weird ! java -cp tla2tools.jar tlc2.TLC -cleanup -config HelloWorld.cfg -workers auto HelloWorld.tla works fine at my side.

Did you try the releases from here - https://github.com/tlaplus/tlaplus/releases
or modelator-py is fetching that by itself?

[ivan-gavran]

Thanks @rnbguy : it seems the problem exists only with the version fetched by modelator-py. Running the same command with the version from my machine goes without problem. Here is one difference: modelator-py fetched the version 2.18, and I have 2.16.

I'll dig deeper to understand the difference between those versions.

[rnbguy]

For me, the latest 2.18 and the latest stable 2.17 worked fine.

The problem with tla2tools releases is that they release new 2.18.x releases overwriting old 2.18 releases! Probably modelator-py is fetching or fetched a buggy 2.18 release.

[ivan-gavran]

I checked with 2.17 and it works fine. Thus, I created a pull request #54 in which I changed the version to 2.17 .

My assumption is that the .jar I had was added by hand. @danwt , is that true or is there at some point in the installation a step which downloads a particular release of TLC?

[danwt]

@ivan-gavran I simply included a version of TLC in the repository using Git large file storage. The purpose of this is to have a version to run tests with. The purpose isn't for users to use the downloaded version as users can specify any absolute path to a jar in all the commands.

[ivan-gavran]

Yes, I did so.
I think it still makes sense to have a default version which works for tests. Shall we proceed with #54?

[danwt]

Yes, please go ahead with any changes as you see fit