Add RPC for loading a model

[shonfeder]

Work on this will involve adding the RPC calls for these the following methods, specified in RFC10

  def loadModel(spec: String, aux: List[String] = List()): Either[LoadErr, UninitializedModel]

It will include:

• Defining the data types
• Adding the proto specs for the RPC call
• Calling from the server module into specification loading code
• Adding unit and integration tests

[thpani]

As discussed in MondApalache, looks like this is blocked by #1761

[shonfeder]

I think I should be able to work around for the moment, either by making the tests run in sequence, or manipulating the temp dir system attribute.

[shonfeder]

So, after adding a workaround for the race condition of the temp dir, I think I've found the actual problem, which is a deeper issue. Not yet sure if there will be workarounds or if we'll need to submit a fix upstream.

The failure I am seeing from Shai when trying parse two specs concurrently is seems to be related to a detail of the JavaCC parser generator (used by Sany). Here's the error:

ERROR: Second call to constructor of static parser.  You must
       either use ReInit() or set the JavaCC option STATIC to false
       during parser generation.

And the documentation on this in the JavaCC docs:

STATIC: If true, all methods and class variables are specified as static in the generated parser and token manager. This allows only one parser object to be present, but it improves the performance of the parser. To perform multiple parses during one run of your Java program, you will have to call the ReInit() method to reinitialize your parser if it is static. If the parser is non-static, you may use the new operator to construct as many parsers as you wish. These can all be used simultaneously from different threads.

[shonfeder]

Looks like the SANY object provides a method to take care of this, so the fix should be simple here :)

[shonfeder]

Oh, and in fact that method is getting called at the start of every invocation of the method we are invoking, so I'm back to confusion about the problem here and how to fix it, lol.

So we call

https://github.com/informalsystems/apalache/blob/2a60f813b264ef8e21f80b0c78afa5adad7721b9/tla-io/src/main/scala/at/forsyte/apalache/tla/imp/SanyImporter.scala#L72-L76

and that calls a function meant to set up the global environment on each call:

https://github.com/tlaplus/tlaplus/blob/421bc3d16f869d9c9bb493e5950c445c25c916ea/tlatools/org.lamport.tlatools/src/tla2sany/drivers/SANY.java#L121-L127

So maybe the problem I'm hitting, as @thpani pointed out, that one parse invocation is being called before another has finished.... but I think I'm sequencing the calls.

Will continue investigating.

[shonfeder]

Ok, so of course we can run the parses in sequence, because we run them in the same VM in our tests (:facepalm:), and confirmed that if I ensure strict sequencing of the parses everything works out as expected:

      testM("cal load two valid specs in sequence") {
        val specA =
          """|---- MODULE A ----
             |Foo == TRUE
             |====
             |""".stripMargin

        val specB =
          """|---- MODULE B ----
             |Foo == TRUE
             |====
             |""".stripMargin

        for {
          s <- service
          conn <- s.openConnection(ConnectRequest())
          respA <- s.loadModel(LoadModelRequest(conn.id, specA))
          respB <- s.loadModel(LoadModelRequest(conn.id, specB))
        } yield assert(respA.result.isSpec && respB.result.isSpec)(isTrue)
      },

So I just need to ensure that we're only allowing one instance of the parser to run at a time.

[konnov]

This looks like a limitation of the SANY parser, which was generated by JavaCC. I am not sure how hard it would be for the tlaplus team to make sure that SANY works in a multithreaded environment. Since parsing works relatively fast in comparison to other passes, I can only think of a very simple solution: introduce a mutex that gets locked on every call to SANY. We would lose the ability to call the parser in parallel, but avoid other unexpected issues.

[thpani]

Shon's already using a semaphore in #1855. I also agree that this is the best workaround.