Race conditions in parallel Apalache runtimes

[rnbguy]

While running our integration tests in parallel, we noticed (#111 (comment)) some unexpected behaviors from Apalache.

This has been confirmed by Apalache team.

This is due to SANY - tlaplus/tlaplus#688.

$ cat run-sany.sh 
#!/bin/sh
java -cp tla2tools.jar tla2sany.SANY T.tla
$ seq 1 10 | parallel ./run-sany.sh
****** SANY2 Version 2.1 created 24 February 2014

Parsing file /Users/igor/Downloads/T.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 T

****** SANY2 Version 2.1 created 24 February 2014

Parsing file /Users/igor/Downloads/T.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 T
Encountered an exception while attempt to validate /var/folders/42/77j16l715bd5k68fffptzgvw0000gn/T/Naturals.tla - /var/folders/42/77j16l715bd5k68fffptzgvw0000gn/T/Naturals.tla (No such file or directory)