Set a unique java.io.tmpdir for each call to SANY

[shonfeder]

This should provide a workaround for the concurrency bug noted
tlaplus/tlaplus#688, while we wait on an upstream fix.

Note that this only allows concurrent executions of SANY in parallel processes.
AFAICT, the deeper issue noted at
#1114 (comment)
will still prevent concurrent runs of SANY within the same JVM.

---

• Entries added to ./unreleased/ for any new functionality

[codecov-commenter]

Codecov Report

Merging #1959 (b1e13e0) into unstable (2a60f81) will increase coverage by 0.00%.
The diff coverage is 100.00%.

❗ Current head b1e13e0 differs from pull request most recent head 35e7ad2. Consider uploading reports for the commit 35e7ad2 to get more accurate results

@@            Coverage Diff            @@
##           unstable    #1959   +/-   ##
=========================================
  Coverage     77.11%   77.12%           
=========================================
  Files           415      415           
  Lines         12695    12697    +2     
  Branches        570      586   +16     
=========================================
+ Hits           9790     9792    +2     
  Misses         2905     2905           

Impacted Files	Coverage Δ
...ala/at/forsyte/apalache/tla/imp/SanyImporter.scala	82.81% <100.00%> (+0.55%)	⬆️
.../forsyte/apalache/tla/pp/ConstSimplifierBase.scala	96.47% <0.00%> (-1.18%)	⬇️
...a/at/forsyte/apalache/tla/lir/TlaLevelFinder.scala	100.00% <0.00%> (+2.63%)	⬆️

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 2a60f81...35e7ad2. Read the comment docs.

[thpani]

Just want to type this out, to wrap my head around it:

If loading from string sources, this will create $TMPDIR/sanyimpXXX and write the string sources to that directory. Then it sets java.io.tmpdir to $TMPDIR/sanyimpYYY (where YYY != XXX) and calls SANY, which writes its temporary files to the latter directory.

We're not doing the first part if loading directly from files, right?

If this is all accurate, feel free to merge :)

[shonfeder]

That is all accurate! One temp
dir is always created for SANY to use. And one is only created if we need to write strings into files to load from, and the two dots are different.