[FEATURE] Server Mode

[konnov]

This is probably a better solution for #542 and #79.

In the current implementation, when one wants to run the commands check and test multiple times, one has to wait for the bootstrapping times of Java/Scala and the preprocessing steps by Apalache. We considered adding the --continue flag, similar to TLC. Now I think that it would be a bad design choice.

Since the number of use cases is proliferating, it is better to build a JSON server in Apalache. This server would serve model checking queries. For better UX, we would write problem-specific scripts that interact with the Apalache server, in order to solve a specific task that the user has in mind.

---

Sub issue tracking

• Design: Write RFC to propose architecture for server mode #815
• Features:
  • Tool output in JSON format for integration #529
  • Add RPC for loading a model #1114
  • Add RPC to prepare transitions, apply transitions, and assert new constraints #1116
  • Add RPCs for retrieving executions of model and checking sate.  #1117
• Infrastructure:
  • [FEATURE] Select and add RPC system #906
  • [FEATURE] Add CLI command for running in server mode #1115
  • [FEATURE] Add RPCs for creating and terminating a connection to server #1113
  • Add CLI client for server #1118

[konnov]

We have to find a good library to serve http requests in json. For instance, here is Akka HTTP: https://doc.akka.io/docs/akka-http/current/common/json-support.html

[shonfeder]

Does it have to be HTTP? Rather, is it obvious that the protocol should be http? I don't have anything against HTTP, of course! Just asking out of curiosity. Wondering if we should rule out stuff like https://en.wikipedia.org/wiki/JSON-RPC, or something else listed here https://en.wikipedia.org/wiki/Remote_procedure_call#General?

[lemmy]

FWIW: One design bug of TLC (perhaps down to SANY) has always been that it cannot check two (or more) specs within the same JVM instance. Not sure if that's relevant here, but this restriction has turned out to be a pain. In light of refinement, a "model-checking query" might include a spec.

[konnov]

FWIW: One design bug of TLC (perhaps down to SANY) has always been that it cannot check two (or more) specs within the same JVM instance. Not sure if that's relevant here, but this restriction has turned out to be a pain. In light of refinement, a "model-checking query" might include a spec.

That's a good point. However, we are spending most of the time on spec preprocessing. So I would fix the spec. However, we definitely have to figure out how not to restart the tool, if the user wants to check several properties. I believe that annotations would help us here. E.g., by annotating invariants with @invariant, we can tell the tool to do all preprocessing upfront and then let the user to run the queries.

[konnov]

@Kukovec would you like to write an RFC, similar to RFC001. I remember that the discussion in RFC001 was a big success. The RFC should also relate to ADR003.

[konnov]

On a second thought, we have all passes integrated via Guice, so reloading a spec via a new pipeline should be really easy.