MBT-core: test configuration

[andrey-kuprianov]

We need to design a configuration format to describe model-based tests.

The config format should provide the fields to specify:

• the TLA+ model
• whether to generate monitor for the model (see MBT-core: auto-generate TLA+ monitor #3)
• whether to generate history for the model (see MBT-core: auto-generate TLA+ history #4)
• the instantiation parameters (see MBT-core: auto-instantiate model for given parameters #5)
• the TLA+ test assertions: inline in the config, or via a file reference. The test assertions can be built using the auto-generated monitor and history
• the weight for the test assertions and instantiation parameters (see MBT-core: weights for test instantiation #7)

[andrey-kuprianov]

Choice of configuration format

The choice of a config file format is not simple.

• The current format (JSON) doesn't seem to be flexible enough to cover present and future needs. E.g., there config file should allow to specify weights, and then based on them to flexibly describe the space of tests to be executed, depending on the instantiation parameters. This should allow e.g. to include/exclude some test assertions independently on their weights, to cover some special cases. Besides, though a minor issue, JSON is not very user-friendly for manual editing.
• Initially I was considering TOML/YAML as alternatives to JSON. They partially address the user-friendliness issue, i.e. it's initially easier to write a TOML config than a JSON config. They do bring along a lot of their own weirdness, e.g. specifying arrays in TOML is very verbose, or space indentation for structuring in YAML is awkward. Also, these languages do not address at all the required flexibility.

Having ruled out the TOML/YAML, and having recognised the need for more flexibility, these seems to be the main alternatives:

• Dhall is essentially a programming language, which adds to JSON variables, functions, types, etc. It is used e.g. in Themis-Tracer. The syntax of Dhall is quite on-its-own, and seems to be heavily inspired by Haskell.
• Jsonnet is another alternative that I've discovered only recently by chance. It is also JSON + variables + functions, etc. But the design principles are different. E.g. any valid JSON file is valid Jsonnet file. This means the user has the option to write his config in pure JSON, or slowly explore additional benefits of Jsonnet on the go.

Here are a couple of comparisons between different alternatives:

• Comparing Dhall and Jsonnet for Ansible Playbooks
• Why are we templating yaml?
• Jsonnet comparison to other approaches
• Dhall comparison to other approaches

I am very much in favour of using Jsonnet. Here are the reasons:

• see the design principles
• in particular the hermeticity principle is very important for test reproducibility
• it is very well designed, even with the strict specification
• it will be very easy for the users to gradually explore the language, because it's possible to start with pure JSON
• it is stable and well-maintained (comes from Google), but open-sourced under Apache 2.0
• it has a very good compiler/interpreter in Rust, which is also by far the fastest among all Jsonnet interpreters. Also licensed under Apache 2.0

As it occurs to me, we will be also able to use the Rust Jsonnet implementation above (probably a fork with slight tweaking) as a replacement for our homegrown Jsonatr tool. Here is why:

• we have developed Jsonatr because we needed to extract information from Apalache counterexamples, which are ASTs for a context-free language. That's why we have taken JsonPath as the basis for extraction, and added some programming features to it.
• the programming language features in Jsonatr, while functional, are ugly to use, and are already too restrictive for our purposes.
• it seems much easier to take the Jsonnet programming language already implemented, and, if needed, extend it with JsonPath expressions for extracting the data from counterexamples. This approach seems to be future-proof.

[shonfeder]

A few words in favor of Dhall:

• It is based on System-F, so it is easy and solid to reason about as soon as you learn the base principles (this is opposed to being based on a grab back of ad hoc language features)
• There is also a rust implementation
• It is total (as opposed to Jasonnet's turing completeness), which guarantees termination and a certain critical level of simplicity in the configuration.
  • As a result, it has no need for hermeticity as a design principle, since it formally guaranteed as a program property
• The way to use Dhall is to compile down to json, then read in the json. This means it is trivial to also support json configuration for simple configs.
• Dhall is also stable and actively maintained
• Configs are checked statically, which means you know your configuration is right if it loads: you don't have to wait to find out at runtime.

That said, like many of these cases, given the more familiar syntax and OOP features, I imagine the initial learning curve for Jsonnet is gentler (but would not be surprised if you pay for it later, due to turing completeness and complexity of object inheritance).

[andrey-kuprianov]

wow, @shonfeder thanks for commenting on this:)

Those are good points. But I think one of the most important points is that the learning curve should be as flat as possible. Having pure JSON as the entry point is perfect for that.

Another thing, as far as I understand about Dhall, is that everything needs to be typed. There is a huge obstacle if e.g. we want to process Apalache counterexample, i.e. import it, and extract smth. from it. Try to define types for TLA+ in Dhall;)

Also, as far as I understand, importing JSON in Dhall is not even implemented yet, though people are asking about this already for 2+ years now. Seems not possible to do. In Jsonnet this is trivial.

Honestly, I don't care too much about theoretical correctness provided by the language itself. I care much more about its practicality. At the end, it is we who are mostly going to write code for these tools, so we can take care of the correctness by good design and simplicity -- this is our speciality.

Also, doesn't hurt if we pursue different approaches for Themis-Tracer and MBT; it's even good if we can compare them.

[shonfeder]

Dhall is not a serialization format and is not designed to be machine writeable, so if what you need is something you can generate programmatically, I totally agree Dhall is not the right choice.

But I'd encourage differentiating configuration from serialization. Expecting to have one format that is both a serialization for communicating between machines and a human-focused configuration language is a bad idea IMO. Whether you go with Dhall or Jasonnet or something else, I think trying to use the same format for both data exchange and human config will end up leading to pain.

Honestly, I don't care too much about theoretical correctness provided by the language itself. I care much more about its practicality. At the end, it is we who are mostly going to write code for these tools, so we can take care of the correctness by good design and simplicity -- this is our speciality.

I disagree on this point almost entirely, but that is out of band :)

I agree there's no need for uniformity between completely unrelated projects :)