Repository: informalsystems/modelator-py (language: python)

Issue:
Bug: test_tlc.py hangs
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](https://github.com/informalsystems/modelator-py/blob/main/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](https://github.com/informalsystems/modelator-py/blob/abd39125aab952f72772874324240b5333407003/modelator_py/tlc/raw.py#L116)).
 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](https://github.com/informalsystems/modelator-py/files/8407471/HelloWorld.tla.txt)
[HelloWorld.cfg.txt](https://github.com/informalsystems/modelator-py/files/8407472/HelloWorld.cfg.txt)
My java version is 1.8.0_321






Discussion / hints:
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?
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.
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.

Fix patch:
diff --git a/large/tlc_2_17.jar b/large/tlc_2_17.jar
new file mode 100644
index 0000000..a44e138
Binary files /dev/null and b/large/tlc_2_17.jar differ
diff --git a/samples/helper.py b/samples/helper.py
index e942b81..04c6fa2 100644
--- a/samples/helper.py
+++ b/samples/helper.py
@@ -5,7 +5,7 @@ def tlc_path():
     # For demo purposes, find the path to TLC in this repo, but you can use
     # a path to your own TLC jar.
     return os.path.abspath(
-        os.path.join(os.path.dirname(__file__), "..", "large/tlc_2_18.jar")
+        os.path.join(os.path.dirname(__file__), "..", "large/tlc_2_17.jar")
     )
 
 


Test patch:
diff --git a/tests/helper.py b/tests/helper.py
index d25eb82..f38763b 100644
--- a/tests/helper.py
+++ b/tests/helper.py
@@ -1,7 +1,7 @@
 import os
 from pathlib import Path
 
-TLC_PATH = "large/tlc_2_18.jar"
+TLC_PATH = "large/tlc_2_17.jar"
 APALACHE_PATH = "large/apa_0_23_0.jar"