Shai: Should we support TLC .cfg files in the server RPC calls?

[shonfeder]

Ongoing work tracked under #2121 is making it possible to load a specification for checking from a string, which allows passing in a spec via RPC calls (and could be extended for other uses). @konnov has posed the question of whether we should alson support supplying TLC .cfg files in the RPC calls to the server.

I've so far assumed that we do NOT need support for TLC configs in the server, since the server is for advanced use and we can assume any users making use of the feature will opt instead for the more flexible and expressive configuration mechanisms exposed via the apalache.cfg system.

But Igor rightly suggested we ask the @informalsystems/mbt team whether they anticipate a need for this functionality.

Concretely, the question is whether we need to support RPC calls of the form:

session.check({"input": {"source": <specdata>}, "checker": {"length": 20, "config": <INLINE-TLC-CFG-DATA>}})

Or if we can instead require RPC's to specify the configs via the direct JSON encoding supported by the apalche config system. E.g.,

session.check({"input": {"source": <specdata>}, "checker": {"length": 20, "init": ["Init"], "inv": "Inv", <etc...>})

[andrey-kuprianov]

@shonfeder on the MBT side we are also going away from TLC config files towards more flexible TOML configuration; please check out the example. The [Model] section there is generic, and [Apalache] is specific to Apalache. We can and should discuss, and probably agree on a common configuration format.

[shonfeder]

Related to #2261